ricart_abdulla.cub

type state = Idle | Wait | Use

type msg = Empty | Req | Ack | Ok

var Timer : real

array State[proc] : state

array Clock[proc] : real
array Last[proc] : real

array Channel_msg[proc,proc] : msg
array Channel_timestamp[proc,proc] : real

const Tick : real

init (z z1) { State[z] = Idle &&
              Clock[z] = 0.0 &&
              Last[z] = 0.0 && 
              Timer = 1.0 && 
              Channel_msg[z,z1] = Empty && 
              Channel_timestamp[z,z1] = 0.0 }

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

unsafe (z1 z2) {
  State[z1] = Use && State[z2] = Use &&
  Channel_msg[z1,z2] = Ok && Channel_msg[z2,z1] = Ok
}


transition t1 (z)
requires { State[z] = Idle (* && Sender[z] = Receiver[z] *) && 0.0 < Tick }
{
  Timer := Timer + Tick;
  State[z] := Wait;
  Clock[z] := Timer;
  Last[z] := Timer;

  Channel_msg[s,r] := case
      | s = z && Channel_msg[s,r] = Empty : Req
      | _ : Channel_msg[s,r];
  Channel_timestamp[s,r] :=  case
      | s = z && Channel_msg[s,r] = Empty : Timer
      | _ : Channel_timestamp[s,r];

}

transition t2 (z r)
requires { State[z] = Wait &&
           Channel_msg[z,r] = Ack &&
           0.0 < Tick}
{
  Timer := Timer + Tick;
  Clock[z] := Timer;
  Channel_msg[z,r] := Ok;
  Channel_timestamp[z,r] := Timer;
 }


transition t3 (z)
requires { State[z] = Wait &&
           forall_other j. Channel_msg[z,j] = Ok }
{
  State[z] := Use;
}


transition t4 (z)
requires { State[z] = Use && 0.0 < Tick }
{
  Timer := Timer + Tick;

  State[z] := Idle;
  Clock[z] := Timer;

  Channel_msg[s,r] := case
      | s = z && Channel_msg[s,r] = Ok : Empty
      | r = z && Channel_msg[s,r] = Req : Ack
      | _ : Channel_msg[s,r];

  Channel_timestamp[s,r] := case
      | r = z && Channel_msg[s,r] = Req : Timer
      | _ : Channel_timestamp[s,r];

}


transition t5 (z s)
requires { State[z] = Idle &&
           Channel_msg[s,z] = Req &&
           Channel_timestamp[s,z] < Clock[z] && 0.0 < Tick }
{
  Timer := Timer + Tick;
  Clock[z] := Timer;

  Channel_msg[s,z] := Ack;
  Channel_timestamp[s,z] := Timer;
}

transition t6 (z s)
requires { State[z] = Wait &&
           Channel_msg[s,z] = Req &&
           Channel_timestamp[s,z] < Last[z] && 0.0 < Tick }
{
  Timer := Timer + Tick;
  Clock[z] := Timer;

  Channel_msg[s,z] := Ack;
  Channel_timestamp[s,z] := Timer;
}

transition t7 (z s)
requires { State[z] = Wait &&
           Channel_msg[s,z] = Req &&
           Channel_timestamp[s,z] = Last[z] &&
           s < z && 0.0 < Tick }
{
  Timer := Timer + Tick;
  Clock[z] := Timer;

  Channel_msg[s,z] := Ack;
  Channel_timestamp[s,z] := Timer;
}