---------------------------------------------------------
-- 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,e,r) = rename(apply(DUAL_PROT_IMP, (P,e)), r)

---------------------------------------------------------
-- 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))

-- 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>)