4. Modelowanie z u˙zyciem tagów
4.4. Konwersja diagramów XCCS do algebr XCCS
Jako ostatni przykład rozpatrzymy model wzajemnego wykluczania dla procesów P1i P2 przy pomocy semafora Sem.
P1 beg P get Sem Sem Sem = 'get.put.Sem; end P P2 beg put end P = beg.cs.'end.P;
Rysunek 4.15: Wzajemne wykluczanie P1i P2
Nazwy akcji wyst˛epuj ˛acych w algebrach CSS przypisanych do bloczków oznaczaj ˛a:
’beg – pocz ˛atek sekcji krytycznej;
sc – sekcja krytyczna;
end – koniec sekcji krytycznej;
’get – uzyskanie pozwolenia na wej´scie do sekcji krytycznej;
put – oddanie pozwolenia na wej´scie do sekcji krytycznej.
Zwró´cmy uwag˛e, ˙ze akcja sc nie jest etykiet ˛a ˙zadnego portu, a zatem jest to akcja wewn˛etrzna, która nie mo˙ze bra´c udziału w synchronizacji. Równowa˙zny skrypt XCCS ma posta´c:
Mx = (P1|P2|Sem)\{1, 2} (4.38a) P1= beg{1}.cs.end{2}.P1 (4.38b) P2= beg{1}.cs.end{2}.P2 (4.38c) Sem = get{1}.put{2}.Sem (4.38d)
Dla porównania podamy równowa˙zny skrypt CCS, który mo˙ze mie´c posta´c:
Mx = (P1|P2|Sem)\{get, put} (4.39a) P1 = get.cs.put.P1 (4.39b) P2 = get.cs.put.P2 (4.39c) Sem = get.put.Sem (4.39d)
W zaprezentowanych przykładach bardzo wyra´znie wida´c korzy´sci z zastosowania tagów.
4.4. Konwersja diagramów XCCS do algebr XCCS
Konwersja diagramów XCCS do skryptów XCCS zamiast do skryptów CCS pozwala na znaczne uproszczenie algorytmu konwersji. Je´sli zastosujemy mocn ˛a semantyk˛e operacyjn ˛a dla algebr
4.4. Konwersja diagramów XCCS do algebr XCCS 73
XCCS, to automatycznie wyeliminujemy problemy z konfliktami i przesłoni˛eciami opisane w po-przednim rozdziale.
Przyjmiemy nast˛epuj ˛ace oznaczenia i definicje pomocnicze:
– Agents jest zbiorem wszystkich stałych agentowych nale˙z ˛acych do algebr ze zbioru CSS
Agents = [
CSSi∈CSS
K(CSSi), (4.40)
– T jest niesko´nczonym zbiorem tagów
– C jest niesko´nczonym zbiorem stałych agentowych, gdzie C ∩ Agents = ∅.
W algorytmie konwersji b˛edziemy rozpatrywa´c pewien podzbiór T0 ⊂ T zbioru tagów T oraz pewien podzbiór C0 ⊂ C zbioru stałych agentowych C. W opisie algorytmu pomijamy szczegóły implementacyjne generowania zbioru stałych agentowych C0i zbioru tagów T0. Najpro´sciej przyj ˛a´c, ˙ze tagami b˛ed ˛a kolejne liczby naturalne. Przyjmiemy nast˛epuj ˛ace oznaczenia:
– Uporz ˛adkowana para (Bi, CSSi) reprezentuje bloczek Bi ∈ B, do którego przypisana jest algebra CSSi = ρ(Bi) ∈ CSS .
– Symbol Bi∗oznacza nazw˛e bloczka Bi a symbol CSS∗i oznacza nazw˛e algebry CSSi.
Algorytm konwersji diagramów XCCS do algebr XCCS ma posta´c:
1. Nazwy algebr przypisanych do bloczków przyjmuj ˛a nazwy bloczków. Tworzymy nowy zbiór CSS0zredukowanych algebr procesów, czyli zbiór ci ˛agów równa´n agentowych. Dla ka˙zdego bloczka Bi ∈ B:
a) Je´sli dla pary (Bi, CSSi) nazwa bloczka jest taka sama, jak nazwa algebry, czyli Bi∗ = CSS∗i, to do zbioru CSS0 dodajemy algebr˛e CSSi.
b) Je´sli dla pary (Bi, CSSi) nazwa bloczka jest inna ni˙z nazwa algebry, czyli Bi∗ 6= CSS∗i, oraz stała agentowa Bi∗ ∈ K(CSS/ i), to nazw˛e algebry CSSi i wszystkie stałe agentowe CSS∗i, które w niej wyst˛epuj ˛a, zamieniamy na Bi∗i do zbioru CSS0dodajemy algebr˛e B∗i.
c) Je´sli dla pary (Bi, CSSi) nazwa bloczka jest inna ni˙z nazwa algebry, czyli Bi∗ 6= CSS∗i, ale stała agentowa B∗i ∈ K(CSSi), to wszystkie stałe agentowe Bi∗, które wyst˛epuj ˛a w algebrze CSSi zamieniamy na kolejn ˛a stał ˛a ze zbioru C, a nast˛epnie nazw˛e algebry CSSi
i wszystkie stałe agentowe CSS∗i, które w niej wyst˛epuj ˛a, zamieniamy na Bi∗ i do zbioru CSS0dodajemy algebr˛e Bi∗.
2. Eliminujemy ewentualne konflikty mi˛edzy nazwami stałych agentowych. Tworzymy nowy zbiór XCSS00zredukowanych algebr procesów, czyli zbiór ci ˛agów równa´n agentowych. Dla ka˙zdej algebry CSSi ∈ CSS0:
4.4. Konwersja diagramów XCCS do algebr XCCS 74
a) Dla ka˙zdej stałej agentowej A ∈ K(CSSi) takiej, ˙ze nazwa stałej A jest inna ni˙z nazwa algebry, czyli A 6= CSS∗i: je´sli istnieje inna algebra CSSj ∈ CSS0, taka ˙ze A ∈ K(CSSj), to wszystkie stałe agentowe A w algebrze CSSizamieniamy na kolejn ˛a stał ˛a ze zbioru C. b) Do zbioru XCSS00dodajemy algebr˛e CSSi.
3. Je´sli diagram XCCS jest płaski, to dla ka˙zdego Bi.a ∈ OutP wszystkie akcje a ∈ A(Bi∗) w algebrze Bi∗zamieniamy na ko-akcje a.
4. Dokonujemy podziału zbioru portów P na klasy abstrakcji relacji SR. Do klas abstrakcji relacji SR przypisujemy kolejne tagi ze zbioru T lub tag pusty {} w nast˛epuj ˛acy sposób:
a) Do wieloelementowych klas abstrakcji relacji SR przypisujemy kolejne tagi ze zbioru T . b) Do jednoelementowych klas abstrakcji relacji SR, które zawieraj ˛a niewidoczne porty,
przypisujemy kolejne tagi ze zbioru T .
c) Do jednoelementowych klas abstrakcji relacji SR, które zawieraj ˛a widoczne porty, przy-pisujemy tag pusty {}.
5. Przypisujemy tagi do akcji oraz ko-akcji w algebrach ze zbioru XCSS . Dla ka˙zdego portu Bi.a ∈ InP i dla ka˙zdego portu Bi.a ∈ OutP wykonujemy:
a) je´sli do klasy abstrakcji [Bi.a]SR przypisany jest tag t ∈ T , to w algebrze Bi∗ wszystkie akcje a zamieniamy na a{t};
b) je´sli do klasy abstrakcji [Bi.a]SR przypisany jest tag t ∈ T , to w algebrze Bi∗ wszystkie ko-akcje a zamieniamy na a{t}.
6. Tworzymy skrypt XCCS w nast˛epuj ˛acy sposób. Główne wyra˙zenie agentowe ma posta´c:
S = (B1|B2| . . . |Bn)\{Tags} (4.41)
gdzie B1, B2, . . . , Bn∈ XCSS00, a w zbiorze Tags znajduj ˛a si˛e wszystkie tagi przypisane do klas abstrakcji relacji SR zawieraj ˛acych porty niewidoczne. Po głównym wyra˙zeniu agento-wym umieszczamy definicje wszystkich algebr ze zbioru XCSS00.
Przykłady konwersji
Poni˙zej podajemy w jaki sposób przebiega wykonanie ka˙zdego z podpunktów algorytmu kon-wersji dla modelu bramki NAND z rys. 4.16.
Definicje algebr CSS przypisanych do bloczków tego diagramu maj ˛a posta´c:
And = a0.(b0.’c0.And + b1.’c0.And) + a1.(b0.’c0.And + b1.’c1.And); Neg = a0.’b1.Neg + a1.’b0.Neg;
Ad. 1.
4.4. Konwersja diagramów XCCS do algebr XCCS 75 And a1 a0 c1 b0 b1 And c0 Neg b1 a0 Neg a1 b0
Rysunek 4.16: XCCS model bramki NAND
– And = a0.(b0.c0.And + b1.c0.And) + a1.(b0.c0.And + b1.c1.And)
– N eg = a0.b1.N eg + a1.b0.N eg
Ad. 2.
W zbiorze CSS0nie ma konfliktów mi˛edzy nazwami stałych agentowych, a zatem XCSS00= CSS0.
Ad. 3.
Ten punkt pomijamy, gdy˙z nie jest to diagram płaski.
Ad. 4.
Wyznaczamy klasy abstrakcji relacji SR. Do wieloelementowych klas abstrakcji przypisujemy ko-lejno tagi {1} i {2}. Do jednoelementowych klas abstrakcji przypisujemy tag pusty {}.
– [And.a0]SR= {And.a0} 7→ {}
– [And.a1]SR= {And.a1} 7→ {}
– [And.b0]SR = {And.b0} 7→ {}
– [And.b1]SR = {And.b1} 7→ {}
– [And.c0]SR = {And.c0, N eg.a0} 7→ {1}
– [And.c1]SR = {And.c1, N eg.a1} 7→ {2}
– [N eg.b0]SR= {N eg.b0} 7→ {}
– [N eg.b1]SR= {N eg.b1} 7→ {}
Ad. 5.
Po przypisaniu tagów do akcji i ko-akcji zbiór XCSS00ma posta´c:
– And = a0{}.(b0{}.c0{1}.And + b1{}.c0{1}.And)
And+ a1{}.(b0{}.c0{1}.And + b1{}.c1{2}.And)
4.4. Konwersja diagramów XCCS do algebr XCCS 76
Ad. 6.
Okre´slamy skrypt XCCS:
NAND = (And|N eg)\{1, 2}
And = a0{}.(b0{}.c0{1}.And + b1{}.c0{1}.And)
And+ a1{}.(b0{}.c0{1}.And + b1{}.c1{2}.And)
N eg = a0{1}.b1{}.N eg + a1{2}.b0{}.N eg
Rozpatrzmy teraz poznany ju˙z przez nas XCCS model problemu trzech jedz ˛acych filozofów. Tym razem diagram z rys. 4.17 nie zawiera etykiet na łukach, a mimo to uda si˛e nam wygenerowa´c czytelny skrypt XCCS. Ph1 Ph Ph3 Ph2 pr Ph gl Ph F1 Ph = gl.gr.Next + gr.gl.Next; Next = eat.(pl.pr.Ph + pr.pl.Ph); F = get.U; U = put.F; gr pl get put get put pr gr gl pl F3 gr gl pl F F F2 F get put pr
Rysunek 4.17: XCCS diagram trzech filozofów z mo˙zliwo´sci ˛a blokady
Ad. 1.
Dla ka˙zdego bloczka Bi∈ B wykonywany jest podpunkt b. Zbiór CSS0ma posta´c:
– P h1 = gl.gr.N ext + gr.gl.N ext, N ext = eat.(pl.pr.P h1+ pr.pl.P h1)
– F1 = get.U, U = put.F1
– P h2 = gl.gr.N ext + gr.gl.N ext, N ext = eat.(pl.pr.P h2+ pr.pl.P h2)
– F2 = get.U, U = put.F2
– P h3 = gl.gr.N ext + gr.gl.N ext, N ext = eat.(pl.pr.P h3+ pr.pl.P h3)
4.4. Konwersja diagramów XCCS do algebr XCCS 77
Ad. 2.
Przyjmijmy, ˙ze w zbiorze C0stałych agentowych znajduj ˛a si˛e stałe:
C0 = {N ext1, N ext2, N ext3, N ext4, N ext5, U1, U2, U3, U4, U5} ⊂ C
Po zmianie nazw stałych agentowych zbiór XCSS00ma posta´c:
– P h1 = gl.gr.N ext1+ gr.gl.N ext1, N ext1= eat.(pl.pr.P h1+ pr.pl.P h1)
– F1 = get.U1, U1 = put.F1
– P h2 = gl.gr.N ext2+ gr.gl.N ext2, N ext2= eat.(pl.pr.P h2+ pr.pl.P h2)
– F2 = get.U2, U2 = put.F2
– P h3 = gl.gr.N ext3+ gr.gl.N ext3, N ext3= eat.(pl.pr.P h3+ pr.pl.P h3)
– F3 = get.U3, U3 = put.F3
Ad. 3.
Mamy OutP = {P h1.pl, P h1.pr, F1.get, P h2.pl, P h2.pr, F2.get, P h3.pl, P h3.pr, F3.get} i otrzymujemy:
– P h1 = gl.gr.N ext1+ gr.gl.N ext1, N ext1= eat.(pl.pr.P h1+ pr.pl.P h1)
– F1 = get.U1, U1 = put.F1
– P h2 = gl.gr.N ext2+ gr.gl.N ext2, N ext2= eat.(pl.pr.P h2+ pr.pl.P h2)
– F2 = get.U2, U2 = put.F2
– P h3 = gl.gr.N ext3+ gr.gl.N ext3, N ext3= eat.(pl.pr.P h3+ pr.pl.P h3)
– F3 = get.U3, U3 = put.F3
Ad. 4.
Wyznaczamy klasy abstrakcji relacji SR i mapujemy do nich kolejne tagi w postaci liczb natural-nych. Dla ka˙zdej klasy abstrakcji relacji SR wykonywany jest podpunkt a.
– [P h1.pl]SR = {F1.put, P h2.pr, P h1.pl} 7→ {1} – [P h1.gl]SR= {F1.get, P h2.gr, P h1.gl} 7→ {2} – [P h1.pr]SR= {F3.put, P h3.pl, P h1.pr} 7→ {3} – [P h1.gr]SR= {F3.get, P h1.gr, P h3.gl} 7→ {4} – [P h2.pl]SR = {F2.put, P h3.pr, P h2.pl} 7→ {5} – [P h2.gl]SR= {F2.get, P h3.gr, P h2.gl} 7→ {6}