Formális módszerek - Zárthelyik (2020 tavasz)

Tartalom:

Követelmények

A tantárgy követelményeinek teljesítéséhez két zárthelyi sikeres megírása szükséges..

  • Mindkét zárthelyi pótolható a tanulmányi teljesítményértékelési terv szerinti ütemezésben (ld. lentebb).
  • Sikeres zárthelyi javító célzattal történő újraírására is van lehetőség, ez esetben a legutolsó kapott osztályzat lesz érvényes (tehát rontani is lehet).
  • Pót-pótzárthelyi nincs.

Az első zárthelyi

  • Időpont: 2020. március 17. kedd, 18:15. Az egyetemi intézkedéseknek megfelelően a zárthelyi új időpontja 2020. március 24. kedd, 18:00.
    A zárthelyi megírására online eszközökkel kerül sor, erről előzetes információ lentebb olvasható.
  • A zárthelyi témája: Az első 5 oktatási hét anyaga (EA01 - EA05):
    • Alapszintű modellezési formalizmusok.
    • Követelmények formalizálása temporális logikákkal.
    • Modellellenőrzési módszerek.
    • Hatékony modellellenőrzés.
    • Állapottérképek.
  • Mintapéldák, gyakorló feladatok:
  • Referencia megoldások:
  • Pontozás: [0-15) elégtelen, [15-20) elégséges, [20-25) közepes, [25-30) jó, [30-35] jeles.
  • Eredmények
    • Belépve a HF portálra az eredmények elérhetők "ZH1 pontszám" alatt.
    • A pontszámokat mindenki ellenőrizni tudja a saját megoldása és a fenti referencia megoldás összevetésével.
    • Ha valaki javítási hibát észlel, akkor a probléma részletes leírásával jelezze emailben a tárgyfelelősnek (majzik@mit.bme.hu).
  • Általános pontozási szempontok (minden lehetséges problémára itt nem tudunk kitérni; itt nem említett hibák vagy hiányosságok esetén is történhetett pontlevonás):
    • 1.1. Jó válasz 1 pont, rossz válasz 0 pont.
    • 1.2. -1 pont minden olyan kifejezésre, aminek teljesülnie kellene, de nem teljesül; vagy nem kellene teljesülnie, de teljesül. -1 pont minden felesleges állapotért (ha nem a legkevesebb állapotból áll az állapotsorozat), de ezért legfeljebb 2 pont levonás.
    • 1.3. 0 pont, ha nem jó a példaként felírt kifejezés. LTL kifejezés kezdő útvonal kvantor nélkül nem ér pontot.
    • 2. Ha hiányzik vagy túl sok az állapot, akkor az első ilyen állapotra 1 pont levonás jár. Ha jó az állapotok száma, de valahol nem jó a címke, akkor 0,5 pont levonás jár. Ha valahol hiányzik egy él, vagy túl sok van, akkor az első ilyen élért 1 pont levonás jár. Ha már van egy-egy pontlevonás állapotra és élre, akkor a további pontlevonások minimalizáltak, és attól függően, hogy még hány hiba van, max. 1 pont levonás jár. 0 vagy 1 pontot azok kapnak, akik nagyon nem voltak képben, hogy mit kell csinálni.
    • 3.1. 0,5 pontot ér, ha jó a kiindulási állapot függvénye. 1,5 pontot ért, ha jó az útvonal függvénye. Az útvonal esetén fél-fél pontok járnak, ha jól vannak felírva az állapotok, ha jók az operátorok, és ha a jelölés is megfelelő. Egyéb hibáért fél pont levonás jár.
    • 3.2. Ha nincs levezetés és nem jó a lerajzolt diagram, akkor nem jár pont. Részeredményként a kiindulási függvény vagy döntési fa felírásáért 1 pont jár. Ha van jó diagram, de nem minden redukálási lépés jó, azért 2 pont jár. Véletlennek látszó hibáért 0,5 pont levonás jár.
    • 4. ZH1A részpontszámok: „not p” címkézés S, A állapotra: 1 pont. „EX q” címkézés B, C állapotra: 2 pont. „A((not p) U (EX q))” címkézés B, C állapotokra: 1 pont. „A((not p) U (EX q))” címkézés S állapotra: 1 pont. „A((not p) U (EX q))” címkézés lépései követhetők: 1 pont. Az algoritmus nem értésének explicit bizonyítéka pontlevonással jár.
    • 4. ZH1B részpontszámok: „AX p” címkézés S, A, C, D állapotra: 2 pont. „E((AX p) U q)” címkézés A, D, majd C állapotokra külön iterációban: 1 pont. „q” címke felhasználása az iterációban világos: 1 pont. „E((AX p) U q)” címkézés S állapotra: 1 pont. „E((AX p) U q)” címkézés lépései követhetők: 1 pont. Az algoritmus nem értésének explicit bizonyítéka pontlevonással jár.
    • 5.1-5.3. 0,5 pont jár, ha szerepel a kifejezésben valami, ami "hasonlít" az elvárt temporális operátorra. 1 pont, ha jó az operátor szintaktikailag. 1,5 pont, ha csak kisebb hiba van a kifejezésben. 2 pont, ha teljesen jó a kifejezés. Az első három feladatra adható 6 pontból összesen 0,5 pont levonás jár, ha nem szerepel a G operátor (tehát ha minden jó, de 3 helyen hiányzik a G, az 5,5 pontot ér összesen).
    • 5.4. 1 pontot ér a negálás a tabló építése előtt; 1 pont az U kifejtése; 1 pont, ha van jól megkezdett tabló építés; 2 pont a befejezett tabló a két visszamutató éllel; 1 pont az explicit kimondott ellenpélda (bekarikázásra, kipipálásra stb. nem jár pont).

Részletes információk az első zárthelyi megírásához (frissítve 2020-03-23):

A zárthelyi megírásához a következők szükségesek:

  • Internet kapcsolat.
  • Web böngésző és PDF olvasó alkalmazás a ZH1 feladatok elolvasásához.
  • Jól láthatóan író toll (kék vagy fekete) és üres fehér A4-es papírlapok (legalább 3 lap) a megoldás elkészítéséhez.
  • Digitális fényképezőgép, lapszkenner, vagy mobiltelefonos fényképező vagy szkenner alkalmazás (pl. Cam Scanner, Office Lens, Genius Scan) a megoldás oldalainak PDF vagy JPG formátumba történő digitalizálásához.
    Ha a digitalizálás nem megoldható, akkor sajnos ez a ZH alkalom nem lesz kihasználható; ilyen esetekre is számítva lesz egy plusz pótlási lehetőség a félév végén (pót-pótZH más technikával).

A ZH1 feladatokhoz való hozzáférés és a megoldások beadása elektronikusan történik (részleteket lásd lentebb), a következő lépésekben:

  • A ZH1 kezdő időpontjában lesz olvasható illetve letölthető a ZH1 feladatsor.
  • Oldja meg a feladatokat kézírással illetve ábrák rajzolásával, az üres papírokat és a tollat használva úgy, hogy minden feladatot külön oldalon kezdjen. Minden oldalon szerepeljen a neve, Neptun kódja és aláírása is!
  • A feladatok megoldására 60 perc áll rendelkezésre. ZH közben az esetleges közérdekű (feladat értelmezési) kérdéseket az MS Teams "ZH" csatornáján válaszoljuk meg.
  • Ezután a megoldásokat tartalmazó oldalakat digitalizálja PDF (javasolt) vagy JPG formátumba, olyan felbontásban, hogy jól olvasható legyen, de egy oldal digitalizált mérete ne haladja meg az 1 MB-ot (kb. 300 dpi; ha szükséges, akkor képfeldolgozó alkalmazásban csökkentse a felbontást, élesítse a képet stb.). Ha PDF-be digitalizál, akkor fűzze össze az oldalakat, ha pedig JPG-be digitalizál, akkor a fájlokat egy ZIP-be csomagolja össze.
  • A PDF vagy ZIP csomagot töltse fel (a feltöltés a ZH1 kezdetétől már lehetséges, tehát aki hamarabb készen van, fel tudja tölteni a megoldását). A feltölthető fájl maximális mérete 10 MB.
  • A megoldásokat tartalmazó lapok digitalizálására és feltöltésére a 60 perc megoldási idő után még 20 perc áll rendelkezésre. A ZH1 kezdő időpontjától számított 60+20 perc után beadást már nem fogadunk el.

A feladatok elérése és a megoldás feltöltése:
A ZH1 feladatokhoz való hozzáférés és a megoldások beadása a https://hf.mit.bme.hu portál segítségével történik. A portálra a BME Címtár segítségével lehet belépni (a házi feladatok letöltéséhez hasonló módon). A terhelés elosztása érdekében csoportonként kissé eltérő hozzáférési és beadási idők lesznek:

  • Akinek a házi feladata HF01-HF05, az 18:00-kor lépjen be a portálra. Itt a Formális módszerek tárgyhoz kapcsolódóan, a kiírt feladatok között talál egy "ZH csoport" sort. Az ebben megadott érték (ZH1A vagy ZH1B) alapján kattintson a lentebb található ZH1A vagy a ZH1B sorra. Itt a "Link" mező adja meg a ZH1 feladatok elérését (a link csak 18:00-kor jelenik meg). Ugyanitt lehetséges majd a digitalizált megoldást (PDF vagy ZIP fájl) feltölteni.
    A feltöltési határidő 19:20.
  • Akinek a házi feladata HF06-HF10, az 18:15-kor lépjen be a portálra. Itt a Formális módszerek tárgyhoz kapcsolódóan, a kiírt feladatok között talál egy "ZH csoport" sort. Az ebben megadott érték (ZH1A vagy ZH1B) alapján kattintson a lentebb található ZH1A vagy a ZH1B sorra. Itt a "Link" mező adja meg a ZH1 feladatok elérését (a link csak 18:15-kor jelenik meg). Ugyanitt lehetséges majd a digitalizált megoldást (PDF vagy ZIP fájl) feltölteni.
    A feltöltési határidő 19:35.

Tanácsok:

  • Az A4-es oldalak digitalizálását gyakorolja be, ne a ZH1 során kezdje el az alkalmazásokat megtanulni, kipróbálni. A digitalizálás során fontos, hogy minden felírt szöveg, ábra jól olvasható legyen: pontot csak arra tudunk adni, amit egyértelműen el tudunk olvasni (homály, csillogás, elmosódás esetén találgatni nem tudunk és nem fogunk).
  • A 60 perces megoldási időt és a 20 perces digitalizálási+feltöltési időt azért javasoljuk ilyen megosztásban, hogy a feltöltés határidőre és jó minőségben megtörténhessen. Mihamarabb célszerű a feltöltés, mert az utolsó pillanatban a szerver terhelése miatt nagyobb késleltetés lehetséges.
  • A ZH1 ilyen formában történő megírása során sok technikai probléma előfordulhat (hálózati kapcsolat megszakadása, túlterhelés, alkalmazások leállása stb.). Ezeket nem tudjuk kezelni és figyelembe venni; csak azt fogjuk kijavítani, amit határidőre feltöltve megtalálunk (emailben vagy más egyéb módon ne adjanak be megoldást, se határidőre, se később). Az esetleges problémákra számítva van lehetőség a meghiúsult vagy sikertelen ZH1 pótlására 2 alkalommal is (pótZH1 és pót-pótZH, ezeken más technikákat próbálunk majd alkalmazni).
  • Kérjük, mindenki őrizze meg a saját megoldását (fizikailag és elektronikusan is).

Sok szerencsét, és reméljük, nem lesz semmilyen technikai probléma a ZH1 során!


Az első zárhelyi pótlása

  • Időpont: 2020. március 31. kedd, 18:15 2020. április 7. kedd, 18:00. A zárthelyi megírására online eszközökkel kerül sor, erről előzetes információ lentebb olvasható.
  • A zárthelyi témája: A pótolandó zárthelyi témájával egyezik meg.
  • Mintapéldák:
  • Referencia megoldások:
    • TBA
  • Pontozás: [0-15) elégtelen, [15-20) elégséges, [20-25) közepes, [25-30) jó, [30-35] jeles.
  • Eredmények: 
    • TBA
  • Általános pontozási szempontok:
    • TBA

Részletes információk az első pótzárthelyi megírásához (frissítve 2020-04-04):

Az első pótzárthelyi (PZH1) megírására online eszközökkel kerül sor, ugyanolyan módon, mint a ZH1 esetén volt (kapcsolódó tanácsok és részletek fentebb olvashatók).

  • 18:00-kor kérjük lépjen be a házi feladat portálra (https://hf.mit.bme.hu). Itt a Formális módszerek tárgyhoz kapcsolódóan, a kiírt feladatok között talál egy "PZH1" sort. Erre kattintva a "Link" mező adja meg a PZH1 feladatok elérését (a link csak 18:00-kor jelenik meg).
  • Oldja meg a feladatokat kézírással illetve ábrák rajzolásával, üres papírokat és a tollat használva úgy, hogy minden feladatot külön oldalon kezdjen. Minden oldalon szerepeljen a neve, Neptun kódja és aláírása is!
    60 perc áll rendelkezésre a feladatok megoldására.
  • Ezután a megoldásokat tartalmazó oldalakat digitalizálja PDF (javasolt) vagy JPG formátumba, olyan felbontásban, hogy jól olvasható legyen, de az összes oldal digitalizált mérete ne haladja meg a 10 MB-ot. Ha PDF-be digitalizál, akkor fűzze össze az oldalakat, ha pedig JPG-be digitalizál, akkor a fájlokat egy ZIP-be csomagolja össze.
  • Töltse fel a PDF vagy ZIP csomagot a házi feladat portálra legkésőbb 19:20-ig (a feltöltés a PZH1 kezdetétől már lehetséges, tehát aki hamarabb készen van, fel tudja tölteni a megoldását). A feltöltés ugyanazon a web lapon történik, ahol a feladatok linkje volt található.

Sok szerencsét, és reméljük, nem lesz semmilyen technikai probléma a PZH1 során!


A második zárthelyi

  • Időpont: 2020. május 19. kedd, 18:15
  • Helyszín: TBA
  • A zárthelyi témája: A 6-13. oktatási hetek anyaga (EA06-EA13):
    • Szoftverek modellellenőrzése.
    • Petri hálók alapelemei és kiterjesztései.
    • Petri hálók dinamikus tulajdonságai. Petri hálók redukciója.
    • Petri hálók strukturális tulajdonságai.
    • Modellezés Petri hálókkal. Hierarchikus Petri hálók.
    • Színezett Petri hálók.
    • Sztochasztikus Petri-hálók.
  • Mintapéldák, gyakorló feladatok:
  • További tudnivalók:
    • A zárthelyi megírásához csak üres papír és toll szükséges, más segédeszköz nem használható.
    • Azonosításra alkalmas fényképes igazolványt hozzanak magukkal!
  • Eredmények:
    • TBA
    • Pontozás: TBA
  • Megtekintés:
    • TBA

A második zárthelyi pótlása

  • Időpont: 2020. május 28. csütörtök, 10:15
  • Helyszín: TBA
  • A zárthelyi témája: A pótolandó zárthelyi témájával egyezik meg.
  • Mintapéldák:
  • További tudnivalók:
    • A zárthelyi megírásához csak üres papír és toll szükséges, más segédeszköz nem használható.
    • Azonosításra alkalmas fényképes igazolványt hozzanak magukkal!
  • Eredmények:
    • TBA
    • Pontozás: Mint a pótolandó zárthelyi pontozása
  • Megtekintés:
    • TBA

Pót-pótzárthelyi

  • Az egyetemi intézkedéseknek megfelelően pót-pótzárhelyit is kell tartanunk. Ezen bármelyik zárthelyi (de csak az egyik) pótolható lesz. Részletes információkat később tudunk adni.