4. Modelowanie z u˙zyciem tagów
4.1. Wprowadzenie do koncepcji tagów
4.1. Wprowadzenie do koncepcji tagów
Rozwa˙zmy diagram XCCS pokazany na rys. 4.1. Model jest zło˙zeniem równoległym bloczków B1 i B2. Zachowanie bloczków jest okre´slone przez agenta A. Jako ˙ze diagram ten jest płaski, to akcj˛e a bloczka B1, która odpowiada etykiecie portu B1.a zamieniamy na ko-akcj˛e a. Zatem bloczek B1 cyklicznie wykonuje ko-akcj˛e a a po niej akcj˛e b. Podobnie, bloczek B2 cyklicznie wykonuje akcj˛e a a po niej akcj˛e b.
a A B2 a b b A B1 A = a.b.A A Rysunek 4.1: Przykład nr 1
Niech E1 oznacza zło˙zenie równoległe agentów B1 i B2. Diagram z rys. 4.1 jest równowa˙zny poni˙zszemu skryptowi CCS:
E1 = B1|B2 (4.1a) B1 = a.b.B1 (4.1b) B2 = a.b.B2 (4.1c)
W prezentowanym zło˙zeniu równoległym ko-akcja a agenta B1 mo˙ze synchronizowa´c z akcj ˛a a agenta B2. Zachowanie agenta E1a tym samym modelu z rys. 4.1 jest precyzyjnie opisane przez graf przej´s´c lub ogólnie etykietowany system przej´s´c (Labeled Transition System LTS) pokazany na rys. 4.2. B1|B2 b.B1|b.B2 B1|b.B2 b.B1|B2 a b a b a b a b τ {a, a}
Rysunek 4.2: LTS dla przykładu 1
W wielu przypadkach rzeczywisty system współbie˙zny mo˙zna w naturalny sposób opisa´c w po-staci zło˙zenia równoległego z operatorem obci˛ecia ([35, s. 68]).
4.1. Wprowadzenie do koncepcji tagów 60
Definicja 4.1. Mówimy, ˙ze agent P jest standardow ˛a form ˛a współbie˙zn ˛a (z ang. Standard Concur-rent Form, SCF) lub jest w standardowej formie współbie˙znej, je´sli zachodzi
P ≡ (P1[f1]|P2[f2]| . . . |Pn[fn])\K (4.2)
W naszych rozwa˙zaniach powy˙zszy wzór bardzo cz˛esto przyjmuje posta´c
P ≡ (P1|P2| . . . |Pn)\K (4.3)
gdzie agenty Pimaj ˛a posta´c skryptów CSS, czyli w zapisie wyst˛epuje tylko operator nast˛epstwa (.) i operator wyboru (+).
Rozwa˙zmy nieco zmodyfikowany model XCCS, który przedstawiono na rys. 4.3. Poł ˛aczenie mi˛edzy portami B1.a i B2.a zostało usuni˛ete, a zatem ko-akcja a bloczka B1 nie mo˙ze synchroni-zowa´c z akcj ˛a a bloczka B2. Mo˙zemy zatem oczekiwa´c, ˙ze LTS dla modelu z rys. 4.3 jest prawie taki sam, jak pokazany na rys. 4.2, ale nie zawiera kraw˛edzi z etykiet ˛a τ {a, a}, która reprezentuje synchronizacj˛e mi˛edzy ko-akcj ˛a a i akcj ˛a a. Graf taki przedstawiono na rys. 4.4.
a A B2 A a b b A B1 A = a.b.A Rysunek 4.3: Przykład nr. 2 B1|B2 b.B1|b.B2 B1|b.B2 b.B1|B2 a b a b a b a b
Rysunek 4.4: LTS dla przykładu 2
Niestety, nie jest mo˙zliwe przekonwertowanie diagramu z rys. 4.3 do skryptu CCS w postaci Standard Concurrent Form (SCF), który miałby taki sam LTS, jak ten przedstawiony na rys. 4.4. W takim przypadku musimy zmieni´c nazwy etykiet portów, które znajduj˛e si˛e w konflikcie. Rodzina
4.1. Wprowadzenie do koncepcji tagów 61
skryptów SCF, które s ˛a równowa˙zne diagramowi z rys. 4.3 ma posta´c:
E2 = B1|B2 gdzie x 6= b i y 6= b i x 6= y (4.4a)
B1 = x.b.B1 (4.4b)
B2 = y.b.B2 (4.4c)
Agent E2 jest równoległym zło˙zeniem agentów B1 i B2, ale ko-akcja x i akcja y nie mog ˛a ze sob ˛a synchronizowa´c, bo maj ˛a ró˙zne nazwy. Rodzin˛e LTS’ów dla powy˙zszego skryptu CCS pokazano na rys. 4.5. B1|B2 b.B1|b.B2 B1|b.B2 b.B1|B2 y b x b x b y b x 6= b y 6= b x 6= y
Rysunek 4.5: Rodzina LTS’ów dla przykładu nr 2
Jak wida´c, dowolny LTS, który mo˙zna otrzyma´c na podstawie szablonu z rys. 4.5 jest izomor-ficzny do LTS’a z rys. 4.4, ale nie ma takich samych nazw akcji. Z tego powodu, je´sli konwertujemy diagramy XCCS do skryptów CCS, aby zbada´c ich własno´sci przy pomocy metod analitycznych zaimplementowanych w programie CWB ([37]), to musimy zastosowa´c sprz˛e˙zenie zwrotne:
x 7→ B1.a (4.5a)
y 7→ B2.a (4.5b)
Definicja 4.2. Mówimy, ˙ze ko-akcja a bloczka B1i akcja a bloczka B2maj ˛a własno´sci odpowiednio P1i P2, wtedy i tylko wtedy, gdy ko-akcja x i akcja y równowa˙znego skryptu CCS maj ˛a własno´sci odpowiednio P1i P2.
Sprz˛e˙zenie zwrotne jest przydatne przy badaniu własno´sci niezale˙zno´sci, sprawiedliwo´sci i uczciwo´sci. Natomiast je´sli chcemy bada´c relacj˛e bisymulacji dla modeli XCCS, to konieczne jest reetykietowanie grafów przej´s´c.
Podamy teraz definicj˛e ([35, p. 161, Definition 8]) jeszcze jednej charakterystycznej postaci dla skryptów CCS, któr ˛a wykorzystamy w naszych dalszych rozwa˙zaniach.
Definicja 4.3. Mówimy, ˙ze agent P jest form ˛a standardow ˛a (z ang. Standard Form) lub jest w formie standardowej, je´sli zachodzi
P ≡
m
X
i=1
αi.Pi (4.6)
4.1. Wprowadzenie do koncepcji tagów 62
Zwró´cmy uwag˛e, ˙ze agent 0 jest form ˛a standardow ˛a, gdy przyjmiemy, ˙ze m = 0. Rozwa˙zmy kilka przykładów: agenty a.0, a.0+b.(c.0+τ.0) s ˛a w formie standardowej, natomiast agenty 0+b.0, a.(0 + b.0) nie s ˛a w formie standardowej.
Wracaj ˛ac do modelu z rys. 4.3, warto podkre´sli´c, ˙ze zawsze mo˙zliwe jest przekonwertowanie takiego diagramu do postaci Standard Form (SF), która ma LTS izomorficzny do LTS’a z rys. 4.4 oraz identyczne etykietowanie łuków:
S1= a.S2+ a.S3 (4.7a) S2 = b.S1+ a.S4 (4.7b) S3 = b.S1+ a.S4 (4.7c) S4= b.S2+ b.S3 (4.7d)
Graf LTS dla skryptu SF pokazano na rys. 4.6.
S1 S4 S2 S3 a b a b a b a b
Rysunek 4.6: LTS dla skryptu SF
Problem polega jednak na tym, ˙ze skrypty SF maj ˛a liczb˛e stałych agentowych równ ˛a liczbie stanów w grafie przej´s´c dla danego diagramu XCCS. Ka˙zdemu stanowi w grafie przej´s´c odpowiada jedna stała agentowa skryptu SF. Kolejny problem polega na tym, ˙ze w skryptach SF stałe agentowe oraz ich definicje nie odzwierciedlaj ˛a w sposób ´scisły struktury diagramu XCCS. Innymi słowy, je´sli diagram XCCS składa si˛e z bloczków B1, B2, . . . , Bnto chcieliby´smy, aby równowa˙zny do niego skrypt CCS był zło˙zeniem równoległym B1|B2| . . . |Bn zredukowanych algebr CSS przypisanych do bloczków o nazwach odpowiadaj ˛acych nazwom bloczków. Z opisanych wzgl˛edów skrypty SF nie mog ˛a by´c traktowane jako model systemu, ale raczej jako algebraiczna reprezentacja LTS’a dla danego diagramu XCCS.
W rzeczywisto´sci przydatne jest generowanie LTS’a dla diagramu XCCS z pomini˛eciem etapu generowania równowa˙znego skryptu CCS z dwóch powodów. Po pierwsze, nasze do´swiadczenia z narz˛edziem CWB wykazały, ˙ze nie nadaje si˛e ono do zastosowa´n przemysłowych. Po drugie, do analizy LTS’ów chcemy zastosowa´c narz˛edzia takie jak NuSMV, SPIN, LTSA a w szczególno´sci CADP ([20], [21]), które jest narz˛edziem przemysłowym i jest w stanie analizowa´c bardzo du˙ze LTS’y w rozs ˛adnym przedziale czasowym.
4.1. Wprowadzenie do koncepcji tagów 63
Proponowane w rozprawie rozszerzenie algebry CCS o mechanizm tagów pozwala konwertowa´c diagramy XCCS do skryptów XCCS, które w sposób ´scisły odzwierciedlaj ˛a ich struktur˛e. Tym samym nie jest konieczne stosowanie sprz˛e˙zenia zwrotnego i reetykietowania grafów przej´s´c.
Zanim podamy przykłady skryptów XCCS, czyli skryptów CCS rozszerzonych o mechanizm tagów, zdefiniujemy najpierw pewnego rodzaju strukturalne równowa˙zno´sci mi˛edzy diagramami XCCS a odpowiadaj ˛acymi im skryptami algebraicznymi.
Definicja 4.4. Mówimy, ˙ze diagram XCCS zło˙zony z bloczków B1, B2, . . . , Bn, które maj ˛a przy-pisane skrypty CSS jest:
a) ´sci´sle równowa˙zny SCF, je´sli mo˙ze by´c przekonwertowany do skryptu w postaci Standard Con-current Form bez konieczno´sci zamiany nazw akcji;
b) równowa˙zny SCF, je´sli mo˙ze zosta´c przekonwertowany do skryptu w postaci Standard Concur-rent Form,
c) ´sci´sle równowa˙zny SF je´sli mo˙ze zosta´c przekonwertowany do skryptu w postaci Standard Form bez konieczno´sci zamiany nazw akcji,
d) ´sci´sle równowa˙zny SCF z tagami je´sli mo˙ze zosta´c przekonwertowany do skryptu w postaci Standard Concurrent Form z tagami bez konieczno´sci zamiany nazw akcji.
W powy˙zszej definicji u˙zywamy sformułowania „które maj ˛a przypisane skrypty CCS” gdy˙z przyszłe wersje j˛ezyka modelowania XCCS b˛ed ˛a pozwalały na przypisywanie do bloczków oprócz skryptów CSS równie˙z skryptów XCSS. Rozszerzenie to uczyni j˛ezyk modelowania bardziej ela-stycznym i zwi˛ezłym m.in. przez łatw ˛a implementacj˛e synchronizacji dwukierunkowej.
Twierdzenie 4.1. Ka˙zdy diagram, który mo˙zna przekonwertowa´c do skryptu CCS ze sko´nczonym grafem przej´s´c LTS jest ´sci´sle równowa˙zny do SF.
Dowód. LTS dla wynikowego skryptu CCS jest sko´nczony, a zatem mo˙zemy ponumerowa´c wszyst-kie jego stany. Przyjmijmy, ˙ze stan z numerem i odpowiada stałej agentowej Si. Je´sli stan i ma przej´scia z etykietami αj, αk, . . . , αl i prowadz ˛a one do stanów Sj, Sk, . . . , Sl, to definicja stałej agentowej Siprzyjmie posta´c Si = αj.Sj+ αk.Sk+ . . . + αl.Sl. W kolejnych krokach powtarzamy opisany schemat dla wszystkich pozostałych stanów. Łatwo zauwa˙zy´c, ze skrypt SF otrzymany w ten sposób ma LTS izomorficzny do LTS’a dla skryptu CCS i takie same jak on etykietowania łuków. W ostatnim kroku powracamy do oryginalnych nazw akcji przy pomocy sprz˛e˙zenia zwrotnego.
Na obecnym etapie rozwoju j˛ezyka modelowania XCCS wszystkie diagramy maj ˛a równowa˙zne skrypty CCS ze sko´nczony grafami przej´s´c, a zatem s ˛a one ´sci´sle równowa˙zne do SF. W odniesieniu do innych przykładów rozwa˙zanych w tym podrozdziale mamy:
a) Diagram na rys. 4.1 jest ´sci´sle równowa˙zny SCF.
b) Diagram na rys. 4.3 jest równowa˙zny SCF.
4.1. Wprowadzenie do koncepcji tagów 64
Zauwa˙zmy, ˙ze ka˙zdy diagram XCCS ´sci´sle równowa˙zny SCF jest równowa˙zny SCF. Rozwa˙zmy skrypt XCCS, który jest równowa˙zny diagramowi na rys. 4.3:
E20 = B1|B2 (4.8a) B1 = a{}.b.B1 (4.8b) B2 = a{}.b.B2 (4.8c) lub E20 = B1|B2 (4.9a) B1= a{}.b.B1 (4.9b) B2= a{}.b.B2 (4.9c)
Ko-akcja a i akcja a maj ˛a przypisany tag pusty , a zatem nie mog ˛a synchronizowa´c, mimo tego, ˙ze s ˛a to akcje komplementarne o tych samych nazwach. Dla wygody, w definicji skryptu mo˙zemy pomin ˛a´c tag pusty . LTS dla powy˙zszego skryptu XCCS jest dokładnie taki sam jak ten na rys. 4.4.
Rozwa˙zmy inne przykłady, w których wykorzystano tagi.
a a c B B1 B2 A b A = a.b.A B = a.c.B Rysunek 4.7: Przykład nr 3
Skrypt XCCS równowa˙zny do diagramu na rys. 4.7 ma posta´c:
E3 = B1|B2 (4.10a) B1 = a{}.b{1}.B1 (4.10b) B2 = a{}.c{1}.B2 (4.10c)
Ko-akcja a i akcja a nie mog ˛a ze sob ˛a synchronizowa´c, gdy˙z maj ˛a przypisany tag pusty. Akcja b mo˙ze synchronizowa´c z ko-akcj ˛a c gdy˙z s ˛a one komplementarne i maj ˛a przypisany ten sam tag reprezentowany przez liczb˛e 1. Akcja b i ko-akcja c mog ˛a równie˙z wykona´c si˛e pojedynczo, gdy˙z ˙zadna z nich ani tag 1 nie zostały umieszczone w zbiorze restrykcji dla agenta E3. LTS dla skryptu XCCS jest podany na rys. 4.8. Zwró´cmy uwag˛e, ˙ze w LTS’ach mo˙zemy pomin ˛a´c tagi przy etykietach łuków, gdy˙z słu˙z ˛a one jedynie do celów synchronizacyjnych.
Podobny przykład pokazany jest na rys. 4.9. Równowa˙zny skrypt XCCS ma posta´c:
E4= (B1|B2)\{1} (4.11a) B1= a{}.b{1}.B1 (4.11b) B2= a{}.c{1}.B2 (4.11c)
4.1. Wprowadzenie do koncepcji tagów 65 B1|B2 b{1}.B1|c{1}.B2 b{1}.B1|B2 B1|c{1}.B2 b a c a c a b a τ {b, c}
Rysunek 4.8: LTS dla przykładu nr 3
a a c B1 B2 A b A = a.b.A B = a.c.B B Rysunek 4.9: Przykład nr 4
Powy˙zszy skrypt jest podobny do skryptu dla przykłady na rys. 4.7. Jedyna ró˙znica polega na tym, ˙ze tag 1 akcji b i ko-akcji c znajduje si˛e w zbiorze restrykcji i dlatego akcje te nie mog ˛a wykonywa´c si˛e pojedynczono. Jak wida´c, tagi mo˙zna równie˙z umieszcza´c w zbiorze restrykcji. LTS dla powy˙zszego skryptu XCCS jest podany na rys. 4.10.
(B1|B2)\{1} (b{1}.B1|c{1}.B2)\{1} (b{1}.B1|B2)\{1} (B1|c{1}.B2)\{1} a a a a τ {b, c}
Rysunek 4.10: LTS dla przykładu nr 4
Diagram na rys. 4.11 nie jest ani ´sci´sle równowa˙zny ani równowa˙zny SCF. Z definicji algebry procesów XCCS wynika, ˙ze je´sli porty poł ˛aczone s ˛a w taki sposób, ˙ze tworz ˛a drog˛e, to w obr˛ebie tej drogi ka˙zda para portów komplementarnych musi by´c ze sob ˛a poł ˛aczona. Porty poł ˛aczone lini ˛a ci ˛agł ˛a tworz ˛a drog˛e, a zatem poł ˛aczenie okre´slone lini ˛a przerywan ˛a musi równie˙z pojawi´c si˛e na diagramie. To poł ˛aczenie nie wyst˛epuje, a zatem powy˙zszy diagram jest niepoprawny, ale mimo
4.1. Wprowadzenie do koncepcji tagów 66
tego jest on ´sci´sle równowa˙zny SF i do nast˛epuj ˛acego skryptu XCCS:
E = (A|B|C|D)\{1, 2} (4.12a) A = a.b{1}.A (4.12b) B = c.d{1, 2}.B (4.12c) C = e.f {2}.C (4.12d) D = g.h{2}.D (4.12e) A = a.b.A; B = c.d.B; C = e.f.C; D = g.h.D; A B A B C C D D b d h f
Rysunek 4.11: Warunek niesymetrycznej trój-przechodnio´sci
W powy˙zszym skrypcie XCCS ko-akcja b mo˙ze synchronizowa´c z akcj ˛a d, gdy˙z s ˛a one komple-mentarne i maj ˛a przypisany wspólny tag reprezentowany przez liczb˛e 1. Podobnie, ko-akcja h mo˙ze synchronizowa´c z akcjami d i f , gdy˙z s ˛a one do niej komplementarne i wszystkie one maj ˛a przy-pisany wspólny tag reprezentowany przez liczb˛e 2. Ko-akcja b nie mo˙ze synchronizowa´c z akcj ˛a f , gdy˙z nie maj ˛a one przypisanego wspólnego taga.
Ostatni przykład pokazuje, ˙ze na kolejnym etapie rozwoju algebry procesów XCCS mo˙zemy usun ˛a´c z definicji algebry tak wiele warunków, jak to tylko mo˙zliwe i umie´sci´c je w zało˙zeniach twierdze´n, które b˛ed ˛a nam mówiły o ró˙znego rodzaju strukturalnych równowa˙zno´sciach modeli do skryptów CCS i XCCS.
Na rysunku 4.12 podamy jeszcze przykład pełnego diagramu XCCS. Tego typu diagramy, jak ten poni˙zszy przydaj ˛a si˛e przy modelowaniu układów cyfrowych, gdzie nazwy akcji reprezentuj ˛a warto´sci logiczne.
B1 B2
A = a.'a.A;
a a a a
A A