Grafický editor parametrizovaných modelů pro DiVinE

MASARYKOVA UNIVERZITA FAKULTA INFORMATIKY

•P

%, \J/

&

Grafický editor parametrizovaných modelů pro DiVinE BAKALÁŘSKÁ PRÁCE

Roman Plašil

Brno, 2008

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. 11

Poděkování Rád bych poděkoval vedoucímu mé práce, RNDr. Jiřímu Barnatovi, Ph.D., za odborné vedení a užitečné připomínky. Chtěl bych také poděkovat své kočičce Marcele a rodině za poskytnutí zázemí a podporu při práci.

m

Shrnutí Práce v teoretické části diskutuje možnosti parametrizace modelů v několika současných nástrojích pro model checking. V praktické části představuje program DiVinE Editor, který umožňuje graficky tvořit parametrizované modely pro DiVinE.

IV

Klíčová slova DiVinE, Paxion, model checking, editor modelů, parametrizace

v

Obsah 1

2

3

4

5 A

B

Existující řešení 1.1 PRISM 1.2 Uppaal 1.3 SPIN 1.4 DiVinE Představení DiVinE Editoru 2.1 Výchozí bod - Paxion 2.2 Nová verze - DiVinE Editor 2.3 Šablony procesů 2.4 Parametrizace hran 2.5 Kopírovaní hran 2.6 Vícerozměrná pole 2.7 Ostatní Použité technologie 3.1 Java 3.2 SableCC 3.3 XStream 3.4 JUnit Architektura a implementace 4.1 Pomocné třídy 4.2 Součásti modelu 4.3 Zpracování výrazů 4.4 Převod do DVE 4.5 Nové uživatelské rozhraní 4.6 Ukládání modelu do XML Závěr Průvodce tvorbou modelu A.l Základní verze A.2 Varianta s jedním levákem A.3 Omezení počtu filozofů u stolu Technické podrobnosti

3 3 5 7 8 11 11 11 14 15 16 17 17 19 19 19 20 21 22 22 24 26 27 28 28 30 33 33 35 36 38

vi

Úvod V poslední době roste trend v používání paralelních a distribuovaných výpo četních systémů. Nástup vícejádrových procesorů, které se dnes již prodávají v běžných osobních počítačích, to jen potvrzuje. Programování paralelních programů je však mnohem náročnější než vývoj klasických sekvenčních sys témů. Model checking umožňuje ověřit vlastnosti paralelních systémů, a tak zvýšit jejich spolehlivost. Ověřování vlastností se provádí zjednodušeně řečeno následovně. Vytvoří se model systému, obvykle sestávající z něko lika procesů určených konečně stavovým přechodovým systémem. Poté se sestaví formule temporální logiky, která vyjadřuje vlastnost, již chceme na modelu ověřit. Nakonec se model a formule vloží do programu, který provede model checking (tzv. model checker). Výstupem je b u ď potvrzení, že daný model formuli splňuje nebo protipříklad - běh programu, který danou formuli nesplňuje [2]. Modely je možné zadávat různými způsoby. Existují matematické forma lismy, počítačové jazyky, ale i částečně grafické prostředky pro popis modelů paralelních systémů. Model checkery často mají svůj vlastní textový nebo grafický jazyk. Tyto jazyky mohou být jen jednoduchá rozšíření konečných automatů, nebo mohou být poměrně komplexní a mohou od konečných automatů abstrahovat. Některé model checkery (například Java Pathfin der) pracují přímo nad zdrojovým kódem programu. Tuto variantu zde ale nebudeme uvažovat. Praktickým požadavkem na modelovací jazyky je podpora parametrizace modelů. Parametrizovaný model je takový, který lze dobře definovaným způsobem měnit úpravou hodnot k tomu určených pro měnných - parametrů. Mezi typicky používané parametry patří například počet účastníků protokolu nebo zapnutí/vypnutí alternativního chování části modelu. Nástrojů pro model checking existuje celá řada. V laboratoři ParaDiSe na Fakultě informatiky Masarykovy univerzity je vyvíjen program DiVinE. DiVinE se liší od ostatních programů především v tom, že provádí model checking distribuovane. Díky tomu může tuto výpočetně náročnou úlohu zvládnout i pro větší modely a formule. DiVinE čte modely zadané ve vlast ním formátu DVE nebo v jazyce ProMeLa. Jazyk DVE popisuje procesy 1

pomocí konečných automatů. Takové modely může být pohodlnější vytvá řet interaktivně graficky a je to i snazší způsob práce pro nové uživatele. Program pro grafickou editaci modelů pro DiVinE již existuje, je jím Paxion [10], který napsal Gaětan de Menten. Tento program ale nepodporuje parametrizované modely a ani formát DVE sám o sobě žádné parametri zování neumožňuje. V laboratoři ParaDiSe se parametrizace řeší použitím programu M4. Toto je ale čistě textová metoda. Cílem práce je rozšířit funkci onalitu Paxionu o zadávání parametrizovaných modelů, aby takové modely bylo možné vytvářet i interaktivně v grafickém uživatelském rozhraní. Práce je dělena do pěti kapitol. V první kapitole jsou formulovány přes nější požadavky na parametrizaci a porovnává současné přístupy k zadávání modelů a k jejich parametrizaci ve čtyřech nástrojích. V další kapitole je před staven program DiVinE Editor, jeho funkce a způsob řešení nastíněného problému. Ve třetí kapitole jsou předloženy technologie použité při imple mentaci programu. Předposlední kapitola se zaobírá detaily organizace a implementace programu. Poslední kapitola hodnotí výsledný produkt a nastiňuje možnosti dalšího vývoje. V první příloze lze nalézt podrobný návod k vytvoření parametrizovaného modelu večeřejících filozofů v pro gramu DiVinE Editor. Ve druhé příloze je obsah přiloženého CD a pokyny k instalaci programu.

2

Kapitola 1

Existující řešení Nejprve probereme stávající způsob zadávání modelů v některých zná mých nástrojích pro model checking. Přihlédneme přitom také k možnostem tvorby parametrizovaných modelů. Jde spíše o přehled, pro kompletní in formace je nutné nahlédnout do manuálu ke konkrétnímu programu. Podle existujících parametrizovaných modelů z databáze BEEM [1] mů žeme vybrat několik běžných způsobů využití parametrizace. Velmi často se používá parametr pro počet účastníků komunikace. Z toho plyne potřeba zkopírování určitého procesu s případnými drobnými úpravami a někdy také proměnný počet globálních proměnných. Občas s rostoucím počtem účastníků potřebujeme přidávat hrany v některém procesu a simulovat tak například nedeterministický výběr. Obvykle je potřeba pojmenovat čísel nou konstantu a používat v modelu místo konkrétního čísla jeho jméno, například velikost bufferu, zpoždění při předávání zpráv a podobně. Ně které modely umožňují parametrem vybrat jedno z alternativních chování systému. To můžeme využít pro volitelné zapnutí chyby v komunikačních protokolech nebo nespolehlivého média v jiných modelech. U každého z hodnocených programů zjistíme, zda a jak podporuje každý způsob para metrizace.

1.1

PRISM

Nástroj PRISM [11], pocházející z univerzity v Oxfordu, má grafické uživa telské rozhraní, ve kterém lze psát modely v jazyce specifickém pro PRISM. Grafické rozhraní kromě zvýrazňovaní syntaxe a zobrazení seznamu částí modelu neposkytuje žádné další nástroje pro sestavování modelu. PRISM se zaměřuje na pravděpodobnostní modely, ale to z našeho po hledu není příliš důležité. Model v jazyce PRISM začíná určením typu mo delu, následují globální konstanty a proměnné. V PRISM se explicitně ne definují žádné stavy. Stav systému je vždy určen aktuální hodnotou všech globálních a všech lokálních proměnných všech procesů. 3

1. EXISTUJÍCÍ ŘEŠENÍ

Jazyk dovoluje nadefinovat takzvané formule. Formule je pojmenovaný výraz, který se vloží všude tam, kde je použito její jméno. Slouží k omezení duplicitního kódu. Jednoduchá formule n o n z e r o se definuje takto: formula nonzero = x != 0; Procesy j sou uzařeny mezi klíčovými slovy m o d u l e a e n d m o d u l e . Každý proces má lokální proměnné a příkazy. Příkazy definují možné přechody mezi stavy procesu. Jejich zápis vypadá například takto: [syne] x != 0 -> 0 . 2 : ( x ' 0.8:(y'

= x - l)S(y' = y + 1);

= y + 1) +

Výraz sync v hranaté závorce je název akce, který se používá pro synchro nizaci a nemusí být uveden. Výraz před šipkou je podmínka, která musí být splněna, aby systém mohl provést danou akci. Za šipkou je seznam změn proměnných, které jsou odděleny symbolem + a jsou uvedeny svou pravděpodobností. Nová hodnota proměnné je označena apostrofem, pů vodní hodnota je bez apostrofu. Následuje příklad celého modulu převzatý z manuálu PRISM. module Ml x : [0. .2] i n i t

0;

[] x=0 -> 0 . 8 : ( x ' = 0 ) + 0 . 2 : ( x ' = l ) ; [] x=l & y!=2 -> ( x ' = 2 ) ; [] x=2 -> 0 . 5 : ( x ' = 2 ) + 0 . 5 : ( x ' = 0 ) ; endmodule Dalšími součástmi modelu je výraz popisující způsob složení procesů do paralelní kompozice a přiřazení ceny stavům. Obojí je mimo rámec této práce. Pomocí konstrukce přejmenování lze vytvořit nový proces přejmenová ním identifikátorů v existujícím procesu. Nový proces tak může pracovat s jinými proměnnými, ale základní princip jeho chování zůstává zachován. Například z procesu Ml lze vyrobit nový proces M2, který bude zcela stejný, pouze všechny výskyty identifikátoru a budou zaměněny za b takto: module M2 = Ml

[a=b];

Tímto způsobem ale nedosáhneme proměnného počtu procesů, v souboru modelu jsou vždy všechny procesy definovány pevně. PRISM také nepod poruje pole. 4


Žádné další nástroje pro parametrizaci modelů PRISM nenabízí. Ze zmi ňovaných programů je tedy v hodnocené oblasti spíše slabší.

1.2

Uppaal

Program Uppaal [14], vyvíjený společně univerzitami v Aalborgu a Uppsale, nabízí také grafické uživatelské rozhraní. Zde je ale editace modelů založena na interaktivní editaci grafů přechodových systémů. Uppaal podporuje časové automaty, které jsou rozšířením konečných automatů. Tím se ale nebudeme zabývat, protože ostatní programy tuto funkci nemají a z hlediska parametrizace modelů je to nepodstatné. Na obrázku 1.1 je zobrazeno grafické rozhraní pro editaci procesů v Uppaalu. Vlevo je seznam součástí modelu, vpravo šablona procesu Torch. C : / S c í e n c e / u p p a a [ - 4 . 0 . ů / d e m o / b r i d g e . x m [ - UPPAAL File

Edit

View

Tools

Options

Help

j R « O % % «i %% * * ^ Editor 1 Simulator] Verifier| Drag out

' Name:

Torch

Parameters:

^ Project •

Declarations

j - o ä Soldier •

take?

Declarations

J - o ä Torch • L

•

/^*~

..take?

free ^ - ^

Declarations

System declarations

L= 1-L

^ \ ^ release?

m

-

^-^—

^^

i"

release?

~~1

J

ra

Obrázek 1.1: Uživatelské rozhraní Uppaalu Model v Uppaalu má opět globální proměnné, procesy a lokální pro měnné. Chování procesu je určeno konečným automatem. Stavy tohoto automatu se zde nazývají umístění (location). Stavy výsledného systému tedy nejsou už dány pouze proměnnými, ale také tím, ve kterém z umís tění se nachází každý proces. Hrana v procesu má čtyři vlastnosti. První z nich jsou výběry (selections), které nedeterministicky vyberou hodnotu ze zadaného rozmezí. Například tímto zápisem x : int[0,4], y : s c a l a r [2] 5


dostane proměnná x jednu z hodnot 0,1,2,3 a proměnná y b u ď 0, nebo 1. Podmínka hrany (guard) je logický výraz, jímž lze povolit nebo zaká zat přechod po dané hraně. Synchronizační výraz (syne) se používá pro synchronizaci procesů mezi sebou. Pro synchronizaci je třeba použít kanál a jeho jméno uvést do synchronizačního výrazu v obou procesech. V jednom z procesů za něj potom doplníme symbol ? a ve druhém symbol !. Hrany se stejným symbolem se nemohou synchronizovat. Poslední vlastností hrany je efekt (update). Jde o výraz, který mění hodnoty proměnných v systému. Kromě standardních výrazů jsou v Upaalu podporovány operátory f o r a l l a e x i s t s , které odpovídají kvantifikátorům v predikátové lo gice. Jejich syntaxe vypadá takto (ID je identifikátor, Type je typ pole a E x p r e s s i o n je výraz): forall

(ID : Type)

Expression

Na globální úrovni nebo lokálně v procesu lze deklarovat funkce. V nich se dají použít konstrukce w h i l e , f o r , d o . . . w h i l e , i f známé z jazyka C. Konstrukce f o r ( i : p o l e ) představuje průchod polem a připomíná podobnou konstrukci například z Javy Funkce lze použít v podmínce hrany, v synchronizačním výrazu nebo v efektu. Až na efekt je vyžadováno, aby funkce pouze vracely hodnotu a neměly žádný vedlejší efekt. Parametry funkcí mohou být navíc předávány odkazem. Díky tomu je možné napsat například funkci swap, která zamění dvě hodnoty: v o i d s w a p ( i n t Sa, i n t c = a; a = b; b = c;

i n t &b) {

}

Možnosti Uppaalu v parametrizaci modelů jsou mnohem širší než u pro gramu PRISM. Uživatel definuje šablony procesů, které mohou mít vlastní parametry. Pro vložení šablony do modelu se vytvoří její instance zadá ním jména šablony a konkrétních hodnot parametrů v sekci systémových deklarací (System d e c l a r a t i o n s ) . Díky tomuto přistupuje definování několika podobných procesů jednoduché a přehledné. Na druhou stranu Uppaalu chybí možnost vytvářet procesy v závislosti na parametru. Není tak možné parametrizovat počet účastníků protokolu. Uppaal dokáže pracovat s polem proměnných i s polem kanálů. Oba druhy polí mohou být vícerozměrné a jejich rozměry mohou být definovány s použitím pojmenované konstanty. Vícerozměrná pole je ale nutné vytvořit nepřímo s pomocí t y p e d e f . Podporována je i konstrukce s t r u c t , kterou 6


můžeme vytvořit složený typ. Přidávání hran podle parametrů v Uppaalu není možné. Pokud bychom chtěli zapnout pomocí parametru alternativní chování, mohli bychom to v Uppaalu realizovat definováním pojmenované konstanty, přidáním hran reprezentujících alternativu a přidáním podmínky na hodnotu dané kon stanty do všech nových hran. Závěrem můžeme říci, že Uppaal poskytuje poměrně silné nástroje pro parametrizaci. Některé užitečné funkce mu ale chybí. 1.3

SPIN

Modelovacím jazykem nástroje SPIN [13] je ProMeLa. Jedná se o abstraktní jazyk určený pro popis paralelních systémů. Zápis modelu se před zpraco váním převede na konečný přechodový systém [6]. Alternativou k ProMeLe je překlad z jazyka C do ProMeLy dostupný v nástroji SPIN verze 4 [7]. Zde probereme jen základní principy modelování v ProMeLe, pro po drobnější informace bych čtenáře odkázal na knihu The Spin Model Checker [8] a na webovou stránku programu [13]. Používání proměnných a konstant se nijak výrazně neliší od předchozích programů. SPIN podporuje t y p e d e f a složené typy stejně jako Uppaal. Kanály jsou zde o něco složitější. Mohou být b u ď synchronní (hodnota je předána okamžitě), nebo asynchronní (pak fungují jako buffer). Procesy si přes kanály mohou předávat zprávy, které se skládají z více než jedné hodnoty. ProMeLa, podobně jako jazyk Uppaalu, popisuje šablony procesů, které mohou mít parametry. Pro přidání procesu do systému je třeba šablonu explicitně spustit příkazem r u n . V kombinaci s příkazy pro řízení toku programu můžeme snadno parametrem vyjádřit počet procesů v systému. Šablona procesu se skládá z deklarací lokálních proměnných a dále ze sekvence příkazů. Každý příkaz může být povolený, nebo blokující. Když proces narazí na blokující příkaz, čeká, dokud se z něj nestane povolený příkaz. Příkladem příkazu, který může být blokující, je prostý výraz. Ten je povolený právě tehdy, když jeho hodnotou je nenulová hodnota. Tato konstrukce se používá k zápisu podmínky (guard). Mezi další příkazy patří přiřazení, skok (goto), přerušení cyklu (break), nedeterministický výběr ( i f ) , opakovaný nedeterministický výběr (do) a další. Nedeterministický výběr vypadá takto: if ::

prikazy 7


:: fi

prikazy

Tento příkaz blokuje, dokud alespoň jeden z příkazů uvedených : : není povolený. Potom nedeterministicky vybere jeden z povolených a provede ho. Název příkazu i f pochází z toho, že obvykle je prvním příkazem každé možnosti je výraz, který musí platit, aby se příkaz mohl spustit. Opako vaný výběr funguje stejně, jen se provádí stále znovu, dokud není přerušen příkazem b r e a k nebo g o t o . Možnosti parametrizace modelů v jazyce ProMeLa jsou široké. I pole proměnných nebo kanálů parametrizované velikosti jazyk ProMeLa na tivně podporuje. Co se týče přidávání hran v závislosti na parametru, tato funkcionalita by byla v tomto případě nahrazena dobrými vyjadřovacími schopnostmi ProMeLy (například pro nedeterministický výběr nabízí přímo syntaktickou konstrukci i f ) . Pojmenované konstanty jsou samozřejmostí. Výběr alternativ v závislosti na parametru je možné provést pomocí kon strukce if. Závěrem můžeme říct, že SPIN poskytuje kvalitní možnosti parametri zace modelů. 1.4

DiVinE

Program DiVinE Tool [3], vyvíjený zde, na Fakultě informatiky, podporuje dva vstupní formáty - vlastní formát DVE a jazyk ProMeLa. Jazyk DVE se principem podobá Uppaalu. Systém se skládá z procesů, globálních a lokálních proměnných a komunikačních kanálů. V každém procesu uživatel explicitně definuje stavy (umístění) a přechody mezi nimi. Aktuální hodnoty všech proměnných spolu s tím, v jakém umístění se na chází každý proces, dávají dohromady stav výsledného systému. Přechody mezi stavy mají tři vlastnosti, podmínku hrany (guard), synchronizační výraz (syne) a efekt (effect). Jejich význam je stejný jako v Uppaalu. Komunikační kanály jsou podobné jako v jazyce ProMeLa. Mohou být synchronní, nebo asynchronní a je možné jimi předávat více než jednu hodnotu. Syntaxe DVE přesně odpovídá výše popsané struktuře modelu a neu možňuje žádnou parametrizaci. Tento problém je řešen použitím makroprocesoru M4 [9]. Ten v libovolném vstupním souboru nahradí všechna volání maker jejich definovaným obsahem. Makra mohou být buď vestavěná nebo uživatelsky definovaná. 8


M4 je Turingovsky úplný [12], takže modely s jeho pomocí můžeme parametrizovat takřka libovolně. Nevýhodou je jistá nepřehlednost zápisu, jak můžeme vidět na příkladu na konci této kapitoly. S pomocí programu M4 by samozřejmě bylo možné snadno parame trizovat jakýkoliv model pro každý nástroj, jehož vstupy jsou v textové formě. Kopírování procesu, případně i s parametry, se provádí definováním šablony procesu jako makro a jeho následnou expanzí podle potřeby. Jedno rozměrná pole proměnných podporuje jazyk DVE nativně, vícerozměrná pole se realizují makry, která převedou indexový vektor do indexu v jedno rozměrné reprezentaci pole. Hrany opakované v závislosti na parametru jsou podobně jako procesy deklarovány jako makro a následně expandovány. Pojmenované konstanty podporuje DVE částečně nativně, ale kvůli jistým omezením je preferováno využití makra. Nakonec výběr z alternativ lze snadno uskutečnit použitím vestavěného makra i f e l s e . Spojení programu M4 s jazykem DVE je silné a poskytuje značné mož nosti v oblasti parametrizace modelů. Na druhou stranu pro nezkušeného člověka není snadné takové modely psát ani číst. Zde by měl pomoci pro gram DiVinE Editor, vytvořený v rámci této práce. Zde je příklad jednoduchého modelu v jazyce DVE parametrizovaného pomocí M4. Jedná se o Petersonův protokol vzájemného vyloučení. / / p e t e r s o n mutual exclusion p r o t o c o l for N p r o c e s s e s d e f a u l t (N,3) d e f a u l t (LOOPS,0) default(ERROR,0) byte pos[N]; byte step[N]; b y t e i n _ c r i t i c a l = 0; d e f i n e (P, ' p r o c e s s P_$l { b y t e j = 0 , k=0; s t a t e NCS, CS, w a i t , q 2 , q 3 ; i n i t NCS; trans i f e l s e ( L O O P S , 1, 'NCS -> NCS { } , ' , w ) NCS -> w a i t { e f f e c t j = 1; }, w a i t -> q2 { g u a r d j < N; e f f e c t p o s [ $ l ] = j ; }, q2 -> q3 { e f f e c t s t e p [ j - l ] = $ 1 , k = 0; }, ifelse(ERROR, 0, ' q 3 -> q3 { 9


guard (k == $1 || pos[k]< j) && k < N; effect k = k+1; },', ERROR, 1, "q3 -> q3 { guard (k == $1 || pos[k]<= j) && k < N; effect k = k+1; },') q3 -> wait { g u a r d s t e p [ j - l ] != $1 | | k == N; effect j = j+1, k=0; }, wait -> CS { guard j == N; effect in_critical = in_critical+l;}, CS -> NCS { effect pos[$l] = 0, in_critical = in_critical-l, j=0;}; } ') forloop(i,0,decr(N), 'Pfi)') system async;

10

Kapitola 2

Představení DiVinE Editoru Stěžejním bodem této práce je rozšíření existujícího grafického editoru Paxion o možnost parametrizace. Nejprve se stručně podíváme na původní program a poté přistoupíme k popisu nového programu. 2.1

Výchozí bod - Paxion

Paxion je editor modelů pro DiVinE, který napsal v rámci své diplomové práce Gaětan de Menten [10]. Grafy procesů se v něm editují interaktivně s pomocí myši, vlastnosti objektů (přechodů, stavů apod.) se editují stan dardně pomocí grafického uživatelského rozhraní. Stejně tak proměnné a kanály. Možnosti poměrně přesně odpovídají možnostem jazyka DVE. Program nenabízí žádnou další funkcionalitu než jaká je podporována v ja zyce DVE. Na obrázku 2.1 je zobrazeno hlavní (a prakticky jediné) okno programu. 2.2

Nová verze - DiVinE Editor

DiVinE Editor používá kód z Paxionu pro grafické editování procesů, velká část ostatního kódu je nová nebo přepracovaná. Podporuje šablony procesů i s parametry, kopírování hran, parametrizování hran, vícerozměrná pole a pojmenované konstanty. Zbytek této kapitoly představuje popis principů tvorby a parametrizace modelů v DiVinE Editoru. Detailní technické infor mace jsou uvedeny v DiVinE Editor Reference Manual, který je součástí instalace programu. Součásti modelu se v programu editují takzvanými editory. Editor je samostatná část grafického uživatelského rozhraní, ve které má uživatel možnost měnit vlastnosti daného objektu. Každý editor je třída odvozená od J P a n e l z Java Swing. V hlavním okně DiVinE Editoru (obrázek 2.2) se v levém panelu nachází seznam součástí modelu uspořádaný do stromu a v pravém panelu je editor 11

2. PŘEDSTAVENÍ DIVINE EDITORU

File

Process B | ä

View H

6

%

%

Select I States]) [Processi[

async

•

T r a

"sl"°"s

Process2 |

observer none |Process1

new

edit

delete acceptation sets

mark states new

edit

delete

new

edit

delete

"lew process created.

Obrázek 2.1: Hlavní obrazovka Paxionu aktuálně vybrané části modelu. První částí modelu je kořenový uzel Model. Po vybrání tohoto uzlu můžeme vpravo vybrat druh modelu - synchronní nebo asynchronní. Následuje uzel Parameters. Zde se v textovém editoru zapisují parametry modelu a jejich výchozí hodnoty. V uzlu Variables se v textovém editoru zapisují globální proměnné, kanály a použité šablony procesů. Syntaxe proměnných a kanálů odpovídá syntaxi jazyka DVE, za tímco pro šablony procesů je syntaxe nová. Pod uzlem Processes jsou uzly reprezentující šablony procesů. Každá šablona se edituje grafickým editorem znázorněným na obrázku 2.2. Každý proces má navíc poduzel Variables sloužící k definici lokálních proměnných procesu. Více informací o šablonách lze nalézt v 2.3. V rámci editoru šablony procesu se pracuje klasickým způsobem s myší. Kliknutím na tlačítko States přepneme do módu vkládání stavů. Tlačít kem Transitions vstoupíme do módu vkládání přechodů. V tomto módu kliknutím na počáteční a na koncový stav vytvoříme přechod mezi těmito stavy. Klikneme-li mezi tím ve volném prostoru, vznikne zahnutá šipka. V módu Selecting můžeme myší pohybovat s objekty a klávesou Del je mazat. Vybráním objektu se v pravé části okna zobrazí editor jeho vlast ností. Na obrázku 2.2 je vybrána hrana, která nemá nastavenou žádnou vlastnost. Políčka označená Guard editor, Effect editor a Syne editor slouží k zapsání podmínky, efektu a synchronizačního výrazu dané hrany. Tlačítko 12


Add point přidá řídící bod do křivky hrany. Zbývající políčka se používají pro parametrizaci a jsou rozebrána v následujícím textu. Editor vlastností stavu je mnohem jednodušší - obsahuje pouze název stavu, přepínač pro nastavení stavu jako počátečního a přepínač akceptujícího stavu. • M - Divine Editor File

Edit

View

| New ;••

^p New process = | Delete process Jw1' Save as,,, . " V i Save ^ y Export to DVE,,, ;

': Open.,,

I Model •••• Parameters ••-•# Variables I Processes ŕ--f^lProcess2 d- ^Processi ••• Variables

l^

Process name: Processi "Guard editor Guard:

•

Extended guard

"Effect editor

?

•

extended

Sync editor

"Origin editor •

y

J

Extended origin:

"Destination editor — •

Extended destination:

Enabled expression •

Enabled expression:

Add point

S

JĽ

Obrázek 2.2: Hlavní obrazovka DiVinE Editoru Každý model z DiVinE Editoru se musí před použitím v DiVinE nejprve převést do formátu DVE, který DiVinE dokáže přečíst. K tomu slouží tla čítko Export to DVE na panelu nástrojů. Po jeho stisknutí se zobrazí okno (obrázek 2.3), které provádí uživatele procesem převodu. Nejprve se přečte definice parametrů a zobrazí se tabulka, do které uživatel zapíše požado vané hodnoty parametrů. Poté kliknutím na tlačítko Export převod dokončí. Pokud v jeho průběhu (během čtení definice parametrů, při čtení hodnot zadaných uživatelem nebo během vlastního převodu) dojde k chybě, zob razí se popis chyby v bílém poli pod tabulkou. Součástí hlášení o chybě jsou i tlačítka Take me there a Try again. První z nich zobrazí konkrétní místo v modelu, kde k chybě došlo. Uživatel tak má možnost rychle chybu rozpoznat a opravit. Druhým tlačítkem se převod spustí znovu. Pokud vše 13


proběhlo bez problémů, okno se zavře a převod můžeme považovat za dokončený. ^TT"Tn

, ransform w i n d o w Enter the values of the parameters: Parameter name

Value

N LEFT ROOM

4 0 0

Status:

Parameters have been read successfuly, Enter their values and then click Export to finish.

g l Close on success

Export

Close

Obrázek 2.3: Okno pro převod modelu do DVE Převod můžeme spustit také z příkazové řádky. Určíme jako hlavní spouštěcí třídu d i v i n e . e d i t o r . C m d l i n e T r a n s f orma předáme jí cestu k uloženému modelu a hodnoty parametrů. Podrobnější informace o syntaxi jsou uvedeny v DiVinE Editor Reference Manual. 2.3

Šablony procesů

V DiVinE Editoru se graficky editují takzvané šablony procesů, které se použijí pro vytvoření skutečného procesu. Tento užitečný koncept lze nalézt i v programech Uppaal, SPIN nebo v modelech pro DiVinE parametrizo vaných pomocí M4. Šablona může používat celočíselné parametry, jejichž hodnotu určíme při vytváření procesu ze šablony. To se provádí zápisem názvu šablony, jejích parametrů a názvu takto vzniklého procesu do místa pro tento účel vyhrazeného - editoru globálních proměnných. Zápis vypadá například takto: P e r s o n ( i n t k = 4)

person_instance;

Aby bylo možné parametrem volit počet procesů určitého druhu v modelu, lze použít syntaktickou konstrukci s hranatými závorkami obsahujícími výraz udávající požadovaný počet vzniklých procesů. Například v klasickém modelu večeřejících filozofů se vytvoří sada N filozofů takto: 14


phil()

p h i l _ i n s t a n c e [N];

Parametry šablony nejsou nikde explicitně vyjmenovány, jak je zvykem u funkcí v běžných programovacích jazycích. Místo toho se jednoduše ty parametry, které jsou uvedeny v závorkách při použití šablony, přidají do tabulky symbolů šablony. Díky tomu mohou být použity v šabloně. Při hromadném vytváření procesů dostane každý proces v sadě stejné hodnoty parametrů, rozlišit mezi nimi je možné jen pomocí proměnné p r o c _ i d , která obsahuje pořadové číslo aktuálního procesu v sadě. 2.4

Parametrizace hran

Editor hrany nabízí dvě možnosti jak zapsat podmínku hrany (guard) a efekt hrany (effect). Můžeme jednoduše přímo zapsat požadovaný výraz do pří slušného políčka, nebo můžeme využít rozšířeného zadávání (políčko exten ded). Při použití rozšířeného zadaní se efekt nebo podmínka sestaví z kopií textového vzoru obsahujícího výraz, který se vyhodnotí pro každou kopii zvlášť. V případě efektu se provedou všechny kopie, v případě podmínky je možné použít disjunkci nebo konjunkci. Na obrázku 2.4 je zobrazeno roz šířené zadávání efektu. Text zadaný v políčku P a t t e r n se opakuje a výrazy uzavřené do $ [ ] jsou vyhodnoceny. Ve výrazu můžeme použít proměnnou x, která nabývá hodnoty z množiny definované v části označené x domain. Effect editor

F^ extended Pattern:

x domain:

I Range range:

1-10

Obrázek 2.4: Editor rozšířeného efektu hrany Například pro následující hodnoty zadané v editoru Pattern:

done[$[x]]

= 0 15

2. PŘEDSTAVENÍ DIVINE EDITORU x domain: Range 1 - N vznikne efekt, který vynuluje všechny položky v poli done od 1 po N: done[l] = 0,done[2]

= 0,done[3]

= 0,...,done[N]

= 0

Další vlastností hrany je Enabled expression. Zaškrtnutím stejně pojme novaného políčka se objeví místo, kam lze zadat podmínku pro to, aby byla hrana zařazena do výstupního modelu. Tímto způsobem je možné přidat do modelu přechody alternativního chování, které se používají pouze pokud jsou nějakým parametrem zapnuty. 2.5

Kopírovaní hran

V DiVinE Editoru je možné určit hranám množinu zdrojových a množinu cílových stavů. Hrana je pak vytvořena mezi každým zdrojovým a každým cílovým stavem. Zdrojové a cílové stavy se stejně jako u rozšířeného efektu zadávají kopírováním textového vzoru. Tak se získá seznam názvů stavů, mezi kterými hrana povede. Například pro následující hodnoty zadané v editoru rozšířeného počátku (origin) hrany Pattern: State$[x] x domain: Range

1-3

a následující hodnoty zadané v editoru cíle (destination) Pattern: State$[x] x domain: Range 10 - 11 budou výsledkem tyto hrany: Statel -* StatelO State2 -* StatelO State3 -* StatelO Statel -* Statel 1 State2 -* Statel 1 State3 -* Statel 1

V grafickém editoru není hrana s násobným cílem připojena svým cílo vým koncem k žádnému stavu (viz obrázek 2.5). Stejné pravidlo platí i pro 16


počátek hrany. Kdyby totiž byla hrana připojena k nějakému stavu, mohlo by to uživatele mást. DiVinE Editor tedy umožňuje pracovat s hranami, které nejsou připojeny k žádnému stavu. Odpojený konec hrany je znázor něn modrým čtverečkem, připojený konec modrým kruhem. Pro vytvoření nepřipojené hrany stačí kliknout ve volné ploše, pokud nechceme připojit koncový stav hrany, ukončíme hranu kliknutím pravým tlačítkem.

StateO

Obrázek 2.5: Hrana s násobným cílovým stavem

2.6

Vícerozměrná pole

Jazyk DVE podporuje pouze jednorozměrná pole proměnných. DiVinE Edi tor toto omezení už nemá. Je možné v něm definovat a používat pole libo volné dimenze. Při výstupu do DVE jsou pole převedena na jednorozměrná a všechny přístupy do nich (v efektu, podmínce nebo synchronizaci) jsou odpovídajícím způsobem také převedeny Převod indexů podporuje pou žití proměnných. Například máme-li definované pole a o rozměru 10 x 10, potom bude přístup a [ 4, x ] převeden na a [10 * x + 10 * 4 ] .

2.7

Ostatní

Jazyk DVE podporuje pojmenované konstanty (prefix c o n s t ) , ale nepod poruje jejich použití v deklaraci pole. DiVinE Editor toto umožňuje, do výsledného souboru DVE na místo konstanty dosadí její hodnotu. Za pojme novanou konstantu lze považovat i parametr deklarovaný v sekci Parame ters. Rozdíl je v tom, že parametr je dosazený z vnějšku, zatímco konstanta deklarovaná v sekci Variables je vnitřní hodnota a není určena k modifikaci. 17


Operátory ~ * r

+, 0 « , & " | i

<, / && ||

Typ unární aritmetické unární aritmetické aritmetické 'i % aritmetické aritmetické ? : aritmetické >> aritmetické aritmetické aritmetické unární logické >= logické >, <=, > — logické • logické logické

Význam převrácení bitů převrácená hodnota násobení, dělení, modulo sčítání, odčítání ternární operátor bitový posun vlevo, vpravo operace AND po bitech operace XOR po bitech operace OR po bitech negace porovnávání porovnávání AND OR

Tabulka 2.1: Tabulka operátorů v DiVinE Editoru. Výrazy v DiVinE Editoru jsou buď aritmetické nebo logické. Tabulka 2.7 obsahuje seznam všech podporovaných operátorů a jejich druh. Priorita je udána pořadím v tabulce - první řádek má nejvyšší prioritu. Všechny tyto výrazy podporuje i DiVinE, až na ternární operátor. V efektu, podmínce a synchronizačním výrazu ho proto nelze použít, protože tyto hodnoty se přímo předávají do souboru DVE. Podobně i při indexování polí je třeba dávat pozor, protože pokud je v indexu použit neznámý symbol, vloží se do výsledného DVE souboru výraz tak, jak byl zadán. Pokud jsou při vyhodnocování indexu všechny symboly známy, vloží se pouze výsledek vý razu a případné použití ternárního operátoru nezpůsobí problém. Ve všech ostatních případech se výrazy vyhodnocují na konkrétní čísla a tedy ternární operátor použít lze. To platí i pro výrazy uzavřené v $ [ ] v rozšířeném efektu nebo podmínce hrany.

18

Kapitola 3

Použité technologie 3.1

Java

Program Paxion (a v důsledku i DiVinE Editor) je napsán v jazyce Java firmy Sun Microsystems. Tento jazyk se pro program tohoto typu hodí, protože podporuje objektově orientované programování, má standardní knihovnu pro grafické uživatelské rozhraní, obsahuje algoritmy pro 2D kreslení a v neposlední řadě programy napsané v Jávě jsou bezproblémově přenositelné mezi hlavními platformami. DiVinE běží v současné době na Linuxu a mnoho jeho uživatelů tento systém používá i jako svůj primární operační systém. Na druhou stranu existují i uživatelé systému Windows, kteří využívají vzdálený cluster linuxových počítačů, na kterých běží DiVinE. Takoví uživatelé budou preferovat editaci modelů na jejich osobním počítači s Windows. Proto je přenositelnost programu žádoucí. Navíc DiVinE GUI [4] je rovněž naprogramováno v Jávě a díky tomu se otevírá možnost integrovat oba programy dohromady a usnadnit tak uživateli práci. 3.2

SableCC

Na mnoha místech v DiVinE Editoru se používají aritmetické nebo logické výrazy. Parametry a proměnné se editují rovněž textově (proměnné kopírují syntaxi DVE). Proto bylo potřeba najít parser, kterým by se dalo snadno s ta kovými výrazy pracovat. Volba padla na program SableCC [5], který vznikl v rámci diplomové práce Etienne Gagnona z McGill University v Kanadě. SableCC je „compiler compiler", který vytváří LALR(l) parser v jazyce Java. Od ostatních programů svého druhu se odlišuje v několika bodech. Parser generovaný SableCC vytváří ze vstupního textu silně typovaný abs traktní syntaktický strom. Například z útržku gramatiky e x p r -> {add} e x p r p l u s e x p r

| {sub} e x p r minus e x p r

vznikne třída PExpr (production e x p r ) s podtřídami AAddExpr (alterna tive) a ASubExpr. Takové třídy se skládají do syntaktického stromu. Tento 19

3. P O U Ž I T É T E C H N O L O G I E

strom se prochází použitím návrhového vzoru Návštěvník bleCC vygeneruje třídu obsahující prázdnou metodu tvaru void case(

(Visitor). Sa

node);

pro každou uzlovou třídu (v našem případě ASubExpr, AAddSubExpr). Od této třídy zdědíme novou a implementujeme metody pro jednotlivé uzly. Po tom zavoláme na jakémkoliv uzlu metodu a p p l y s instancí naší třídy a uzel už sám zavolá příslušnou metodu podle svého typu. SableCC navíc gene ruje i třídu pro procházení syntaktického stromu do hloubky, s jejíž pomocí můžeme snadno implementovat vyhodnocování výrazů. V následujícím příkladu je část vyhodnocovací třídy implementované tímto způsobem: p r i v a t e c l a s s ArithmeticWalker extends DepthFirstAdapter { @Override public void outAAddExpr(AAddExpr node) { int r = stack.pop (); int 1 = stack.pop (); stack.push(l + r ) ; } } Dále program SableCC podporuje transformaci z konkrétního syntak tického stromu na abstraktní. Často je třeba konkrétní gramatiku kvůli definování asociativity a priority operátorů nebo kvůli řešení shift/reduce konfliktů neintuitivním způsobem transformovat. Pracovat pak s konkrét ním syntaktickým stromem odpovídajícím takové gramatice je nepohodlné. S pomocí SableCC můžeme už v souboru s gramatikou definovat překlad z konkrétní gramatiky na abstraktní, která více odpovídá původní myšlence. V programu pak už pracujeme s přehlednějším abstraktním stromem. Im plementačním jazykem SableCC je Java. Program v aktuální verzi dokáže generovat parsery i pro další jazyky jako například C++, C# a další. 3.3

XStream

Pro ukládání modelů do formátu XML používá DiVinE Editor knihovnu XStream. XStream je knihovna pro serializaci javových objektů do XML a případně i do jiných formátů. Proces je zcela automatický a částečně konfigurovatelný. 20

3. P O U Ž I T É T E C H N O L O G I E

3.4

JUnit

Všechny nově napsané třídy DiVinE Editoru, které netvoří grafické uživa telské rozhraní, mají jednotkové testy. Jako rámcovou knihovnu pro tyto testy jsem použil knihovnu JUnit. Jedná se o standardní rámcovou knihovnu pro jednotkové testování programů v jazyce Java, kterou spravuje komunita JUnit.org.

21

Kapitola 4

Architektura a implementace V této kapitole se blíže seznámíme s architekturou a implementačními po drobnostmi programu DiVinE Editor. Zaměříme se především na novou funkcionalitu v porovnání s programem Paxion, tedy parametrizaci modelů. Bližší informace o architektuře kódu převzatého z Paxionu se nacházejí v diplomové práci o Paxionu [10]. Na obrázcích 4.1 a 4.2 jsou zobrazeny významné vztahy mezi nejdůleži tějšími třídami z oblasti editace modelu a převádění do DVE. V textu pak následují stručné popisky účelu a implementace nejdůležitějších tříd. 4.1

Pomocné třídy

Nejprve se seznámíme s důležitými pomocnými třídami, které jsou odkazo vány v následujícím textu. ValueGenerator Hrana může mít jako svůj koncový bod i celou mno žinu stavů (viz 2.5). Třídy odvozené od V a l u e G e n e r a t o r poskytují způsob, jak takovou množinu určit. Každá odvozená třída generuje podle svého nastavení seznam textových řetězců přístupných pomocí rozhraní I t e r a t o r < S t r i n g > . Pro účely grafického editoru by měla navíc každá odvozená třída rozumným způsobem implementovat metodu t o S t r i n g ( ) , jejíž návratová hodnota se kreslí k hraně, je-li ValueGenerator použit pro vytvoření podmínky nebo efektu hrany. Enumeration Tato implementace třídy V a l u e G e n e r a t o r dává na vý stup předem dané hodnoty. Používá se v případě, kdy chce uživatel definovat všechny hodnoty ručně. ExprRange Generuje celá čísla v intervalu. Koncové body intervalu lze zadat aritmetickým výrazem. P a t t e r n Třída Pattern má jeden textový parametr a jeden parametr doma i n typu V a l u e G e n e r a t o r . Postupně bere hodnoty z domain, vkládá je 22

ŕ" > n H M H ProlectEdrtor

ProcessEdHor

TranaltlonEdltor

C

> ModelOverview

r1 Strom součástí modelu

OJ

í

Obrázek 4.1: Diagram tříd z pohledu editace modelu

M H

> n

4. ARCHITEKTURA A IMPLEMENTACE

ParserFactory «use»

^ ^

DveTransform

ExprEvaluator «use»

""---^

«use»

«use»

^

>

SymbolTable

^ ArrayTransfönm

''

'«use»

výstup

«Interface» IModelBuilder

Obrázek 4.2: Diagram tříd z pohledu převodu do DVE do tabulky symbolů pod názvem x a vyhodnocuje s ní všechny výrazy uzavřené do závorek tvaru $ [ ] v textovém parametru. Závorky jsou pak nahrazeny hodnotou výrazu (viz 2.4). SimpleOrGenerator Hned u několika vlastností hrany je možné na stavit buď jednu jednoduchou hodnotu, nebo celou množinu hodnot generovaných některým potomkem třídy V a l u e G e n e r a t o r . Tato třída slouží jako úložiště takových přepínacích vlastností. Typ jedno duché hodnoty je možné určit typovým parametrem T. 4.2

Součásti modelu

Jako úložiště informací o modelu slouží stejně jako v Paxionu třídy S t a t e , T r a n s i t i o n , P r o c e s s , P r o j e c t . Nové jsou třídy T r a n s i t i o n E n d p o i n t , Guard, E f f e c t a třídy odvozené od V a l u e G e n e r a t o r . P r o j e c t Tato třída reprezentuje model jako celek. Je úložištěm procesů, globálních proměnných a parametrů. Proměnné a parametry jsou ulo ženy v textové podobě v syntaxi shodné s DVE. Pro přístup k nim slouží vnořené třídy Var i a b l e sMo d e l a P a r a m e t e r sModel imple mentující rozhraní I V a r i a b l e s M o d e l . Díky nim je možné používat stejný editor jak pro parametry, tak pro proměnné. Pokud je v definici proměnných chyba, funguje I V a r i a b l e s M o d e l jako zástupce chyby pro snadnější orientaci uživatele (viz 4.4). P r o c e s s Zde jsou v seznamech uloženy všechny stavy a přechody z da ného procesu. Dále tato třída ukládá lokální proměnné procesu pří stupné stejně jako u projektu přes vnořenou třídu Var i a b l e sMo d e l 24


S t a t e Tato třída nedoznala od Paxionu podstatných změn. Vedle ukládání informací o stavu rovněž zajišťuje vykreslování grafické reprezentace stavu na kreslicí plochu. T r a n s i t i o n Zde jsou uloženy informace o daném přechodu. Mezi ně patří: •

odkazy na třídy T r a n s i t i o n E n d p o i n t pro koncové body hrany

•

Guard pro podmínku hrany

•

E f f e c t pro efekt hrany

•

položka typu S t r i n g obsahující synchronizační výraz

•

výraz pro povolení nebo zakázání hrany

T r a n s i t i o n dále spravuje nastavení svých koncových bodů. Pokud je koncovým bodem jediný stav, je třeba mít na příslušnou instanci odkaz a daný stav musí mít tuto hranu ve svém seznamu. Naopak je-li koncových stavů celá množina, musí být stav prázdný a hrana musí mít odkaz na příslušného potomka třídy V a l u e G e n e r a t o r . Stejně jako S t a t e i tato třída kreslí grafickou reprezentaci hrany na kreslicí ploše. Dále aktualizuje texty popisků hrany (efekt, podmínka, synchronizace) v případě změny. T r a n s i t i o n E n d p o i n t Konec hrany může být, jak už bylo řečeno, b u ď prostý stav, nebo celá množina stavů (viz 2.5). T r a n s i t i o n E n d p o i n t je specializací třídy S i m p l e O r G e n e r a t o r < T > , kde jednoduchou hodnotou je třída S t a t e . Každá hrana má jednu instanci této třídy pro svůj počátek a jednu pro svůj konec. Tato třída dále zastupuje umístění chyby při převodu do DVE. Guard Podmínka hrany může být jednoduchý řetězec, který bude přímo předán do souboru DVE, nebo může být složena z několika kopií tex tového vzoru (viz 2.4). Guard je rovněž specializací generické třídy S i m p l e O r G e n e r a t o r < T > , a navíc ukládá i způsob vytvoření logic kého výrazu z jednotlivých částí (spojení konjunkcí nebo disjunkcí). I tato třída zastupuje umístění chyby. E f f e c t Tato třída je analogií třídy Guard pro ukládání efektu hrany. 25


4.3

Zpracování výrazů

Podstatnou součástí DiVinE Editoru je vyhodnocování výrazů. Aritme tické výrazy je možné použít v deklaraci velikosti pole nebo bufferu ka nálu, jako počáteční hodnotu proměnné nebo konstanty, v potomcích třídy V a l u e G e n e r a t o r , při přístupu do pole (v efektu, podmínce nebo synchro nizačním výrazu na hraně), výrazy dávají hodnotu parametrům šablony procesu a pomocí výrazu určujeme i počet vytvořených procesů z dané šablony Následující třídy obstarávají vyhodnocování všech výrazů. P a r s e r F a c t ory Vytváří a sestavuje třídy vygenerované parserem SableCC potřebné k vytvoření syntaktického stromu z výrazu v textové podobě. Dále poskytuje metody pro spuštění vlastní syntaktické analýzy. V pro gramu je třeba analyzovat několik druhů textu (například aritmetický výraz, logický výraz, deklarace proměnných a podobně). Gramatika a vygenerovaný parser je však jen jediný - kořenový neterminál gra matiky se přepisuje na klíčové slovo a kořenový neterminál pro každý druh textu. Klíčové slovo slouží k zajištění jednoznačnosti gramatiky. P a r s e r F a c t o r y automaticky přidává k textu potřebné klíčové slovo podle druhu vstupního textu. Symbol Table Výrazy obsahují symboly (proměnné), jejichž hodnota se při vyhodnocování hledá v tabulce symbolů implementované touto třídou. V každém z výše vyjmenovaných použití výrazů jsou defino vány jiné symboly. Například při vyhodnocování výrazu v procesu jsou definovány všechny globální symboly a navíc lokální symboly procesu (mezi ně patří parametry šablony nebo lokální pojmenované konstanty). Při vyhodnocování výrazů na hraně jsou známy všechny globální a lokální symboly a navíc některé symboly specifické pro hranu. Pro jednodušší práci s takto strukturovanými tabulkami sym bolů podporuje třída Symbol T a b l e řetězení. Pokud jí nastavíme jinou tabulku symbolů jako rodiče, dotáže se v případě neúspěšného hledání symbolu ve vlastním seznamu i svého rodiče. Symboly jsou ve třídě SymbolTable ukládány podle svého typu do tří seznamů. Jedná se o seznam pro celá čísla, textové řetězce a pole. Poslední z jmenovaných se využívá pro transformaci vícerozměrných polí na jednorozměrné, ke kterému je třeba znát rozměry pole. ExprEvaluator Třída provádějící vlastní vyhodnocování výrazů. Kom binuje služby tříd P a r s e r F a c t o r y a SymbolTable s procházením 26


abstraktního syntaktického stromu do hloubky pomocí třídy odvozené od D e p t h F i r s t A d a p t e r ze SableCC. 4.4

Převod do DVE

Vlastní převod modelu do jazyka DVE zajišťují následující třídy: IModelBuilder Toto rozhraní definuje metody, které přidávají na nějaký výstup elementy modelu v jazyce DVE. Díky tomuto abstraktnímu rozhraní lze snáze programovat jednotkové testy převodu. Teoreticky by bylo možné naprogramovat i alternativní výstupní formát pros tou implementací tohoto rozhraní. Jisté omezení spočívá v tom, že I M o d e l B u i l d e r je poměrně těsně svázán s principem a myšlenkou formátu DVE. D v e B u i l d e r Konkrétní implementace rozhraní I M o d e l B u i l d e r pro ja zyk DVE. I E r r o r S i t e Chyby v modelu jsou detekovány ve fázi převodu do DVE a příslušné výjimky drží odkaz na datovou třídu implementující roz hraní I E r r o r S i t e obsahující chybná data. Jediná metoda rozhraní musí aktivovat příslušné místo v grafickém uživatelském rozhraní. Datové třídy a jejich editory jsou ale oddělené a proto datové třídy přesměrovávají požadavek na jednu z metod třídy P r o j e c t E d i t o r , která má ve své správě všechny editory. Zde se opět uplatňuje návr hový vzor Návštěvník. ModelExcept i o n Třída pro zabalení výjimky zjištěné při převodu do DVE. Obsahuje odkaz na vnitřní výjimku, informaci pro uživatele a odkaz na objekt implementující rozhraní I E r r o r S i t e , ve kterém k chybě došlo. DveTransf orm Tato třída provádí vlastní převod modelu do DVE. Jedná se o všechny transformace popsané v kapitole 2. Třída postupně zpra covává všechny části modelu a výsledek předává do třídy odvozené od rozhraní I M o d e l B u i l d e r dodané zvenčí. Pokud při převodu na razí na jakoukoliv chybu, vytvoří výjimku typu M o d e l E x c e p t i o n , doplní informaci pro uživatele a místo, kde k chybě došlo. ArrayTransf orm Tato třída převádí indexy polí z vícerozměrného inde xování na jednorozměrné. Funguje jako pomocná třída volaná z trans formačního procesu probíhajícího v DveTransf orm. 27


4.5

N o v é uživatelské r o z h r a n í

Struktura grafického uživatelského rozhraní v Paxionu byla příliš jedno duchá a nedostačovala komplexnější organizaci modelu v DiVinE Editoru. Proto byla přepracována po vzoru Uppaalu. Následující třídy tvoří novou strukturu uživatelského rozhraní: D i v i n e E d i t o r Hlavním oknem a také spouštěcí třídou DiVinE Editoru je tato třída. Sama obsahuje pouze menu, panel nástrojů a instanci třídy P r o j e c t E d i t o r . Spravuje akce které tvoří položky v menu a na panelech nástrojů. ModelOverview Strom součástí modelu je implementován touto třídou. Aktualizaci uzlů po přidání nebo smazání procesu provádí automa ticky díky přijímání příslušných událostí od třídy P r o j e c t . Každý uzel ve stromu má přiřazenu jednu ze tříd implementujících rozhraní INodeType. Tyto třídy jsou vnořeny ve třídě ModelOverview a zpra covávají požadavky na text popisku svého uzlu. Dále reagují na udá losti vybrání nebo zrušení výběru svého uzlu, typicky aktivací grafic kého editoru dané části modelu. Pro j e c t E d i t o r Tato třída tvoří kontejner pro ModelOverview a editory jednotlivých částí modelu. Podle potřeby je také vytváří a spravuje. Je likož úložné třídy, které implementují I E r r o r S i t e , jsou odděleny od svých editorů, požadavky na zobrazení místa chyby jsou směrovány na P r o j e c t E d i t o r . P r o c e s s E d i t o r Editor procesů sestává především z kreslicí plochy imple mentované třídou D r a w i n g P a n e l a z místa v pravé části okna, kam se umisťují editory komponent na kreslicí ploše (stavů a hran). Tato třída spravuje kreslicí plochu a editory komponent, které vytváří jako reakci na událost mouseDownOnComponent třídy D r a w i n g P a n e l . Transf ormWindow Okno, které se zobrazí po kliknutí na položku Export to DVE je instancí této třídy. Celý proces převodu je jí řízen. Každá fáze se provádí v jedné z vnořených tříd ReadParams, Make SymbolTable a RunTransform. 4.6

Ukládání modelu do XML

DiVinE Editor ukládá své modely do formátu XML s pomocí knihovny XStream. To je další bod, ve kterém se liší od svého předchůdce Paxionu. Ten 28


sice rovněž ukládal modely do XML, ale prováděl to jednodušším způsobem. Každá třída, která skladovala nějaká data, měla metodu writeXML, která ručně uložila všechna data v dané třídě. Tento přístup považuji za těžko rozšiřitelný a neudržovatelný a rozhodl jsem se použít automatizované řešení. Ve výchozím nastavení knihovna XStream prochází objektový graf do hloubky a ukládá odpovídající strukturu jako strom v XML. Když narazí na cyklus (odkaz na objekt, který již byl navštíven), vloží pouze odkaz. Pro účely editoru jsem zakázal ukládání některých proměnných, které se dají vygenerovat po načtení. K obnově po načtení slouží metoda r e a d R e s o l v e , kterou knihovna XStream volá pro každý načtený objekt. Dále jsem ukládání nastavil tak, aby stavy byly společně na jednom místě a stejně tak přechody. Jinak by je XStream ukládal tak, jak by na ně narazil, a jelikož každý stav má odkazy na všechny hrany, které do něj vedou, a stejně tak hrany mají odkazy na své koncové stavy, byl by výsledný XML soubor nepřehledný. Následující třídy zajišťují ukládání a načítání modelů: XStreamFactory Vytváří a konfiguruje instanci třídyXStream. XmlPro j e c t W r i t e r Ukládá projekt do XML pomocí X S t r e a m F a c t o r y . XmlPro j e c t R e a d e r Načítá projekt z XML a obnovuje původní strukturu objektů tam, kde byla uložením změněna.

29

Kapitola 5

Závěr V této práci jsme prostudovali požadavky na parametrizovatelnost modelů pro model checking a zhodnotili možnosti 4 programů v této oblasti. Rozší řením existujícího grafického editoru modelů pro DiVinE vznikl program DiVinE Editor, který podporuje parametrizaci modelů. Při návrhu tohoto roz šíření jsme brali v úvahu ty vzory parametrizace, které se často vyskytovaly v modelech z databáze BEEM. Už při samotném vývoji se naskytlo několik způsobů, jak program ještě více vylepšit. Například by bylo užitečné mít možnost přidávat na kreslicí plochu poznámky a dokumentaci, umožnit editovat podmínku, efekt nebo synchronizační výraz pouhým kliknutím přímo na příslušný popisek anebo naprogramovat funkci Zpět (undo). Vývoj každého programu musí ale někdy skončit, a proto tyto funkce v současné verzi implementovány nejsou. Další návrhy na zlepšení jistě vzniknou až bude program uveden do praxe. I současný způsob parametrizace efektů, podmínek a případně množiny koncových stavů hrany pomocí třídy P a t t e r n je omezený a nelze s ním vy jádřit všechny možné případy. Pokud nebude implementován mechanismus ekvivalentní Turingově stroji, vždy půjde jen o jisté omezené zjednodušení. Výsledný program může dobře posloužit k tvorbě jednoduchých až středně složitých modelů. Díky funkcím, jako jsou vícerozměrná pole, šab lony procesů s parametry a grafické „kreslení" procesů, by mělo být sesta vování modelu pro uživatele poměrně snadné. Implementace byla provedena s důrazem na kvalitní objektový návrh a většina nového kódu je dostatečně zdokumentována, aby byl program snadno rozšiřitelný a údržba bezproblémová.

30

Literatura [1] Benchmarks for Explicit Model checkers. URL h t t p : / / a n n a , f i .muni . c z / m o d e l s / (26. 4. 2008) [2] Clarke, E. M.; Grumberg, O.; Peled, D. A.: Model Checking. Cambridge, Massachusetts: The MIT Press, 1999. [3] Domovská stránka DiVinE. URL h t t p : / / a n n a , f i . m u n i . c z / d i v i n e (26.4.2008) [4] Forejt, V.: Grafické rozhraní pro komunikaci s nástrojem DiVinE. Baka lářská práce, Fakulta informatiky, Masarykova univerzita, 2005. [5] Gagnon, É.: SableCC, An Object-Oriented Compiler Framework. Diplo mová práce, School of Computer Science, McGill University, 1998. [6] Holzmann, G. J.: The Model Checker Spin. IEEE Trans, on Software Engineering, ročník 23,5, May 1997: s. 279-295, special issue on Formal Methods in Software Practice. [7] Holzmann, G. J.: Logic Verification of ANSI-C code with SPIN. In Proc. of the 7th International SPIN Workshop, ročník 1885, Springer-Verlag, 2000, s. 131 - 147. [8] Holzmann, G. J.: The SPIN Model Checker: Primer and Reference Ma nual. Addison-Wesley Professional, 2003, ISBN 0-321-22862-6. [9] Domovská stránka M4. URL h t t p : //www. g n u . o r g / s o f t w a r e / m 4 (26.4. 2008) [10] de Menten, G.: Graphical Environment for Buchi Automata. Diplomová práce, University of Namur(FUNDP), 2004. [11] Domovská stránka PRISMu. URL h t t p : / / w w w . p r i s m m o d e l c h e c k e r . o r g / (26. 4. 2008) [12] Raymond, E. S.: The Art of Unix Programming, kapitola Minilanguages. Addison-Wesley, 2004, ISBN 0131429019, str. 193. 31

6. LITERATURA

[13] Domovská stránka Spinu. URL h t t p : / /www. s p i n r o o t . com (26. 4. 2008) [14] Domovská stránka Uppaalu. URL h t t p : //www. u p p a a l . com/ (26. 4. 2008)

32

Příloha A

Průvodce tvorbou modelu V této kapitole si krok po kroku ukážeme, jak v programu DiVinE Editor namodelovat klasický problém večeřejících filozofů. N filozofů sedí u kulatého stolu, na kterém je uprostřed velká mísa s rýží. Mají k dispozici N hůlek, mezi každými dvěma sousedícími filozofy je na stole položena jedna hůlka. Na začátku všichni filozofové přemýšlejí. Když chce některý z nich začít jíst, zvedne nejprve hůlku po své pravici (pokud je volná), potom hůlku po své levici (pokud je volná) a pak začne jíst. Když dojí, hůlky odloží na místo ve stejném pořadí, v jakém je vzal. Náš model bude mít vedle parametru N také parametr ROOM. Ten udává maximální počet filozofů sedících zároveň u stolu. Pokud je ROOM roven 0, sedí u stolu všichni filozofové (a tak na každého vychází právě jedna hůlka). Další parametr, LEFT, změní prvního filozofa na leváka, takže bude zvedat nejprve levou a poté pravou hůlku. A . l Základní verze Když spustíme DiVinE Editor, máme před sebou projekt obsahující jednu prázdnou šablonu procesu nazvanou P r o c e s s i . Začneme definicí parame trů. Klikneme ve stromu vlevo na uzel P a r a m e t e r s . Do textového editoru vpravo zapíšeme parametry N, ROOM a LEFT: int N = 4; int LEFT = 0; int ROOM = 0; Dále nastavíme model na asynchronní. To provedeme jednoduše kliknu tím na uzel Model a zaškrtnutím příslušného políčka v okně v pravé části programu. Nyní nadeklarujeme proměnné, do kterých se bude ukládat počet filo zofů u stolu a stav hůlek. Klikneme na uzel V a r i a b l e s a vpravo se nám zobrazí globální deklarace. Uvidíme tam použití šablony P r o c e s s i : Processi()

x; 33

A. PRŮVODCE TVORBOU MODELU

Tento řádek smažeme a místo něj vytvoříme pole typu b y t e o velikosti N a dále celočíselnou proměnou c o u n t : b y t e c h o p s t i c k [N]; i n t count; V poli c h o p s t i c k bude na i-tém místě hodnota 0 pokud i-tá hůlka leží na stole, nebo hodnota 1 když ji nějaký filozof drží v ruce. Proměnná c o u n t zaznamenává počet filozofů sedících u stolu a používá se pouze pokud je parametrem ROOM zapnuta varianta s omezením počtu současně sedících filozofů. Nyní můžeme začít modelovat procesy. Šablonu P r o c e s s i přejmenu jeme na p h i l tak, že na ni klikneme a vpravo nahoře, v políčku označeném P r o c e s s name, napíšeme p h i l . Nyní začneme vytvářet stavy. Klikneme na ikonku S t a t e s a do bílého prostoru uprostřed programu vložíme 4 stavy. Klikneme postupně na každý z nich a pomocí okna vpravo je přejmenujeme na t h i n k , one, e a t a f i n i s h . Stav t h i n k také určíme za počáteční zaškrt nutím příslušného políčka v jeho vlastnostech. Filozof je ve stavu one, když má jednu hůlku a čeká na druhou. Podobně f i n i s h je stav, kdy už jednu hůlku položil a chystá se položit i druhou. Význam stavů e a t a t h i n k je zřejmý z jejich názvů. V dalším kroku přidáme přechody mezi stavy. Klikneme na tlačítko T r a n s i t i o n s a vytvoříme přechod mezi stavem t h i n k a o n e (klikneme na první stav a pak na druhý). Další přechody budou one —• e a t , e a t —> f i n i s h a nakonec f i n i s h —> t h i n k . Dále musíme nastavit vlastnosti těchto přechodů. Začneme s prvním z nich, t h i n k —• one. Filozof může zvednou pravou hůlku pouze pokud leží na stole. Klikneme na ní a do políčka Guard napíšeme následující výraz: chopstick[proc_id]

== 0

Hůlka napravo od i-tého filozofa má stejný index, i. Proměnná p r o c _ i d představuje pořadové číslo aktuálního procesu, takže celkový výraz platí právě tehdy, když je hůlka vpravo od aktuálního filozofa volná. Změnu hůlky na zvednutou provedeme pomocí následujícího výrazu v políčku Effect chopstick[proc_id]

= 1

To je prozatím vše pro tuto hranu. Podobně nastavíme i hranu one —• e a t , na které filozof zvedne druhou hůlku. Výrazy tentokrát budou vypadat takto: guard: 34


chopstick[(proc_id +1) effect: chopstick[(proc_id +1)

% N]

==0

% N]

=1

Levá hůlka má index o 1 vyšší. N-tý filozof má jako levou nultou hůlku. Přechody e a t —> f i n i s h a f i n i s h —> t h i n k jsou podobné. Tentokrát ale chybí guard, protože položení hůlky nic nebrání. e f f e c t na e a t -> f i n i s h : chopstick[proc_id] = 0 e f f e c t na f i n i s h -> e a t : chopstick[(proc_id +1)

% N]

=0

Posledním krokem k dokončení základního modelu večeřejících filozofů je vložení šablony p h i l do systému. Klikneme na uzel V a r i a b l e s ve stromu vlevo. Pod proměnné zapíšeme následující: phil()

instance_phil[N];

Tento zápis nám do systému vloží N instancí procesu p h i 1, které se budou jmenovat i n s t a n c _ p h i l _ 0 - i n s t a n c e _ p h i l _ N - l . A.2 Varianta s jedním levákem Nyní implementujeme parametr LEFT. Ten může mít dvě hodnoty, 0 a 1. Když je nastaven na 0, všichni filozofové zvedají nejprve pravou hůlku a poté levou. Když je nastaven na 1, první filozof zvedá nejprve levou a potom pravou. Ostatní zůstávají nezměněni. Pro náš model to znamená, že levoruký filozof musí na přechodu t h i n k —> one pracovat s hůlkou číslo 1 a na přechodu one —• e a t s hůlkou číslo 0. Stejným způsobem se změní i přechody e a t —• f i n i s h a f i n i s h —• t h i n k . Index hůlky tedy nyní závisí na hodnotě parametru LEFT a na indexu filozofa. Abychom nemuseli psát složitý podmíněný výraz opakovaně na všechny hrany, pomůžeme si deklarací lokálních konstant f i r s t _ i d a s e c o n d _ i d . První z nich bude vždy pro aktuálního filozofa udávat index té hůlky, kterou zvedne (a po jídle položí) jako první a s e c o n d _ i d bude index druhé hůlky. Začneme tedy deklarací lokálních konstant f i r s t _ i d a s e c o n d _ i d . Ve stromu na levé straně otevřeme uzel p h i l a klikneme na jeho poduzel V a r i a b l e s . Do textového editoru vpravo napíšeme tyto deklarace: c o n s t i n t f i r s t _ i d = ((LEFT = = 1 ) && ( p r o c _ i d ? ( ( p r o c _ i d + 1 ) % N) : proc_id;

==0))

35


c o n s t i n t s e c o n d _ i d = ((LEFT == 1) && ( p r o c _ i d == 0)) ? proc_id : ( ( p r o c _ i d + 1) % N) ; Hodnota první konstanty je určena podmíněným výrazem, jehož podmínka říká, že máme zapnutý parametr LEFT a že aktuální filozof je první. Pokud je tato podmínka splněna, přijde jako první na řadu hůlka s indexem o 1 větším, v ostatních případech to bude hůlka se stejným indexem. Druhá konstanta má symetrický význam. V dalším kroku musíme v procesu pře psat podmínky a efekty hran. Místo přímého výpočtu indexu hůlky tam napíšeme naše dvě nové konstanty. Tím se model trochu zpřehlední a na víc bude reagovat na parametr LEFT. Nové hodnoty budou tedy vypadat následovně: t h i n k -> one g u a r d : chopstick[first_id] t h i n k -> one e f f e c t : chopstick[first_id] one -> e a t g u a r d : chopstick[second_id] one -> e a t e f f e c t : chopstick[second_id] e a t -> f i n i s h e f f e c t : chopstick[first_id] f i n i s h -> t h i n k e f f e c t : chopstick[second_id]

== 0 = 1

== 0 = 1

= 0

= 0

A.3 Omezení počtu filozofů u stolu Tím jsme hotovi s parametrem LEFT. Zbývá ještě parametr ROOM. Pokud bude tento parametr zapnut, bude mít proces filozofa trochu jinou strukturu. Vytvoříme proto novou šablonu a nazveme ji p h i l _ r oom. Do jejích lokálních proměnných zkopírujeme deklarace konstant f i r s t _ i d a s e c o n d _ i d . Šablona bude mít 5 stavů, t h i n k , i n s i d e , one, e a t a f i n i s h . Přechody mezi nimi budou tyto: t h i n k s i n s i d e Filozof usedne ke stolu. 36


i n s i d e ^ one Zvedne první hůlku. one —> e a t Zvedne druhou hůlku. e a t —> f i n i s h Položí první hůlku. f i n i s h —> i n s i d e Položí druhou hůlku. i n s i d e —> t h i n k Zvedne se od stolu a začne opět přemýšlet. Podmínky a efekty na hranách mezi stavy i n s i d e , one, e a t a f i n i s h budou stejné jako v předchozím případě. Na hraně t h i n k —• i n s i d e musíme kontrolovat počet filozofů u stolu a pokud k němu filozof usedne, příslušně zvýšit počítadlo c o u n t . Na opačné hraně stačí počítadlo snížit. Podmínky a efekty budou tedy vypadat takto: t h i n k -> count t h i n k -> count

inside guard: <= ROOM inside effect: = count + 1

i n s i d e -> t h i n k e f f e c t : count = count - 1 Nakonec zbývá určit, kdy se má která šablona použít. Klikneme na uzel V a r i a b l e s na nejvyšší úrovni. Zde máme pod globálními proměnnými zapsáno, že v modelu má být N procesů šablony p h i l . Změníme to na následující dva řádky: p h i l ( ) instance_phil[(ROOM = = 0 ) ? N : 0 ] ; phil_room() instance_phil_room[(ROOM = = 0 ) ? 0 : N]; V hranatých závorkách máme nyní podmíněné výrazy, jejichž hodnotami je v závislosti na parametru ROOM b u ď 0, nebo N. Tím dosáhneme toho, aby v systému bylo vždy b u ď N procesů jednoho typu, nebo N druhého typu. A to je vše, model je v této podobě kompletní. Můžeme ho nyní vyexpor tovat se zvolenými hodnotami parametrů do jazyka DVE.

37

Příloha B

Technické podrobnosti Obsah přiloženého CD b i n Tento adresář obsahuje spustitelnou verzi programu včetně všech po třebných knihoven. s r c Zde naleznete veškeré zdrojové kódy k programu. Jde o zdrojové soubory v jazyce Java, gramatiku pro SableCC, projektové soubory pro Eclipse a obrázky. examples V tomto adresáři jsou ukázkové modely vytvořené v DiVinE Editoru. doc/manual V tomto adresáři se nachází referenční příručka, včetně zdroje ve formátu Dep late. d o c / p r a c e Zde je text této práce v elektronické podobě, opět se zdrojo vými soubory ve formátu Deplate. Instalace a spuštění programu Program DiVinE Editor je standardní program v jazyce Java. K instalaci stačí zkopírovat soubory DivineEditor.jar sablecc.jar xstream-1.2.2.jar z adresáře b i n do počítače. Pro jeho spuštění je třeba mít v systému Java Runtime Environment 0RE) alespoň ve verzi 1.5. Program se spouští standardně příkazem Java - j a r

DivineEditor.jar

nebo jednoduše dvojklikem na soubor D i v i n e E d i t o r . j a r , pokud to sys tém podporuje. 38

Grafický editor parametrizovaných modelů pro DiVinE

Recommend Documents