ricart_abdulla_int1.cub

type state = Idle | Wait | Use

type msg = Empty | Req | Ack | Ok

var Timer : int

array State[proc] : state

array Clock[proc] : int
array Last[proc] : int

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

init (z z1) { State[z] = Idle &&
              Clock[z] = 0 &&
              Last[z] = 0 && 
              Timer = 1 && 
              Channel_msg[z,z1] = Empty && 
              Channel_timestamp[z,z1] = 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 }
{
  Timer := Timer + 1;
  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 }
{
  Timer := Timer + 1;
  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 }
{
  Timer := Timer + 1;

  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] }
{
  Timer := Timer + 1;
  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] }
{
  Timer := Timer + 1;
  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 }
{
  Timer := Timer + 1;
  Clock[z] := Timer;

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