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