Narzędzie Edinburgh Concurrency Workbench pozwala na modelowanie, analizę i testowanie procesów współbieżnych.
Wszystkie komendy kończą się średnikiem (;) i nową linią. Mogą zajmować więcej niż jedną linię.
Gwiazdka (*) rozpoczyna komentarz. Napisy za średnikiem lub gwiazdką są ignorowane. Gwiazdki oraz średnika nie można stosować nigdzie indziej (np. w komendzie echo). Kombinacja ctrl-c powraca do trybu wpisywania komend.
Nazwy czynności i parametrów formalnych dla czynności rozpoczynamy małą literą (a-z).
Identyfikatory zbiorów, funkcji przemianowujących, procesów i parametrów formalnych dla tych rzeczy rozpoczynamy wielką literą (A-Z)
Pozostałe znaki w nazwie identyfikatora ze zbioru: a-z, A-Z, 0-9, ?!_`'-, oraz #^, jednak ostatnie dwa w innym modelu (SCCS) mają specjalne znaczenie, i nie można ich w nim używać. Na końcu identyfikatora można wstawić dowolne znaki pomiędzy dwoma znakami (%).
Raczej nie jest zalecane używanie innych znaków niż liter, cyfr i znaku podkreślenia, z powodu ewentualnych przyszłych rozszerzeń.
Z oczywistych powodów nie można używać 'tau' i 'eps' ( a także T i F) jako nazw identyfikatorów.
| ACT Czynności | tau | czynność niejawna |
| n | nazwa czynności (z małej litery) | |
| 'n | konazwa czynności - zamiast daszkowania apostrof | |
| eps | obserwacja pusta - niedozwolona w procesach | |
| AGENT Procesy | 0 | blokada(nil) |
| a.A | czynność - prefiks | |
| A + A | suma (wybór) | |
| A | A | złożenie równoległe | |
| A \ a | zakaz czynności | |
| A \ S | zakaz wielu czynności | |
| A[R] | przemianowanie | |
| (A) | nawiasy jak zwykle | |
| X | zmienne procesów z wielkiej litery | |
| X(P,...) | proces z parametrem | |
| RELABEL | [a/a,...] | funkcja przemianowująca dana jako zbiór par |
| V | zmienne przemianowujące zaczynają się wielką literą | |
Priorytety operacji:
Procesy można parametryzować innymi procesami (ale już bezparametrowymi), czynnościami i zbiorami czynności w celu zwiększenia elastyczności języka.
Parametry formalne użyte w definicji procesu mają jeden z trzech typów:
agentParamType := act | set | agent
z tym, że:
CWB próbuje dojść typów parametrów z ich definicji; jednak czasem jest to niemożliwe - wtedy poprosi o uściślenie, lub (w trybie wsadowym) zasygnalizuje błędem.
Można jawnie podać typ:
agent A(X : set) = a.0\X;ale tylko po lewej stronie definicji procesu.
Środowiskiem nazywamy (częściowe) przyporządkowanie identyfikatorom obiektów, co pozwala globalnie odwoływać się do obiektów, poprzez identyfikator do nich przypisany. Istnieje kilka oddzielnych środowisk. Będziemy omawiać środowiska dla procesów oraz zestawów czynności (inne pominiemy).
Jak już zauważyliśmy, możemy związać identyfikator z procesem przy pomocy polecenia agent, np.
agent Cell = a.'b.Cell;
Związanie jest dynamiczne, co znaczy, że zmiana definicji jednego procesu może mieć zasadniczy wpływ na działanie innego. Jeśli na przykład:
agent B = b.0; agent A = a.B; agent B = c.0;
to A będzie mógł wykonać tranzycję –a–>–c–>.
Dynamiczne powiązanie procesów z ich identyfikatorami jest przydatne w interaktywnej modyfikacji związań.
Możemy wiązać zbiory czynności z identyfikatorami przy pomocy komendy set. W zbiorach czynności nie wolno używać tau oraz eps (z oczywistych powodów). Czynności wpisane w zbiór muszą się mieścić w całości w jednej linii, oddzielone przecinkami lub spacją.
Użycie:
| help; | pomoc |
| help commands; | listuje dostępne komendy z opisem |
| help <komenda>; | sposób użycia komendy |
| ccs; | pokazuje składnię CCS |
| ccs act; | pokazuje składnię czynności |
| ccs agent; | pokazuje składnię procesów |
| ccs relabel; | pokazuje składnię funkcji przemianowujących |
Użycie:
quit;
exit;
bye;
agent: zmiana lub wypisanie definicji procesu.
Użycie:agent X = A; związanie procesu A z identyfikatorem X
agent X(FP) = A; związanie sparametryzowanego procesu A
agent X; wypisuje definicję procesu.Jeśli P jest parametrem formalnym, to nie wolno używać P(...) po prawej stronie definicji.
Jeśli nazwa parametru formalnego zaczyna się małą literą, oznacza czynność. Jeśli nazwa parametru formalnego zaczyna się wielką literą, oznacza proces lub zbiór czynności, w zależności od kontekstu.Synonimy: bi, pi
set: zmiana lub wypisanie definicji zbioru czynności.
Użycie:set S = a,b,...; związanie S ze zbiorem czynności.
set S; wypisuje zbiór czynności.Identyfikator musi zaczynać się wielką literą. Nazwane zbiory czynności nie mogą (aktualnie) zawierać eps ani tau.
Synonimy: basi, pasi
relabel: zmiana lub wypisanie definicji funkcji przemianowującej.
Użycie:print: wypisuje wszystkie definicje i powiązania.relabel R = [a/p,...]; związanie R z funkcją przemianowującą.
relabel R; wypisuje funkcję przemianowującą związaną z R.
Użycie: print;clear: usuwa wszystkie powiązania i definicje obiektów.
Użycie: clear;
input: wykonanie komend CWB z pliku.
Użycie:input "plik"; (cudzysłów konieczny)
Plik może zawierać tylko nieinterakcyjne komendy. Może zawierać inne komendy input. Jeśli nastąpi błąd, wykonywanie pliku jest przerywane.
Nazwa pliku nie może zawierać składowych takich jak ".."
output: ustalenie wyjścia standardowego.
Użycie:output "plik"; będzie wypisywać rezultaty do pliku
output; będzie wypisywać rezultaty na stdout.
save: ustalenie wyjścia standardowego.
Użycie:save "plik"; działa jak:
output "plik"; print; output;Zobacz też: input
prefixform:wyświetla proces w prefiksowej formie.
Użycie:prefixform A; tworzy proces silnie równoważny do A będący sumą prefiksów, np. a.A + b.B + c.C;
Synonimy: pf
Zobacz też: sim, transitions,
transitions: listuje jednokrokowe tranzycje procesu.
Użycie:transitions A;
Synonimy: tr
Zobacz też: sim, derivatives, closure, obs, vs, random, init
graph: wypisuje graf tranzycji
Użycie:graph A;
Uwaga. procedura obliczania grafu nie jest efektywna, stosować ją należy tylko w przypadku prostych i skończonych procesów.
size: wylicza liczbę stanów w skończenie stanowym procesie
Użycie:size A;
Uwaga. Obliczenie ilości stanów procesu nie jest tak łatwe, jak się wydaje. Wynik tej operacji należy traktować z grubsza.
closure:
Użycie:closure(a,A); lista procesów osiągalnych z A przez czynność a.
closure(a,b,...,A); to samo, ale dla a,b,...
Pierwszy przypadek listuje wszystkie takie B, że A =a=> B, gdzie a może być czynnością obserwowalną, tau lub eps.
Drugi przypadek: a,b,... może być czynnością obserwowalną, tau lub eps, przy czym tau i eps zostaną zignorowane. Jeśli l-ciąg czynności, wypisze wszystkie B takie, że A =^l=> B.
Synonimy: cl, actctl
Zobacz też: sim, transitions, derivatives, obs, vs, random, init
deadlocks: znajduje zakleszczenia lub zapętlenia oraz ciągi czynności do nich prowadzące
Użycie:deadlocks A;
Osiągnięty stan zwany jest zakleszczeniem, gdy nie jest możliwa żadna obserwowalna czynność.
Komenda ta wypisuje po jednym scenariuszu prowadzącym do zakleszczenia dla każdego takiego stanu.Zobacz też: findinit, findinitobs, deadlocksobs
deadlocksobs: znajduje zakleszczenia lub zapętlenia oraz ciągi czynności do nich prowadzące.
Użycie:deadlocksobs A;
Komenda ta wypisuje po jednej sekwencji obserwowalnych czynności prowadzącej do zakleszczenia dla każdego takiego stanu.Zobacz też: findinit, findinitobs, deadlocks
derivatives: znajduje potomków procesu poprzez daną czynność.
Użycie:derivatives(a,A);
Zobacz też: sim, transitions, closure, obs, vs, random, init
findinit: znajduje stany z podanym zbiorem możliwych czynności.
Użycie:findinit(a,b,...,A);
Wypisuje wszystkie takie stany D, że A--->D, D=a=> D=b=> i nie D=c=> dla dow. obserwowalnego c (słabe tranzycje!)
Dla każdego takiego stanu wypisuje ścieżkę do niego prowadzącąZobacz też: findinitobs, deadlocks
findinitobs: znajduje stany z podanym zbiorem możliwych czynności.
Użycie:findinitobs(a,b,...,A);
To samo co findinit, lecz pomijamy wszystkie tau.
freevars: wypisuje zmienne wolne procesu
Użycie:freevars A;
Użyteczne, aby sprawdzić, czy rekurencyjne definicje są poprawnie zdefiniowane.
Synonimy: fv, freevariables
init: znajduje obserwowalne czynności procesu możliwe do wykonania natychmiast.
Użycie:init A;
Zobacz też: sim, transitions, derivatives, closure, obs, vs, random
obs: znajduje obserwacje długości n i ich wyniki
Użycie:obs(n,A);
wyświetla wszystkie obserwacje długości n wraz ze stanami kończącymi. Jeśli istnieje wiele stanów możliwych do osiagnięcia przez tę samą obserwację, wszystkie zostaną wypisane.
Użycie:
deadlocksobs A;
Zobacz też: sim, transitions, derivatives, closure, vs, random, init
random:
Użycie:random (n,A); wypisuje pseudo-losową obserwację długości <=n
Zobacz też: sim, transitions, derivatives, closure, obs, vs, init
sort: znajduje syntaktyczne uporządkowanie procesu.
Użycie:sort A;
Zobacz też: freevars
stable: sprawdza, czy proces jest stabilny.
Użycie:stable A;
states: wypisuje przestrzeń stanów procesu skończenie stanowego.
Użycie:states A;
statesexp: wypisuje przestrzeń stanów oraz ścieżkę prowadzącą do każdego stanu.
Użycie:statesexp A;
Uwaga. Tylko dla skończenie stanowych procesów.
statesobs: wypisuje przestrzeń stanów oraz obserwację prowadzącą do każdego stanu.
Użycie:statesexp A;
Uwaga. Tylko dla skończenie stanowych procesów.
vs: znajduje obserwacje o danej długości.
Użycie:vs (n,A);
wyświetla wszystkie obserwacje długości n z A. To jest to samo co obs(n,A), ale nie dbamy o stan końcowy.
Zobacz też: sim, transitions, derivatives, closure, obs, random, init
min: minimalizuje proces względem słabej bisymulacji
Użycie:min (X,A); minimalizuje A, rezultat przypisuje na X
Gdy użyjemy zmiennej X, CWB użyje identyfikatorów w stylu XminStateNNN aby określić stany zminimalizowanego procesu.
Wszelkie istniejące związania zostają zachowane.Zobacz też: eq
cong: czy A i B są obserwacyjnie kongruentne (równe)?
Użycie:cong(A,B);
Zwraca true jeśli są równe, false w p. p.
eq: czy A i B są słabo równoważne?
Użycie:eq(A,B);
Zwraca true jeśli są w relacji słabej bisymulacji, false w p. p.
strongeq: czy A i B są w relacji silnej bisymulacji?
Użycie:strongeq(A,B);
Zwraca true jeśli są w relacji silnej bisymulacji, false w p. p.
pb: wypisuje największą słabą bisymulację nad przestrzenią stanów dwóch procesów
Użycie:pb(A,B);
Zobacz też: eq
dftrace: wypisuje ciąg obserwowalnych czynności możliwych do wykonania przez jeden proces, a niemożliwych przez drugi.
Użycie:dftrace(A,B);
Użycie:sim A;
(Na Solaris 2.x ciekawiej będzie użyć prototypowego symulatora graficznego.)
Komendy symulatora:
sim B; porzuca bieżącą symulację (usuwa breakpointy i rozpoczyna symulację B) menu; listuje możliwe tranzycje (jednokrokowe) z bieżącego stanu. n; wybiera tranzycję n z menu i podąża nią random n; symuluje nie więcej niż n kroków wybierając losowo tranzycje. ; = random 1; history; wyświetla stany i tranzycje, poprzez które został osiągnięty bieżący stan return n; wznawia symulację od kroku n bieżącej symulacji (np.return 0; od początku)break a,b,...; ustawia breakpointy na czynności a,b,... lb; wypisuje wszystkie breakpointy db a,b,...; usuwa a,b,... z listy breakpointów bind A; powoduje związanie stanu bieżącego z identyfikatorem A help; pomoc quit; zatrzymuje symulację i wraca do głównej linii komend CWB