jml.cub

type location = Idle | Owner | Handin | Handout | Waiting
type lock = C0 | C1 | C2 | C3

var Busy : bool
var H : lock
var C : int

array A[proc] : location

init (z) { A[z] = Idle && Busy = False && H = C0 && 0<C }
 
unsafe (z1 z2) { A[z1]=Owner && A[z2]=Owner }
(* unsafe () { H = C1 && C = 0 } *)
 
transition t1 (x)
requires { A[x]=Idle && Busy=False && 0 < C }
{ Busy := True ;
  A[j] := case | j = x : Owner | _ : A[j]; }

transition t2 (x)
requires { A[x] = Idle && Busy = True && 0 < C }
{ C := C + 1 ;	
  A[j] := case | j = x : Handin | _ : A[j]; }
 
transition t3 (x)
requires { A[x] = Owner && Busy = True && C = 0 }
{ Busy := False;
  A[j] := case | j = x : Idle | _ : A[j]; }

transition t4 (x)
requires { A[x] = Owner && Busy = True && 0 < C }
{ C := C - 1 ;
  A[j] := case | j = x : Handout | _ : A[j]; }

transition t5 (x)
requires { A[x] = Handin && H = C0 && 0 < C }
{ H := C1;
  A[j] := case | j = x : Waiting | _ : A[j]; }

transition t6 (x)
requires { A[x] = Handout && H = C0 && 0 < C }
{ H := C2 ;
  A[j] := case | j = x : Idle | _ : A[j]; }

transition t7 (x)
requires { A[x] = Handout && H = C1 && 0 < C }
{ H := C3;
  A[j] := case | j = x : Idle | _ : A[j]; }

transition t8 (x)
requires { A[x] = Handin && H = C2 && 0 < C }
{ H := C3;
  A[j] := case | j = x : Waiting | _ : A[j]; }

transition t9 (x)
requires { A[x] = Waiting && H = C3 && 0 < C }
{ H := C0;
  A[j] := case | j = x : Owner | _ : A[j]; }