---------------------------------------------------------
-- Auxiliar Functions
---------------------------------------------------------
inc(x,n) = (x + 1) % n
dec(x,n) = (x - 1) % n
-- Rename channels in a process using a mapping < (old1, new1), ..., (oldn, newn)>
rename(P, <>) = P
rename(P, <(c1,c2)>^rs) = rename(P[[c1 <- c2]], rs)
-- Replaces events in a set using the mapping < (old1, new1), ..., (oldn, newn)>
replace_aux(oldc, newc, S) =
let other_events = {e | e <- S, not member(e, productions(oldc))}
new_events = {newc.v | v <- inter(extensions(newc), extensions(oldc)), member(oldc.v, S)}
within union (other_events, new_events)
replace(S, <>) = S
replace(S, <(c1,c2)>^rs) = replace(replace_aux(c1,c2,S),rs)
-- Filters inputs or outputs from a given set of events
filter(inout,S) =
if inout == in then inter(allInputs,S) else inter(allOutputs,S)
---------------------------------------------------------
-- Side Condition FUNCTIONS --
---------------------------------------------------------
events(P) = union(inputs(P),outputs(P))
allInputs = Union({ inputs(P) | P <- dom(GET_CHANNELS)})
allOutputs = Union({ outputs(P) | P <- dom(GET_CHANNELS)})
HideOutputs(P) = P \ outputs(P)
HideInputs(P) = P \ inputs(P)
HideAll(P) = P \ union(outputs(P),inputs(P))
CollapseOutputs(P) = P [[ x <- o | x <- outputs(P) ]] \ allInputs
-- Renaming I/O
R_IO(P, a, b) = seq({(a.x, b.x) | x <- extensions(a), member(a.x, outputs(P))})
inputs_R_IO(P,a,b) = inputs(P)
outputs_R_IO(P,a,b) = { b.x | x <- extensions(a), member(a.x, outputs(P)) }
-- Protocol Implementation
inputs_PROT_IMP(P,c) = inter(inputs(P),{|c|})
outputs_PROT_IMP(P,c) = inter(outputs(P),{|c|})
-- Protocol Implementation and renaming
PROT_IMP_R(P,r) = rename(P, r) --modifidado por sarah
inputs_PROT_IMP_R(P,e,r) = replace(inputs_PROT_IMP(P,e), r)
outputs_PROT_IMP_R(P,e,r) = replace(outputs_PROT_IMP(P,e), r)
-- Dual Protocol Implementation and renaming R_IO
DUAL_PROT_IMP_R(P,r) = rename(P, r) --modifidado por sarah
---------------------------------------------------------
-- Side Condition PROCESSES --
---------------------------------------------------------
RUN(A) = [] x:A @ x -> RUN(A)
CHAOS(A) = STOP |~| ([] x:A @ x -> CHAOS(A))
-- Test if a given condition is met
channel error
ERROR = error -> SKIP
Test(c) = not c & ERROR
-- Used for testing protocols
-- This is not used in the CSP framework, but will be used in the Circus/CML Framework
channel out
channel in
channel mid
CP(a,b) = a -> b -> CP(a,b)
C(a, P) = (P[[ a <- mid ]] [| {| mid |} |] CP(a,mid)) \ {|mid|}
CIO(P) = C(in, C(out, P))
--InBufferProt(P,c) = CIO(P[[ c.in.x <- i, c.out.y <- o | x <- extensions(c.in), y <- extensions(c.out)]])
InBufferProt(P,c) = CIO(P[[ x <- in, y <- out | x <- inputs(P), y <- outputs(P)]])
-- Channels Projection
PROJECTION(P,cs) = P \ (diff(Events, Union({ {| c |} | c <- cs})))
-- Channels
INTER_PROT_IMP(P,cs) = ||| c:cs @ apply(PROT_IMP,(P,c))
--INTER_PROT_IMP(P,cs) = ||| c:cs @ apply(P,c) --modificado por sarah
-- Protocol Implementation
PROT_IMP_def(P,c) = P \ (diff(Events, {|c|}))
COPY (LR) = [] x : dom(LR) @ x -> apply(LR,x) -> COPY (LR)
BUFF_IO(BF, LR1, LR2) = (BF (LR1) ||| BF (LR2))
BUFF_IO_1(LR1,LR2) = BUFF_IO(COPY, LR1, LR2)
----------------------------------------
-- These processes are only used when we have a optimization due to the use of architectural styles
-- Client-Server Specification
CS(c) = CS_CLIENT(c) [] CS_SERVER(c)
CS_CLIENT(c) = c.in?v1 -> c.out?v2 -> CS_CLIENT(c)
CS_SERVER(c) = c.out?v1 -> c.in?v2 -> CS_SERVER(c)
----------------------------------------
-- Protocol does not speak anything else
----------------------------------------
NOT(c) = diff(Events, {| c |})
PRUNE(A) = [] ev: A @ ev -> STOP
ProtCheck(P,c) = P [| NOT(c) |] PRUNE(NOT(c))
----assert ProtCheck(<PROCESS>,<CHANNEL>) :[deadlock free [FD]]
----------------------------------------
-- "... and nothing else matters..."
----------------------------------------
----assert <PROCESS> [| Events |] (<PROCESS> ||| RUN(NOT(<CHANNEL>))) [T= <PROCESS>
----assert <PROCESS> [T= <PROCESS> [| Events |] (<PROCESS> ||| RUN(NOT(<CHANNEL>)))
----------------------------------------
-- Input Determinism
----------------------------------------
channel clunk
AllButClunk = diff(Events, {clunk})
Clunking(P) = P [| AllButClunk |] Clunker
Clunker = [] x:AllButClunk @ x -> clunk -> Clunker
Repeat = [] x:AllButClunk @ x -> x -> Repeat
RHS_InputDet(P) = (Clunking(P)[|{clunk}|]Clunking(P)) \ {clunk} [|AllButClunk|] Repeat
-- Original Lazic`s Algorithm (adapted by Roscoe)
LHS' = STOP |~| ([] x:AllButClunk @ x -> x -> LHS')
-- Changed Lazic`s Algorithm (proposed by Roscoe) to consider only a particular set of events
Deterministic(S) =
STOP
|~|
([] x:AllButClunk @ x -> (if member(x,S)
then x -> Deterministic(S)
else (STOP |~| x -> Deterministic(S))))
LHS_InputDet(P) = Deterministic(inputs(P))
--assert LHS_InputDet(<PROCESS>) [F= RHS_InputDet(<PROCESS>)
-----------------
-----------------
----------------------------------------
-- Strong output decisive
----------------------------------------
-- Roscoe's Strong output decisive
SSET(P,c) = inter({|c|},outputs(P))
F(P,c) = P [| SSET(P,c) |] S(SSET(P,c))
G(P,c) = P [| SSET(P,c) |] CHAOS(SSET(P,c))
S(X) =
if (card(X) > 1) then
(|~| x:X @ [] y:diff(X, {x}) @ y -> S(X))
else
(STOP |~| ([] x:X @ x -> S(X)))
--assert F(<PROCESS>,<CHANNEL>) [F= G(<PROCESS>,<CHANNEL>)
----------------------------------------------------
-- Bill's Solution for Rodrigo's Output Decisiveness
----------------------------------------------------
----------------------------------------------------
-- Part A. If there is a trace s^<c.x>, after s, it cannot refuse all events on {|c|}
-- Outputs events with same prefixing of a given output event
chan(ev,P) = inter(outputs(P), {| c | c <- GET_CHANNELS(P), member(ev, {|c|})|})
-----------------------------------------------------------------
-----------------------------------------------------------------
--PREVIOUS DEFINITIONS
--One2Many(S) =
-- ([] x:diff(Events,union(S, {clunk})) @ x -> One2Many(S))
-- [] ([] c:S @ [] x:{|c|} @ x -> One2Many'(S,c,x))
--One2Many'(S,c,x) = [] y:{|c|} @ y -> if x==y then One2Many(S) else STOP
--RHS_OutputDec_A(P) =
-- (Clunking(P)[|diff(Events, outputs(P))|]Clunking(P)) \ {clunk}
-- [| AllButClunk |]
-- One2Many(outputs(P))
-- Definition above is sliglty wrong because One2Many'(S,c,x) enforces the following event to be a repetition
-- if the given c is not a channel bout the full event.
--NEW DEFINITIONS
One2Many(P) =
([] x:diff(Events,union(outputs(P), {clunk})) @ x -> One2Many(P))
[] ([] c:outputs(P) @ [] x:{|c|} @ x -> One2Many'(P,c,x))
One2Many'(P,c,x) = [] y:chan(c,P) @ y -> if x==y then One2Many(P) else STOP
RHS_OutputDec_A(P) =
(Clunking(P)[|diff(Events, outputs(P))|]Clunking(P)) \ {clunk}
[| AllButClunk |]
One2Many(P)
-----------------------------------------------------------------
-----------------------------------------------------------------
LHS_OutputDec_A(P) =
STOP
|~|
([] x:diff(Events,union(outputs(P), {clunk})) @ x -> LHS_OutputDec_A(P))
[]
([] x:outputs(P) @ x -> (|~| y:chan(x,P) @ y -> LHS_OutputDec_A(P)))
--assert LHS_OutputDec_A(<PROCESS>) [F= RHS_OutputDec_A(<PROCESS>)
----------------------------------------------------
-- Part B. After trace s^<c.x> it might refuse all events on {|c|} \ {c.x}
FirstCopy(P) = P [| AllButClunk |] DoubleClunker
SecondCopy(P) = P [| AllButClunk |] clunk -> DoubleClunker
DoubleClunker = [] x:AllButClunk @ x -> clunk -> clunk -> DoubleClunker
LHS_Test(S) =
[] x:S @
x -> (x -> LHS_Test(S) [>
([] y:diff(S, {x}) @ y -> STOP)
)
[] ([] y:diff(Events,S) @ y -> y -> LHS_Test(S))
LHS_OutputDec_B(P,c) = (FirstCopy(P)[|{clunk}|]SecondCopy(P))\{clunk} [|Events|] LHS_Test(inter({|c|}, outputs(P)))
RHS_Test(S) =
[] x:S @
x ->
( ([] y:S @ y -> if x==y then RHS_Test(S) else STOP)
|~| STOP )
[] ([] y:diff(Events,S) @ y -> y -> RHS_Test(S))
RHS_OutputDec_B(P,c) = (FirstCopy(P)[|{clunk}|]SecondCopy(P))\{clunk} [|Events|] RHS_Test(inter({|c|}, outputs(P)))
--assert LHS_OutputDec_B(<PROCESS>,<CHANNEL>) [F= RHS_OutputDec_B(<PROCESS>,<CHANNEL>)