```(*****************************************************************************)
(* 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                                                  *)
(*                                                                           *)
(* A simple solution to Lamport's concurrent programming problem with        *)
(* linear wait.  Boleslaw K. Szymanski. ICS, page 621-626. (1988)            *)
(*****************************************************************************)

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 t2 (x)
requires { A[x] = L2 }
{ A[x] := L3; S[x] := True; W[x] := True }

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_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_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_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 }
```