Rachunek z przesyłaniem danych

Przedstawiony w podrozdziale 3.1 j˛ezyk CCS nie pozwala na modelowanie w prosty spo-sób przesyłania danych. Tymczasem w rzeczywistych problemach bardzo cz˛esto istotn ˛a rol˛e odgrywa nie tylko sam fakt komunikacji, ale tak˙ze dane jakie w trakcie tej komunikacji s ˛a prze-syłane. Próba modelowania przesyłanych warto´sci w j˛ezyku CCS powoduje, ˙ze konieczne jest zdefiniowanie oddzielnej akcji dla ka˙zdej z przesyłanych warto´sci i oddzielnej nazwy agenta dla ka˙zdej z przechowywanych przez niego warto´sci.

Rozwa˙zmy przykład jednokomórkowego bufora, w którym mo˙zna przechowywa´c liczby całkowite z zakresu od 1 do 3. Definicja agenta B reprezentuj ˛acego ten bufor mo˙ze mie´c nast˛e-puj ˛ac ˛a posta´c: B = in₁.B₁+ in₂.B₂+ in₃.B₃ B₁ = out₁.B B₂ = out₂.B B3 = out3.B (3.15)

Liczba etykiet i stanów mo˙ze znacz ˛aco wzrosn ˛a´c, je´sli b˛edziemy rozwa˙za´c bardziej licz-ne dziedziny dla parametrów, lub agent b˛edzie mógł przechowywa´c wi˛ecej ni˙z jeden parametr. Jako rozwi ˛azanie tego typu problemów zaproponowany został rachunek CCS z przesyłaniem danych tzw. Value Passing CCS (w skrócie VP CCS, [56, 57]). Powy˙zszy model zapisany w al-gebrze VP CCS mo˙ze mie´c nast˛epuj ˛ac ˛a posta´c:

B = in(x).B(x)

B(x) = out(x).B ^(3.16)

Oczywi´scie zapis takiego modelu w formie przeznaczonej do automatycznego przetwarza-nia wymaga zdefiniowaprzetwarza-nia równie˙z dziedziny parametru x ([22]). W ka˙zdym przypadku musz ˛a to by´c dziedziny sko´nczone ze wzgl˛edu na mo˙zliwo´s´c konwersji do rachunku elementarnego. Dopuszczalne s ˛a m.in. podzbiory zbioru liczb całkowitych, typy wyliczeniowe, typ logiczny, listy warto´sci, krotki itp.

W celu formalnego zdefiniowania składni j˛ezyka VP CCS przyjmijmy zało˙zenie, ˙ze rozpa-trywany jest j˛ezyk z dost˛epnym tylko jednym typem danych V (zob. [26]). Ograniczenie to nie wpływa istotnie na opisywany j˛ezyk, bo mo˙zna przyj ˛a´c, ˙ze V jest sum ˛a wszystkich wymaga-nych typów dawymaga-nych. Przyjmijmy nast˛epuj ˛ace oznaczenia:

• e jest wyra˙zeniem typu V, tzn. wyra˙zeniem, które w wyniku warto´sciowania daje warto´s´c nale˙z ˛ac ˛a do V;

• x jest zmienn ˛a typu V (mog ˛ac ˛a przyjmowa´c warto´sci z V)

• b jest wyra˙zeniem logicznym na elementach typu V, tzn. wyra˙zeniem, które mo˙ze zawie-ra´c zmienne i warto´sci typu V i które w wyniku warto´sciowania daje warto´s´c logiczn ˛a.

Definicja 4. Zbiór wszystkich wyra˙ze´n algebraicznych E+rachunku VP CCS definiowany jest indukcyjnie zgodnie z nast˛epuj ˛acymi regułami konstrukcji:

(1) Je˙zeli X ∈ E to X jest tak˙ze wyra˙zeniem algebraicznym j˛ezyka E⁺,

(2) Je˙zeli e₁, . . . , e_k s ˛a wyra˙zeniami typu V i A ∈ K, to A(e₁, . . . , e_k) jest wyra˙zeniem alge-braicznym j˛ezyka E⁺.

(3) Je˙zeli E jest wyra˙zeniem algebraicznym j˛ezyka E⁺ i f : Act → Act jest funkcj ˛a przeety-kietowuj ˛ac ˛a, to równie˙z E[f ] jest wyra˙zeniem algebraicznym j˛ezyka E+.

(4) Je˙zeli E jest wyra˙zeniem algebraicznym j˛ezyka E⁺, x jest zmienn ˛a typu V, a ∈ L i α ∈ Act, to wyra˙zeniami algebraicznymi j˛ezyka E+s ˛a równie˙z: (E), α.E, a(x).E i a(x).E. (5) Je˙zeli E₁, E₂ s ˛a wyra˙zeniami algebraicznymi j˛ezyka E+, to równie˙z E₁ + E₂ i E₁|E₂ s ˛a

wyra˙zeniami algebraicznymi j˛ezyka E⁺.

(6) Je˙zeli E s ˛a wyra˙zeniem algebraicznym j˛ezyka E⁺ i b jest wyra˙zeniem logicznym na ele-mentach typu V, to równie˙z if b then E jest wyra˙zeniem algebraicznym j˛ezyka E+.

Przyjmujemy ponadto zało˙zenia, ˙ze:

• Ta sama akcja nie mo˙ze by´c jednocze´snie parametryzowana i nieparametryzowana w ra-mach jednego modelu.

• Nie mo˙zna u˙zy´c w modelu bezpo´srednio parametryzowanej akcji τ .

• Ka˙zdy agent A(e₁, . . . , e_k) jest zdefiniowany równaniem postaci A(e₁, . . . , e_k) = E, gdzie E mo˙ze zawiera´c wył ˛acznie zmienne wolne typu V.

J˛ezyk E⁺nie posiada wi˛ekszych mo˙zliwo´sci w zakresie modelowania ni˙z j˛ezyk E . Pozwala on jedynie uzyska´c bardziej zwi˛ezł ˛a, łatwiejsz ˛a do zapisania i zrozumienia z punktu widze-nia człowieka form˛e modelu. Analiza modeli zapisanych w j˛ezyku VP CCS odbywa si˛e po ich (automatycznej) translacji na j˛ezyk elementarny. Zasady translacji przedstawiono we wzo-rze (3.17). Dla ka˙zdego wyra˙zenia E ∈ E⁺ podano odpowiadaj ˛ace mu wyra˙zenie bE ∈ E . Zakłada si˛e, ˙ze w wyra˙zeniu podlegaj ˛acym translacji wszystkie zmienne s ˛a zwi ˛azane.

A(e₁, . . . , e_k) 7−→ A_e1,...,ek (3.17a) a(x).E 7−→ ^X v∈V a_v. \E{v\V} (3.17b) a(e).E 7−→ a_e. bE (3.17c) τ.E 7−→ τ. bE (3.17d) E₁ | E₂ 7−→ cE₁ | cE₂ (3.17e) X i∈I E_i 7−→ ^X i∈I c E_i (3.17f) E\L 7−→ E\{lb _v: l ∈ L, v ∈ V} (3.17g) E[f ] 7−→ E[ bb f ] gdzie bf (l_v) = f (l)_v (3.17h) if b then E else F 7−→ ( b

E je´sli b jest prawd ˛a

b

F w przeciwnym przypadku ^(3.17i)

X 7−→ X (3.17j)

Reguła (3.17a) pokazuje sposób konwersji agenta parametrycznego. Polega ona na zamia-nie jego parametrów na odpowiadaj ˛acy im indeks. Dzi˛eki temu tworzona jest unikalna nazwa. Przykładowo agent parametryczny A(4, alpha, omega) zostanie według tej reguły zamieniony na A4,alpha,omega(zobacz tak˙ze (3.18) i (3.19)).

Reguła (3.17b) przedstawia konwersj˛e prefiksu wej´sciowego. Warto zwróci´c uwag˛e, ˙ze w tym przypadku kluczowe znaczenie ma dziedzina parametru lub parametrów wyst˛epuj ˛acych w wyra˙zeniu. Dzieje si˛e tak dlatego, ˙ze wyra˙zenie po konwersji zast˛epowane jest przez su-m˛e wszystkich mo˙zliwych kombinacji warto´sci prefiksu wej´sciowego. Przykład zastosowania i ró˙znice wynikaj ˛ace ze zdefiniowanego zakresu parametrów obrazuj ˛a przykłady (3.19) i (3.20).

Reguła (3.17c) prezentuje konwersj˛e prefiksu wyj´sciowego. W odró˙znieniu od prefiksu wej-´sciowego gdzie zmienne nie s ˛a zwi ˛azane, w tym przypadku operuje si˛e na konkretnej warto´sci. St ˛ad ta reguła ogranicza si˛e do uzupełnienie etykiety o odpowiedni indeks.

Reguły (3.17d), (3.17e) oraz (3.17f) dotycz ˛a konwersji operacji τ , zło˙zenia agentów i sumy agentów. Ograniczaj ˛a si˛e one do konwersji wyra˙ze´n b˛ed ˛acych ich składowymi.

Reguły (3.17g) i (3.17h) wynikaj ˛a ze sposobu konwersji prefiksu (zobacz (3.17b) i (3.17c)). Pierwsza z nich dotyczy konwersji nazw przy restrykcji. Przy tym operatorze nale˙zy pami˛eta´c o tym, ˙ze translacja prefiksu polega na uzupełnieniu etykiety przez odpowiednie indeksy wyni-kaj ˛ace z obecno´sci parametrów oraz ich zakresu. St ˛ad w trakcie konwersji mo˙ze powsta´c cały zbiór etykiet, dla którego baz ˛a jest prefiks i nale˙zy uwzgl˛edni´c to w operatorze restrykcji. Przy operacji reetykietowania nale˙zy wykona´c zamian˛e cz˛e´sci bazowej etykiety wynikaj ˛acej z nazwy prefiksu, pozostawiaj ˛ac indeks wynikaj ˛acy z parametrów oraz ich zakresu.

Reguła (3.17i) przedstawia konwersj˛e wyra˙zenia warunkowego. Forma tego wyra˙ze-nia ró˙zni si˛e od tej zawartej w definicji 4 i jest jedynie skrótowym zapisem wyra˙zewyra˙ze-nia if b then E if ¬b then F . Jej przyj˛ecie skraca zapis i poprawia czytelno´s´c kodu.

Ostatnia reguła (3.17j) pokazuje, ˙ze wyra˙zenia nale˙z ˛ace do j˛ezyka podstawowego E nie podlegaj ˛a konwersji.

Rozwa˙zmy nast˛epuj ˛acy przykład. Dany jest agent A procesuj ˛acy dane w sposób okre´slony przez równanie (3.18) i mog ˛acy operowa´c na warto´sciach z przedziału {0..2}.

A = in(x).A(x)

A(x) = if x = 2 then 0 else out(x).A ^(3.18)

Po zastosowaniu metod translacji agent A przyjmie nast˛epuj ˛ac ˛a posta´c: A = in₀.A₀+ in₁.A₁+ in₂.A₂

A₀ = out₀.A A1 = out1.A A₂ = 0

(3.19)

Je´sli agent A z równania (3.18) miałby operowa´c na danych z zakresu {0..3} to odpowia-daj ˛acy mu zapis dla j˛ezyka CCS b˛edzie wygl ˛adał nast˛epuj ˛aco:

A = in₀.A₀+ in₁.A₁+ in₂.A₂+ in₃.A₃ A₀ = out₀.A A₁ = out₁.A A₂ = 0 A₃ = out₃.A (3.20)

Konwersja wygl ˛ada analogicznie je´sli dziedzina parametru jest np. napisem. Niech równa-nie (3.18) przyjmie nast˛epuj ˛ac ˛a posta´c:

A = in(x).A(x)

A(x) = if x = ”metal” then 0 else out(x).A ^(3.21)

Dziedzin ˛a parametru x niech b˛edzie zbiór {metal, papier}. Wynik translacji do j˛ezyka CCS pokazuje równanie (3.22).

A = in_metal.A_metal+ in_papier.A_papier A_metal = 0

Apapier = outpapier.A

Narz˛edziem, które w praktyce wykorzystuje zasady konwersji z j˛ezyka VP-CCS do CCS podane we wzorze (3.17) jest jvp ([22]). Pozwala ono zapisa´c model z wykorzystaniem składni j˛ezyka VP-CCS i automatycznie przekonwertowa´c go do czystego j˛ezyka CCS. Przykład (3.18) zapisany w formacie zrozumiałym dla jvp przedstawiono na listingu 3.2.

const I = range(0,2)

label in(I), out(I)

agent A = in(x).A(x)

agent A(x:I) = if x=2 then 0 else ’out(x).A

Listing 3.2. Przykład z równania 3.18 zapisany w formacie jvp

Pierwsza linia zawiera definicj˛e typu I, który jest zbiorem liczb naturalnych z zakresu od 0 do 2. Linia 2 zawiera deklaracje etykiet wraz z typami parametrów jakie b˛ed ˛a przesyła´c. Linie 3 i 4 to definicje agenta A.

agent A = in%0%.A%0% + in%1%.A%1% + in%2%.A%2%;

agent A%0% = ’out%0%.A;

agent A%1% = ’out%1%.A;

agent A%2% = 0;

Listing 3.3. Wynik konwersji przykładu z listingu 3.2 do formatu CWB

Rezultat konwersji za pomoc ˛a programu jvp przedstawiono na listingu 3.3. Jest to skrypt zgodny z formatem wej´sciowym CWB. Podstawowa ró˙znica mi˛edzy wersj ˛a teoretyczn ˛a (3.17) a t ˛a implementacj ˛a, to zast ˛apienie indeksów wyra˙zeniami zawartymi mi˛edzy znakami %.