szymanski_na2.cub

(* Szymanski's mutual exclusion algorithm - Non atomic version
   Universal quantifications are replaced by iterative checks inside
   for loops

0 : Bx := true
1 : await forall y. x <> y => not Sy then Bx := false
2 : Wx := true ; Sx := true ;
3 : if exists y. x <> y not By /\ not Wy
       then Sx := false ; goto 4
       else Wx := false ; goto 5
4 : await exists y. x <> y => Sy /\ not Wy then Wx := false ; Sx := true;
5 : await forall y. x <> y => not Wy
6 : await forall y. y < x => not Sy
7 : {Critical section}
    Sx := false ; goto 0
*)


type location = L0 | L1 | L2 | L3 | L4 | L5 | L6 | L7 

array A[proc] : location
array B[proc] : bool
array S[proc] : bool
array W[proc] : bool 
array X[proc, proc] : bool (* counters for non atomic loops *)

init (x y) { A[x] = L0 && S[x] = False && W[x] = False && B[x] = False &&
             X[x, y] = False }
 
unsafe (z1 z2) { A[z1] = L7 && A[z2] = L7 }

transition t0 (x)
requires { A[x] = L0 }
{ A[x] := L1; B[x] := True }

transition t1 (x)
requires { A[x] = L1 && forall_other y. S[y] = False }
{ A[x] := L2; B[x] := False }

(* transition t1_enter_for (x y) *)
(* requires { A[x] = L1 && X[x,y] = False && S[y] = False && *)
(*            forall_other z. (y < z || X[x,z] = True ) } *)
(* { X[x,y] := True } *)

(* transition t1_exit_for (x) *)
(* requires { A[x] = L1 && forall_other y. X[x,y] = True } *)
(* {  *)
(*   A[x] := L2; *)
(*   B[x] := False; *)
(*   (\* Reset counter *\) *)
(*   X[i,j] := case | i = x : False | _ : X[i,j]; *)
(* } *)

transition t2 (x)
requires { A[x] = L2 }
{ A[x] := L3; S[x] := True; W[x] := True }

(* transition t3_then (x y) *)
(* requires { A[x] = L3 && B[y] = False && W[y] = False } *)
(* { A[x] := L4; S[x] := False } *)

(* transition t3_else (x) *)
(* requires { A[x] = L3 && forall_other y. ( B[y] =  True || W[y] = True ) } *)
(* { A[x] := L5; W[x] := False } *)

transition t3_abort_for (x y)
requires { A[x] = L3 &&
           X[x,y] = False && B[y] = False && W[y] = False (* && *)
           (* forall_other z. (y < z || X[x,z] = True ) *) }
{ 
  A[x] := L4;
  S[x] := False;
  (* Reset counter *)
  X[i,j] := case | i = x : False | _ : X[i,j];
}

transition t3_incr_for1 (x y)
requires { A[x] = L3 &&
           X[x,y] = False && B[y] = True (* && *)
           (* forall_other z. (y < z || X[x,z] = True ) *) }
{ X[x,y] := True }

transition t3_incr_for2 (x y)
requires { A[x] = L3 &&
           X[x,y] = False && W[y] = True (* && *)
           (* forall_other z. (y < z || X[x,z] = True ) *) }
{ X[x,y] := True }


transition t3_exit_for (x)
requires { A[x] = L3 && forall_other y. X[x,y] = True }
{ 
  A[x] := L5;
  W[x] := False;
  (* Reset counter *)
  X[i,j] := case | i = x : False | _ : X[i,j];
}


(* transition t4 (x y) *)
(* requires { A[x] = L4 && S[y] = True && W[y] = False } *)
(* { A[x] := L5; S[x] := True; W[x] := False } *)

transition t4_incr_for1 (x y)
requires { A[x] = L4 &&
           X[x,y] = False && S[y] = False (* && *)
           (* forall_other z. (y < z || X[x,z] = True ) *) }
{  X[x,y] := True }

transition t4_incr_for2 (x y)
requires { A[x] = L4 &&
           X[x,y] = False && W[y] = True (* && *)
           (* forall_other z. (y < z || X[x,z] = True ) *) }
{ X[x,y] := True }

transition t4_exit_for (x y)
requires { A[x] = L4 &&
           X[x,y] = False && S[y] = True && W[y] = False (* && *)
           (* forall_other z. (y < z || X[x,z] = True ) *) }
{ 
  A[x] := L5;
  S[x] := True;
  W[x] := False;
  (* Reset counter *)
  X[i,j] := case | i = x : False | _ : X[i,j];
}

transition t4_restart_for (x)
requires { A[x] = L4 && forall_other y. X[x,y] = True }
{ 
  (* Reset counter *)
  X[i,j] := case | i = x : False | _ : X[i,j];
}

(* transition t5 (x) *)
(* requires { A[x] = L5 && forall_other y. W[y] = False } *)
(* { A[x] := L6 } *)

transition t5_enter_for (x y)
requires { A[x] = L5 &&
           X[x,y] = False && W[y] = False (* && *)
           (* forall_other z. (y < z || X[x,z] = True ) *) }
{ X[x,y] := True }

transition t5_exit_for (x)
requires { A[x] = L5 && forall_other y. X[x,y] = True }
{ 
  A[x] := L6;
  (* Reset counter *)
  X[i,j] := case | i = x : False | _ : X[i,j];
}


(* transition t6 (x) *)
(* requires { A[x] = L6 && forall_other j. (x <= j || S[j] = False) } *)
(* { A[x] := L7 } *)


transition t6_enter_for (x y)
requires { A[x] = L6 && y < x && 
           X[x,y] = False && S[y] = False (* && *)
           (* forall_other z. (y < z || X[x,z] = True ) *) }
{ X[x,y] := True }

transition t6_exit_for (x)
requires { A[x] = L6 && forall_other y. (x < y || X[x,y] = True) }
{ 
  A[x] := L7;
  (* Reset counter *)
  X[i,j] := case | i = x : False | _ : X[i,j];
}


transition t7 (x)
requires { A[x] = L7 }
{ A[x] := L0; S[x] := False }