VYTVOŘENÍ MODELU VÝTAHŮ SE SBĚRNÝM ŘÍZENÍM

MASARYKOVA UNIVERZITA FAKULTA INFORMATIKY

VYTVOŘENÍ MODELU VÝTAHŮ SE SBĚRNÝM ŘÍZENÍM

BAKALÁŘSKÁ PRÁCE

Ondřej Plotěný

Brno, 2009

Prohlášení Prohlašuji, že tato bakalářská práce je mým původním autorským dílem, které jsem vypracoval samostatně. Všechny zdroje, prameny a literaturu, které jsem při vypracování používal nebo z nich čerpal, v práci řádně cituji s uvedením úplného odkazu na příslušný zdroj.

Vedoucí práce: RNDr. Jiří Barnat, Ph.D.

ii

Poděkování

Považuji za svou milou povinnost poděkovat pánům Mgr. Pavlu Moravcovi, Ph.D. a RNDr. Jiřímu Barnatovi, Ph.D., za odborné a organizační vedení, za cenné a věcné připomínky, a rady při zpracování této práce. Dále i svým blízkým za projevenou trpělivost a volný prostor k tvůrčímu myšlení. Mimo jiné i mým přátelům a známým, zejména z rodných Jiříkovic a divadelníkům z ochotnického divadla Stodola a divadelního souboru Amadis.

iii

Shrnutí Cílem této bakalářské práce je vytvořit formální model systému výtahů se sběrným řízením ve vstupním jazyce verifikačního nástroje DiVinE. V práci je uveden zobecněný model obsahující více variant řešení daného zadání a několik formulí v logice LTL zajímavých pro tento model.

iv

Klíčová slova verifikace, ověřování modelu, abstraktní model, DiVinE, výtah, controller

v

OBSAH 1 2 3

4 5 A B

Úvod Výtahy se sběrným řízením Modelování 3.1 Modelovací jazyk 3.2 Modelování systému výtahů se sběrným řízením 3.3. Abstraktní model systému výtahů se sběrným řízením 3.4. Modelování některých vlastností dle parametrů Vlastnosti modelu Závěr Zdrojový kód parametrizovaného modelu Zdrojový kód LTL vlastností

2 3 4 4 7 9 11 15 24 26 41

Kapitola 1

Úvod Je stále zvyšován důraz na důkaz korektnosti systémů v důsledku jejich neustálého rozvoje složitosti a rozmanitosti, k čemuž se využívají různé kontrolní techniky: ●

Automated theorem proving (ATP)1

●

Formal equivalence checking2

●

Model checking (ověřování modelu)3

Tato práce využívá techniku model checking. Mezi jeho největší výhodu patří vlastnost posouzení korektnosti nad všemi možnými situacemi. Tuto vlastnost posuzování lze funkčně rozdělit na několik částí. První část skýtá zhotovení potřebného abstraktního modelu systému. Druhá část formuluje specifické vlastnosti. A třetí, poslední část, verifikuje daný model, což se však děje ve většině případů automaticky. V případě výskytu chyby umí technika ukázat protipříklad, který nám pomůže odhalit chybu, kterou potom můžeme opravit. Plnému využití této techniky v praxi brání její hardwarové nároky, zejména nároky na paměť. Velká kapacita paměti je potřebná pro uchování celého stavového prostoru při hledání všech možných situací. Nejvíce lze náročnost vidět při verifikaci velkého množství asynchronně komunikujících procesů nebo datových struktur s nemalým množstvím různých hodnot. Tato situace se často označuje jako problém stavové exploze. Proto často dochází k situaci, že se stavový prostor nevejde do paměti, a tudíž daný systém nelze verifikovat. V této práci popisujeme modelování a verifikaci systému výtahů se sběrným řízením. Popisu systému se věnujeme ve druhé kapitole. Ve třetí kapitole popisujeme dané modelování, rozepisujeme zde základní strukturu úkolu, který dále obohacujeme o popis vlastností. Dále se zde věnujeme přepisu požadavků do zdrojového, syntakticky správného, kódu DiVinE, který je následně rozšiřován o další možné funkce modelu. Ve čtvrté kapitole se zabýváme zajímavými vlastnostmi různých parametrů modelu s jejich verifikací pomocí DiVinE. U těchto parametrů ukážeme jejich možné závislosti a podmínky na modelu. V závěru se věnujeme velikostem modelu v různých parametrických hodnotách. 1 http://en.wikipedia.org/wiki/Automated_theorem_proving 2 http://en.wikipedia.org/wiki/Formal_equivalence_checking 3 http://en.wikipedia.org/wiki/Model_checking

2

Kapitola 2

Výtahy se sběrným řízením S velkým rozvojem ve stavebnictví, kdy se nestaví jen do plochy, ale i do výšky, je systém výtahů velmi důležitým aspektem. Pokud chceme dopravu výtahy ještě dále zefektivnit, je použití výtahů se sběrným řízením téměř nutností. V současnosti se nejvíce používají 3 typy, a to podle počtu spolupracujících výtahů, jmenovitě typu simplex (pro jeden výtah), duplex (pro dva výtahy) a triplex (pro tři výtahy). Sběrné řízení spočívá ve spolupráci výtahů a řídící jednotky při vyřizování požadavků, kdy se na požadavek odpoví. Dle nastavení daného systému zareaguje bližší volný výtah nebo bližší používaný výtah jedoucí požadovaným směrem, čemuž pomáhají dvojtlačítka u výtahu označující směr budoucí jízdy. Je samozřejmé, že u první a poslední „stanice“ je tlačítko jen jedno. Cílem tohoto systému je efektivní práce výtahů, kdy zareaguje vždy bližší výtah, aby zákazník dlouho nečekal. Pod pojmem (vlastností) bližší volný výtah, předpokládáme volný výtah, který stojí nejblíže patru s požadavkem. A pojem (vlastnost) bližší používaný výtah jedoucí požadovaným směrem, vysvětlujeme jako používaný výtah, který je nejblíže patru s požadavkem, zároveň přesun výtahu směřuje k danému patru a požadavek má stejný směr jako pohyb výtahu. Dále uvnitř výtahu lze zvolit více cílových pater v jednom směru jízdy od nástupního patra, která jsou pak postupně obsluhována.

3

Kapitola 3

Modelování V modelování je cílem vytvořit co nejpřesnější (věrný) formální model ověřovaného systému. Mezitím můžeme formulovat vlastnosti (v některém druhu temporální logiky), které budeme po modelu požadovat, a následně je na modelu verifikovat. Při modelování, pomocí různých formalismů, se přibližujeme funkčnosti formulovaných vlastností.

3.1

Modelovací jazyk

Jazyk DVE Základním prvkem jazyka DiVinE je proces, kde procesy v modelu pracují synchronně nebo asynchronně. Proces lze připodobnit konečnému automatu, neboť definuje množinu možných stavů, iniciální (počáteční) stav a podmínky přechodů mezi stavy. Dále obsahuje lokální, nebo globální proměnné jednoduchých typů, jako např. byte, int nebo jednoduché pole nad nimi. Jazyk dále umožňuje synchronizaci pomocí kanálů s předáváním proměnné nebo pomocí handshake. Obecný model obsahuje globální proměnné, nestejnojmenné procesy a určení synchronizace procesů, tj. system async nebo system sync. Proces obsahuje lokální proměnné, deklaraci přechodových stavů (state ...), určení výchozího stavu (init ...) a přechody mezi stavy (trans ...). Tyto přechody ukazují z kterého stavu do kterého se přechází (A → B), za jakých podmínek se přechod uskuteční (guard x>10), a jak přechod ovlivní proměnné (effect x=x-1). Příklad na obrázku 3.1 ukazuje jednoduchý model skladiště o určité kapacitě, pak dělníka, který jej naplňuje (nepřeplní), ale může vyrobit jen určitý počet výrobků za „směnu“; a pak kamion o kapacitě 50-ti výrobků, který je vždy plně naložen a odváží zboží ze skladu.1

1 Stavový prostor tohoto modelu obsahuje 1198 stavů, 2396 přechodů

4

byte goods = 0; //value 200 max storage capacity process Worker { byte created_goods = 0; //value 15 max one line created limit state idle, working; init idle; trans idle -> idle {guard goods == 200;}, idle -> working {guard goods < 200;}, working -> working {guard created_goods < 15 and goods < 200; effect created_goods = created_goods + 1, goods = goods + 1;}, working -> idle {guard created_goods==15 or goods==200; effect created_goods=0;}; } process Truck { //transport capacity 50 goods and have to be fully loaded state idle, transport; init idle; trans idle -> idle {guard goods < 50;}, idle -> transport {guard goods >= 50;}, transport -> idle {effect goods = goods - 50;}; } system async; Obrázek 3.1: Ukázka v jazyce DVE.

Jazyk MDVE Ačkoliv je jazyk DVE jednoduchý, v případě složitějších konstrukcí typu více (téměř) stejných procesů či parametrizovaných modelů, se stává zdrojový kód modelu nepřehledným a nesnadným na úpravu. Pro ulehčení je definován makrojazyk MDVE nad jazykem DVE, pro překlad se používá interpret m4 a parametrizovaný model. Obecný parametrizovaný model obsahuje výchozí hodnoty parametrů, dále může obsahovat volný kód v jazyce DVE, nebo vázaný pod definicí části kódu, a pak kód jazyka MDVE. Definice části kódu je parametrizovaná, tudíž se při jejím zavolání předávají parametry, které se mohou používat v dané části modelu. Jazyk MDVE zase umožňuje používat podmínku (ifelse(podmínka,true , false )) nebo opakovací cyklus (forloop(název zvyšující se parametrické proměnné, počáteční hodnota, konečná hodnota, )). Jazyk MDVE též zjednodušuje parametrické modely, neboť stačí změnit hodnotu parametru na jednom místě a nemusí se explicitně, např. vytvářet 50 mírně jiných procesů „výtah“, když chci model s 50 výtahy, apod.

5

Na následujícím obrázku 3.2 je podobný příklad jako na obrázku 3.1, ale zdrojový kód modelu je optimalizován a napsán v jazyce MDVE. Díky tomu můžeme při volání zvolit počet dělníků a kamionů, a interpret nám daný potřebný model bez problémů vytvoří.1 default(WRK,1)dnl; default(TRK,1)dnl; byte goods = 0; //value 200 max storage capacity define(workers, `process Worker_$1{ byte created_goods = 0; //value 15 max one line created limit state idle, working; init idle; trans idle -> idle {guard goods == 200;}, idle -> working {guard goods < 200;}, working -> working {guard created_goods < 15 and goods < 200; effect created_goods = created_goods + 1, goods = goods + 1;}, working -> idle {guard created_goods==15 or goods==200; effect created_goods=0;}; } ') define (trucks, `process Truck_$1{ //transport capacity 50 goods and have to be fully loaded state idle, transport; init idle; trans idle -> idle {guard goods < 50;}, idle -> transport {guard goods >= 50;}, transport -> idle {guard goods >=50; effect goods = goods - 50;}, transport -> idle {guard goods < 50;}; } ') forloop(x, 0, decr(WRK), `workers(x)') forloop(y, 0, decr(TRK), `trucks(y)') system async; Obrázek 3.2: Ukázka v jazyce MDVE.

1 Stavový prostor modelu pro 2 dělníky a 2 kamiony obsahuje 217902 stavů, 871608 přechodů

6

3.2

Modelování systému výtahů se sběrným řízením

Při modelování uvažujeme výtahy jako samostatné jednotky v rámci jejich vnitřního ovládání/reakcí na požadavky, a řídící jednotku, která zadává výtahům úkoly dle vnějších požadavků zákazníků. Jako iniciální bod systému, jak při prvotním startu nebo po výpadku proudu, jsou všechny výtahy v první zastávce a bez požadavků.1

Obrázek 3.3: Počáteční stav výtahů.

Vnější ovládání výtahů –

jedno tlačítko – při volbě požádá o výtah pro dané patro, nepoužitelné pro plnou funkčnost sběrného řízení, ale lze s ním využít vlastnost přivolání bližšího volného výtahu. Náš abstraktní model s ním umí pracovat v rámci parametrického rozšíření.

Obrázek 3.4: Vnější jednotlačítkové ovládání.

1 V ilustracích budeme předkládat systém 2 výtahů používaných v 5-ti patrové budově

7

–

dvě tlačítka – při volbě požádá o výtah pro dané patro a určuje budoucí směr jízdy výtahu, používané pro plnou funkčnost sběrného řízení, a to vlastností přivolání bližšího volného výtahu a použití bližšího používaného výtahu jedoucího požadovaným směrem. Náš abstraktní model s nimi umí pracovat v rámci parametrického rozšíření.

Obrázek 3.5: Vnější dvoutlačítkové ovládání.

Vnitřní ovládání výtahů Vnitřní panel pro ovládání daného výtahu, funkčně se neliší v žádném parametrickém rozšíření abstraktního modelu.

Obrázek 3.6: Vnitřní ovládací panel.

8

3.3

Abstraktní model systémů výtahů se sběrným řízením

Konečný model systémů popisujeme globálními proměnnými a dvěma druhy procesů, první nazýváme controller a má funkci řídící jednotky. A druhý, násobný dle počtu výtahů, nazýváme elevator, který popisuje jeden výtah. Komunikace mezi procesy probíhá přes globální proměnné.

Obrázek 3.7: Komunikace procesů.

Konečný model se vytváří z parametrizovaného modelu a zadaných parametrů:

ELEVS –

určuje počet výtahů v daném systému (výchozí hodnota je 2)

FLOORS –

zadává počet pater pro daný systém (výchozí hodnota je 3)

TYPE –

určuje typ systému výtahů (výchozí hodnota je 2) –

0) systém výtahů pro jednotlačítkové vnější ovládání, implementuje vlastnost přivolání bližšího volného výtahu.

–

1) systém výtahů pro dvoutlačítkové vnější ovládání, implementuje však jen vlastnost přivolání bližšího volného výtahu.

–

2) systém výtahů pro dvoutlačítkové vnější ovládaní, implementuje vlastnosti sběrného řízení (tj. přivolání bližšího volného výtahu a použití bližšího používaného výtahu jedoucího požadovaným směrem).

MEM –

určuje vlastnost zapamatování vnějších požadavků, které nemohly být žádným způsobem obslouženy (výchozí hodnota je 0) –

0) zapomíná

–

1) pamatuje si

9

V globálních proměnných se uchovávají některé hodnoty od výtahů nutné pro controller, jako číslo patra (floor[]) kde se právě nachází, směr jízdy výtahu (-1/0/1, m[]) a zda je výtah používán (0-není, 1-je, 2-teprve jede k místu přivolání, usage[]). Mezi další globálně uchovávané hodnoty patří tzv. stop-stav (s), jelikož jazyk DVE neumožňuje "atomic" konstrukci, jako je např. v modelovacím jazyce ProMeLa (SPIN tool). Konstrukce "atomic" umožňuje provést blok příkazů najednou (ostatní procesy během toho stojí). Stop-stav tedy zastaví průběh procesů elevator, a controller má tak „čas“ na vyřízení požadavku nebo výpočet. Další globální proměnné se používají k zapamatování nevyřízených požadavků (MEM = 1) nebo k zapamatování vyřizovaného požadavku. Proces elevator se při parametrech liší jen minimálně, neboť základní vlastnosti pohybu výtahu, vyřizování požadavků a přivolání zůstávají pořád stejné. Proces se liší jen vnějším ovládáním a při použití vlastnosti použití bližšího používaného výtahu jedoucího požadovaným směrem. V lokálních proměnných si uchovává místa, která má obsloužit (lightv[]) a počet těchto míst (pro usnadnění, jobs). Proces controller má jednoduchou základní kostru, jejímž účelem je zareagovat na požadavek o výtah. Jakým způsobem proces zareaguje, je dáno hlavně parametrem TYPE a pak MEM. Lokální proměnné se liší dle parametrů, ale v celku uchovávají hodnoty výpočtu nutné pro dané vlastnosti. Model pracuje bez reálných zákazníků, zadávání požadavků na přepravu si procesy vytváří náhodně, čímž je zajištěna velká variabilita a pokrytí většiny možných situací/stavů.

10

3.4

Modelování některých vlastností dle parametrů

Přivolání výtahu – TYPE = 0, MEM = 0 Při zmáčknutí vnějšího tlačítka (viz Obr. 3.8), přechází model do stavu stop-stav, kdy pracuje jen proces controller, který prochází všechny výtahy. Pokud je výtah používán, dále se s ním nepracuje. Pokud je výtah volný, porovnává se jeho absolutní hodnota rozdílu nynějšího patra výtahu a požadovaného patra. Pokud je menší než poslední nejmenší hodnota, zapamatovává se tento výtah a daná hodnota. Při skončení procházení se zjistí, zda-li se našel některý nejbližší volný výtah, pokud ne, požadavek se zapomíná a končí stop-stav. Pokud volný výtah existuje, pomocí stop-stavu se na tento výtah přepíná řízení (výpočet), kdy se mu předá požadované patro, výtah požadavek přijme a předá řízení zpět controlleru, který ukončí stop-stav a celý model dál pokračuje.

Obrázek 3.8: přivolání výtahu při TYP = 0 a MEM = 0.

Přivolání výtahu – TYPE = 0, MEM = 1 Předchozí model je rozšířen o zapamatování požadavků, které nemohly být obslouženy, protože všechny výtahy pracovaly. Ty se pak ukládají do globální proměnné (pole hodnot) podle pořadí zadání, např. 3.patro = 1, 1.patro = 2, 5.patro = 3 (obr. 3.9). V případě vyřízení požadavku se

11

čísla u pater sníží, a to až k hodnotě 0, která je výchozí. Při výpočtu se napřed zkusí obsloužit nejstarší (hodnota 1) požadavek, pokud existuje, a až pak dostává možnost případný další vnější požadavek.

Obrázek 3.9: pole zapamatovaných požadavků (TYP=0, MEM=1).

Přivolání výtahu – TYPE = 1, MEM = 0 Při zmáčknutí vnějšího tlačítka určujícího směr požadované jízdy, přechází model do stavu stop-stav, kdy pracuje jen proces controller, který prochází všechny výtahy. Pokud je výtah používán, dále se s ním nepracuje. Pokud je výtah volný, porovnává se jeho absolutní hodnota rozdílu nynějšího patra výtahu a požadovaného patra. Pokud je menší než poslední nejmenší hodnota, zapamatovává se tento výtah a daná hodnota. Při skončení procházení se zjistí, zda-li se našel některý nejbližší volný výtah, pokud ne, požadavek se zapomíná a končí stop-stav. Pokud volný výtah existuje, pomocí stop-stavu se na tento výtah přepíná řízení (výpočet), kdy se mu předá požadované patro a budoucí směr jízdy v daném patře. Výtah požadavek přijme a předá řízení zpět controlleru, který ukončí stop-stav a celý model dál pokračuje. Po příjezdu výtahu do daného patra se už pohybuje jen požadovaným směrem.

Přivolání výtahu – TYPE = 1, MEM = 1 Stejný princip jako předchozí model se zapamatováním, změna spočívá v pamatování požadavků v obou směrech, tj. dvě globální proměnné (pole hodnot), jedna pro jízdu směrem dolů, druhá pro jízdu směrem nahoru.

Obrázek 3.10: pole zapamatovaných požadavků (TYP=1 nebo 2, MEM=1).

12

Přivolání výtahu – TYPE = 2, MEM = 0 Při zmáčknutí vnějšího tlačítka určujícího směr požadované jízdy, přechází model do stavu stop-stav, kdy pracuje jen proces controller, který prochází všechny výtahy. Pokud je výtah používán a projíždí dané patro v požadovaném směru, nebo není používán, porovnává se jeho absolutní hodnota rozdílu nynějšího patra výtahu a požadovaného patra, pokud je menší než poslední nejmenší hodnota, zapamatovává se tento výtah, typ přenosu (volný/používaný výtah) a daná hodnota. Po projití všech výtahů se zjistí, zda-li se našel vhodný výtah, pokud ne, požadavek se zapomíná. Pokud ano, předá se pomocí stop-stavu na tento výtah řízení (výpočet), kdy se mu předá požadované patro. Výtah požadavek přijme, pokud je typ přenosu „volný výtah“, nachystá se výtah pro jeho obsluhu. Pokud je typ přenosu „používaný výtah“, vloží výtah dané patro do seznamu vyřizovaných požadavků, čímž zajistí zastavení výtahu v daném patře. Pokud na dané patro již existoval požadavek na zastavení, požadavky se neduplikují, novější se zapomíná. Pak výtah předá řízení zpět controlleru, který ukončí stop-stav a celý model dál pokračuje.

Obrázek 3.11: ukázka možné situace vnitřních požadavků.

13

Přivolání výtahu – TYPE = 2, MEM = 1 Již úplný model systému výtahu se sběrným řízením.

Použití volného výtahu Při vnitřním požadavku u volného/prázdného výtahu, se tento výtah přepne do režimu používání. Výtah zařadí požadavek a je schopen přijmout další požadavky, ale už jen směrem určeným prvotním požadavkem; pak se výtah začne přesouvat daným směrem. Dle parametrů je schopen si do seznamu požadavků přidat další požadavek. Pokud přijede do patra, které má být obslouženo, zastaví, odebere si požadavek ze seznamu a je schopen přijmout další požadavky, jinak pokračuje dál v přesunu. Pokud byl odebrán poslední požadavek, přechází výtah do režimu nepoužívaný/volný. V případě parametru MEM = 1 a zastavení výtahu z důvodu vnitřního požadavku v patře zapamatovaným s požadavkem, je tento požadavek smazán a zapamatované požadavky setříděny do platné sestavy (tj. 1, 2, 3... až poslední požadavek, bez číselné mezery).

14

Kapitola 4

Vlastnosti modelu Tato kapitola se zabývá formulací některých zajímavých vlastností a následným ověřením jejich platnosti pomocí nástroje DiVinE.

Vlastnosti byly popsány pomoci logiky LTL, která je nejpoužívanější logika při specifikování software, a jejíž syntaxe je: LTL := A | ς1 ˄ ς2 | ¬ ς | Xς | ς1 U ς2 Při popisu vlastností v logice LTL používáme tyto zkratky : • •

F p = true U p G p = ¬ (F (¬ p))

Velikosti stavových prostorů základních modelů při neuvažovaní LTL vlastností: Typ modelu

Počet stavů

Počet přechodů

ELEVS=2, FLOORS=3. TYPE = 0, MEM = 0

19609

42529


327900

695708


23278

49028


1035377

1986753


46214

76592


2079949

3710197

Tabulka 4.1: velikost základního modelu.

Následuje seznam vlastností zajímavých pro daný model: 1. vlastnost: „Výtah není volný dokud má určen směr jízdy.“ Při vstupu zákazníka do prázdného nepřivolaného výtahu nebo při zavolání výtahu controllerem, se výtahu přidělí směr jeho budoucí jízdy a změní i jeho stav použitelnosti (usage[číslo_výtahu] = 1 nebo 2). Výtah se stává volným při snížení jemu zadaných požadavků na přepravu na hodnotu 0 (jobs = 0), kdy se nuluje směr jízdy daného výtahu. Vlastnost v LTL pro 1.výtah: G((usage[0] != 0)U(m[0] = 0))

15

Následující tabulka (4.2) ukazuje velikosti stavového prostoru pro tuto vlastnost. Typ modelu

Počet stavů

Počet přechodů


36167

114034


611832

1858413


43924

136770


1992899

5539195


88882

216682


4021492

10389573

Tabulka 4.2: 1.vlastnost.

2. vlastnost: „Při přivolání výtahu controllerem přijede tento výtah do cílového patra“ Pokud po přivolání výtahu najde controller vhodný výtah, označí jej (s = 0; tj.1.výtah) a předá mu jako úkol číslo patra s požadavkem (job = 2). Výtah si jej zapamatuje (ligtv = 2) a začne k němu přijíždět (m[0] != 0). Jakmile do něj přijede (floor[0] = 2), zastavuje (m = 0) a nechá si zadat požadavek na přepravu. Vlastnost v LTL pro 1.výtah a 2.patro (poslední): G((s = 0 ˄ job = 2) => F(floor[0] = 2)) Následující tabulka (4.3) ukazuje velikosti stavového prostoru pro tuto vlastnost. Typ modelu

Počet stavů

Počet přechodů


20438

43977


337388

711556


24316

50846


1050742

2011367


58042

95028


2347993

4147978

Tabulka 4.3: 2.vlastnost pro 1.výtah a 2.patro (poslední).

Vlastnost v LTL pro 2.výtah a 0.patro (první): G((s = 1 ˄ job = 0) => F(floor[1] = 0)) Následující tabulka (4.4) ukazuje velikosti stavového prostoru pro tuto vlastnost. Vlastnost v LTL pro 1.výtah a 1.patro (mezipatro): G((s = 0 ˄ job = 1) => F(floor[0] = 1)) Tabulka (4.5) ukazuje velikosti stavového prostoru pro tuto vlastnost.

16

Typ modelu

Počet stavů

Počet přechodů


20419

43939


333585

705534


24314

50842


1050708

2011299


58059

94972


2346660

4142815

Tabulka 4.4: 2.vlastnost pro 2.výtah a 0.patro (první).

Typ modelu

Počet stavů

Počet přechodů


20513

43917


341442

716292


24966

51600


1064249

2026469


61740

99614


2371479

4158577

Tabulka 4.5: 2.vlastnost pro 1.výtah v 1.patře (mezipatro).

3. vlastnost: „Když uživatel zavolá výtah stisknutím tlačítka, bude na to zareagováno“ Pokud uživatel přivolá výtah (v daném patře, job = 0), tak controller se pokusí najít možný výtah. Pokud se vhodný najde, je zaúkolován daným požadavkem. Jinak se zde vlastnost dělí dle parametru MEM. Pokud je hodnota MEM 0, je tento požadavek zapomenut. Pokud je hodnota MEM 1, je tento požadavek zapamatován a bude někdy obsloužen. Vlastnost v LTL pro 0.patro (první):

G((job = 0) => F (s != -1 ˄ s != 2 ˄ job = 0)) Následující tabulka (4.6) ukazuje velikosti stavového prostoru pro tuto vlastnost. Typ modelu

Počet stavů

Počet přechodů


39005

126522


654504

2079909


46331

145806


2067655

5942229


91577

223736


4142230

11007721

Tabulka 4.6: 3.vlastnost pro 0.patro (první).

17

Vlastnost v LTL pro 1.patro (mezipatro):


Počet stavů

Počet přechodů


38230

118288


652135

2066925


45343

135356


2063450

5923675


90523

212988


4131852

10983477

Tabulka 4.7: 3.vlastnost pro 1.patro (mezipatro).

Vlastnost v LTL pro 2.patro (poslední):


Počet stavů

Počet přechodů


38218

118264


653014

2068683


45496

135662


2065985

5928745


90742

213592


4142230

11007721

Tabulka 4.8: 3.vlastnost pro 2.patro (poslední).

4. vlastnost: „Výtah nelze nikdy přivolat pomocí controlleru pokud je používán“ Pokud je výtah používán (usage[0] = 1), nelze jej vnějším požadavkem přímo přivolat do daného patra (usage[0] = 2). Přivolat výtah přímo vnějším požadavkem lze jen z volného výtahu (usage[0] = 0). Vlastnost v LTL pro 1.výtah: G((usage[0] = 1) => X (usage[0] != 2 U usage[0] = 0)) Následující tabulka (4.9) ukazuje velikosti stavového prostoru pro tuto vlastnost.

18

Typ modelu

Počet stavů

Počet přechodů


34023

106295


594491

1808759


39058

117220


1918879

5256361


81674

191596


3788870

9572409


5. vlastnost: „Používaný výtah se může stát po uvolnění opět používaným“ Používaný výtah (usage[0] = 1) se po dokončení úkolů a jeho uvolnění (usage[0] = 0), může opět stát používaným (usage[0] = 1). Vlastnost v LTL pro 1.výtah: G(((usage[0] = 1) => F(usage[0] = 0)) => F(usage[0] = 1)) Následující tabulka (4.10) ukazuje velikosti stavového prostoru pro tuto vlastnost. Typ modelu

Počet stavů

Počet přechodů


26061

63419


414855

968028


31734

78498


1261864

2654575


57942

113970


2587770

5194973


6. vlastnost: „Přivolaný výtah musí být použit, jinak nedojde k jeho uvolnění“ Jakmile přivolaný výtah (usage[0] = 2) přijede do požadovaného patra, musí být použit, jinak stojí a čeká na vnitřní požadavek, tj. nelze jej znova zavolat controllerem. Vlastnost v LTL pro 1.výtah: G((usage[0] = 2) => X (usage[0] != 0 U usage[0] = 1)) Následující tabulka (4.11) ukazuje velikosti stavového prostoru pro tuto vlastnost.

19

Typ modelu

Počet stavů

Počet přechodů


23519

55996


372505

849863


28998

69278


1123903

2279617


54340

102360


2345673

4541459


7. vlastnost: „Všechny zapamatované požadavky se vyřeší“ Pokud nějaký požadavek nemohl být obsloužen a parametr MEM má hodnotu 1, požadavek se zapamatuje a zvýší hodnotu v proměnné max_memory o 1 (max_memory obsahuje počet zapamatovaných požadavků). Po vyřízení všech zapamatovaných požadavků bude mít proměnná max_memory opět hodnotu 0. Pokud má parametr MEM hodnotu 0, nelze ověřit platnost, neboť model neobsahuje proměnnou max_memory. Vlastnost v LTL: G((max_memory != 0) => F(max_memory = 0)) Následující tabulka (4.12) ukazuje velikosti stavového prostoru pro tuto vlastnost. Typ modelu

Počet stavů

Počet přechodů


nelze

nelze


597490

1808962


nelze

nelze


2021339

5723509


nelze

nelze


3968043

10360753


Grafy počtu stavů vlastností dle modelu Na níže uvedených grafech lze vypozorovat značný nárůst složitosti u první, třetí a čtvrté vlastnosti. U sedmé, taktéž složité, vlastnosti nelze v některých případech (MEM = 0) výpočet uskutečnit.

20

●

Model - MEM = 0, TYPE = 0 (obr.4.1): 45000 40000

Základ 1.vlastnost 2.A vlastnost 2.B vlastnost 2.C vlastnost 3.A vlastnost 3.B vlastnost 3.C vlastnost 4.vlastnost 5.vlastnost 6.vlastnost 7.vlastnost

35000 30000 25000 20000 15000 10000 5000 0

Obrázek 4.1: MEM = 0, TYPE = 0. ●

Model - MEM = 1, TYPE = 0 (obr.4.2): 700000 Základ

600000

1.vlastnost 2.A vlastnost

500000

2.B vlastnost 2.C vlastnost

400000

3.A vlastnost

300000


200000

4.vlastnost 5.vlastnost

100000


0



Základ

40000

1.vlastnost

35000

2.A vlastnost

30000


25000

3.A vlastnost 3.B vlastnost

20000

3.C vlastnost

15000

4.vlastnost

10000


5000

7.vlastnost

0

Obrázek 4.3: MEM = 0, TYPE = 1.

21

●

Model - MEM = 1, TYPE = 1(obr.4.4): 2500000 Základ

2000000

1.vlastnost 2.A vlastnost 2.B vlastnost

1500000

2.C vlastnost 3.A vlastnost 3.B vlastnost

1000000

3.C vlastnost 4.vlastnost

500000

5.vlastnost 6.vlastnost 7.vlastnost

0



Základ 1.vlastnost

80000 70000

2.A vlastnost 2.B vlastnost

60000

2.C vlastnost 3.A vlastnost

50000

3.B vlastnost

40000

3.C vlastnost 4.vlastnost

30000 20000


10000

7.vlastnost

0

●

Model (MEM = 1, TYPE = 2 (obr.4.6): 4500000 4000000

Základ 1.vlastnost 2.A vlastnost 2.B vlastnost 2.C vlastnost 3.A vlastnost 3.B vlastnost 3.C vlastnost 4.vlastnost 5.vlastnost 6.vlastnost 7.vlastnost

3500000 3000000 2500000 2000000 1500000 1000000 500000 0

Obrázek 4.6: MEM = 1, TYPE = 2.

22

Experimenty: V níže uvedené tabulce uvádíme velikosti stavového prostoru i u jiných parametrů a bez použití LTL vlastností. Typ modelu

Počet stavů

Počet přechodů


126796

324428


3025042

10033088


8079054

18730946


182518

448808


419408

763394


2645074

5258888

...

???

???1

Tabulka 4.13: Experimenty.

1 Další hodnoty experimentů pro vysokou výpočetní náročnost dodám později.

23

Kapitola 5

Závěr Cílem této práce bylo navrhnout model systému výtahů se sběrným řízením a sepsat několik formulí v LTL logice, které mohou platit na daném modelu. Práce je rozdělena na několik částí, první část pojednává o jazyce DiVinE a základním pohledu na systém výtahů se sběrným řízením. Druhá se zabývá modelováním daného systému spolu s vytvářením jeho vlastností a tvorbou parametrického modelu s vysvětlením jeho parametrů. Ve třetí části se hovoří o vlastnostech modelu a hodnotách jejich výpočtu. Při modelování jsme používali tzv.stop-stav náhradou za chybějící konstrukci „atomic“ používanou modelovacím jazykem ProMela. Hodilo by se tedy, aby jazyk DVE tuto nebo podobnou konstrukci obsahoval.

24

Použitá literatura •

DiVinE. Distributed Verification Environment. .

•

LAPÁČEK, Vladimír. DiVinE – modul pro swapování stavů do sítě [online]. 2005 [cit. 2008-04-01]. Dostupný z www:

•

BEZDĚK, Peter. Modelování pro verifikační nástroj DiVinE [online]. 2005 [cit. 2008-04-03]. Dostupný v archivu závěrečných prací z www:

25

Dodatek A

Zdrojový kód parametrizovaného modelu 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56

default(ELEVS,2)dnl; default(FLOORS,3)dnl; default(TYPE,2)dnl; default(MEM,0)dnl; //stop state for calculation, value -1 == all running, else stop int s = -1; //job for an elevator byte job; //elevator X in use - value 0 - no use, value 1 - used by //customer, value 2 - travels to customer byte usage[ELEVS] = {myloop(x,0,decr(ELEVS),`0',`,')}; //number, where elevator X is byte floor[ELEVS] = {myloop(x,0,decr(ELEVS),`0',`,')}; //direction of elevator's move int m[ELEVS] = {myloop(x,0,decr(ELEVS),`0',`,')}; //direction of future's move in floor X or sending for elevator //in the floor X int dir[FLOORS]={myloop(x,0,decr(FLOORS),`0',`,')}; define(memoryUpdate, `//number of memorized demands byte max_memory = 0; //id working with memorized demand byte mem=0; //various value byte i; ') ifelse(MEM,1,`memoryUpdate',`') define(controlerT0, `process Controler { //number of nearest elevator byte num = ELEVS; //smallest distance byte vzd = FLOORS; //various value byte i; //type of carry - value 1 - nearest non use elevator byte type=0; state A,B,C,G; init A; trans forloop(x0,0,decr(FLOORS), À -> B { guard dir[x0]==0; effect s=ELEVS, job=x0, i=0;}, ') B -> C { guard i<ELEVS and usage[i]==false;}, B -> B { guard i<ELEVS and usage[i]==true; effect i=i+1;}, B -> B { guard i<ELEVS and usage[i]==2; effect i=i+1;}, C -> B { guard job-floor[i]>=0 and job-floor[i] B { guard job-floor[i]<0 and floor[i]-job B { guard job-floor[i]>=0 and job-floor[i]>=vzd;

26

57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123

C -> B B -> A B -> G G -> A }

effect i=i+1;}, { guard job-floor[i]<0 and floor[i]-job>=vzd; effect i=i+1;}, { guard i==ELEVS and type==0; effect s=-1;}, { guard i==ELEVS and type==1; effect usage[num]=2, s=num, num=ELEVS, vzd=FLOORS, type=0, dir[job]=1;}, { guard s==ELEVS; effect s=-1;};

') define(controlerT0M, `//memorized floors of demands byte memory[FLOORS]={myloop(x,0,decr(FLOORS),`0',`,')}; process Controler { //number of nearest elevator byte num = ELEVS; //smallest distance byte vzd = FLOORS; //type of carry - value 1 - nearest non use elevator byte type=0; state A,B,C,G,H,I; init A; trans forloop(x0,0,decr(FLOORS), À -> B { guard s==-1 and memory[x0]==1 and dir[x0]==0; effect s=ELEVS, job=x0, i=0, mem=1;}, ') A -> I { guard s==-1 and max_memory==0; effect s=ELEVS, mem=0; }, B -> C { guard i<ELEVS and usage[i]==false;}, B -> B { guard i<ELEVS and usage[i]==true; effect i=i+1;}, B -> B { guard i<ELEVS and usage[i]==2; effect i=i+1;}, C -> B { guard job-floor[i]>=0 and job-floor[i] B { guard job-floor[i]<0 and floor[i]-job B { guard job-floor[i]>=0 and job-floor[i]>=vzd; effect i=i+1;}, C -> B { guard job-floor[i]<0 and floor[i]-job>=vzd; effect i=i+1;}, B -> A { guard i==ELEVS and type==0 and mem==0; effect num=ELEVS, vzd=FLOORS, s=-1, max_memory=max_memory+1, memory[job]=max_memory;}, B -> I { guard i==ELEVS and type==0 and mem==1; effect num=ELEVS, vzd=FLOORS, mem=0;}, B -> G { guard i==ELEVS and type==1 and mem==0; effect usage[num]=2, s=num, num=ELEVS, vzd=FLOORS, type=0, dir[job]=1;}, B -> H { guard i==ELEVS and type==1 and job>0 and mem==1; effect dir[job]=-1, i=0;}, B -> H { guard i==ELEVS and type==1 and job<2 and mem==1; effect dir[job]=1, i=0;}, G -> A { guard s==ELEVS; effect s=-1;}, H -> H { guard i H { guard i0; effect memory[i]=memory[i]-1, i=i+1; }, H -> G { guard i==FLOORS; effect max_memory=max_memory-1, usage[num]=2, s=num, num=ELEVS, vzd=FLOORS, type=0, mem=0;}, forloop(x8,0,decr(FLOORS),

27

124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190

Ì -> B ') I -> A }

{ guard memory[x8]==0 and dir[x8]==0; effect job=x8, i=0;}, { effect s=-1;};

') define(controlerT1, `process Controler { //number of nearest elevator byte num = ELEVS; //smallest distance byte vzd = FLOORS; //various value byte i; //type of carry - value 1 - nearest non use elevator byte type=0; state A,B,C,G; init A; trans forloop(x0,0,decr(decr(FLOORS)), À -> B { guard dir[x0]==0; effect s=ELEVS, job=x0, i=0, dir[x0]=1;}, ') forloop(x1,1,decr(FLOORS), À -> B { guard dir[x1]==0; effect s=ELEVS, job=x1, i=0, dir[x1]=-1;}, ') B -> C { guard i<ELEVS and usage[i]==false;}, B -> B { guard i<ELEVS and usage[i]==true; effect i=i+1;}, B -> B { guard i<ELEVS and usage[i]==2; effect i=i+1;}, C -> B { guard job-floor[i]>=0 and job-floor[i] B { guard job-floor[i]<0 and floor[i]-job B { guard job-floor[i]>=0 and job-floor[i]>=vzd; effect i=i+1;}, C -> B { guard job-floor[i]<0 and floor[i]-job>=vzd; effect i=i+1;}, B -> A { guard i==ELEVS and type==0; effect s=-1, dir[job]=0;}, B -> G { guard i==ELEVS and type==1; effect usage[num]=2, s=num, num=ELEVS, vzd=FLOORS, type=0;}, G -> A { guard s==ELEVS; effect s=-1;}; } ') define(controlerT1M, `//memorized floors of demands byte memory_down[FLOORS]={myloop(x,0,decr(FLOORS),`0',`,')}; byte memory_up[FLOORS]={myloop(x,0,decr(FLOORS),`0',`,')}; process Controler { //number of nearest elevator byte num = ELEVS; //smallest distance byte vzd=FLOORS; //type of carry - value 1 - nearest non use elevator byte type=0; state A,B,C,G,H,I; init A; trans forloop(x0,0,decr(decr(FLOORS)),

28

191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257

À -> B

{ guard s==-1 and memory_up[x0]==1 and dir[x0]==0; effect s=ELEVS, job=x0, i=0, dir[x0]=1, mem=1;},

') forloop(x1,1,decr(FLOORS), À -> B { guard s==-1 and memory_down[x1]==1 and dir[x1]==0; effect s=ELEVS, job=x1, i=0, dir[x1]=-1, mem=1;}, ') A -> I { guard s==-1 and max_memory==0; effect s=ELEVS, mem=0; }, B -> C { guard i<ELEVS and usage[i]==false;}, B -> B { guard i<ELEVS and usage[i]==true; effect i=i+1;}, B -> B { guard i<ELEVS and usage[i]==2; effect i=i+1;}, C -> B { guard job-floor[i]>=0 and job-floor[i] B { guard job-floor[i]<0 and floor[i]-job B { guard job-floor[i]>=0 and job-floor[i]>=vzd; effect i=i+1;}, C -> B { guard job-floor[i]<0 and floor[i]-job>=vzd; effect i=i+1;}, B -> A { guard i==ELEVS and type==0 and mem==0 and dir[job]==1; effect num=ELEVS, vzd=FLOORS, s=-1, dir[job]=0, max_memory=max_memory+1, memory_up[job]=max_memory;}, B -> A { guard i==ELEVS and type==0 and mem==0 and dir[job]==-1; effect num=ELEVS, vzd=FLOORS, s=-1, dir[job]=0, max_memory=max_memory+1, memory_down[job]=max_memory;}, B -> I { guard i==ELEVS and type==0 and mem==1; effect num=ELEVS, vzd=FLOORS, mem=0, dir[job]=0;}, B -> G { guard i==ELEVS and type==1 and mem==0; effect usage[num]=2, s=num, num=ELEVS, vzd=FLOORS, type=0;}, B -> H { guard i==ELEVS and type==1 and mem==1; effect i=0;}, G -> A { guard s==ELEVS; effect s=-1;}, H -> H { guard i H { guard i0 and memory_down[i]==0; effect memory_up[i]=memory_up[i]-1, i=i+1;}, H -> H { guard i0; effect memory_down[i]=memory_down[i]-1, i=i+1;}, H -> H { guard i0 and memory_down[i]>0; effect memory_down[i]=memory_down[i]-1, memory_up[i]=memory_up[i]-1, i=i+1;}, H -> G { guard i==FLOORS; effect max_memory=max_memory-1, usage[num]=2, s=num, num=ELEVS, vzd=FLOORS, type=0, mem=0;}, forloop(x8,0,decr(decr(FLOORS)), Ì -> B { guard memory_up[x8]==0 and dir[x8]==0; effect job=x8, dir[x8]=1, i=0;}, ') forloop(x9,1,decr(FLOORS), Ì -> B { guard memory_down[x9]==0 and dir[x9]==0; effect job=x9, dir[x9]=-1, i=0;}, ') I -> A { effect s=-1;}; } ') define(controlerT2, `process Controler { //number of nearest elevator byte num = ELEVS;

29

258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324

//smallest distance byte vzd=FLOORS; //various value byte i; //type of carry - value 1 - nearest non use elevator //- value 2 - collecting function byte type=0; state A,B,C,D,E,F,G; init A; trans forloop(x0,0,decr(decr(FLOORS)), À -> B { guard dir[x0]==0; effect s=ELEVS, job=x0, i=0, dir[x0]=-1;}, ') forloop(x1,1,decr(FLOORS), A -> B { guard dir[x1]==0; effect s=ELEVS, job=x1, i=0, dir[x1]=1;}, ') B -> C { guard i<ELEVS and usage[i]==false;}, B -> D { guard i<ELEVS and usage[i]==true;}, B -> B { guard i<ELEVS and usage[i]==2; effect i=i+1;}, D -> B { guard dir[job]+m[i]!=-2 and dir[job]+m[i]!=2; effect i=i+1;}, D -> E { guard dir[job]+m[i]==2 and job>floor[i];}, D -> B { guard dir[job]+m[i]==2 and job<=floor[i]; effect i=i+1;}, D -> F { guard dir[job]+m[i]==-2 and job B { guard dir[job]+m[i]==-2 and job>=floor[i]; effect i=i+1;}, E -> B { guard job-floor[i] B { guard job-floor[i]>=vzd; effect i=i+1;}, F -> B { guard floor[i]-job B { guard floor[i]-job>=vzd; effect i=i+1;}, C -> B { guard job-floor[i]>=0 and job-floor[i] B { guard job-floor[i]<0 and floor[i]-job B { guard job-floor[i]>=0 and job-floor[i]>=vzd; effect i=i+1;}, C -> B { guard job-floor[i]<0 and floor[i]-job>=vzd; effect i=i+1;}, B -> A { guard i==ELEVS and type==0; effect dir[job]=0, s=-1;}, B -> G { guard i==ELEVS and type==1 and job>0; effect usage[num]=2, s=num, num=ELEVS, vzd=FLOORS, type=0, dir[job]=-1;}, B -> G { guard i==ELEVS and type==1 and job<decr(FLOORS); effect usage[num]=2, s=num, num=ELEVS, vzd=FLOORS, type=0, dir[job]=1;}, B -> G { guard i==ELEVS and type==2; effect s=num, num=ELEVS, vzd=FLOORS, type=0, dir[job]=0;}, G -> A { guard s==ELEVS; effect s=-1;}; } ') define(controlerT2M, `//memorized floors of demands byte memory_down[FLOORS]={myloop(x,0,decr(FLOORS),`0',`,')}; byte memory_up[FLOORS]={myloop(x,0,decr(FLOORS),`0',`,')}; process Controler {

30

325 326 327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371 372 373 374 375 376 377 378 379 380 381 382 383 384 385 386 387 388 389 390 391

//number of nearest elevator byte num = ELEVS; //smallest distance byte vzd=FLOORS; //various value byte i; //type of carry - value 1 - nearest non use elevator //- value 2 - collecting function byte type=0; state A,B,C,D,E,F,G,H,I; init A; trans forloop(x0,0,decr(decr(FLOORS)), À -> B { guard s==-1 and memory_up[x0]==1 and dir[x0]==0; effect s=ELEVS, job=x0, i=0, dir[x0]=-1, mem=1;}, ') forloop(x1,1,decr(FLOORS), À -> B { guard s==-1 and memory_down[x1]==1 and dir[x1]==0; effect s=ELEVS, job=x1, i=0, dir[x1]=1, mem=1;}, ') A -> I { guard s==-1 and max_memory==0; effect s=ELEVS, mem=0, i=0;}, B -> C { guard i<ELEVS and usage[i]==false;}, B -> D { guard i<ELEVS and usage[i]==true;}, B -> B { guard i<ELEVS and usage[i]==2; effect i=i+1;}, D -> B { guard dir[job]+m[i]!=-2 and dir[job]+m[i]!=2; effect i=i+1;}, D -> E { guard dir[job]+m[i]==2 and job>floor[i];}, D -> B { guard dir[job]+m[i]==2 and job<=floor[i]; effect i=i+1;}, D -> F { guard dir[job]+m[i]==-2 and job B { guard dir[job]+m[i]==-2 and job>=floor[i]; effect i=i+1;}, E -> B { guard job-floor[i] B { guard job-floor[i]>=vzd; effect i=i+1;}, F -> B { guard floor[i]-job B { guard floor[i]-job>=vzd; effect i=i+1;}, C -> B { guard job-floor[i]>=0 and job-floor[i] B { guard job-floor[i]<0 and floor[i]-job B { guard job-floor[i]>=0 and job-floor[i]>=vzd; effect i=i+1;}, C -> B { guard job-floor[i]<0 and floor[i]-job>=vzd; effect i=i+1;}, B -> I { guard i==ELEVS and type==0 and mem==1; effect dir[job]=0, mem=0, num=ELEVS, vzd=FLOORS, i=0;}, B -> A { guard i==ELEVS and type==0 and mem==0 and dir[job]==-1; effect num=ELEVS, vzd=FLOORS, s=-1, dir[job]=0, max_memory=max_memory+1, memory_up[job]=max_memory;}, B -> A { guard i==ELEVS and type==0 and mem==0 and dir[job]==1; effect num=ELEVS, vzd=FLOORS, s=-1, dir[job]=0, max_memory=max_memory+1, memory_down[job]=max_memory;}, B -> G { guard i==ELEVS and type==1 and mem==0 and dir[job]==1; effect usage[num]=2, s=num, num=ELEVS, vzd=FLOORS, type=0, dir[job]=-1;}, B -> G { guard i==ELEVS and type==1 and mem==0 and dir[job]==-1; effect usage[num]=2, s=num, num=ELEVS, vzd=FLOORS, type=0, dir[job]=1;}, B -> H { guard i==ELEVS and type==1 and mem==1;

31

392 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413 414 415 416 417 418 419 420 421 422 423 424 425 426 427 428 429 430 431 432 433 434 435 436 437 438 439 440 441 442 443 444 445 446 447 448 449 450 451 452 453 454 455 456 457 458

effect i=0;}, { guard i==ELEVS and type==2 and mem==0; effect s=num, num=ELEVS, vzd=FLOORS, type=0, dir[job]=0;}, B -> H { guard i==ELEVS and type==2 and mem==1; effect dir[job]=0, i=0;}, H -> H { guard i H { guard i0 and memory_down[i]==0; effect memory_up[i]=memory_up[i]-1, i=i+1;}, H -> H { guard i0; effect memory_down[i]=memory_down[i]-1, i=i+1;}, H -> H { guard i0 and memory_down[i]>0; effect memory_down[i]=memory_down[i]-1, memory_up[i]=memory_up[i]-1, i=i+1;}, H -> G { guard i==FLOORS and type==1; effect max_memory=max_memory-1, usage[num]=2, s=num, num=ELEVS, vzd=FLOORS, type=0, mem=0;}, H -> G { guard i==FLOORS and type==2; effect max_memory=max_memory-1, s=num, num=ELEVS, vzd=FLOORS, type=0, mem=0;}, G -> A { guard s==ELEVS; effect s=-1;}, forloop(x8,0,decr(decr(FLOORS)), Ì -> B { guard memory_up[x8]==0 and dir[x8]==0; effect job=x8, dir[x8]=-1;}, ') forloop(x9,1,decr(FLOORS), Ì -> B { guard memory_down[x9]==0 and dir[x9]==0; effect job=x9, dir[x9]=1;}, ') I -> A { effect s=-1;}; } B -> G

') define(elevatorT0, `process elevatorT0_$1 { //number of jobs for this elevator byte jobs=0; //lights of floors inside the elevator byte lightv[FLOORS]={myloop(x,0,decr(FLOORS),`0',`,')}; state idle,idle2,idle_up,idle_down,move; init idle; trans //move to floor called by controller move -> move { guard s==-1 and lightv[floor[$1]]==false; effect floor[$1] = floor[$1] + m[$1];}, //called to work by controller idle -> idle2 { guard s==$1 and floor[$1]==job; effect s=ELEVS, m[$1]=dir[floor[$1]], usage[$1]=true;}, idle -> move { guard s==$1 and floor[$1]>job; effect s=ELEVS, m[$1]=-1, lightv[job]=true;}, idle -> move { guard s==$1 and floor[$1]<job; effect s=ELEVS, m[$1]=1, lightv[job]=true;}, //elevator arrives to floor called by controller move -> idle2 { guard s==-1 and usage[$1]==2 and lightv[floor[$1]]==true; effect lightv[floor[$1]]=false, usage[$1]=true;}, //customer use free elevator idle -> idle2 { guard s==-1 and usage[$1]==false and dir[floor[$1]]==0; effect usage[$1]=true, dir[floor[$1]]=1;}, //move of first customer forloop(x2,0,decr(decr(FLOORS)), ìdle2 -> idle_down { guard s==-1 and floor[$1]>x2 and lightv[x2]==false; effect m[$1]=-1, lightv[x2]=true, jobs=jobs+1,

32

459 460 461 462 463 464 465 466 467 468 469 470 471 472 473 474 475 476 477 478 479 480 481 482 483 484 485 486 487 488 489 490 491 492 493 494 495 496 497 498 499 500 501 502 503 504 505 506 507 508 509 510 511 512 513 514 515 516 517 518 519 520 521 522 523 524 525

dir[floor[$1]]=0;}, ') forloop(x3,1,decr(FLOORS), idle2 -> idle_up { guard s==-1 and floor[$1]<x3 and lightv[x3]==false; effect m[$1]=1, lightv[x3]=true, jobs=jobs+1, dir[floor[$1]]=0;}, ') //arrival of others customers, or last job with empty elevator move -> idle_up { guard s==-1 and lightv[floor[$1]]==true and jobs-1>0 and m[$1]==1; effect lightv[floor[$1]]=false, jobs=jobs-1;}, move -> idle_down { guard s==-1 and lightv[floor[$1]]==true and jobs-1>0 and m[$1]==-1; effect lightv[floor[$1]]=false, jobs=jobs-1;}, move -> idle { guard s==-1 and lightv[floor[$1]]==true and jobs-1==0; effect lightv[floor[$1]]=false, jobs=0, usage[$1]=false, m[$1]=0;}, //choice other floors in move direction forloop(x6, 1, decr(FLOORS), ìdle_up -> idle_up { guard s==-1 and floor[$1]<x6 and lightv[x6]==false; effect lightv[x6]=true, jobs=jobs+1;}, ') idle_up -> move {guard s==-1;}, forloop(x7, 0, decr(decr(FLOORS)), ìdle_down -> idle_down { guard s==-1 and floor[$1]>x7 and lightv[x7]==false; effect lightv[x7]=true, jobs=jobs+1;}, ') idle_down -> move {guard s==-1;}; } ') define(elevatorT0M, `process elevatorT0M_$1 { //number of jobs for this elevator byte jobs=0; //lights of floors inside the elevator byte lightv[FLOORS]={myloop(x,0,decr(FLOORS),`0',`,')}; state idle,idle2,idle_up,idle_down,move,del_memory; init idle; trans //move to floor called by controller move -> move { guard s==-1 and lightv[floor[$1]]==false; effect floor[$1] = floor[$1] + m[$1];}, //called to work by controller idle -> idle2 { guard s==$1 and floor[$1]==job; effect s=ELEVS, m[$1]=dir[floor[$1]], usage[$1]=true;}, idle -> move { guard s==$1 and floor[$1]>job; effect s=ELEVS, m[$1]=-1, lightv[job]=true;}, idle -> move { guard s==$1 and floor[$1]<job; effect s=ELEVS, m[$1]=1, lightv[job]=true;}, //elevator arrives to floor called by controller move -> idle2 { guard s==-1 and usage[$1]==2 and lightv[floor[$1]]==true; effect lightv[floor[$1]]=false, usage[$1]=true;}, //customer use free elevator idle -> idle2 { guard s==-1 and usage[$1]==false and dir[floor[$1]]==0; effect usage[$1]=true, dir[floor[$1]]=1;}, //move of first customer forloop(x2,0,decr(decr(FLOORS)), ìdle2 -> idle_down { guard s==-1 and floor[$1]>x2 and lightv[x2]==false;

33

526 527 528 529 530 531 532 533 534 535 536 537 538 539 540 541 542 543 544 545 546 547 548 549 550 551 552 553 554 555 556 557 558 559 560 561 562 563 564 565 566 567 568 569 570 571 572 573 574 575 576 577 578 579 580 581 582 583 584 585 586 587 588 589 590 591 592

effect m[$1]=-1, lightv[x2]=true, jobs=jobs+1, dir[floor[$1]]=0;},

') forloop(x3,1,decr(FLOORS), ìdle2 -> idle_up { guard s==-1 and floor[$1]<x3 and lightv[x3]==false; effect m[$1]=1, lightv[x3]=true, jobs=jobs+1, dir[floor[$1]]=0;}, ') //arrival of others customers, or last job with empty elevator move -> idle_up { guard s==-1 and lightv[floor[$1]]==true and jobs-1>0 and m[$1]==1; effect lightv[floor[$1]]=false, jobs=jobs-1;}, move -> idle_down { guard s==-1 and lightv[floor[$1]]==true and jobs-1>0 and m[$1]==-1; effect lightv[floor[$1]]=false, jobs=jobs-1;}, move -> idle { guard s==-1 and lightv[floor[$1]]==true and jobs-1==0; effect lightv[floor[$1]]=false, jobs=0, usage[$1]=false, m[$1]=0;}, //choice other floors in move direction forloop(x6, 1, decr(FLOORS), ìdle_up -> idle_up { guard s==-1 and floor[$1]<x6 and lightv[x6]==false; effect lightv[x6]=true, jobs=jobs+1;}, ') idle_up -> move {guard s==-1;}, idle_up -> del_memory { guard s==-1 and memory[floor[$1]]>0; effect mem=memory[floor[$1]], memory[floor[$1]]=0, i=0, max_memory=max_memory-1, s=ELEVS;}, del_memory -> del_memory { guard imem; effect memory[i]=memory[i]-1, i=i+1;}, del_memory -> del_memory { guard i move { guard i==FLOORS; effect s=-1;}, forloop(x7, 0, decr(decr(FLOORS)), ìdle_down -> idle_down { guard s==-1 and floor[$1]>x7 and lightv[x7]==false; effect lightv[x7]=true, jobs=jobs+1;}, ') idle_down -> move { guard s==-1;}, idle_down -> del_memory { guard s==-1 and memory[floor[$1]]>0; effect mem=memory[floor[$1]], memory[floor[$1]]=0, i=0, max_memory=max_memory-1, s=ELEVS;}; } ') define(elevatorT1, `process elevatorT1_$1 { //number of jobs for this elevator byte jobs=0; //lights of floors inside the elevator byte lightv[FLOORS]={myloop(x,0,decr(FLOORS),`0',`,')}; state idle,idle2,idle_up,idle_down,move; init idle; trans //move to floor called by controller move -> move { guard s==-1 and lightv[floor[$1]]==false; effect floor[$1] = floor[$1] + m[$1];}, //called to work by controller idle -> idle2 { guard s==$1 and floor[$1]==job; effect s=ELEVS, m[$1]=dir[floor[$1]], usage[$1]=true;}, idle -> move { guard s==$1 and floor[$1]>job;

34

593 594 595 596 597 598 599 600 601 602 603 604 605 606 607 608 609 610 611 612 613 614 615 616 617 618 619 620 621 622 623 624 625 626 627 628 629 630 631 632 633 634 635 636 637 638 639 640 641 642 643 644 645 646 647 648 649 650 651 652 653 654 655 656 657 658 659

effect s=ELEVS, m[$1]=-1, lightv[job]=true;}, { guard s==$1 and floor[$1]<job; effect s=ELEVS, m[$1]=1, lightv[job]=true;}, //elevator arrives to floor called by controller move -> idle2 { guard s==-1 and usage[$1]==2 and lightv[floor[$1]]==true; effect lightv[floor[$1]]=false, usage[$1]=true, m[$1]=dir[floor[$1]];}, //customer use free elevator idle -> idle2 { guard s==-1 and usage[$1]==false and floor[$1]>0 and dir[floor[$1]]==0; effect usage[$1]=true, dir[floor[$1]]=-1, m[$1]=-1;}, idle -> idle2 { guard s==-1 and usage[$1]==false and floor[$1]<decr(FLOORS) and dir[floor[$1]]==0; effect usage[$1]=true, dir[floor[$1]]=1, m[$1]=1;}, //move of first customer forloop(x2,0,decr(decr(FLOORS)), ìdle2 -> idle_down { guard s==-1 and floor[$1]>x2 and dir[floor[$1]]==-1 and lightv[x2]==false; effect lightv[x2]=true, jobs=jobs+1, dir[floor[$1]]=0;}, ') forloop(x3,1,decr(FLOORS), ìdle2 -> idle_up { guard s==-1 and floor[$1]<x3 and dir[floor[$1]]==1 and lightv[x3]==false; effect lightv[x3]=true, jobs=jobs+1, dir[floor[$1]]=0;}, ') //arrival of others customers, or last job with empty elevator move -> idle_up { guard s==-1 and lightv[floor[$1]]==true and jobs-1>0 and m[$1]==1; effect lightv[floor[$1]]=false, jobs=jobs-1;}, move -> idle_down { guard s==-1 and lightv[floor[$1]]==true and jobs-1>0 and m[$1]==-1; effect lightv[floor[$1]]=false, jobs=jobs-1;}, move -> idle { guard s==-1 and lightv[floor[$1]]==true and jobs-1==0; effect lightv[floor[$1]]=false, jobs=0, usage[$1]=false, m[$1]=0;}, //choice other floors in move direction forloop(x6, 1, decr(FLOORS), ìdle_up -> idle_up { guard s==-1 and floor[$1]<x6 and lightv[x6]==false; effect lightv[x6]=true, jobs=jobs+1;}, ') idle_up -> move {guard s==-1;}, forloop(x7, 0, decr(decr(FLOORS)), ìdle_down -> idle_down { guard s==-1 and floor[$1]>x7 and lightv[x7]==false; effect lightv[x7]=true, jobs=jobs+1;}, ') idle_down -> move {guard s==-1;}; } idle

-> move

') define(elevatorT1M, `process elevatorT1M_$1 { //number of jobs for this elevator byte jobs=0; //lights of floors inside the elevator byte lightv[FLOORS]={myloop(x,0,decr(FLOORS),`0',`,')}; state idle,idle2,idle_up,idle_down,move,del_memory; init idle; trans

35

660 661 662 663 664 665 666 667 668 669 670 671 672 673 674 675 676 677 678 679 680 681 682 683 684 685 686 687 688 689 690 691 692 693 694 695 696 697 698 699 700 701 702 703 704 705 706 707 708 709 710 711 712 713 714 715 716 717 718 719 720 721 722 723 724 725 726

//move to floor called by controller -> move { guard s==-1 and lightv[floor[$1]]==false; effect floor[$1] = floor[$1] + m[$1];}, //called to work by controller idle -> idle2 { guard s==$1 and floor[$1]==job; effect s=ELEVS, m[$1]=dir[floor[$1]], usage[$1]=true;}, idle -> move { guard s==$1 and floor[$1]>job; effect s=ELEVS, m[$1]=-1, lightv[job]=true;}, idle -> move { guard s==$1 and floor[$1]<job; effect s=ELEVS, m[$1]=1, lightv[job]=true;}, //elevator arrives to floor called by controller move -> idle2 { guard s==-1 and usage[$1]==2 and lightv[floor[$1]]==true; effect lightv[floor[$1]]=false, usage[$1]=true, m[$1]=dir[floor[$1]];}, //customer use free elevator idle -> idle2 { guard s==-1 and usage[$1]==false and floor[$1]>0 and dir[floor[$1]]==0; effect usage[$1]=true, dir[floor[$1]]=-1, m[$1]=-1;}, idle -> idle2 { guard s==-1 and usage[$1]==false and floor[$1]<decr(FLOORS) and dir[floor[$1]]==0; effect usage[$1]=true, dir[floor[$1]]=1, m[$1]=1;}, //move of first customer forloop(x2,0,decr(decr(FLOORS)), ìdle2 -> idle_down { guard s==-1 and floor[$1]>x2 and dir[floor[$1]]==-1 and lightv[x2]==false; effect lightv[x2]=true, jobs=jobs+1, dir[floor[$1]]=0;}, ') forloop(x3,1,decr(FLOORS), ìdle2 -> idle_up { guard s==-1 and floor[$1]<x3 and dir[floor[$1]]==1 and lightv[x3]==false; effect lightv[x3]=true, jobs=jobs+1, dir[floor[$1]]=0;}, ') //arrival of others customers, or last job with empty elevator move -> idle_up { guard s==-1 and lightv[floor[$1]]==true and jobs-1>0 and m[$1]==1; effect lightv[floor[$1]]=false, jobs=jobs-1;}, move -> idle_down { guard s==-1 and lightv[floor[$1]]==true and jobs-1>0 and m[$1]==-1; effect lightv[floor[$1]]=false, jobs=jobs-1;}, move -> idle { guard s==-1 and lightv[floor[$1]]==true and jobs-1==0; effect lightv[floor[$1]]=false, jobs=0, usage[$1]=false, m[$1]=0;}, //choice other floors in move direction forloop(x6, 1, decr(FLOORS), ìdle_up -> idle_up { guard s==-1 and floor[$1]<x6 and lightv[x6]==false; effect lightv[x6]=true, jobs=jobs+1;}, ') idle_up -> move {guard s==-1 and memory_up[floor[$1]]==0;}, idle_up -> del_memory { guard s==-1 and memory_up[floor[$1]]>0; effect mem=memory_up[floor[$1]], memory_up[floor[$1]]=0, i=0, max_memory=max_memory-1, s=ELEVS;}, del_memory -> del_memory { guard imem and memory_down[i]>mem; effect memory_up[i]=memory_up[i]-1, memory_down[i]=memory_down[i]-1, i=i+1;}, del_memory -> del_memory { guard imem and move

36

727 728 729 730 731 732 733 734 735 736 737 738 739 740 741 742 743 744 745 746 747 748 749 750 751 752 753 754 755 756 757 758 759 760 761 762 763 764 765 766 767 768 769 770 771 772 773 774 775 776 777 778 779 780 781 782 783 784 785 786 787 788 789 790 791 792 793

memory_down[i]<mem; effect memory_up[i]=memory_up[i]-1, i=i+1;}, del_memory -> del_memory { guard imem; effect memory_down[i]=memory_down[i]-1, i=i+1;}, del_memory -> del_memory { guard i move { guard i==FLOORS; effect s=-1;}, forloop(x7, 0, decr(decr(FLOORS)), ìdle_down -> idle_down { guard s==-1 and floor[$1]>x7 and lightv[x7]==false; effect lightv[x7]=true, jobs=jobs+1;}, ') idle_down -> move { guard s==-1 and memory_down[floor[$1]]==0;}, idle_down -> del_memory { guard s==-1 and memory_down[floor[$1]]>0; effect mem=memory_down[floor[$1]], memory_down[floor[$1]]=0, i=0, max_memory=max_memory-1, s=ELEVS;}; } ') define(elevatorT2, `process elevatorT2_$1 { //number of jobs for this elevator byte jobs=0; //lights of floors inside the elevator byte lightv[FLOORS]={myloop(x,0,decr(FLOORS),`0',`,')}; state idle,idle2,idle_up,idle_down,move; init idle; trans //move to floor called by controller move -> move { guard s==-1 and lightv[floor[$1]]==false; effect floor[$1] = floor[$1] + m[$1];}, //called to work by controller idle -> idle2 { guard s==$1 and floor[$1]==job; effect s=ELEVS, m[$1]=dir[floor[$1]], usage[$1]=true;}, idle -> move { guard s==$1 and floor[$1]>job; effect s=ELEVS, m[$1]=-1, lightv[job]=true;}, idle -> move { guard s==$1 and floor[$1]<job; effect s=ELEVS, m[$1]=1, lightv[job]=true;}, //elevator arrives to floor called by controller move -> idle2 { guard s==-1 and usage[$1]==2 and lightv[floor[$1]]==true; effect lightv[floor[$1]]=false, usage[$1]=true, m[$1]=dir[floor[$1]];}, //customer use free elevator idle -> idle2 { guard s==-1 and usage[$1]==false and floor[$1]>0 and dir[floor[$1]]==0; effect usage[$1]=true, dir[floor[$1]]=-1, m[$1]=-1;}, idle -> idle2 { guard s==-1 and usage[$1]==false and floor[$1]<decr(FLOORS) and dir[floor[$1]]==0; effect usage[$1]=true, dir[floor[$1]]=1, m[$1]=1;}, //move of first customer forloop(x2,0,decr(decr(FLOORS)), ìdle2 -> idle_down { guard s==-1 and floor[$1]>x2 and dir[floor[$1]]==-1 and lightv[x2]==false; effect lightv[x2]=true, jobs=jobs+1, dir[floor[$1]]=0;}, idle2 -> idle_down { guard s==-1 and floor[$1]>x2 and dir[floor[$1]]==-1 and lightv[x2]==true;

37

794 795 796 797 798 799 800 801 802 803 804 805 806 807 808 809 810 811 812 813 814 815 816 817 818 819 820 821 822 823 824 825 826 827 828 829 830 831 832 833 834 835 836 837 838 839 840 841 842 843 844 845 846 847 848 849 850 851 852 853 854 855 856 857 858 859 860

effect dir[floor[$1]]=0;}, ') forloop(x3,1,decr(FLOORS), ìdle2 -> idle_up { guard s==-1 and floor[$1]<x3 and dir[floor[$1]]==1 and lightv[x3]==false; effect lightv[x3]=true, jobs=jobs+1, dir[floor[$1]]=0;}, idle2 -> idle_up { guard s==-1 and floor[$1]<x3 and dir[floor[$1]]==1 and lightv[x3]==true; effect dir[floor[$1]]=0;}, ') //arrival of others customers, or last job with empty elevator move -> idle_up { guard s==-1 and lightv[floor[$1]]==true and jobs-1>0 and m[$1]==1; effect lightv[floor[$1]]=false, jobs=jobs-1;}, move -> idle_down { guard s==-1 and lightv[floor[$1]]==true and jobs-1>0 and m[$1]==-1; effect lightv[floor[$1]]=false, jobs=jobs-1;}, move -> idle { guard s==-1 and lightv[floor[$1]]==true and jobs-1==0; effect lightv[floor[$1]]=false, jobs=0, usage[$1]=false, m[$1]=0;}, //other job ********* //add new entry for non free elevator move -> move { guard s==$1 and lightv[job]==false; effect lightv[job]=true, s=ELEVS, jobs=jobs+1;}, move -> move { guard s==$1 and lightv[job]==true; effect s=ELEVS;}, //add new entry for stopped elevator while customers get in/out idle_up -> idle_up { guard s==$1 and lightv[job]==false; effect lightv[job]=true, s=ELEVS, jobs=jobs+1;}, idle_up -> idle_up { guard s==$1 and lightv[job]==true; effect s=ELEVS;}, idle_down -> idle_down { guard s==$1 and lightv[job]==false; effect lightv[job]=true, s=ELEVS, jobs=jobs+1;}, idle_down -> idle_down { guard s==$1 and lightv[job]==true; effect s=ELEVS;}, idle2 -> idle2 { guard s==$1 and lightv[job]==false; effect lightv[job]=true, s=ELEVS, jobs=jobs+1;}, idle2 -> idle2 { guard s==$1 and lightv[job]==true; effect s=ELEVS;}, //choice other floors in move direction forloop(x6, 1, decr(FLOORS), ìdle_up -> idle_up { guard s==-1 and floor[$1]<x6 and lightv[x6]==false; effect lightv[x6]=true, jobs=jobs+1;}, ') idle_up -> move {guard s==-1;}, forloop(x7, 0, decr(decr(FLOORS)), ìdle_down -> idle_down { guard s==-1 and floor[$1]>x7 and lightv[x7]==false; effect lightv[x7]=true, jobs=jobs+1;}, ') idle_down -> move {guard s==-1;}; } ') define(elevatorT2M, `process elevatorT2M_$1 { //number of jobs for this elevator byte jobs=0; //lights of floors inside the elevator byte lightv[FLOORS]={myloop(x,0,decr(FLOORS),`0',`,')}; state idle,idle2,idle_up,idle_down,move,del_memory; init idle; trans

38

861 862 863 864 865 866 867 868 869 870 871 872 873 874 875 876 877 878 879 880 881 882 883 884 885 886 887 888 889 890 891 892 893 894 895 896 897 898 899 900 901 902 903 904 905 906 907 908 909 910 911 912 913 914 915 916 917 918 919 920 921 922 923 924 925 926 927

//move to floor called by controller -> move { guard s==-1 and lightv[floor[$1]]==false; effect floor[$1] = floor[$1] + m[$1];}, //called to work by controller idle -> idle2 { guard s==$1 and floor[$1]==job; effect s=ELEVS, m[$1]=dir[floor[$1]], usage[$1]=true;}, idle -> move { guard s==$1 and floor[$1]>job; effect s=ELEVS, m[$1]=-1, lightv[job]=true;}, idle -> move { guard s==$1 and floor[$1]<job; effect s=ELEVS, m[$1]=1, lightv[job]=true;}, //elevator arrives to floor called by controller move -> idle2 { guard s==-1 and usage[$1]==2 and lightv[floor[$1]]==true; effect lightv[floor[$1]]=false, usage[$1]=true, m[$1]=dir[floor[$1]];}, //customer use free elevator idle -> idle2 { guard s==-1 and usage[$1]==false and floor[$1]>0 and dir[floor[$1]]==0; effect usage[$1]=true, dir[floor[$1]]=-1, m[$1]=-1;}, idle -> idle2 { guard s==-1 and usage[$1]==false and floor[$1]<decr(FLOORS) and dir[floor[$1]]==0; effect usage[$1]=true, dir[floor[$1]]=1, m[$1]=1;}, //move of first customer forloop(x2,0,decr(decr(FLOORS)), ìdle2 -> idle_down { guard s==-1 and floor[$1]>x2 and dir[floor[$1]]==-1 and lightv[x2]==false; effect lightv[x2]=true, jobs=jobs+1, dir[floor[$1]]=0;}, idle2 -> idle_down { guard s==-1 and floor[$1]>x2 and dir[floor[$1]]==-1 and lightv[x2]==true; effect dir[floor[$1]]=0;}, ') forloop(x3,1,decr(FLOORS), ìdle2 -> idle_up { guard s==-1 and floor[$1]<x3 and dir[floor[$1]]==1 and lightv[x3]==false; effect lightv[x3]=true, jobs=jobs+1, dir[floor[$1]]=0;}, idle2 -> idle_up { guard s==-1 and floor[$1]<x3 and dir[floor[$1]]==1 and lightv[x3]==true; effect dir[floor[$1]]=0;}, ') //arrival of others customers, or last job with empty elevator move -> idle_up { guard s==-1 and lightv[floor[$1]]==true and jobs-1>0 and m[$1]==1; effect lightv[floor[$1]]=false, jobs=jobs-1;}, move -> idle_down { guard s==-1 and lightv[floor[$1]]==true and jobs-1>0 and m[$1]==-1; effect lightv[floor[$1]]=false, jobs=jobs-1;}, move -> idle { guard s==-1 and lightv[floor[$1]]==true and jobs-1==0; effect lightv[floor[$1]]=false, jobs=0, usage[$1]=false, m[$1]=0;}, //other job ********* //add new entry for non free elevator move -> move { guard s==$1 and lightv[job]==false; effect lightv[job]=true, s=ELEVS, jobs=jobs+1;}, move -> move { guard s==$1 and lightv[job]==true; effect s=ELEVS;}, //add new entry for stopped elevator while customers get in/out idle_up -> idle_up { guard s==$1 and lightv[job]==false; effect lightv[job]=true, s=ELEVS, jobs=jobs+1;}, idle_up -> idle_up { guard s==$1 and lightv[job]==true; move

39

928 929 930 931 932 933 934 935 936 937 938 939 940 941 942 943 944 945 946 947 948 949 950 951 952 953 954 955 956 957 958 959 960 961 962 963 964 965 966 967 968 969 970 971 972 973 974 975 976 977 978 979 980 981 982 983 984 985 986 987 988 989 990 991

effect s=ELEVS;}, idle_down -> idle_down { guard s==$1 and lightv[job]==false; effect lightv[job]=true, s=ELEVS, jobs=jobs+1;}, idle_down -> idle_down { guard s==$1 and lightv[job]==true; effect s=ELEVS;}, idle2 -> idle2 { guard s==$1 and lightv[job]==false; effect lightv[job]=true, s=ELEVS, jobs=jobs+1;}, idle2 -> idle2 { guard s==$1 and lightv[job]==true; effect s=ELEVS;}, //choice other floors in move direction forloop(x6, 1, decr(FLOORS), ìdle_up -> idle_up { guard s==-1 and floor[$1]<x6 and lightv[x6]==false; effect lightv[x6]=true, jobs=jobs+1;}, ') idle_up -> move {guard s==-1 and memory_up[floor[$1]]==0;}, idle_up -> del_memory { guard s==-1 and memory_up[floor[$1]]>0; effect mem=memory_up[floor[$1]], memory_up[floor[$1]]=0, i=0, max_memory=max_memory-1, s=ELEVS;}, del_memory -> del_memory { guard imem and memory_down[i]>mem; effect memory_up[i]=memory_up[i]-1, memory_down[i]=memory_down[i]-1, i=i+1;}, del_memory -> del_memory { guard imem and memory_down[i]<mem; effect memory_up[i]=memory_up[i]-1, i=i+1;}, del_memory -> del_memory { guard imem; effect memory_down[i]=memory_down[i]-1, i=i+1;}, del_memory -> del_memory { guard i move { guard i==FLOORS; effect s=-1;}, forloop(x7, 0, decr(decr(FLOORS)), ìdle_down -> idle_down { guard s==-1 and floor[$1]>x7 and lightv[x7]==false; effect lightv[x7]=true, jobs=jobs+1;}, ') idle_down -> move { guard s==-1 and memory_down[floor[$1]]==0;}, idle_down -> del_memory { guard s==-1 and memory_down[floor[$1]]>0; effect mem=memory_down[floor[$1]], memory_down[floor[$1]]=0, i=0, max_memory=max_memory-1, s=ELEVS;}; } ') ifelse(MEM,0, ìfelse(TYPE,2,`controlerT2 forloop(y, 0, decr(ELEVS), èlevatorT2(y)')', ìfelse(TYPE,1,`controlerT1 forloop(y, 0, decr(ELEVS), èlevatorT1(y)')',`controlerT0 forloop(y, 0, decr(ELEVS), èlevatorT0(y)')')')', ìfelse(TYPE,2,`controlerT2M forloop(y, 0, decr(ELEVS), èlevatorT2M(y)')', ìfelse(TYPE,1,`controlerT1M forloop(y, 0, decr(ELEVS), èlevatorT1M(y)')',`controlerT0M forloop(y, 0, decr(ELEVS), èlevatorT0M(y)')')')') system async;

40

Dodatek B

Zdrojový kód LTL vlastností Pro hodnoty dle 4.kapitoly: 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54

Atomic propositions ------------------#define used (usage[0]!=0) #define moving (m[0]==0) #define firstcall (s==0) #define secondcall (s==1) #define jobzero (job==0) #define jobone (job==1) #define jobtwo (job==2) #define floorsecondzero (floor[1]==0) #define floorfirstone (floor[0]==1) #define floorfirsttwo (floor[0]==2) #define nononecall (s!=-1) #define nouppermaxcall (s!=2) #define nousagetwo (usage[0]!=2) #define usagezero (usage[0]==0) #define usageone (usage[0]==1) #define usagetwo (usage[0]==2) #define maxmemory (max_memory==0) Properties ---------(1) not free elevator until moving #property G(used U moving) (2) elevator 1 arrives to calling floor 2 #property G((firstcall && jobtwo) -> F(floorfirsttwo)) (3) elevator 2 arrives to calling floor 0 #property G((secondcall && jobzero) -> F(floorsecondzero)) (4) elevator 1 arrives to calling floor 1 #property G((firstcall && jobone) -> F(floorfirstone)) (5) push button in floor 0 -> reaction #property G(jobzero -> F(nononecall && nouppermaxcall && jobzero)) (6) push button in floor 1 -> reaction #property G(jobone -> F(nononecall && nouppermaxcall && jobone)) (7) push button in floor 2 -> reaction #property G(jobtwo -> F(nononecall && nouppermaxcall && jobtwo)) (8) cannot call elevator if he is used #property G(usageone -> X(nousagetwo U usagezero)) (9) used elevator can be again used after idle state #property G((usageone -> Fusagezero) -> Fusageone) (10) called elevator have to be used #property G(usagetwo -> X(used U usageone)) (11) all memorized demands will be served #property G(!maxmemory -> F(maxmemory))

41

VYTVOŘENÍ MODELU VÝTAHŮ SE SBĚRNÝM ŘÍZENÍM

Recommend Documents