------------------ MODULE oneway ---------------
EXTENDS Integers

VARIABLE 
  P0,P1,P2,P3,P4,P5,P6,P7,RA,RB
  
vars == <<P0,P1,P2,P3,P4,P5,P6,P7,RA,RB>>

TypesOK  == (P0 \in 0..6)

T0 == << 1, 9,10,13,15,20,23>>
T1 == << 3, 9,10,13,15,20,24>>
T2 == << 5,27,11,13,16,20,25>>
T3 == << 7,27,11,13,16,20,26>>
T4 == <<23,22,17,18,11, 9, 2>>
T5 == <<24,22,17,18,11, 9, 4>>
T6 == <<25,22,17,18,12,27, 6>>
T7 == <<26,22,17,18,12,27, 8>>

A0 == << 0, 0, 0, 1, 0,-1, 0>>
A1 == << 0, 0, 0, 1, 0,-1, 0>>
A2 == << 0, 0, 1,-1, 0, 1, 0>>
A3 == << 0, 0, 1,-1, 0, 0, 0>>
A4 == << 0, 1, 0, 0,-1, 0, 0>>
A5 == << 0, 1, 0, 0,-1, 0, 0>>
A6 == << 0, 0, 0,-1, 0, 0, 0>>
A7 == << 0, 1, 0,-1, 0, 0, 0>>

B0 == << 0, 0, 0, 1, 0,-1, 0>>
B1 == << 0, 0, 0, 1, 0,-1, 0>>
B2 == << 0, 0, 1,-1, 0, 0, 0>>
B3 == << 0, 0, 1,-1, 0, 1, 0>>
B4 == << 0, 1, 0, 0,-1, 0, 0>>
B5 == << 0, 1, 0, 0,-1, 0, 0>>
B6 == << 0, 1, 0,-1, 0, 0, 0>>
B7 == << 0, 0, 0,-1, 0, 0, 0>>

LA == 7
LB == 7

LL == 6

Init== 
/\ P0=0 /\ P1=0 /\ P2=0 /\ P3=0 /\ P4=0 /\ P5=0 /\ P6=0 /\ P7=0 
/\ RA=1 /\ RB=1

Move0 ==
   /\ P0 < LL 
   /\ T0[P0+2] /= T1[P1+1]
   /\ T0[P0+2] /= T2[P2+1]
   /\ T0[P0+2] /= T3[P3+1]
   /\ T0[P0+2] /= T4[P4+1]
   /\ T0[P0+2] /= T5[P5+1]
   /\ T0[P0+2] /= T6[P6+1]
   /\ T0[P0+2] /= T7[P7+1]
   /\ RA + A0[P0+2] <= LA
   /\ RB + B0[P0+2] <= LB
   /\ P0' = (P0+1)
   /\ RA' = RA + A0[P0+2]
   /\ RB' = RB + B0[P0+2]
   /\ UNCHANGED <<P1,P2,P3,P4,P5,P6,P7>>


Move1 ==
   /\ P1 < LL 
   /\ T1[P1+2] /= T0[P0+1]
   /\ T1[P1+2] /= T2[P2+1]
   /\ T1[P1+2] /= T3[P3+1]
   /\ T1[P1+2] /= T4[P4+1]
   /\ T1[P1+2] /= T5[P5+1]
   /\ T1[P1+2] /= T6[P6+1]
   /\ T1[P1+2] /= T7[P7+1]
   /\ RA + A1[P1+2] <= LA
   /\ RB + B1[P1+2] <= LB
   /\ P1' = (P1+1)
   /\ RA' = RA + A1[P1+2]
   /\ RB' = RB + B1[P1+2]
   /\ UNCHANGED <<P0,P2,P3,P4,P5,P6,P7>>
   

Move2 ==
   /\ P2 < LL 
   /\ T2[P2+2] /= T0[P0+1]
   /\ T2[P2+2] /= T1[P1+1]
   /\ T2[P2+2] /= T3[P3+1]
   /\ T2[P2+2] /= T4[P4+1]
   /\ T2[P2+2] /= T5[P5+1]
   /\ T2[P2+2] /= T6[P6+1]
   /\ T2[P2+2] /= T7[P7+1]
   /\ RA + A2[P2+2] <= LA
   /\ RB + B2[P2+2] <= LB
   /\ P2' = (P2+1)
   /\ RA' = RA + A2[P2+2]
   /\ RB' = RB + B2[P2+2]
   /\ UNCHANGED <<P0,P1,P3,P4,P5,P6,P7>>
   

Move3 ==
   /\ P3 < LL 
   /\ T3[P3+2] /= T0[P0+1]
   /\ T3[P3+2] /= T1[P1+1]
   /\ T3[P3+2] /= T2[P2+1]
   /\ T3[P3+2] /= T4[P4+1]
   /\ T3[P3+2] /= T5[P5+1]
   /\ T3[P3+2] /= T6[P6+1]
   /\ T3[P3+2] /= T7[P7+1]
   /\ RA + A3[P3+2] <= LA
   /\ RB + B3[P3+2] <= LB
   /\ P3' = (P3+1)
   /\ RA' = RA + A3[P3+2]
   /\ RB' = RB + B3[P3+2]
   /\ UNCHANGED <<P0,P1,P2,P4,P5,P6,P7>>
     
Move4 ==
   /\ P4 < LL 
   /\ T4[P4+2] /= T0[P0+1]
   /\ T4[P4+2] /= T1[P1+1]
   /\ T4[P4+2] /= T2[P2+1]
   /\ T4[P4+2] /= T3[P3+1]
   /\ T4[P4+2] /= T5[P5+1]
   /\ T4[P4+2] /= T6[P6+1]
   /\ T4[P4+2] /= T7[P7+1]
   /\ RA + A4[P4+2] <= LA
   /\ RB + B4[P4+2] <= LB
   /\ P4' = (P4+1)
   /\ RA' = RA + A4[P4+2]
   /\ RB' = RB + B4[P4+2]
   /\ UNCHANGED <<P0,P1,P2,P3,P5,P6,P7>>
   

Move5 ==
   /\ P5 < LL 
   /\ T5[P5+2] /= T0[P0+1]
   /\ T5[P5+2] /= T1[P1+1]
   /\ T5[P5+2] /= T2[P2+1]
   /\ T5[P5+2] /= T3[P3+1]
   /\ T5[P5+2] /= T4[P4+1]
   /\ T5[P5+2] /= T6[P6+1]
   /\ T5[P5+2] /= T7[P7+1]
   /\ RA + A5[P5+2] <= LA
   /\ RB + B5[P5+2] <= LB
   /\ P5' = (P5+1)
   /\ RA' = RA + A5[P5+2]
   /\ RB' = RB + B5[P5+2]
   /\ UNCHANGED <<P0,P1,P2,P3,P4,P6,P7>>
   
Move6 ==
   /\ P6 < LL 
   /\ T6[P6+2] /= T0[P0+1]
   /\ T6[P6+2] /= T1[P1+1]
   /\ T6[P6+2] /= T2[P2+1]
   /\ T6[P6+2] /= T3[P3+1]
   /\ T6[P6+2] /= T4[P4+1]
   /\ T6[P6+2] /= T5[P5+1]
   /\ T6[P6+2] /= T7[P7+1]
   /\ RA + A6[P6+2] <= LA
   /\ RB + B6[P6+2] <= LB
   /\ P6' = (P6+1)
   /\ RA' = RA + A6[P6+2]
   /\ RB' = RB + B6[P6+2]
   /\ UNCHANGED <<P0,P1,P2,P3,P4,P5,P7>>
   
   
Move7 ==
   /\ P7 < LL 
   /\ T7[P7+2] /= T0[P0+1]
   /\ T7[P7+2] /= T1[P1+1]
   /\ T7[P7+2] /= T2[P2+1]
   /\ T7[P7+2] /= T3[P3+1]
   /\ T7[P7+2] /= T4[P4+1]
   /\ T7[P7+2] /= T5[P5+1]
   /\ T7[P7+2] /= T6[P6+1]
   /\ RA + A7[P7+2] <= LA
   /\ RB + B7[P7+2] <= LB
   /\ P7' = (P7+1)
   /\ RA' = RA + A7[P7+2]
   /\ RB' = RB + B7[P7+2]
   /\ UNCHANGED <<P0,P1,P2,P3,P4,P5,P6>>
   
Next== 
  \/  Move0 \/  Move1 \/  Move2 \/  Move3
  \/  Move4 \/  Move5 \/  Move6 \/  Move7
    
Arrived == 
  /\ (P0=LL) /\ (P1=LL) /\ (P2=LL) /\ (P3=LL)
  /\ (P4=LL) /\ (P5=LL) /\ (P6=LL) /\ (P7=LL)
 
Property == <>Arrived
  
Spec == Init /\ [][Next]_vars 
SFairSpec == Init /\ [][Next]_vars /\ SF_vars (Next)    (*for LTL verification*)

(**************************************************)
(* Property: <>Arrived,  Behavior Spec: SFairSpec *)
(* States: 1636545, Result: TRUE, Time 3m17s      *)
(**************************************************)

(* Model Overview:  setting Temporal formula == "Spec" *)
(* Deadlock Found:  trace for  P0=6 & P4=6 *)
(* PROPERTIES:    <>Arrived     is FALSE, because of implicit stuttering*)

(* Model Overview:  setting Temporal formula == "SFairSpec" *)
(* Deadlock Found:  trace for P0=6 & P4=6 (stuttering does not avoids deadlocks) *)
(* PROPERTIES:    <>Arrived     is TRUE, stuttering ignored *)
===============================================