Formális Módszerek ZH 2005. 04. 07. (B csoport)
Ez az oldal a korábbi SCH wiki-ről lett áthozva. Az eredeti változata itt érhető el.
Ha úgy érzed, hogy bármilyen formázási vagy tartalmi probléma van vele, akkor kérlek javíts rajta egy rövid szerkesztéssel.
Ha nem tudod, hogyan indulj el, olvasd el a migrálási útmutatót
ZH: 2005-ös ZH B csoport fotózva (infosite)
Hibák simán lehetne benne, aki nem érti/más jött ki, írja hozzá alulra!!!
Tartalomjegyzék
1.1 feladat
- Ezen a helyen volt linkelve a(z) ZH.WAM nevű fájl ("ZH.WAM" link szöveggel) a régi wiki http://wiki-old.sch.bme.hu/bin/view/Infoalap/FormModZh20050407 oldaláról. (Ha szükséged lenne a fájlra, akkor a pontos oldalmegnevezéssel együtt küldd el a wikiHiba a bélyegkép létrehozásakor: Nem lehet a bélyegképet a célhelyre mentenisch.bme.hu címre a kérésedet)
- hiányzik egy rakat "tiltó él" - de szemléltetésnek jó :)
- HAMIS - a tranzíciók nem tüzelhetnek bármely állapotból, van benne pl egy zárt ciklus (lásd lentebb)
- HAMIS - a kezdőállapotba nem minden állapotból, sőt semelyik másikból nem tudunk visszajutni
- HAMIS - a kezdőállapot pl. semmilyen ciklusban, T-Invariánsban nincs benne
- IGAZ - például az (121)-(021)-(120) állapotok egy zárt ciklusban vannak, mindegyik visszatérő állapot
- X - ? (talán hurokéleket nem látjuk, azért...)
- IGAZ - t9 minden tüzelési szekvenciában előfordul, tessék megnézni
- HAMIS - t3 egyedül a (011)-(010) átmenetben fordul elő, innen azonban már csak egy ciklusba kerülhet ahonnan nem tud kitorni - t3 L1 élő
- HAMIS - Az (101)-(011)-(110)-(100) ciklusban követhetik egymást, ahol t9 előfordul , t4 nem, tehát végtelenszer tüzelhet a másik nélkül
- HAMIS - A fenti ciklusban t5 is előfordul, t2 viszont nem
- HAMIS - van zárt ciklus, ahonnan nem tud kitörni a hálózat
1.2
1.2-1.
- HAMIS
- HAMIS
- IGAZ - habár a M-S algoritmus pl nem feltétlen a minimális T-Invariánsokat találja meg, ezeknél "kisebb" potenciális T-Invariánsokból véges sok van. Ha ezeket végignézzük, és a "legkisebb" alapúakat vesszük, biztos megtaláljuk az összes minimális T-Invariánst, tehát igaz (persze lehet van célravezetőbb módszer is, csak erről nem tudok...)
- HAMIS - hmm :) lásd előző /e pont
1.2-2.
- IGAZ - defínció szerint, a fólián is rajtvan (Alosztalyok.ppt - 27.dia 8.)
- IGAZ - ez a speciális metszet nem lehet más, csak egy "kör", amiben 1 token esetén triviális h egy tranzíció tüzelhet
- HAMIS - tranziciok is termelhetnek tokeneket.. (Tudsz a hálóba termelőt rakni anélkül, hogy forrás tranzíciód lenne. Így végtelen sok tokent elő tudsz állítani. Ezért nem igaz, hogy korlátos.)
- IGAZ - könyv 64. o. 2.9-es fejezet utolsó mondata: A következőkben bemutatott alosztályok mindegyikére igaz ezen felül, hogy [...] önhurok-mentesek [...]. Ezután taglalja a jelölt gráfot. Tehát a jelölt gráf önhurok-mentes. GaryT
Példa /c-re:
A gráf folyamatosan tokeneket termel, és korlátlan (persze, el is nyelhet)
1.2-3.
- IGAZ - ha deadlock mentes, bármely állapotból van tüzelhető tranzakció, melyeken elindulva előbbutóbb egy tranzíciónak szükségesszerűen végtelen sokszor szerepelnie kell, azaz részlegesen ismételhető a háló, így igaz - (köszönet Sztahó Dávidnak hogy felhívta erre a figyelmet)
- IGAZ - a strukturálisan élőknél van olyan kezdőállapot, amiből kiindulva élő --> deadlockmentes
- HAMIS - siman lehet h az egyik ciklus porog, a masik meg "ehezik"..
- HAMIS - hasonlo gondolatmenet miatt nem igaz
1.2-4.
- HAMIS - pontosan helyett legalább annyi..
- HAMIS - lehet h a többi tüzelése során nem engedélyezetté válik
- IGAZ - mivel FC-k esetén ha egy állapotból nem egyedüliként indul ki egy él (mint példánkban) , akkor egyedüliként fut be a tranzícióba, az tehát csak a mi vizsgált helyünktől függ. A helyből csak az egyik tranzíció veheti ki a tokent, és a tranzíciókat már helyek nem befolyásolják, ergo mindig a nagyobb prioritású tüzel, a kicsi meg bekussol.
- Szerintem: HAMIS, mert a nagyobb prioritású tranzícióba mehet 2 súlyú él; ha a helyen 1 token van, akkor a kisebb prioritású fog tüzelni. Jó klérdés, hogy a 2 súlyú él sérti-e azt a tulajdonságot, hogy csak egy él mehet be a tranzícióba.
- Ez azért nem igaz amit írtál, mert az FC közönséges, szóval minden élsúly 1. komcsy
- HAMIS - kevesebb helyett _legfeljebb_annyi_ a helyes - BergmannGabor
1.2-5.
- HAMIS - az egy tüzeléssel elérhető állapotokból néhány egybeeshet. Például ha van két tökegyforma tranzíció, vagy pl. csak más place körül vannak a hurokéleik... BergmannGabor
- IGAZ - naná, különben mit keresne a fedési gráfban?
- IGAZ - csak az L0-halott tranzíciók nem jelennek meg, már L1-eseknél is van olyan tüzelési szekvencia, amelyben legalább egyszer megjelennek
- HAMIS - egyáltalán nem biztos (sztem a fedési gráf rajzolásának metodikájával akar megkavarni, ott van hogy ha megjelenik egy állapot, ami már volt, akkor OTT átírjuk w-ra a megfelelő helyeket, de ÁTírjuk és nem írjuk le újra...)
2.1
elég egyértelmű, de ha lesz energiám lerajzolom :]
2.2
2.2-1.
a : 0 , b : 1 , c : -3 , d : -1
Nem, nem elírás az a=0, hurokélek is vannak a világon....
2.2-2.
Matrinez-Silva algoritmus (egy táblázatban az egész, nem lépésenként..)
| 1 | 0 | 0 | 0 | 0 | 0 | -2 | -1 | 0 | 1 |
| 0 | 1 | 0 | 0 | 0 | 0 | -1 | 1 | -1 | 0 |
| 0 | 0 | 1 | 0 | 0 | 0 | 1 | 0 | 1 | -1 |
| 0 | 0 | 0 | 1 | 0 | 0 | 0 | 2 | -1 | -1 |
| 0 | 0 | 0 | 0 | 1 | 0 | 0 | 0 | -1 | 1 |
| 0 | 0 | 0 | 0 | 0 | 1 | 0 | 3 | -3 | 0 |
| első fázis | |||||||||
| 0 | 1 | 1 | 0 | 0 | 0 | 0 | 1 | 0 | -1 |
| 1 | 0 | 2 | 0 | 0 | 0 | 0 | -1 | 2 | -1 |
| második fázis | |||||||||
| 1 | 1 | 3 | 0 | 0 | 0 | 0 | 0 | 2 | -2 |
| 2 | 0 | 4 | 1 | 0 | 0 | 0 | 0 | 3 | -3 |
| 3 | 0 | 6 | 0 | 0 | 1 | 0 | 0 | 3 | -3 |
| harmadik fázis | |||||||||
| 1 | 1 | 3 | 0 | 2 | 0 | 0 | 0 | 0 | 0 |
| 2 | 0 | 4 | 1 | 3 | 0 | 0 | 0 | 0 | 0 |
| 3 | 0 | 6 | 0 | 3 | 1 | 0 | 0 | 0 | 0 |
ebből kiindulva:
- X
- X
- M
- M
egy tipp: úgy is gyorsan el lehet dönteni h valamelyik P-invariáns, hogy a mátrixszal minden oszlopával összeszorozva mindig 0át kapsz. Ez gyors, ha nem invariáns, viszont a minimalizmushoz mindenképp kell a Martinez-Szilva algoritmus...
2.2-3.
Martinez-Silva:
| 1 | 0 | 0 | 0 | -2 | -1 | 1 | 0 | 0 | 0 |
| 0 | 1 | 0 | 0 | -1 | 1 | 0 | 2 | 0 | 3 |
| 0 | 0 | 1 | 0 | 0 | -1 | 1 | -1 | -1 | -3 |
| 0 | 0 | 0 | 1 | 1 | 0 | -1 | -1 | 1 | 0 |
| első fázis | |||||||||
| 0 | 1 | 0 | 1 | 0 | 1 | -1 | 1 | 1 | 3 |
| 1 | 0 | 0 | 2 | 0 | -1 | -1 | -2 | 2 | 0 |
| második fázis | |||||||||
| 0 | 1 | 1 | 1 | 0 | 0 | 0 | 0 | 0 | 0 |
| 1 | 1 | 0 | 3 | 0 | 0 | -2 | 1 | 3 | 3 |
innen:
- I
- X
- X
- X
2.3
2.3-1.
AC, mert p3 és p4 követő tranzíciói nem diszjunktak és nem is esnek egybe, így EFC nem lehet, de AC, mert tartalmazás van minden esetben - BergmannGabor
2.3-2.
SM, mert minden tranzícióból és tranzícióba csak egy él fut be.
2.3-3.
Élő, hiszen erősen összefüggő és van benne legalább egy (sőt kettő) token.
Nem biztos a háló, mert ha kapásból t4 tüzel, p4ben 2 token is lesz. (Definíció szerint is legfeljebb egy token lehet egy biztos SM-ben)
!! Def szerint egy SM acsa biztonságos, ha kezdő tokeneloszlásban legalább egy token van. Élő SM pedig acsa biztonságos, ha pontosan egy token van kezdőeloszlásban.Zsófi
2.4
t1 és t3 összevonása, p3-p4-p5 összevonása, t2 és t4 összevonása, p1 és p6 összevonása, p10 törlése, t9 törlése, t6 és t7 összevonása, t67 törlése, p8 és p9 összevonása, t5 és t8 összevonása, p11 törlése. Ami marad: p16 és t58.
Redukcióval egy tranzíció és egy hely marad egy tokennel, a hely oda-vissza össze van kötve a tranzícióval ("hurokél").
Ezért élő és biztos.
2.5
2.6
2.6-1.
t3: az utolsó sütés egy adott rendelésnél
t4: minden nem utolsó sütés egy rendelésnél
2.6-2.
A sütők egy szimpla oda-vissza élpárral lennénel összekötve a t3 és t4 tranzíciókhoz.
2.6-3.
p6: A vásárló már megkapta a szendvicseit nincs rendelése, hamarosan távozik.
p1: A vásárló most jött, még van rendelése és nincs szendvicse.
2.6-4.
Valahogy így: [{v1,v2,v3},0,0,{x1,x2},{s1,s2},0]
-- RGabo - 2006.04.01.
