dodatki do zar08

ZADANIE 76 (spin/promela) (1pkt)
W algorytmie wzajemnego wykluczania Petersena wykryj błąd, który
pojawia się po przestawieniu 2 pierwszych linii "sekcji we" ...
Do sprawozdania wstaw program .pml, jak i wydruki z okna ispin.
Opis alg Petersena, patrz slajdy, str 5.

CSP = Communicating Sequential Processes

!!! NIEDOKOŃCZONE !!!

literatura i materiały...
https://cocotec.io/fdr/manual/cspm.html opis j. CSP w wersji "maszynowej" (CSPm)
https://www.cs.ox.ac.uk/bill.roscoe/
Roscoe "The Theory and Practice of Concurrency" - to jest główna książka (google "csp book pdf roscoe")
Hoare "Communicating Sequential Processes" - to jest stara książka

narzędzia...
https://prob.hhu.de/w/index.php?title=Documentation ProB
https://github.com/alex-ren/FDR_workspace fdr2 ("akademicka" wersja fdr)
https://cocotec.io/fdr/manual/ fdr4

inne potrzebne materiały/programy są w folderze
obsługa ProB: rozpakować zip; . ./e; . ./r

podstawowe pojęcia... (chaos)

proces: modelowany jako automat, niekoniecznie oznacza węzeł/wierz
proces to "zbiór stanów" oraz "zdarzenia" na strzałkach wychodzących ze stanu (graf skier)
P1 = a -> b -> P1
to^ jest opis procesu emitującego zdarzenia a,b,a,b,a,b,...
"trace" czyli egzekucja (skończona), ciąg zdarzeń emitowanych przez proces
P1 = a -> P1 [] b -> P1
to^ jest opis procesu emitującego zdarzenia a,a,a,...,b,b,...
"[]" to "external choice", czyli wybór (2 strz wych ze stanu, z etykietami "a" i "b")

zdarzenia: opisują co się dzieje w procesie oraz komunikację między procesami
zdarzenie może oznaczać wysłanie lub odebranie komunikatu
zdarzenia deklarujemy jako "channel a,b,c"
są też zdarzenia złożone, np. "channel a,b:{0..2}"
przy zdarzeniach złożonych używa się notacji "a!x" (wysyłanie), "b?y" (czytanie)
stan procesu ma etykietę, która może być złożona (nie tylko P1, np. P1(k), np. P1(<głowa>^ogon))
zdarzenia mogą pochodzić z danych w etykiecie stanu

współbieżne procesy:
P1 ||| P2 - to tzw "interleaving", niezależne współbieżne procesy
komunikacja procesów:
P1 [|{a,b}|] P2 - procesy komunikujące się za pomocą zdarzeń "a" i "b"
gdy P1 emituje zd "a" zostaje zablokowany, aż P2 także wyemituje "a"
współbieżne procesy to też proces!

zadawanie pytań do modelu, asercje:
specyfikacja [?= implementaja
P1 [T= P2 <=> każdy trace P2 jest trace-em P1
P1 [F= P2 <=> ta def jest bardziej skomplikowana...
P1 [FD= P2 <=> ta def jest jeszcze bardziej skomplikowana...

zdarzenia złożone:
channel we, wy: {1,2,3}
Q = P1 [|{|we|}|] BUF(<>) [|{|wy|}|] P2
konstrukcja {|we|} oznacza {we.1, we.2. we3}
użycie "zmiennych" w zd złożonych:
BUF(<>) = we?x -> BUF(<x>)
to^ jest równoważne z:
BUF(<>) = we.1 -> BUF(<1>) [] we.2 -> BUF(<2>) [] we.3 -> BUF(<3>)

inne operacje na procesach:
ukrywanie zdarzeń: P1 \ {c,d}
wymiana zdarzeń: P1 [[a<-x,b<-y]]
c.d.n. (patrz też opis CSPm)

algebra procesów:
opisy procesów można przekształcać jak wzory algebraiczne!
jednak zazwyczaj ograniczamy się do użycia narzędzi typu FDR czy ProB...

przykład 1 CSPm - prosty przykład komunikacji procesów
channel a,b,c
-- ^ zdarzenia trzeba deklarować
P1 = a -> b -> c -> P1
P2 = a -> b -> P2
-- ^ def 2 procesów
P3 = P1 [|{b}|] P2
-- ^ P3 to współbieżne połączenie P1 i P2, które komunikują się przez zd "b"
assert P1 [T= P2
assert P2 [T= P1
-- ^ zadajemy pytania do modelu

przykład 2 CSPm - sprawdzamy czy impl zgadza się ze spec
channel up, down
LICZ(0) = up -> LICZ(1)
LICZ(3) = down -> LICZ(2)
LICZ(k) = (0<k and k<3 ) & (up -> LICZ(k+1) [] down -> LICZ(k-1))
-- ^ modelujemy licznik przyjmujacy wart 0,1,2,3
P1 = up -> up -> up -> down -> down -> down -> STOP
P2 = up -> up -> down -> down -> STOP
P3 = up -> up -> down -> down -> down -> STOP
P4 = up -> up -> up -> up -> down -> down -> down -> STOP
-- ^ różne procesy liczące
assert LICZ(0) [T= P1
assert LICZ(0) [T= P2
assert LICZ(0) [T= P3
assert LICZ(0) [T= P4
-- ^ sprawdzamy czy Pi są zgodne ze spec licznika

przykład 3 CSPm - bufor pamiętający elementy
channel we, wy: {1,2,3}
BUF(<>) = we?x -> BUF(<x>)
BUF(<a>^s) = ( #(<a>^s) < 5 & we?x -> BUF(<a>^s^<x>) ) [] wy!a -> BUF(s)
-- ^ def bufora o pojemności 5 elem
P1 = we.1 -> we.2 -> we.3 -> STOP
P2 = wy.1 -> wy.2 -> wy.3 -> STOP
-- ^ dwa procesy wysyłające/czytające komunikaty
Q = P1 [|{|we|}|] BUF(<>) [|{|wy|}|] P2
-- ^ współbieżne połączenie P1 i P2 z komunikacją przez BUF

....................................

ZADANIE 80 (csp)
???