szymanski_talupur_at.cub

(* 
Szymanski's algorithm from:

          Abstraction Techniques for Parameterized Verification
          Muralidhar Talupur.
          PhD Thesis, Computer Science Department, Carnegie Mellon University 
          CMU-CS-06-169, CMU, 2006

F = {pc}, pc \in {0;1;2;3;4;5;6;7}
pc = 0 : goto pc = 1
pc = 1 : if forall otr <> slf. pc[otr] \in {0;1;2;4} then goto pc = 2
         else goto pc = 1
pc = \in : goto pc = 3
pc = 3 : if forall otr <> slf. pc[otr] \not \in 1;2 then goto pc = 5
         else goto pc = 4
pc = 4 : if forall otr <> slf. pc[otr] \not \in {5;6;7} then goto pc = 4
         else goto pc = 5
pc = 5 : if forall otr <> slf. pc[otr] \not \in {2;3;4} then goto pc = 6
         else goto pc = 5
pc = 6 : if forall otr > slf. pc[otr] \in {0;1;2} then goto pc = 7
         else goto pc = 6
pc = 7 : goto pc = 0

*)


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

array PC[proc] : location

init (x) { PC[x] = L0 }
 
unsafe (z1 z2) { PC[z1] = L7 && PC[z2] = L7 }

transition t0 (x)
requires { PC[x] = L0 }
{ PC[x] := L1 }

transition t1 (x)
requires { PC[x] = L1 && forall_other y. (PC[y] <> L3 && PC[y] <> L5 && PC[y] <> L6 && PC[y] <> L7) }
{ PC[x] := L2 }

transition t2 (x)
requires { PC[x] = L2 }
{ PC[x] := L3 }

transition t3_else1 (x y)
requires { PC[x] = L3 && PC[y] = L1 }
{ PC[x] := L4 }

transition t3_else2 (x y)
requires { PC[x] = L3 && PC[y] = L2 }
{ PC[x] := L4 }

transition t3_then (x)
requires { PC[x] = L3 && forall_other y. (PC[y] <> L1 && PC[y] <> L2) }
{ PC[x] := L5 }


transition t4 (x y)
requires { PC[x] = L4 && PC[y] <> L0 && PC[y] <> L1 && PC[y] <> L2 && PC[y] <> L3 && PC[y] <> L4 }
{ PC[x] := L5 }


transition t5 (x)
requires { PC[x] = L5 && forall_other y. (PC[y] <> L2 && PC[y] <> L3 && PC[y] <> L4) }
{ PC[x] := L6 }


transition t6 (x)
requires { PC[x] = L6 && forall_other j. (x <= j || PC[j] = L0 || PC[j] = L1 || PC[j] = L2 ) }
{ PC[x] := L7 }

transition t7 (x)
requires { PC[x] = L7 }
{ PC[x] := L0 }