ricart_agrawala.cub

type location = L1            | L2               | L3              | L4
(*        Empty | Idle |     Wait | Req |    Use | Ack |   Exiting | Ok *)


var Timer : real

array State[proc] : location

array Sender[proc] : proc
array Receiver[proc] : proc
array Clock[proc] : real
array Last[proc] : real
array Is_proc[proc] : bool

const Tick : real

init (z) { State[z] = L1 && Clock[z] = 0.0 && Last[z] = 0.0 && Timer = 1.0 }


(* invariant () { Tick <= 0.0 } *)

unsafe (z1 z2 z3 z4) { 
  State[z1] = L3 && State[z2] = L3 &&
  Sender[z1] = Receiver[z1] && Sender[z2] = Receiver[z2] &&
  State[z3] = L4 && State[z4] = L4 && 
  Sender[z3] <> Receiver[z3] && Sender[z4] <> Receiver[z4] &&
  Sender[z3] = z1 && Sender[z4] = z2 &&
  Receiver[z3] = z2 && Receiver[z4] = z1
}


transition t1 (z)
requires { State[z] = L1 && Sender[z] = Receiver[z] && 0.0 < Tick }
{
  Timer := Timer + Tick;
  State[j] := case
                | j = z : L2
		| State[j] = L1 && Sender[j] = z : L2
		| _ : State[j] ;
  Clock[j] := case
		| j = z : Timer
                | State[j] = L1 && Sender[j] = z : Timer
		| _ : Clock[j] ;
  Last[j]  := case
		| j = z : Timer
		| _ : Last[j] 

}

transition t2 (z other)
requires { State[z] = L2 && 
           Sender[z] = Receiver[z] &&
           Sender[other] <> Receiver[other] &&
	   State[other] = L3 && Sender[other] = z  && 0.0 < Tick}
{
  Timer := Timer + Tick;
  State[j] := case
                | j = z : L2
                | j = other : L4
		| _ : State[j] ;
  Clock[j] := case
		| j = z : Timer
		| j = other : Timer
		| _ : Clock[j] ;
}


transition t3 (z)
requires { State[z] = L2 && Sender[z] = Receiver[z] && 
           forall_other j. 
	     (Sender[j] = Receiver[j] || Sender[j] <> z || State[j] = L4) }
{
  State[j] := case
                | j = z : L3
		| _ : State[j]
}


transition t4 (z)
requires { State[z] = L3 && Sender[z] = Receiver[z] }
{
  State[j] := case
                | j = z : L4
		| Sender[j] <> Receiver[j] && State[j] = L4 && 
                  Sender[j] = z : L1
		| _ : State[j] ;
}


transition t5 (z)
requires { State[z] = L4 && Sender[z] = Receiver[z] && 0.0 < Tick &&
	   forall_other j.
	    (Sender[j] = Receiver[j] || Receiver[j] <> z || State[j] <> L2) }
{
  Timer := Timer + Tick;
  State[j] := case
                | j = z : L1
		| _ : State[j] ;
  Clock[j] := case
		| _ : Timer ;
}


transition t6 (z other)
requires { State[z] = L1 && Sender[z] = Receiver[z] &&
           State[other] = L2 && Sender[other] <> Receiver[other] &&
	   Receiver[other] = z && Clock[other] <= Clock[z] && 0.0 < Tick }
{
  Timer := Timer + Tick;
  State[j] := case
                | j = z : L1
		| j = other : L3
		| _ : State[j] ;
  Clock[j] := case
		| j = z : Timer
		| j = other : Timer
		| _ : Clock[j] ;
}

transition t7 (z other)
requires { State[z] = L2 && Sender[z] = Receiver[z] &&
           State[other] = L2 && Sender[other] <> Receiver[other] &&
	   Receiver[other] = z && Clock[other] < Last[z] && 0.0 < Tick }
{
  Timer := Timer + Tick;
  State[j] := case
                | j = z : L2
		| j = other : L3
		| _ : State[j] ;
  Clock[j] := case
		| j = z : Timer
		| j = other : Timer
		| _ : Clock[j] ;
}


transition t8 (z other)
requires { State[z] = L2 && Sender[z] = Receiver[z] &&
           State[other] = L2 && Sender[other] <> Receiver[other] &&
	   Receiver[other] = z && Clock[other] = Last[z] && Sender[other] < z && 0.0 < Tick }
{
  Timer := Timer + Tick;
  State[j] := case
                | j = z : L2
		| j = other : L3
		| _ : State[j] ;
  Clock[j] := case
		| j = z : Timer
		| j = other : Timer
		| _ : Clock[j] ;
}