/*
==========================================================
CASE: mini
--------
Concrete (generated) behavioural model, safety properties, and strengthening
invariants. Both generic and concrete models are specified in Interlocking
Dynamic Language (IDL), cf.:

Formal Development and Verification of Railway Control Systems - In the context
of ERTMS/ETCS Level 2. / Vu, Linh Hong;
Kgs. Lyngby : Technical University of Denmark (DTU), 2015.
276p. (DTU Compute PHD-2015; No. 395).
==========================================================
 */
kripke dk_interlocking

encoding

Linear::
  D2U -> [INPUT,"unsigned int",0,0,7]
  U2D -> [INPUT,"unsigned int",0,0,7]
  MODE -> [LOCAL,"unsigned int",0,0,2]
  PREV -> [LOCAL,"unsigned int",0,0,1],
Point::
  S2PM -> [INPUT,"unsigned int",0,0,7]
  P2S -> [INPUT,"unsigned int",0,0,7]
  M2S -> [INPUT,"unsigned int",0,0,7]
  CMD -> [OUTPUT,"unsigned int",0,0,1]
  POS -> [INPUT,"unsigned int",0,0,2]
  MODE -> [LOCAL,"unsigned int",0,0,2]
  PREV -> [LOCAL,"unsigned int",0,0,1],
Route::
  MODE -> [LOCAL,"unsigned int",0,0,4],
Signal::
  ACT -> [INPUT,"unsigned int",0,0,1]
  CMD -> [OUTPUT,"unsigned int",0,0,1]

transrel

([route_dispatching_r_1a] (r_1a.MODE = 0) ==> (r_1a.MODE' = 1)
 [=]
 
 [route_dispatching_r_1b] (r_1b.MODE = 0) ==> (r_1b.MODE' = 1)
 [=]
 
 [route_dispatching_r_2a] (r_2a.MODE = 0) ==> (r_2a.MODE' = 1)
 [=]
 
 [route_dispatching_r_2b] (r_2b.MODE = 0) ==> (r_2b.MODE' = 1)
 [=]
 
 [route_dispatching_r_3_] (r_3_.MODE = 0) ==> (r_3_.MODE' = 1)
 [=]
 
 [route_dispatching_r_4_] (r_4_.MODE = 0) ==> (r_4_.MODE' = 1)
 [=]
 
 [route_dispatching_r_5a] (r_5a.MODE = 0) ==> (r_5a.MODE' = 1)
 [=]
 
 [route_dispatching_r_5b] (r_5b.MODE = 0) ==> (r_5b.MODE' = 1)
 [=]
 
 [route_dispatching_r_6a] (r_6a.MODE = 0) ==> (r_6a.MODE' = 1)
 [=]
 
 [route_dispatching_r_6b] (r_6b.MODE = 0) ==> (r_6b.MODE' = 1)
 [=]
 
 [route_dispatching_r_7_] (r_7_.MODE = 0) ==> (r_7_.MODE' = 1)
 [=]
 
 [route_dispatching_r_8_] (r_8_.MODE = 0) ==> (r_8_.MODE' = 1))
[=]

(([route_allocating_r_1a]
  (r_1a.MODE = 1) /\
  ((r_1b.MODE ~= 2 /\ r_1b.MODE ~= 3) /\
   (r_2a.MODE ~= 2 /\ r_2a.MODE ~= 3) /\
   (r_2b.MODE ~= 2 /\ r_2b.MODE ~= 3) /\
   (r_3_.MODE ~= 2 /\ r_3_.MODE ~= 3) /\
   (r_4_.MODE ~= 2 /\ r_4_.MODE ~= 3) /\
   (r_5a.MODE ~= 2 /\ r_5a.MODE ~= 3) /\
   (r_5b.MODE ~= 2 /\ r_5b.MODE ~= 3) /\
   (r_6b.MODE ~= 2 /\ r_6b.MODE ~= 3) /\
   (r_7_.MODE ~= 2 /\ r_7_.MODE ~= 3)) /\
  ((t10.D2U + t10.U2D = 0) /\ (t12.D2U + t12.U2D = 0) /\
   (t11.S2PM + t11.P2S + t11.M2S = 0)) /\
  ((t10.MODE = 0) /\ (t12.MODE = 0) /\ (t11.MODE = 0)) /\
  (t13.MODE = 0 \/ t13.POS = 1)
  ==>
  (r_1a.MODE' = 2) /\ ((t11.CMD' = 0) /\ (t13.CMD' = 1)) /\
  ((mb11.CMD' = 0) /\ (mb12.CMD' = 0) /\ (mb20.CMD' = 0)) /\
  ((t10.MODE' = 1) /\ (t12.MODE' = 1) /\ (t11.MODE' = 1))
  [=]
  
  [route_allocating_r_1b]
  (r_1b.MODE = 1) /\
  ((r_1a.MODE ~= 2 /\ r_1a.MODE ~= 3) /\
   (r_2a.MODE ~= 2 /\ r_2a.MODE ~= 3) /\
   (r_2b.MODE ~= 2 /\ r_2b.MODE ~= 3) /\
   (r_3_.MODE ~= 2 /\ r_3_.MODE ~= 3) /\
   (r_5a.MODE ~= 2 /\ r_5a.MODE ~= 3) /\
   (r_5b.MODE ~= 2 /\ r_5b.MODE ~= 3) /\
   (r_6a.MODE ~= 2 /\ r_6a.MODE ~= 3) /\
   (r_6b.MODE ~= 2 /\ r_6b.MODE ~= 3) /\
   (r_7_.MODE ~= 2 /\ r_7_.MODE ~= 3) /\
   (r_8_.MODE ~= 2 /\ r_8_.MODE ~= 3)) /\
  ((t10.D2U + t10.U2D = 0) /\ (t12.D2U + t12.U2D = 0) /\
   (t11.S2PM + t11.P2S + t11.M2S = 0)) /\
  ((t10.MODE = 0) /\ (t12.MODE = 0) /\ (t11.MODE = 0))
  ==>
  (r_1b.MODE' = 2) /\ (t11.CMD' = 0) /\
  ((mb11.CMD' = 0) /\ (mb12.CMD' = 0) /\ (mb15.CMD' = 0) /\
   (mb20.CMD' = 0) /\ (mb21.CMD' = 0)) /\
  ((t10.MODE' = 1) /\ (t12.MODE' = 1) /\ (t11.MODE' = 1))
  [=]
  
  [route_allocating_r_2a]
  (r_2a.MODE = 1) /\
  ((r_1a.MODE ~= 2 /\ r_1a.MODE ~= 3) /\
   (r_1b.MODE ~= 2 /\ r_1b.MODE ~= 3) /\
   (r_2b.MODE ~= 2 /\ r_2b.MODE ~= 3) /\
   (r_3_.MODE ~= 2 /\ r_3_.MODE ~= 3) /\
   (r_5b.MODE ~= 2 /\ r_5b.MODE ~= 3) /\
   (r_6a.MODE ~= 2 /\ r_6a.MODE ~= 3) /\
   (r_6b.MODE ~= 2 /\ r_6b.MODE ~= 3) /\
   (r_7_.MODE ~= 2 /\ r_7_.MODE ~= 3) /\
   (r_8_.MODE ~= 2 /\ r_8_.MODE ~= 3)) /\
  ((t10.D2U + t10.U2D = 0) /\ (t20.D2U + t20.U2D = 0) /\
   (t11.S2PM + t11.P2S + t11.M2S = 0)) /\
  ((t10.MODE = 0) /\ (t20.MODE = 0) /\ (t11.MODE = 0)) /\
  (t13.MODE = 0 \/ t13.POS = 0)
  ==>
  (r_2a.MODE' = 2) /\ ((t11.CMD' = 1) /\ (t13.CMD' = 0)) /\
  ((mb11.CMD' = 0) /\ (mb12.CMD' = 0) /\ (mb20.CMD' = 0)) /\
  ((t10.MODE' = 1) /\ (t20.MODE' = 1) /\ (t11.MODE' = 1))
  [=]
  
  [route_allocating_r_2b]
  (r_2b.MODE = 1) /\
  ((r_1a.MODE ~= 2 /\ r_1a.MODE ~= 3) /\
   (r_1b.MODE ~= 2 /\ r_1b.MODE ~= 3) /\
   (r_2a.MODE ~= 2 /\ r_2a.MODE ~= 3) /\
   (r_3_.MODE ~= 2 /\ r_3_.MODE ~= 3) /\
   (r_4_.MODE ~= 2 /\ r_4_.MODE ~= 3) /\
   (r_5a.MODE ~= 2 /\ r_5a.MODE ~= 3) /\
   (r_5b.MODE ~= 2 /\ r_5b.MODE ~= 3) /\
   (r_6a.MODE ~= 2 /\ r_6a.MODE ~= 3) /\
   (r_6b.MODE ~= 2 /\ r_6b.MODE ~= 3) /\
   (r_7_.MODE ~= 2 /\ r_7_.MODE ~= 3)) /\
  ((t10.D2U + t10.U2D = 0) /\ (t20.D2U + t20.U2D = 0) /\
   (t11.S2PM + t11.P2S + t11.M2S = 0)) /\
  ((t10.MODE = 0) /\ (t20.MODE = 0) /\ (t11.MODE = 0))
  ==>
  (r_2b.MODE' = 2) /\ (t11.CMD' = 1) /\
  ((mb11.CMD' = 0) /\ (mb12.CMD' = 0) /\ (mb13.CMD' = 0) /\
   (mb15.CMD' = 0) /\ (mb20.CMD' = 0)) /\
  ((t10.MODE' = 1) /\ (t20.MODE' = 1) /\ (t11.MODE' = 1))
  [=]
  
  [route_allocating_r_3_]
  (r_3_.MODE = 1) /\
  ((r_1a.MODE ~= 2 /\ r_1a.MODE ~= 3) /\
   (r_1b.MODE ~= 2 /\ r_1b.MODE ~= 3) /\
   (r_2a.MODE ~= 2 /\ r_2a.MODE ~= 3) /\
   (r_2b.MODE ~= 2 /\ r_2b.MODE ~= 3) /\
   (r_5a.MODE ~= 2 /\ r_5a.MODE ~= 3) /\
   (r_6b.MODE ~= 2 /\ r_6b.MODE ~= 3) /\
   (r_7_.MODE ~= 2 /\ r_7_.MODE ~= 3)) /\
  ((t10.D2U + t10.U2D = 0) /\ (t11.S2PM + t11.P2S + t11.M2S = 0)) /\
  ((t10.MODE = 0) /\ (t11.MODE = 0))
  ==>
  (r_3_.MODE' = 2) /\ (t11.CMD' = 0) /\
  ((mb10.CMD' = 0) /\ (mb20.CMD' = 0)) /\
  ((t10.MODE' = 1) /\ (t11.MODE' = 1))
  [=]
  
  [route_allocating_r_4_]
  (r_4_.MODE = 1) /\
  ((r_1a.MODE ~= 2 /\ r_1a.MODE ~= 3) /\
   (r_2b.MODE ~= 2 /\ r_2b.MODE ~= 3) /\
   (r_5a.MODE ~= 2 /\ r_5a.MODE ~= 3) /\
   (r_5b.MODE ~= 2 /\ r_5b.MODE ~= 3) /\
   (r_6a.MODE ~= 2 /\ r_6a.MODE ~= 3) /\
   (r_6b.MODE ~= 2 /\ r_6b.MODE ~= 3) /\
   (r_8_.MODE ~= 2 /\ r_8_.MODE ~= 3)) /\
  ((t14.D2U + t14.U2D = 0) /\ (t13.S2PM + t13.P2S + t13.M2S = 0)) /\
  ((t14.MODE = 0) /\ (t13.MODE = 0))
  ==>
  (r_4_.MODE' = 2) /\ (t13.CMD' = 0) /\
  ((mb15.CMD' = 0) /\ (mb21.CMD' = 0)) /\
  ((t14.MODE' = 1) /\ (t13.MODE' = 1))
  [=]
  
  [route_allocating_r_5a]
  (r_5a.MODE = 1) /\
  ((r_1a.MODE ~= 2 /\ r_1a.MODE ~= 3) /\
   (r_1b.MODE ~= 2 /\ r_1b.MODE ~= 3) /\
   (r_2b.MODE ~= 2 /\ r_2b.MODE ~= 3) /\
   (r_3_.MODE ~= 2 /\ r_3_.MODE ~= 3) /\
   (r_4_.MODE ~= 2 /\ r_4_.MODE ~= 3) /\
   (r_5b.MODE ~= 2 /\ r_5b.MODE ~= 3) /\
   (r_6a.MODE ~= 2 /\ r_6a.MODE ~= 3) /\
   (r_6b.MODE ~= 2 /\ r_6b.MODE ~= 3) /\
   (r_8_.MODE ~= 2 /\ r_8_.MODE ~= 3)) /\
  ((t12.D2U + t12.U2D = 0) /\ (t14.D2U + t14.U2D = 0) /\
   (t13.S2PM + t13.P2S + t13.M2S = 0)) /\
  ((t12.MODE = 0) /\ (t14.MODE = 0) /\ (t13.MODE = 0)) /\
  (t11.MODE = 0 \/ t11.POS = 1)
  ==>
  (r_5a.MODE' = 2) /\ ((t11.CMD' = 1) /\ (t13.CMD' = 0)) /\
  ((mb13.CMD' = 0) /\ (mb14.CMD' = 0) /\ (mb21.CMD' = 0)) /\
  ((t12.MODE' = 1) /\ (t14.MODE' = 1) /\ (t13.MODE' = 1))
  [=]
  
  [route_allocating_r_5b]
  (r_5b.MODE = 1) /\
  ((r_1a.MODE ~= 2 /\ r_1a.MODE ~= 3) /\
   (r_1b.MODE ~= 2 /\ r_1b.MODE ~= 3) /\
   (r_2a.MODE ~= 2 /\ r_2a.MODE ~= 3) /\
   (r_2b.MODE ~= 2 /\ r_2b.MODE ~= 3) /\
   (r_4_.MODE ~= 2 /\ r_4_.MODE ~= 3) /\
   (r_5a.MODE ~= 2 /\ r_5a.MODE ~= 3) /\
   (r_6a.MODE ~= 2 /\ r_6a.MODE ~= 3) /\
   (r_6b.MODE ~= 2 /\ r_6b.MODE ~= 3) /\
   (r_7_.MODE ~= 2 /\ r_7_.MODE ~= 3) /\
   (r_8_.MODE ~= 2 /\ r_8_.MODE ~= 3)) /\
  ((t12.D2U + t12.U2D = 0) /\ (t14.D2U + t14.U2D = 0) /\
   (t13.S2PM + t13.P2S + t13.M2S = 0)) /\
  ((t12.MODE = 0) /\ (t14.MODE = 0) /\ (t13.MODE = 0))
  ==>
  (r_5b.MODE' = 2) /\ (t13.CMD' = 0) /\
  ((mb10.CMD' = 0) /\ (mb13.CMD' = 0) /\ (mb14.CMD' = 0) /\
   (mb20.CMD' = 0) /\ (mb21.CMD' = 0)) /\
  ((t12.MODE' = 1) /\ (t14.MODE' = 1) /\ (t13.MODE' = 1))
  [=]
  
  [route_allocating_r_6a]
  (r_6a.MODE = 1) /\
  ((r_1b.MODE ~= 2 /\ r_1b.MODE ~= 3) /\
   (r_2a.MODE ~= 2 /\ r_2a.MODE ~= 3) /\
   (r_2b.MODE ~= 2 /\ r_2b.MODE ~= 3) /\
   (r_4_.MODE ~= 2 /\ r_4_.MODE ~= 3) /\
   (r_5a.MODE ~= 2 /\ r_5a.MODE ~= 3) /\
   (r_5b.MODE ~= 2 /\ r_5b.MODE ~= 3) /\
   (r_6b.MODE ~= 2 /\ r_6b.MODE ~= 3) /\
   (r_7_.MODE ~= 2 /\ r_7_.MODE ~= 3) /\
   (r_8_.MODE ~= 2 /\ r_8_.MODE ~= 3)) /\
  ((t14.D2U + t14.U2D = 0) /\ (t20.D2U + t20.U2D = 0) /\
   (t13.S2PM + t13.P2S + t13.M2S = 0)) /\
  ((t14.MODE = 0) /\ (t20.MODE = 0) /\ (t13.MODE = 0)) /\
  (t11.MODE = 0 \/ t11.POS = 0)
  ==>
  (r_6a.MODE' = 2) /\ ((t11.CMD' = 0) /\ (t13.CMD' = 1)) /\
  ((mb13.CMD' = 0) /\ (mb14.CMD' = 0) /\ (mb21.CMD' = 0)) /\
  ((t14.MODE' = 1) /\ (t20.MODE' = 1) /\ (t13.MODE' = 1))
  [=]
  
  [route_allocating_r_6b]
  (r_6b.MODE = 1) /\
  ((r_1a.MODE ~= 2 /\ r_1a.MODE ~= 3) /\
   (r_1b.MODE ~= 2 /\ r_1b.MODE ~= 3) /\
   (r_2a.MODE ~= 2 /\ r_2a.MODE ~= 3) /\
   (r_2b.MODE ~= 2 /\ r_2b.MODE ~= 3) /\
   (r_3_.MODE ~= 2 /\ r_3_.MODE ~= 3) /\
   (r_4_.MODE ~= 2 /\ r_4_.MODE ~= 3) /\
   (r_5a.MODE ~= 2 /\ r_5a.MODE ~= 3) /\
   (r_5b.MODE ~= 2 /\ r_5b.MODE ~= 3) /\
   (r_6a.MODE ~= 2 /\ r_6a.MODE ~= 3) /\
   (r_8_.MODE ~= 2 /\ r_8_.MODE ~= 3)) /\
  ((t14.D2U + t14.U2D = 0) /\ (t20.D2U + t20.U2D = 0) /\
   (t13.S2PM + t13.P2S + t13.M2S = 0)) /\
  ((t14.MODE = 0) /\ (t20.MODE = 0) /\ (t13.MODE = 0))
  ==>
  (r_6b.MODE' = 2) /\ (t13.CMD' = 1) /\
  ((mb10.CMD' = 0) /\ (mb12.CMD' = 0) /\ (mb13.CMD' = 0) /\
   (mb14.CMD' = 0) /\ (mb21.CMD' = 0)) /\
  ((t14.MODE' = 1) /\ (t20.MODE' = 1) /\ (t13.MODE' = 1))
  [=]
  
  [route_allocating_r_7_]
  (r_7_.MODE = 1) /\
  ((r_1a.MODE ~= 2 /\ r_1a.MODE ~= 3) /\
   (r_1b.MODE ~= 2 /\ r_1b.MODE ~= 3) /\
   (r_2a.MODE ~= 2 /\ r_2a.MODE ~= 3) /\
   (r_2b.MODE ~= 2 /\ r_2b.MODE ~= 3) /\
   (r_3_.MODE ~= 2 /\ r_3_.MODE ~= 3) /\
   (r_5b.MODE ~= 2 /\ r_5b.MODE ~= 3) /\
   (r_6a.MODE ~= 2 /\ r_6a.MODE ~= 3)) /\
  ((t10.D2U + t10.U2D = 0) /\ (t11.S2PM + t11.P2S + t11.M2S = 0)) /\
  ((t10.MODE = 0) /\ (t11.MODE = 0))
  ==>
  (r_7_.MODE' = 2) /\ (t11.CMD' = 1) /\
  ((mb10.CMD' = 0) /\ (mb12.CMD' = 0)) /\
  ((t10.MODE' = 1) /\ (t11.MODE' = 1))
  [=]
  
  [route_allocating_r_8_]
  (r_8_.MODE = 1) /\
  ((r_1b.MODE ~= 2 /\ r_1b.MODE ~= 3) /\
   (r_2a.MODE ~= 2 /\ r_2a.MODE ~= 3) /\
   (r_4_.MODE ~= 2 /\ r_4_.MODE ~= 3) /\
   (r_5a.MODE ~= 2 /\ r_5a.MODE ~= 3) /\
   (r_5b.MODE ~= 2 /\ r_5b.MODE ~= 3) /\
   (r_6a.MODE ~= 2 /\ r_6a.MODE ~= 3) /\
   (r_6b.MODE ~= 2 /\ r_6b.MODE ~= 3)) /\
  ((t14.D2U + t14.U2D = 0) /\ (t13.S2PM + t13.P2S + t13.M2S = 0)) /\
  ((t14.MODE = 0) /\ (t13.MODE = 0))
  ==>
  (r_8_.MODE' = 2) /\ (t13.CMD' = 1) /\
  ((mb13.CMD' = 0) /\ (mb15.CMD' = 0)) /\
  ((t14.MODE' = 1) /\ (t13.MODE' = 1))
  [=]
  
  [route_lock_r_1a]
  r_1a.MODE = 2 /\
  ((mb11.ACT = 0) /\ (mb12.ACT = 0) /\ (mb20.ACT = 0)) /\
  ((t11.POS = 0) /\ (t13.POS = 1)) /\
  ((t10.D2U + t10.U2D = 0) /\ (t12.D2U + t12.U2D = 0) /\
   (t11.S2PM + t11.P2S + t11.M2S = 0)) /\
  ((t10.MODE = 1) /\ (t12.MODE = 1) /\ (t11.MODE = 1))
  ==> r_1a.MODE' = 3 /\ mb10.CMD' = 1
  [=]
  
  [route_lock_r_1b]
  r_1b.MODE = 2 /\
  ((mb11.ACT = 0) /\ (mb12.ACT = 0) /\ (mb15.ACT = 0) /\
   (mb20.ACT = 0) /\ (mb21.ACT = 0)) /\ (t11.POS = 0) /\
  ((t10.D2U + t10.U2D = 0) /\ (t12.D2U + t12.U2D = 0) /\
   (t11.S2PM + t11.P2S + t11.M2S = 0)) /\
  ((t10.MODE = 1) /\ (t12.MODE = 1) /\ (t11.MODE = 1))
  ==> r_1b.MODE' = 3 /\ mb10.CMD' = 1
  [=]
  
  [route_lock_r_2a]
  r_2a.MODE = 2 /\
  ((mb11.ACT = 0) /\ (mb12.ACT = 0) /\ (mb20.ACT = 0)) /\
  ((t11.POS = 1) /\ (t13.POS = 0)) /\
  ((t10.D2U + t10.U2D = 0) /\ (t20.D2U + t20.U2D = 0) /\
   (t11.S2PM + t11.P2S + t11.M2S = 0)) /\
  ((t10.MODE = 1) /\ (t20.MODE = 1) /\ (t11.MODE = 1))
  ==> r_2a.MODE' = 3 /\ mb10.CMD' = 1
  [=]
  
  [route_lock_r_2b]
  r_2b.MODE = 2 /\
  ((mb11.ACT = 0) /\ (mb12.ACT = 0) /\ (mb13.ACT = 0) /\
   (mb15.ACT = 0) /\ (mb20.ACT = 0)) /\ (t11.POS = 1) /\
  ((t10.D2U + t10.U2D = 0) /\ (t20.D2U + t20.U2D = 0) /\
   (t11.S2PM + t11.P2S + t11.M2S = 0)) /\
  ((t10.MODE = 1) /\ (t20.MODE = 1) /\ (t11.MODE = 1))
  ==> r_2b.MODE' = 3 /\ mb10.CMD' = 1
  [=]
  
  [route_lock_r_3_]
  r_3_.MODE = 2 /\ ((mb10.ACT = 0) /\ (mb20.ACT = 0)) /\ (t11.POS = 0) /\
  ((t10.D2U + t10.U2D = 0) /\ (t11.S2PM + t11.P2S + t11.M2S = 0)) /\
  ((t10.MODE = 1) /\ (t11.MODE = 1))
  ==> r_3_.MODE' = 3 /\ mb12.CMD' = 1
  [=]
  
  [route_lock_r_4_]
  r_4_.MODE = 2 /\ ((mb15.ACT = 0) /\ (mb21.ACT = 0)) /\ (t13.POS = 0) /\
  ((t14.D2U + t14.U2D = 0) /\ (t13.S2PM + t13.P2S + t13.M2S = 0)) /\
  ((t14.MODE = 1) /\ (t13.MODE = 1))
  ==> r_4_.MODE' = 3 /\ mb13.CMD' = 1
  [=]
  
  [route_lock_r_5a]
  r_5a.MODE = 2 /\
  ((mb13.ACT = 0) /\ (mb14.ACT = 0) /\ (mb21.ACT = 0)) /\
  ((t11.POS = 1) /\ (t13.POS = 0)) /\
  ((t12.D2U + t12.U2D = 0) /\ (t14.D2U + t14.U2D = 0) /\
   (t13.S2PM + t13.P2S + t13.M2S = 0)) /\
  ((t12.MODE = 1) /\ (t14.MODE = 1) /\ (t13.MODE = 1))
  ==> r_5a.MODE' = 3 /\ mb15.CMD' = 1
  [=]
  
  [route_lock_r_5b]
  r_5b.MODE = 2 /\
  ((mb10.ACT = 0) /\ (mb13.ACT = 0) /\ (mb14.ACT = 0) /\
   (mb20.ACT = 0) /\ (mb21.ACT = 0)) /\ (t13.POS = 0) /\
  ((t12.D2U + t12.U2D = 0) /\ (t14.D2U + t14.U2D = 0) /\
   (t13.S2PM + t13.P2S + t13.M2S = 0)) /\
  ((t12.MODE = 1) /\ (t14.MODE = 1) /\ (t13.MODE = 1))
  ==> r_5b.MODE' = 3 /\ mb15.CMD' = 1
  [=]
  
  [route_lock_r_6a]
  r_6a.MODE = 2 /\
  ((mb13.ACT = 0) /\ (mb14.ACT = 0) /\ (mb21.ACT = 0)) /\
  ((t11.POS = 0) /\ (t13.POS = 1)) /\
  ((t14.D2U + t14.U2D = 0) /\ (t20.D2U + t20.U2D = 0) /\
   (t13.S2PM + t13.P2S + t13.M2S = 0)) /\
  ((t14.MODE = 1) /\ (t20.MODE = 1) /\ (t13.MODE = 1))
  ==> r_6a.MODE' = 3 /\ mb15.CMD' = 1
  [=]
  
  [route_lock_r_6b]
  r_6b.MODE = 2 /\
  ((mb10.ACT = 0) /\ (mb12.ACT = 0) /\ (mb13.ACT = 0) /\
   (mb14.ACT = 0) /\ (mb21.ACT = 0)) /\ (t13.POS = 1) /\
  ((t14.D2U + t14.U2D = 0) /\ (t20.D2U + t20.U2D = 0) /\
   (t13.S2PM + t13.P2S + t13.M2S = 0)) /\
  ((t14.MODE = 1) /\ (t20.MODE = 1) /\ (t13.MODE = 1))
  ==> r_6b.MODE' = 3 /\ mb15.CMD' = 1
  [=]
  
  [route_lock_r_7_]
  r_7_.MODE = 2 /\ ((mb10.ACT = 0) /\ (mb12.ACT = 0)) /\ (t11.POS = 1) /\
  ((t10.D2U + t10.U2D = 0) /\ (t11.S2PM + t11.P2S + t11.M2S = 0)) /\
  ((t10.MODE = 1) /\ (t11.MODE = 1))
  ==> r_7_.MODE' = 3 /\ mb20.CMD' = 1
  [=]
  
  [route_lock_r_8_]
  r_8_.MODE = 2 /\ ((mb13.ACT = 0) /\ (mb15.ACT = 0)) /\ (t13.POS = 1) /\
  ((t14.D2U + t14.U2D = 0) /\ (t13.S2PM + t13.P2S + t13.M2S = 0)) /\
  ((t14.MODE = 1) /\ (t13.MODE = 1))
  ==> r_8_.MODE' = 3 /\ mb21.CMD' = 1
  [=]
  
  [route_in_use_r_1a] r_1a.MODE = 3 /\ ~(t10.D2U + t10.U2D = 0) ==>
  r_1a.MODE' = 4 /\ mb10.CMD' = 0 /\ t10.MODE' = 2
  [=]
  
  [route_in_use_r_1b] r_1b.MODE = 3 /\ ~(t10.D2U + t10.U2D = 0) ==>
  r_1b.MODE' = 4 /\ mb10.CMD' = 0 /\ t10.MODE' = 2
  [=]
  
  [route_in_use_r_2a] r_2a.MODE = 3 /\ ~(t10.D2U + t10.U2D = 0) ==>
  r_2a.MODE' = 4 /\ mb10.CMD' = 0 /\ t10.MODE' = 2
  [=]
  
  [route_in_use_r_2b] r_2b.MODE = 3 /\ ~(t10.D2U + t10.U2D = 0) ==>
  r_2b.MODE' = 4 /\ mb10.CMD' = 0 /\ t10.MODE' = 2
  [=]
  
  [route_in_use_r_3_] r_3_.MODE = 3 /\ ~(t11.S2PM + t11.P2S + t11.M2S = 0) ==>
  r_3_.MODE' = 4 /\ mb12.CMD' = 0 /\ t11.MODE' = 2
  [=]
  
  [route_in_use_r_4_] r_4_.MODE = 3 /\ ~(t13.S2PM + t13.P2S + t13.M2S = 0) ==>
  r_4_.MODE' = 4 /\ mb13.CMD' = 0 /\ t13.MODE' = 2
  [=]
  
  [route_in_use_r_5a] r_5a.MODE = 3 /\ ~(t14.D2U + t14.U2D = 0) ==>
  r_5a.MODE' = 4 /\ mb15.CMD' = 0 /\ t14.MODE' = 2
  [=]
  
  [route_in_use_r_5b] r_5b.MODE = 3 /\ ~(t14.D2U + t14.U2D = 0) ==>
  r_5b.MODE' = 4 /\ mb15.CMD' = 0 /\ t14.MODE' = 2
  [=]
  
  [route_in_use_r_6a] r_6a.MODE = 3 /\ ~(t14.D2U + t14.U2D = 0) ==>
  r_6a.MODE' = 4 /\ mb15.CMD' = 0 /\ t14.MODE' = 2
  [=]
  
  [route_in_use_r_6b] r_6b.MODE = 3 /\ ~(t14.D2U + t14.U2D = 0) ==>
  r_6b.MODE' = 4 /\ mb15.CMD' = 0 /\ t14.MODE' = 2
  [=]
  
  [route_in_use_r_7_] r_7_.MODE = 3 /\ ~(t11.S2PM + t11.P2S + t11.M2S = 0) ==>
  r_7_.MODE' = 4 /\ mb20.CMD' = 0 /\ t11.MODE' = 2
  [=]
  
  [route_in_use_r_8_] r_8_.MODE = 3 /\ ~(t13.S2PM + t13.P2S + t13.M2S = 0) ==>
  r_8_.MODE' = 4 /\ mb21.CMD' = 0 /\ t13.MODE' = 2
  [=]
  
  [element_in_use_r_1a_t12]
  t11.MODE = 2 /\ r_1a.MODE = 4 /\ t12.MODE = 1 /\ ~(t12.D2U + t12.U2D = 0)
  ==> t12.MODE' = 2
  [=]
  
  [element_in_use_r_1a_t11]
  t10.MODE = 2 /\ r_1a.MODE = 4 /\ t11.MODE = 1 /\
  ~(t11.S2PM + t11.P2S + t11.M2S = 0) /\ t11.POS = 0 /\ t12.MODE = 1
  ==> t11.MODE' = 2
  [=]
  
  [element_in_use_r_1b_t12]
  t11.MODE = 2 /\ r_1b.MODE = 4 /\ t12.MODE = 1 /\ ~(t12.D2U + t12.U2D = 0)
  ==> t12.MODE' = 2
  [=]
  
  [element_in_use_r_1b_t11]
  t10.MODE = 2 /\ r_1b.MODE = 4 /\ t11.MODE = 1 /\
  ~(t11.S2PM + t11.P2S + t11.M2S = 0) /\ t11.POS = 0 /\ t12.MODE = 1
  ==> t11.MODE' = 2
  [=]
  
  [element_in_use_r_2a_t20]
  t11.MODE = 2 /\ r_2a.MODE = 4 /\ t20.MODE = 1 /\ ~(t20.D2U + t20.U2D = 0)
  ==> t20.MODE' = 2
  [=]
  
  [element_in_use_r_2a_t11]
  t10.MODE = 2 /\ r_2a.MODE = 4 /\ t11.MODE = 1 /\
  ~(t11.S2PM + t11.P2S + t11.M2S = 0) /\ t11.POS = 1 /\ t20.MODE = 1
  ==> t11.MODE' = 2
  [=]
  
  [element_in_use_r_2b_t20]
  t11.MODE = 2 /\ r_2b.MODE = 4 /\ t20.MODE = 1 /\ ~(t20.D2U + t20.U2D = 0)
  ==> t20.MODE' = 2
  [=]
  
  [element_in_use_r_2b_t11]
  t10.MODE = 2 /\ r_2b.MODE = 4 /\ t11.MODE = 1 /\
  ~(t11.S2PM + t11.P2S + t11.M2S = 0) /\ t11.POS = 1 /\ t20.MODE = 1
  ==> t11.MODE' = 2
  [=]
  
  [element_in_use_r_3__t10]
  t11.MODE = 2 /\ r_3_.MODE = 4 /\ t10.MODE = 1 /\ ~(t10.D2U + t10.U2D = 0)
  ==> t10.MODE' = 2
  [=]
  
  [element_in_use_r_4__t14]
  t13.MODE = 2 /\ r_4_.MODE = 4 /\ t14.MODE = 1 /\ ~(t14.D2U + t14.U2D = 0)
  ==> t14.MODE' = 2
  [=]
  
  [element_in_use_r_5a_t12]
  t13.MODE = 2 /\ r_5a.MODE = 4 /\ t12.MODE = 1 /\ ~(t12.D2U + t12.U2D = 0)
  ==> t12.MODE' = 2
  [=]
  
  [element_in_use_r_5a_t13]
  t14.MODE = 2 /\ r_5a.MODE = 4 /\ t13.MODE = 1 /\
  ~(t13.S2PM + t13.P2S + t13.M2S = 0) /\ t13.POS = 0 /\ t12.MODE = 1
  ==> t13.MODE' = 2
  [=]
  
  [element_in_use_r_5b_t12]
  t13.MODE = 2 /\ r_5b.MODE = 4 /\ t12.MODE = 1 /\ ~(t12.D2U + t12.U2D = 0)
  ==> t12.MODE' = 2
  [=]
  
  [element_in_use_r_5b_t13]
  t14.MODE = 2 /\ r_5b.MODE = 4 /\ t13.MODE = 1 /\
  ~(t13.S2PM + t13.P2S + t13.M2S = 0) /\ t13.POS = 0 /\ t12.MODE = 1
  ==> t13.MODE' = 2
  [=]
  
  [element_in_use_r_6a_t20]
  t13.MODE = 2 /\ r_6a.MODE = 4 /\ t20.MODE = 1 /\ ~(t20.D2U + t20.U2D = 0)
  ==> t20.MODE' = 2
  [=]
  
  [element_in_use_r_6a_t13]
  t14.MODE = 2 /\ r_6a.MODE = 4 /\ t13.MODE = 1 /\
  ~(t13.S2PM + t13.P2S + t13.M2S = 0) /\ t13.POS = 1 /\ t20.MODE = 1
  ==> t13.MODE' = 2
  [=]
  
  [element_in_use_r_6b_t20]
  t13.MODE = 2 /\ r_6b.MODE = 4 /\ t20.MODE = 1 /\ ~(t20.D2U + t20.U2D = 0)
  ==> t20.MODE' = 2
  [=]
  
  [element_in_use_r_6b_t13]
  t14.MODE = 2 /\ r_6b.MODE = 4 /\ t13.MODE = 1 /\
  ~(t13.S2PM + t13.P2S + t13.M2S = 0) /\ t13.POS = 1 /\ t20.MODE = 1
  ==> t13.MODE' = 2
  [=]
  
  [element_in_use_r_7__t10]
  t11.MODE = 2 /\ r_7_.MODE = 4 /\ t10.MODE = 1 /\ ~(t10.D2U + t10.U2D = 0)
  ==> t10.MODE' = 2
  [=]
  
  [element_in_use_r_8__t14]
  t13.MODE = 2 /\ r_8_.MODE = 4 /\ t14.MODE = 1 /\ ~(t14.D2U + t14.U2D = 0)
  ==> t14.MODE' = 2
  [=]
  
  [sequential_release_e_r_1a_t10]
  r_1a.MODE = 4 /\ t10.MODE = 2 /\ (t10.D2U + t10.U2D = 0) /\
  t11.PREV = 0 /\ t11.MODE = 2 /\ (((t11.S2PM & 2) >> 1) ~= 0) /\
  t11.POS = 0
  ==> t10.MODE' = 0 /\ t10.PREV' = 0 /\ t11.PREV' = 1
  [=]
  
  [sequential_release_e_r_1a_t11]
  r_1a.MODE = 4 /\ t11.MODE = 2 /\
  (t11.S2PM + t11.P2S + t11.M2S = 0) /\ t11.PREV = 1 /\
  t12.PREV = 0 /\ t12.MODE = 2 /\ (((t12.D2U & 2) >> 1) ~= 0) /\
  t11.POS = 0
  ==> t11.MODE' = 0 /\ t11.PREV' = 0 /\ t12.PREV' = 1
  [=]
  
  [sequential_release_e_r_1b_t10]
  r_1b.MODE = 4 /\ t10.MODE = 2 /\ (t10.D2U + t10.U2D = 0) /\
  t11.PREV = 0 /\ t11.MODE = 2 /\ (((t11.S2PM & 2) >> 1) ~= 0) /\
  t11.POS = 0
  ==> t10.MODE' = 0 /\ t10.PREV' = 0 /\ t11.PREV' = 1
  [=]
  
  [sequential_release_e_r_1b_t11]
  r_1b.MODE = 4 /\ t11.MODE = 2 /\
  (t11.S2PM + t11.P2S + t11.M2S = 0) /\ t11.PREV = 1 /\
  t12.PREV = 0 /\ t12.MODE = 2 /\ (((t12.D2U & 2) >> 1) ~= 0) /\
  t11.POS = 0
  ==> t11.MODE' = 0 /\ t11.PREV' = 0 /\ t12.PREV' = 1
  [=]
  
  [sequential_release_e_r_2a_t10]
  r_2a.MODE = 4 /\ t10.MODE = 2 /\ (t10.D2U + t10.U2D = 0) /\
  t11.PREV = 0 /\ t11.MODE = 2 /\ (((t11.S2PM & 2) >> 1) ~= 0) /\
  t11.POS = 1
  ==> t10.MODE' = 0 /\ t10.PREV' = 0 /\ t11.PREV' = 1
  [=]
  
  [sequential_release_e_r_2a_t11]
  r_2a.MODE = 4 /\ t11.MODE = 2 /\
  (t11.S2PM + t11.P2S + t11.M2S = 0) /\ t11.PREV = 1 /\
  t20.PREV = 0 /\ t20.MODE = 2 /\ (((t20.D2U & 2) >> 1) ~= 0) /\
  t11.POS = 1
  ==> t11.MODE' = 0 /\ t11.PREV' = 0 /\ t20.PREV' = 1
  [=]
  
  [sequential_release_e_r_2b_t10]
  r_2b.MODE = 4 /\ t10.MODE = 2 /\ (t10.D2U + t10.U2D = 0) /\
  t11.PREV = 0 /\ t11.MODE = 2 /\ (((t11.S2PM & 2) >> 1) ~= 0) /\
  t11.POS = 1
  ==> t10.MODE' = 0 /\ t10.PREV' = 0 /\ t11.PREV' = 1
  [=]
  
  [sequential_release_e_r_2b_t11]
  r_2b.MODE = 4 /\ t11.MODE = 2 /\
  (t11.S2PM + t11.P2S + t11.M2S = 0) /\ t11.PREV = 1 /\
  t20.PREV = 0 /\ t20.MODE = 2 /\ (((t20.D2U & 2) >> 1) ~= 0) /\
  t11.POS = 1
  ==> t11.MODE' = 0 /\ t11.PREV' = 0 /\ t20.PREV' = 1
  [=]
  
  [sequential_release_e_r_3__t11]
  r_3_.MODE = 4 /\ t11.MODE = 2 /\
  (t11.S2PM + t11.P2S + t11.M2S = 0) /\ t10.PREV = 0 /\ t10.MODE = 2 /\
  (((t10.U2D & 2) >> 1) ~= 0) /\ t11.POS = 0
  ==> t11.MODE' = 0 /\ t11.PREV' = 0 /\ t10.PREV' = 1
  [=]
  
  [sequential_release_e_r_4__t13]
  r_4_.MODE = 4 /\ t13.MODE = 2 /\
  (t13.S2PM + t13.P2S + t13.M2S = 0) /\ t14.PREV = 0 /\ t14.MODE = 2 /\
  (((t14.D2U & 2) >> 1) ~= 0) /\ t13.POS = 0
  ==> t13.MODE' = 0 /\ t13.PREV' = 0 /\ t14.PREV' = 1
  [=]
  
  [sequential_release_e_r_5a_t14]
  r_5a.MODE = 4 /\ t14.MODE = 2 /\ (t14.D2U + t14.U2D = 0) /\
  t13.PREV = 0 /\ t13.MODE = 2 /\ (((t13.S2PM & 2) >> 1) ~= 0) /\
  t13.POS = 0
  ==> t14.MODE' = 0 /\ t14.PREV' = 0 /\ t13.PREV' = 1
  [=]
  
  [sequential_release_e_r_5a_t13]
  r_5a.MODE = 4 /\ t13.MODE = 2 /\
  (t13.S2PM + t13.P2S + t13.M2S = 0) /\ t13.PREV = 1 /\
  t12.PREV = 0 /\ t12.MODE = 2 /\ (((t12.U2D & 2) >> 1) ~= 0) /\
  t13.POS = 0
  ==> t13.MODE' = 0 /\ t13.PREV' = 0 /\ t12.PREV' = 1
  [=]
  
  [sequential_release_e_r_5b_t14]
  r_5b.MODE = 4 /\ t14.MODE = 2 /\ (t14.D2U + t14.U2D = 0) /\
  t13.PREV = 0 /\ t13.MODE = 2 /\ (((t13.S2PM & 2) >> 1) ~= 0) /\
  t13.POS = 0
  ==> t14.MODE' = 0 /\ t14.PREV' = 0 /\ t13.PREV' = 1
  [=]
  
  [sequential_release_e_r_5b_t13]
  r_5b.MODE = 4 /\ t13.MODE = 2 /\
  (t13.S2PM + t13.P2S + t13.M2S = 0) /\ t13.PREV = 1 /\
  t12.PREV = 0 /\ t12.MODE = 2 /\ (((t12.U2D & 2) >> 1) ~= 0) /\
  t13.POS = 0
  ==> t13.MODE' = 0 /\ t13.PREV' = 0 /\ t12.PREV' = 1
  [=]
  
  [sequential_release_e_r_6a_t14]
  r_6a.MODE = 4 /\ t14.MODE = 2 /\ (t14.D2U + t14.U2D = 0) /\
  t13.PREV = 0 /\ t13.MODE = 2 /\ (((t13.S2PM & 2) >> 1) ~= 0) /\
  t13.POS = 1
  ==> t14.MODE' = 0 /\ t14.PREV' = 0 /\ t13.PREV' = 1
  [=]
  
  [sequential_release_e_r_6a_t13]
  r_6a.MODE = 4 /\ t13.MODE = 2 /\
  (t13.S2PM + t13.P2S + t13.M2S = 0) /\ t13.PREV = 1 /\
  t20.PREV = 0 /\ t20.MODE = 2 /\ (((t20.U2D & 2) >> 1) ~= 0) /\
  t13.POS = 1
  ==> t13.MODE' = 0 /\ t13.PREV' = 0 /\ t20.PREV' = 1
  [=]
  
  [sequential_release_e_r_6b_t14]
  r_6b.MODE = 4 /\ t14.MODE = 2 /\ (t14.D2U + t14.U2D = 0) /\
  t13.PREV = 0 /\ t13.MODE = 2 /\ (((t13.S2PM & 2) >> 1) ~= 0) /\
  t13.POS = 1
  ==> t14.MODE' = 0 /\ t14.PREV' = 0 /\ t13.PREV' = 1
  [=]
  
  [sequential_release_e_r_6b_t13]
  r_6b.MODE = 4 /\ t13.MODE = 2 /\
  (t13.S2PM + t13.P2S + t13.M2S = 0) /\ t13.PREV = 1 /\
  t20.PREV = 0 /\ t20.MODE = 2 /\ (((t20.U2D & 2) >> 1) ~= 0) /\
  t13.POS = 1
  ==> t13.MODE' = 0 /\ t13.PREV' = 0 /\ t20.PREV' = 1
  [=]
  
  [sequential_release_e_r_7__t11]
  r_7_.MODE = 4 /\ t11.MODE = 2 /\
  (t11.S2PM + t11.P2S + t11.M2S = 0) /\ t10.PREV = 0 /\ t10.MODE = 2 /\
  (((t10.U2D & 2) >> 1) ~= 0) /\ t11.POS = 1
  ==> t11.MODE' = 0 /\ t11.PREV' = 0 /\ t10.PREV' = 1
  [=]
  
  [sequential_release_e_r_8__t13]
  r_8_.MODE = 4 /\ t13.MODE = 2 /\
  (t13.S2PM + t13.P2S + t13.M2S = 0) /\ t14.PREV = 0 /\ t14.MODE = 2 /\
  (((t14.D2U & 2) >> 1) ~= 0) /\ t13.POS = 1
  ==> t13.MODE' = 0 /\ t13.PREV' = 0 /\ t14.PREV' = 1
  [=]
  
  [sequential_release_last_elem_r_1a]
  r_1a.MODE = 4 /\ t12.MODE = 2 /\ (t12.D2U + t12.U2D = 0) /\ t12.PREV = 1
  ==> t12.MODE' = 0 /\ t12.PREV' = 0 /\ r_1a.MODE' = 0
  [=]
  
  [sequential_release_last_elem_r_1b]
  r_1b.MODE = 4 /\ t12.MODE = 2 /\ (t12.D2U + t12.U2D = 0) /\ t12.PREV = 1
  ==> t12.MODE' = 0 /\ t12.PREV' = 0 /\ r_1b.MODE' = 0
  [=]
  
  [sequential_release_last_elem_r_2a]
  r_2a.MODE = 4 /\ t20.MODE = 2 /\ (t20.D2U + t20.U2D = 0) /\ t20.PREV = 1
  ==> t20.MODE' = 0 /\ t20.PREV' = 0 /\ r_2a.MODE' = 0
  [=]
  
  [sequential_release_last_elem_r_2b]
  r_2b.MODE = 4 /\ t20.MODE = 2 /\ (t20.D2U + t20.U2D = 0) /\ t20.PREV = 1
  ==> t20.MODE' = 0 /\ t20.PREV' = 0 /\ r_2b.MODE' = 0
  [=]
  
  [sequential_release_last_elem_r_3_]
  r_3_.MODE = 4 /\ t10.MODE = 2 /\ (t10.D2U + t10.U2D = 0) /\ t10.PREV = 1
  ==> t10.MODE' = 0 /\ t10.PREV' = 0 /\ r_3_.MODE' = 0
  [=]
  
  [sequential_release_last_elem_r_4_]
  r_4_.MODE = 4 /\ t14.MODE = 2 /\ (t14.D2U + t14.U2D = 0) /\ t14.PREV = 1
  ==> t14.MODE' = 0 /\ t14.PREV' = 0 /\ r_4_.MODE' = 0
  [=]
  
  [sequential_release_last_elem_r_5a]
  r_5a.MODE = 4 /\ t12.MODE = 2 /\ (t12.D2U + t12.U2D = 0) /\ t12.PREV = 1
  ==> t12.MODE' = 0 /\ t12.PREV' = 0 /\ r_5a.MODE' = 0
  [=]
  
  [sequential_release_last_elem_r_5b]
  r_5b.MODE = 4 /\ t12.MODE = 2 /\ (t12.D2U + t12.U2D = 0) /\ t12.PREV = 1
  ==> t12.MODE' = 0 /\ t12.PREV' = 0 /\ r_5b.MODE' = 0
  [=]
  
  [sequential_release_last_elem_r_6a]
  r_6a.MODE = 4 /\ t20.MODE = 2 /\ (t20.D2U + t20.U2D = 0) /\ t20.PREV = 1
  ==> t20.MODE' = 0 /\ t20.PREV' = 0 /\ r_6a.MODE' = 0
  [=]
  
  [sequential_release_last_elem_r_6b]
  r_6b.MODE = 4 /\ t20.MODE = 2 /\ (t20.D2U + t20.U2D = 0) /\ t20.PREV = 1
  ==> t20.MODE' = 0 /\ t20.PREV' = 0 /\ r_6b.MODE' = 0
  [=]
  
  [sequential_release_last_elem_r_7_]
  r_7_.MODE = 4 /\ t10.MODE = 2 /\ (t10.D2U + t10.U2D = 0) /\ t10.PREV = 1
  ==> t10.MODE' = 0 /\ t10.PREV' = 0 /\ r_7_.MODE' = 0
  [=]
  
  [sequential_release_last_elem_r_8_]
  r_8_.MODE = 4 /\ t14.MODE = 2 /\ (t14.D2U + t14.U2D = 0) /\ t14.PREV = 1
  ==> t14.MODE' = 0 /\ t14.PREV' = 0 /\ r_8_.MODE' = 0
  [=]
  
  [release_last_elem_pseudo_timer_r_1a]
  r_1a.MODE = 4 /\ t12.MODE = 2 /\ t12.D2U = 0b111 /\ mb13.ACT = 0 /\
  t12.PREV = 1
  ==> t12.MODE' = 0 /\ t12.PREV' = 0 /\ r_1a.MODE' = 0
  [=]
  
  [release_last_elem_pseudo_timer_r_1b]
  r_1b.MODE = 4 /\ t12.MODE = 2 /\ t12.D2U = 0b111 /\ mb13.ACT = 0 /\
  t12.PREV = 1
  ==> t12.MODE' = 0 /\ t12.PREV' = 0 /\ r_1b.MODE' = 0
  [=]
  
  [release_last_elem_pseudo_timer_r_2a]
  r_2a.MODE = 4 /\ t20.MODE = 2 /\ t20.D2U = 0b111 /\ mb21.ACT = 0 /\
  t20.PREV = 1
  ==> t20.MODE' = 0 /\ t20.PREV' = 0 /\ r_2a.MODE' = 0
  [=]
  
  [release_last_elem_pseudo_timer_r_2b]
  r_2b.MODE = 4 /\ t20.MODE = 2 /\ t20.D2U = 0b111 /\ mb21.ACT = 0 /\
  t20.PREV = 1
  ==> t20.MODE' = 0 /\ t20.PREV' = 0 /\ r_2b.MODE' = 0
  [=]
  
  [release_last_elem_pseudo_timer_r_3_]
  r_3_.MODE = 4 /\ t10.MODE = 2 /\ t10.U2D = 0b111 /\ mb11.ACT = 0 /\
  t10.PREV = 1
  ==> t10.MODE' = 0 /\ t10.PREV' = 0 /\ r_3_.MODE' = 0
  [=]
  
  [release_last_elem_pseudo_timer_r_4_]
  r_4_.MODE = 4 /\ t14.MODE = 2 /\ t14.D2U = 0b111 /\ mb14.ACT = 0 /\
  t14.PREV = 1
  ==> t14.MODE' = 0 /\ t14.PREV' = 0 /\ r_4_.MODE' = 0
  [=]
  
  [release_last_elem_pseudo_timer_r_5a]
  r_5a.MODE = 4 /\ t12.MODE = 2 /\ t12.U2D = 0b111 /\ mb12.ACT = 0 /\
  t12.PREV = 1
  ==> t12.MODE' = 0 /\ t12.PREV' = 0 /\ r_5a.MODE' = 0
  [=]
  
  [release_last_elem_pseudo_timer_r_5b]
  r_5b.MODE = 4 /\ t12.MODE = 2 /\ t12.U2D = 0b111 /\ mb12.ACT = 0 /\
  t12.PREV = 1
  ==> t12.MODE' = 0 /\ t12.PREV' = 0 /\ r_5b.MODE' = 0
  [=]
  
  [release_last_elem_pseudo_timer_r_6a]
  r_6a.MODE = 4 /\ t20.MODE = 2 /\ t20.U2D = 0b111 /\ mb20.ACT = 0 /\
  t20.PREV = 1
  ==> t20.MODE' = 0 /\ t20.PREV' = 0 /\ r_6a.MODE' = 0
  [=]
  
  [release_last_elem_pseudo_timer_r_6b]
  r_6b.MODE = 4 /\ t20.MODE = 2 /\ t20.U2D = 0b111 /\ mb20.ACT = 0 /\
  t20.PREV = 1
  ==> t20.MODE' = 0 /\ t20.PREV' = 0 /\ r_6b.MODE' = 0
  [=]
  
  [release_last_elem_pseudo_timer_r_7_]
  r_7_.MODE = 4 /\ t10.MODE = 2 /\ t10.U2D = 0b111 /\ mb11.ACT = 0 /\
  t10.PREV = 1
  ==> t10.MODE' = 0 /\ t10.PREV' = 0 /\ r_7_.MODE' = 0
  [=]
  
  [release_last_elem_pseudo_timer_r_8_]
  r_8_.MODE = 4 /\ t14.MODE = 2 /\ t14.D2U = 0b111 /\ mb14.ACT = 0 /\
  t14.PREV = 1
  ==> t14.MODE' = 0 /\ t14.PREV' = 0 /\ r_8_.MODE' = 0)
 [>]
 
 ([point_switch_1_t11] t11.POS ~= t11.CMD /\ t11.POS ~= 2 ==> t11.POS' = 2
  [=]
  
  [point_switch_1_t13] t13.POS ~= t13.CMD /\ t13.POS ~= 2 ==> t13.POS' = 2
  [=]
  
  [point_switch_2_t11] t11.POS = 2 ==> t11.POS' = t11.CMD
  [=]
  
  [point_switch_2_t13] t13.POS = 2 ==> t13.POS' = t13.CMD
  [=]
  
  [communicate_signal_aspect_mb10] mb10.ACT ~= mb10.CMD ==>
  mb10.ACT' = mb10.CMD
  [=]
  
  [communicate_signal_aspect_mb11] mb11.ACT ~= mb11.CMD ==>
  mb11.ACT' = mb11.CMD
  [=]
  
  [communicate_signal_aspect_mb12] mb12.ACT ~= mb12.CMD ==>
  mb12.ACT' = mb12.CMD
  [=]
  
  [communicate_signal_aspect_mb13] mb13.ACT ~= mb13.CMD ==>
  mb13.ACT' = mb13.CMD
  [=]
  
  [communicate_signal_aspect_mb14] mb14.ACT ~= mb14.CMD ==>
  mb14.ACT' = mb14.CMD
  [=]
  
  [communicate_signal_aspect_mb15] mb15.ACT ~= mb15.CMD ==>
  mb15.ACT' = mb15.CMD
  [=]
  
  [communicate_signal_aspect_mb20] mb20.ACT ~= mb20.CMD ==>
  mb20.ACT' = mb20.CMD
  [=]
  
  [communicate_signal_aspect_mb21] mb21.ACT ~= mb21.CMD ==>
  mb21.ACT' = mb21.CMD)
 [>]
 
 ([head_movement_linear_up_t10] (t10.D2U & 5) = 5 ==>
  t10.D2U' = (t10.D2U ^ 4) /\ t11.S2PM' = (t11.S2PM ^ 5)
  [=]
  
  [head_movement_linear_up_t12] (t12.D2U & 5) = 5 /\ mb13.ACT = 1 ==>
  t12.D2U' = (t12.D2U ^ 4) /\ t13.P2S' = (t13.P2S ^ 5)
  [=]
  
  [head_movement_linear_up_t20] (t20.D2U & 5) = 5 /\ mb21.ACT = 1 ==>
  t20.D2U' = (t20.D2U ^ 4) /\ t13.M2S' = (t13.M2S ^ 5)
  [=]
  
  [head_movement_linear_down_t12] (t12.U2D & 5) = 5 /\ mb12.ACT = 1 ==>
  t12.U2D' = (t12.U2D ^ 4) /\ t11.P2S' = (t11.P2S ^ 5)
  [=]
  
  [head_movement_linear_down_t14] (t14.U2D & 5) = 5 ==>
  t14.U2D' = (t14.U2D ^ 4) /\ t13.S2PM' = (t13.S2PM ^ 5)
  [=]
  
  [head_movement_linear_down_t20] (t20.U2D & 5) = 5 /\ mb20.ACT = 1 ==>
  t20.U2D' = (t20.U2D ^ 4) /\ t11.M2S' = (t11.M2S ^ 5)
  [=]
  
  [tail_movement_linear_up_t10] t10.D2U = 3 ==>
  t10.D2U' = 0 /\ t11.S2PM' = (t11.S2PM ^ 2)
  [=]
  
  [tail_movement_linear_up_t12] t12.D2U = 3 ==>
  t12.D2U' = 0 /\ t13.P2S' = (t13.P2S ^ 2)
  [=]
  
  [tail_movement_linear_up_t20] t20.D2U = 3 ==>
  t20.D2U' = 0 /\ t13.M2S' = (t13.M2S ^ 2)
  [=]
  
  [tail_movement_linear_down_t12] t12.U2D = 3 ==>
  t12.U2D' = 0 /\ t11.P2S' = (t11.P2S ^ 2)
  [=]
  
  [tail_movement_linear_down_t14] t14.U2D = 3 ==>
  t14.U2D' = 0 /\ t13.S2PM' = (t13.S2PM ^ 2)
  [=]
  
  [tail_movement_linear_down_t20] t20.U2D = 3 ==>
  t20.U2D' = 0 /\ t11.M2S' = (t11.M2S ^ 2)
  [=]
  
  [head_movement_point_stem_to_plus_t11] (t11.S2PM & 5) = 5 /\ t11.POS = 0 ==>
  t11.S2PM' = (t11.S2PM ^ 4) /\ t12.D2U' = (t12.D2U ^ 5)
  [=]
  
  [head_movement_point_stem_to_plus_t13] (t13.S2PM & 5) = 5 /\ t13.POS = 0 ==>
  t13.S2PM' = (t13.S2PM ^ 4) /\ t12.U2D' = (t12.U2D ^ 5)
  [=]
  
  [head_movement_point_stem_to_minus_t11] (t11.S2PM & 5) = 5 /\ t11.POS = 1
  ==> t11.S2PM' = (t11.S2PM ^ 4) /\ t20.D2U' = (t20.D2U ^ 5)
  [=]
  
  [head_movement_point_stem_to_minus_t13] (t13.S2PM & 5) = 5 /\ t13.POS = 1
  ==> t13.S2PM' = (t13.S2PM ^ 4) /\ t20.U2D' = (t20.U2D ^ 5)
  [=]
  
  [head_movement_point_plus_to_stem_t11] (t11.P2S & 5) = 5 /\ t11.POS = 0 ==>
  t11.P2S' = (t11.P2S ^ 4) /\ t10.U2D' = (t10.U2D ^ 5)
  [=]
  
  [head_movement_point_plus_to_stem_t13] (t13.P2S & 5) = 5 /\ t13.POS = 0 ==>
  t13.P2S' = (t13.P2S ^ 4) /\ t14.D2U' = (t14.D2U ^ 5)
  [=]
  
  [head_movement_point_minus_to_stem_t11] (t11.M2S & 5) = 5 /\ t11.POS = 1 ==>
  t11.M2S' = (t11.M2S ^ 4) /\ t10.U2D' = (t10.U2D ^ 5)
  [=]
  
  [head_movement_point_minus_to_stem_t13] (t13.M2S & 5) = 5 /\ t13.POS = 1 ==>
  t13.M2S' = (t13.M2S ^ 4) /\ t14.D2U' = (t14.D2U ^ 5)
  [=]
  
  [tail_movement_point_stem_to_plus_t11] t11.S2PM = 3 /\ t11.POS = 0 ==>
  t11.S2PM' = 0 /\ t12.D2U' = (t12.D2U ^ 2)
  [=]
  
  [tail_movement_point_stem_to_plus_t13] t13.S2PM = 3 /\ t13.POS = 0 ==>
  t13.S2PM' = 0 /\ t12.U2D' = (t12.U2D ^ 2)
  [=]
  
  [tail_movement_point_stem_to_minus_t11] t11.S2PM = 3 /\ t11.POS = 1 ==>
  t11.S2PM' = 0 /\ t20.D2U' = (t20.D2U ^ 2)
  [=]
  
  [tail_movement_point_stem_to_minus_t13] t13.S2PM = 3 /\ t13.POS = 1 ==>
  t13.S2PM' = 0 /\ t20.U2D' = (t20.U2D ^ 2)
  [=]
  
  [tail_movement_point_plus_to_stem_t11] t11.P2S = 3 /\ t11.POS = 0 ==>
  t11.P2S' = 0 /\ t10.U2D' = (t10.U2D ^ 2)
  [=]
  
  [tail_movement_point_plus_to_stem_t13] t13.P2S = 3 /\ t13.POS = 0 ==>
  t13.P2S' = 0 /\ t14.D2U' = (t14.D2U ^ 2)
  [=]
  
  [tail_movement_point_minus_to_stem_t11] t11.M2S = 3 /\ t11.POS = 1 ==>
  t11.M2S = 0 /\ t10.U2D' = (t10.U2D ^ 2)
  [=]
  
  [tail_movement_point_minus_to_stem_t13] t13.M2S = 3 /\ t13.POS = 1 ==>
  t13.M2S = 0 /\ t14.D2U' = (t14.D2U ^ 2)
  [=]
  
  [change_direction_up_to_down_t12] t12.D2U = 0b111 /\ mb13.ACT = 0 ==>
  t12.D2U' = t12.U2D /\ t12.U2D' = t12.D2U
  [=]
  
  [change_direction_up_to_down_t20] t20.D2U = 0b111 /\ mb21.ACT = 0 ==>
  t20.D2U' = t20.U2D /\ t20.U2D' = t20.D2U
  [=]
  
  [change_direction_down_to_up_t12] t12.U2D = 0b111 /\ mb12.ACT = 0 ==>
  t12.D2U' = t12.U2D /\ t12.U2D' = t12.D2U
  [=]
  
  [change_direction_down_to_up_t20] t20.U2D = 0b111 /\ mb20.ACT = 0 ==>
  t20.D2U' = t20.U2D /\ t20.U2D' = t20.D2U
  [=]
  
  [enter_interlocked_area_head_from_down_b10] mb10.ACT = 1 ==>
  t10.D2U' = (t10.D2U ^ 5)
  [=]
  
  [enter_interlocked_area_tail_from_down_b10] (t10.D2U & 3) = 1 ==>
  t10.D2U' = (t10.D2U ^ 2)
  [=]
  
  [enter_interlocked_area_head_from_up_b14] mb15.ACT = 1 ==>
  t14.U2D' = (t14.U2D ^ 5)
  [=]
  
  [enter_interlocked_area_tail_from_up_b14] (t14.U2D & 3) = 1 ==>
  t14.U2D' = (t14.U2D ^ 2)
  [=]
  
  [leave_interlocked_area_head_to_down_b10] (t10.U2D & 5) = 5 ==>
  t10.U2D' = (t10.U2D ^ 4)
  [=]
  
  [leave_interlocked_area_tail_to_down_b10] t10.U2D = 3 ==> t10.U2D' = 0
  [=]
  
  [leave_interlocked_area_head_to_up_b14] (t14.D2U & 5) = 5 ==>
  t14.D2U' = (t14.D2U ^ 4)
  [=]
  
  [leave_interlocked_area_tail_to_up_b14] t14.D2U = 3 ==> t14.D2U' = 0))

invariant

[no_head_to_head_collisions_linear]
((t10.D2U * t10.U2D = 0) /\ (t12.D2U * t12.U2D = 0) /\
 (t14.D2U * t14.U2D = 0) /\ (t20.D2U * t20.U2D = 0)),

[no_head_to_tail_collisions_linear]
((t10.D2U * (1 - (t10.D2U & 1)) + t10.U2D * (1 - (t10.U2D & 1)) = 0) /\
 (t12.D2U * (1 - (t12.D2U & 1)) + t12.U2D * (1 - (t12.U2D & 1)) = 0) /\
 (t14.D2U * (1 - (t14.D2U & 1)) + t14.U2D * (1 - (t14.U2D & 1)) = 0) /\
 (t20.D2U * (1 - (t20.D2U & 1)) + t20.U2D * (1 - (t20.U2D & 1)) = 0)),

[no_head_to_head_collisions_point]
((t11.M2S * t11.S2PM + t11.P2S * t11.S2PM + t11.P2S * t11.M2S = 0) /\
 (t13.M2S * t13.S2PM + t13.P2S * t13.S2PM + t13.P2S * t13.M2S = 0)),

[no_head_to_tail_collisions_point]
((t11.S2PM * (1 - (t11.S2PM & 1)) + t11.P2S * (1 - (t11.P2S & 1)) +
  t11.M2S * (1 - (t11.M2S & 1)) = 0) /\
 (t13.S2PM * (1 - (t13.S2PM & 1)) + t13.P2S * (1 - (t13.P2S & 1)) +
  t13.M2S * (1 - (t13.M2S & 1)) = 0)),

[no_derailments]
((t11.POS * t11.P2S + (1 - (t11.POS & 1)) * t11.M2S +
  (t11.POS >> 1) * t11.S2PM = 0) /\
 (t13.POS * t13.P2S + (1 - (t13.POS & 1)) * t13.M2S +
  (t13.POS >> 1) * t13.S2PM = 0)),

[train_integrity_linear_up]
((((t10.D2U & 5) = 1 => (t11.S2PM & 3) = 1) /\
  ((t11.S2PM & 3) = 1 => (t10.D2U & 5) = 1)) /\
 (((t12.D2U & 5) = 1 => (t13.P2S & 3) = 1) /\
  ((t13.P2S & 3) = 1 => (t12.D2U & 5) = 1)) /\
 (((t20.D2U & 5) = 1 => (t13.M2S & 3) = 1) /\
  ((t13.M2S & 3) = 1 => (t20.D2U & 5) = 1))),

[train_integrity_linear_down]
((((t12.U2D & 5) = 1 => (t11.P2S & 3) = 1) /\
  ((t11.P2S & 3) = 1 => (t12.U2D & 5) = 1)) /\
 (((t14.U2D & 5) = 1 => (t13.S2PM & 3) = 1) /\
  ((t13.S2PM & 3) = 1 => (t14.U2D & 5) = 1)) /\
 (((t20.U2D & 5) = 1 => (t11.M2S & 3) = 1) /\
  ((t11.M2S & 3) = 1 => (t20.U2D & 5) = 1))),

[train_integrity_point_stem_to_plusminus]
((((t11.S2PM & 5) = 1 =>
   (((t12.D2U & 3) = 1 /\ t11.POS = 0) xor
    ((t20.D2U & 3) = 1 /\ t11.POS = 1))) /\
  ((t12.D2U & 3) = 1 => ((t11.S2PM & 5) = 1 /\ t11.POS = 0)) /\
  ((t20.D2U & 3) = 1 => ((t11.S2PM & 5) = 1 /\ t11.POS = 1)) /\
  ~((t12.D2U & 3) = 1 /\ (t20.D2U & 3) = 1)) /\
 (((t13.S2PM & 5) = 1 =>
   (((t12.U2D & 3) = 1 /\ t13.POS = 0) xor
    ((t20.U2D & 3) = 1 /\ t13.POS = 1))) /\
  ((t12.U2D & 3) = 1 => ((t13.S2PM & 5) = 1 /\ t13.POS = 0)) /\
  ((t20.U2D & 3) = 1 => ((t13.S2PM & 5) = 1 /\ t13.POS = 1)) /\
  ~((t12.U2D & 3) = 1 /\ (t20.U2D & 3) = 1))),

[train_integrity_point_plusminus_to_stem]
((((t11.P2S & 5) = 1 => ((t10.U2D & 3) = 1 /\ t11.POS = 0)) /\
  ((t11.M2S & 5) = 1 => ((t10.U2D & 3) = 1 /\ t11.POS = 1)) /\
  ((t10.U2D & 3) = 1 =>
   (((t11.P2S & 5) = 1 /\ t11.POS = 0) xor
    ((t11.M2S & 5) = 1 /\ t11.POS = 1)))) /\
 (((t13.P2S & 5) = 1 => ((t14.D2U & 3) = 1 /\ t13.POS = 0)) /\
  ((t13.M2S & 5) = 1 => ((t14.D2U & 3) = 1 /\ t13.POS = 1)) /\
  ((t14.D2U & 3) = 1 =>
   (((t13.P2S & 5) = 1 /\ t13.POS = 0) xor
    ((t13.M2S & 5) = 1 /\ t13.POS = 1))))),

[conflicting_routes_are_not_set_together]
(((r_1a.MODE = 2 \/ r_1a.MODE = 3) =>
  ((r_1b.MODE ~=
    2 /\
    r_1b.MODE ~= 3) /\
   (r_2a.MODE ~= 2 /\
    r_2a.MODE ~= 3) /\
   (r_2b.MODE ~= 2 /\
    r_2b.MODE ~= 3) /\
   (r_3_.MODE ~= 2 /\
    r_3_.MODE ~= 3) /\
   (r_4_.MODE ~= 2 /\
    r_4_.MODE ~= 3) /\
   (r_5a.MODE ~= 2 /\
    r_5a.MODE ~= 3) /\
   (r_5b.MODE ~= 2 /\ r_5b.MODE ~= 3) /\
   (r_6b.MODE ~= 2 /\ r_6b.MODE ~= 3) /\
   (r_7_.MODE ~= 2 /\ r_7_.MODE ~= 3))) /\
 ((r_1b.MODE = 2 \/ r_1b.MODE = 3) =>
  ((r_1a.MODE ~=
    2 /\
    r_1a.MODE ~= 3) /\
   (r_2a.MODE ~= 2 /\
    r_2a.MODE ~= 3) /\
   (r_2b.MODE ~= 2 /\
    r_2b.MODE ~= 3) /\
   (r_3_.MODE ~= 2 /\
    r_3_.MODE ~= 3) /\
   (r_5a.MODE ~= 2 /\
    r_5a.MODE ~= 3) /\
   (r_5b.MODE ~= 2 /\
    r_5b.MODE ~= 3) /\
   (r_6a.MODE ~= 2 /\ r_6a.MODE ~= 3) /\
   (r_6b.MODE ~= 2 /\ r_6b.MODE ~= 3) /\
   (r_7_.MODE ~= 2 /\ r_7_.MODE ~= 3) /\
   (r_8_.MODE ~= 2 /\ r_8_.MODE ~= 3))) /\
 ((r_2a.MODE = 2 \/ r_2a.MODE = 3) =>
  ((r_1a.MODE ~= 2 /\
    r_1a.MODE ~= 3) /\
   (r_1b.MODE ~= 2 /\
    r_1b.MODE ~= 3) /\
   (r_2b.MODE ~= 2 /\
    r_2b.MODE ~= 3) /\
   (r_3_.MODE ~= 2 /\
    r_3_.MODE ~= 3) /\
   (r_5b.MODE ~= 2 /\ r_5b.MODE ~= 3) /\
   (r_6a.MODE ~= 2 /\ r_6a.MODE ~= 3) /\
   (r_6b.MODE ~= 2 /\ r_6b.MODE ~= 3) /\
   (r_7_.MODE ~= 2 /\ r_7_.MODE ~= 3) /\
   (r_8_.MODE ~= 2 /\ r_8_.MODE ~= 3))) /\
 ((r_2b.MODE = 2 \/ r_2b.MODE = 3) =>
  ((r_1a.MODE ~= 2 /\
    r_1a.MODE ~= 3) /\
   (r_1b.MODE ~= 2 /\
    r_1b.MODE ~= 3) /\
   (r_2a.MODE ~= 2 /\
    r_2a.MODE ~= 3) /\
   (r_3_.MODE ~= 2 /\
    r_3_.MODE ~= 3) /\
   (r_4_.MODE ~= 2 /\ r_4_.MODE ~= 3) /\
   (r_5a.MODE ~= 2 /\ r_5a.MODE ~= 3) /\
   (r_5b.MODE ~= 2 /\ r_5b.MODE ~= 3) /\
   (r_6a.MODE ~= 2 /\ r_6a.MODE ~= 3) /\
   (r_6b.MODE ~= 2 /\ r_6b.MODE ~= 3) /\
   (r_7_.MODE ~= 2 /\ r_7_.MODE ~= 3))) /\
 ((r_3_.MODE = 2 \/ r_3_.MODE = 3) =>
  ((r_1a.MODE ~= 2 /\ r_1a.MODE ~= 3) /\
   (r_1b.MODE ~= 2 /\ r_1b.MODE ~= 3) /\
   (r_2a.MODE ~= 2 /\ r_2a.MODE ~= 3) /\
   (r_2b.MODE ~= 2 /\ r_2b.MODE ~= 3) /\
   (r_5a.MODE ~= 2 /\ r_5a.MODE ~= 3) /\
   (r_6b.MODE ~= 2 /\ r_6b.MODE ~= 3) /\
   (r_7_.MODE ~= 2 /\ r_7_.MODE ~= 3))) /\
 ((r_4_.MODE = 2 \/ r_4_.MODE = 3) =>
  ((r_1a.MODE ~= 2 /\ r_1a.MODE ~= 3) /\
   (r_2b.MODE ~= 2 /\ r_2b.MODE ~= 3) /\
   (r_5a.MODE ~= 2 /\ r_5a.MODE ~= 3) /\
   (r_5b.MODE ~= 2 /\ r_5b.MODE ~= 3) /\
   (r_6a.MODE ~= 2 /\ r_6a.MODE ~= 3) /\
   (r_6b.MODE ~= 2 /\ r_6b.MODE ~= 3) /\
   (r_8_.MODE ~= 2 /\ r_8_.MODE ~= 3))) /\
 ((r_5a.MODE = 2 \/ r_5a.MODE = 3) =>
  ((r_1a.MODE ~= 2 /\ r_1a.MODE ~= 3) /\
   (r_1b.MODE ~= 2 /\ r_1b.MODE ~= 3) /\
   (r_2b.MODE ~= 2 /\ r_2b.MODE ~= 3) /\
   (r_3_.MODE ~= 2 /\ r_3_.MODE ~= 3) /\
   (r_4_.MODE ~= 2 /\ r_4_.MODE ~= 3) /\
   (r_5b.MODE ~= 2 /\ r_5b.MODE ~= 3) /\
   (r_6a.MODE ~= 2 /\ r_6a.MODE ~= 3) /\
   (r_6b.MODE ~= 2 /\ r_6b.MODE ~= 3) /\
   (r_8_.MODE ~= 2 /\ r_8_.MODE ~= 3))) /\
 ((r_5b.MODE = 2 \/ r_5b.MODE = 3) =>
  ((r_1a.MODE ~= 2 /\ r_1a.MODE ~= 3) /\
   (r_1b.MODE ~= 2 /\ r_1b.MODE ~= 3) /\
   (r_2a.MODE ~= 2 /\ r_2a.MODE ~= 3) /\
   (r_2b.MODE ~= 2 /\ r_2b.MODE ~= 3) /\
   (r_4_.MODE ~= 2 /\ r_4_.MODE ~= 3) /\
   (r_5a.MODE ~= 2 /\ r_5a.MODE ~= 3) /\
   (r_6a.MODE ~= 2 /\ r_6a.MODE ~= 3) /\
   (r_6b.MODE ~= 2 /\ r_6b.MODE ~= 3) /\
   (r_7_.MODE ~= 2 /\ r_7_.MODE ~= 3) /\
   (r_8_.MODE ~= 2 /\ r_8_.MODE ~= 3))) /\
 ((r_6a.MODE = 2 \/ r_6a.MODE = 3) =>
  ((r_1b.MODE ~= 2 /\ r_1b.MODE ~= 3) /\
   (r_2a.MODE ~= 2 /\ r_2a.MODE ~= 3) /\
   (r_2b.MODE ~= 2 /\ r_2b.MODE ~= 3) /\
   (r_4_.MODE ~= 2 /\ r_4_.MODE ~= 3) /\
   (r_5a.MODE ~= 2 /\ r_5a.MODE ~= 3) /\
   (r_5b.MODE ~= 2 /\ r_5b.MODE ~= 3) /\
   (r_6b.MODE ~= 2 /\ r_6b.MODE ~= 3) /\
   (r_7_.MODE ~= 2 /\ r_7_.MODE ~= 3) /\
   (r_8_.MODE ~= 2 /\ r_8_.MODE ~= 3))) /\
 ((r_6b.MODE = 2 \/ r_6b.MODE = 3) =>
  ((r_1a.MODE ~= 2 /\ r_1a.MODE ~= 3) /\
   (r_1b.MODE ~= 2 /\ r_1b.MODE ~= 3) /\
   (r_2a.MODE ~= 2 /\ r_2a.MODE ~= 3) /\
   (r_2b.MODE ~= 2 /\ r_2b.MODE ~= 3) /\
   (r_3_.MODE ~= 2 /\ r_3_.MODE ~= 3) /\
   (r_4_.MODE ~= 2 /\ r_4_.MODE ~= 3) /\
   (r_5a.MODE ~= 2 /\ r_5a.MODE ~= 3) /\
   (r_5b.MODE ~= 2 /\ r_5b.MODE ~= 3) /\
   (r_6a.MODE ~= 2 /\ r_6a.MODE ~= 3) /\
   (r_8_.MODE ~= 2 /\ r_8_.MODE ~= 3))) /\
 ((r_7_.MODE = 2 \/ r_7_.MODE = 3) =>
  ((r_1a.MODE ~= 2 /\ r_1a.MODE ~= 3) /\
   (r_1b.MODE ~= 2 /\ r_1b.MODE ~= 3) /\
   (r_2a.MODE ~= 2 /\ r_2a.MODE ~= 3) /\
   (r_2b.MODE ~= 2 /\ r_2b.MODE ~= 3) /\
   (r_3_.MODE ~= 2 /\ r_3_.MODE ~= 3) /\
   (r_5b.MODE ~= 2 /\ r_5b.MODE ~= 3) /\
   (r_6a.MODE ~= 2 /\ r_6a.MODE ~= 3))) /\
 ((r_8_.MODE = 2 \/ r_8_.MODE = 3) =>
  ((r_1b.MODE ~= 2 /\ r_1b.MODE ~= 3) /\
   (r_2a.MODE ~= 2 /\ r_2a.MODE ~= 3) /\
   (r_4_.MODE ~= 2 /\ r_4_.MODE ~= 3) /\
   (r_5a.MODE ~= 2 /\ r_5a.MODE ~= 3) /\
   (r_5b.MODE ~= 2 /\ r_5b.MODE ~= 3) /\
   (r_6a.MODE ~= 2 /\ r_6a.MODE ~= 3) /\
   (r_6b.MODE ~= 2 /\ r_6b.MODE ~= 3)))),

[route_allocating_cnd]
(((r_1a.MODE = 2) =>
  (((t11.CMD = 0) /\
    (t13.CMD = 1)) /\
   ((mb11.CMD = 0) /\
    (mb12.CMD = 0) /\
    (mb20.CMD = 0)) /\
   ((t10.MODE = 1) /\ (t12.MODE = 1) /\
    (t11.MODE = 1)) /\
   ((t10.D2U + t10.U2D = 0) /\
    (t12.D2U + t12.U2D = 0) /\
    (t11.S2PM + t11.P2S + t11.M2S = 0)))) /\
 ((r_1b.MODE = 2) =>
  ((t11.CMD = 0) /\
   ((mb11.CMD = 0) /\
    (mb12.CMD = 0) /\
    (mb15.CMD = 0) /\
    (mb20.CMD = 0) /\
    (mb21.CMD = 0)) /\
   ((t10.MODE = 1) /\ (t12.MODE = 1) /\
    (t11.MODE = 1)) /\
   ((t10.D2U + t10.U2D = 0) /\
    (t12.D2U + t12.U2D = 0) /\
    (t11.S2PM + t11.P2S + t11.M2S = 0)))) /\
 ((r_2a.MODE = 2) =>
  (((t11.CMD = 1) /\ (t13.CMD = 0)) /\
   ((mb11.CMD = 0) /\ (mb12.CMD = 0) /\
    (mb20.CMD = 0)) /\
   ((t10.MODE = 1) /\ (t20.MODE = 1) /\
    (t11.MODE = 1)) /\
   ((t10.D2U + t10.U2D = 0) /\
    (t20.D2U + t20.U2D = 0) /\
    (t11.S2PM + t11.P2S + t11.M2S = 0)))) /\
 ((r_2b.MODE = 2) =>
  ((t11.CMD = 1) /\
   ((mb11.CMD = 0) /\ (mb12.CMD = 0) /\
    (mb13.CMD = 0) /\ (mb15.CMD = 0) /\
    (mb20.CMD = 0)) /\
   ((t10.MODE = 1) /\ (t20.MODE = 1) /\
    (t11.MODE = 1)) /\
   ((t10.D2U + t10.U2D = 0) /\
    (t20.D2U + t20.U2D = 0) /\
    (t11.S2PM + t11.P2S + t11.M2S = 0)))) /\
 ((r_3_.MODE = 2) =>
  ((t11.CMD = 0) /\
   ((mb10.CMD = 0) /\ (mb20.CMD = 0)) /\
   ((t10.MODE = 1) /\ (t11.MODE = 1)) /\
   ((t10.D2U + t10.U2D = 0) /\
    (t11.S2PM + t11.P2S + t11.M2S = 0)))) /\
 ((r_4_.MODE = 2) =>
  ((t13.CMD = 0) /\
   ((mb15.CMD = 0) /\ (mb21.CMD = 0)) /\
   ((t14.MODE = 1) /\ (t13.MODE = 1)) /\
   ((t14.D2U + t14.U2D = 0) /\
    (t13.S2PM + t13.P2S + t13.M2S = 0)))) /\
 ((r_5a.MODE = 2) =>
  (((t11.CMD = 1) /\ (t13.CMD = 0)) /\
   ((mb13.CMD = 0) /\ (mb14.CMD = 0) /\ (mb21.CMD = 0)) /\
   ((t12.MODE = 1) /\ (t14.MODE = 1) /\ (t13.MODE = 1)) /\
   ((t12.D2U + t12.U2D = 0) /\ (t14.D2U + t14.U2D = 0) /\
    (t13.S2PM + t13.P2S + t13.M2S = 0)))) /\
 ((r_5b.MODE = 2) =>
  ((t13.CMD = 0) /\
   ((mb10.CMD = 0) /\ (mb13.CMD = 0) /\
    (mb14.CMD = 0) /\ (mb20.CMD = 0) /\
    (mb21.CMD = 0)) /\
   ((t12.MODE = 1) /\ (t14.MODE = 1) /\ (t13.MODE = 1)) /\
   ((t12.D2U + t12.U2D = 0) /\ (t14.D2U + t14.U2D = 0) /\
    (t13.S2PM + t13.P2S + t13.M2S = 0)))) /\
 ((r_6a.MODE = 2) =>
  (((t11.CMD = 0) /\ (t13.CMD = 1)) /\
   ((mb13.CMD = 0) /\ (mb14.CMD = 0) /\ (mb21.CMD = 0)) /\
   ((t14.MODE = 1) /\ (t20.MODE = 1) /\ (t13.MODE = 1)) /\
   ((t14.D2U + t14.U2D = 0) /\ (t20.D2U + t20.U2D = 0) /\
    (t13.S2PM + t13.P2S + t13.M2S = 0)))) /\
 ((r_6b.MODE = 2) =>
  ((t13.CMD = 1) /\
   ((mb10.CMD = 0) /\ (mb12.CMD = 0) /\ (mb13.CMD = 0) /\
    (mb14.CMD = 0) /\ (mb21.CMD = 0)) /\
   ((t14.MODE = 1) /\ (t20.MODE = 1) /\ (t13.MODE = 1)) /\
   ((t14.D2U + t14.U2D = 0) /\ (t20.D2U + t20.U2D = 0) /\
    (t13.S2PM + t13.P2S + t13.M2S = 0)))) /\
 ((r_7_.MODE = 2) =>
  ((t11.CMD = 1) /\ ((mb10.CMD = 0) /\ (mb12.CMD = 0)) /\
   ((t10.MODE = 1) /\ (t11.MODE = 1)) /\
   ((t10.D2U + t10.U2D = 0) /\ (t11.S2PM + t11.P2S + t11.M2S = 0)))) /\
 ((r_8_.MODE = 2) =>
  ((t13.CMD = 1) /\ ((mb13.CMD = 0) /\ (mb15.CMD = 0)) /\
   ((t14.MODE = 1) /\ (t13.MODE = 1)) /\
   ((t14.D2U + t14.U2D = 0) /\ (t13.S2PM + t13.P2S + t13.M2S = 0))))),

[route_lock_cnd]
(((r_1a.MODE = 3) =>
  ((t11.POS = 0 /\
    t11.POS = t11.CMD) /\
   (t13.POS = 1 /\
    t13.POS = t13.CMD)) /\
  ((mb11.ACT = 0 /\
    mb11.ACT = mb11.CMD) /\
   (mb12.ACT = 0 /\
    mb12.ACT = mb12.CMD) /\
   (mb20.ACT = 0 /\
    mb20.ACT = mb20.CMD)) /\
  ((t10.MODE = 1) /\
   (t12.MODE = 1) /\
   (t11.MODE = 1)) /\
  ((t12.D2U + t12.U2D = 0) /\
   (t11.S2PM + t11.P2S + t11.M2S = 0)) /\
  ((t10.D2U + t10.U2D = 0) \/
   t10.D2U = 5) /\ mb10.CMD = 1) /\
 ((r_1b.MODE = 3) =>
  (t11.POS = 0 /\
   t11.POS = t11.CMD) /\
  ((mb11.ACT = 0 /\
    mb11.ACT =
    mb11.CMD) /\
   (mb12.ACT = 0 /\
    mb12.ACT = mb12.CMD) /\
   (mb15.ACT = 0 /\
    mb15.ACT = mb15.CMD) /\
   (mb20.ACT = 0 /\
    mb20.ACT = mb20.CMD) /\
   (mb21.ACT = 0 /\
    mb21.ACT = mb21.CMD)) /\
  ((t10.MODE = 1) /\
   (t12.MODE = 1) /\
   (t11.MODE = 1)) /\
  ((t12.D2U + t12.U2D = 0) /\
   (t11.S2PM + t11.P2S + t11.M2S = 0)) /\
  ((t10.D2U + t10.U2D = 0) \/ t10.D2U = 5) /\
  mb10.CMD = 1) /\
 ((r_2a.MODE = 3) =>
  ((t11.POS = 1 /\
    t11.POS = t11.CMD) /\
   (t13.POS = 0 /\
    t13.POS = t13.CMD)) /\
  ((mb11.ACT = 0 /\
    mb11.ACT = mb11.CMD) /\
   (mb12.ACT = 0 /\
    mb12.ACT = mb12.CMD) /\
   (mb20.ACT = 0 /\
    mb20.ACT = mb20.CMD)) /\
  ((t10.MODE = 1) /\ (t20.MODE = 1) /\
   (t11.MODE = 1)) /\
  ((t20.D2U + t20.U2D = 0) /\
   (t11.S2PM + t11.P2S + t11.M2S = 0)) /\
  ((t10.D2U + t10.U2D = 0) \/ t10.D2U = 5) /\
  mb10.CMD = 1) /\
 ((r_2b.MODE = 3) =>
  (t11.POS = 1 /\ t11.POS = t11.CMD) /\
  ((mb11.ACT = 0 /\
    mb11.ACT = mb11.CMD) /\
   (mb12.ACT = 0 /\
    mb12.ACT = mb12.CMD) /\
   (mb13.ACT = 0 /\
    mb13.ACT = mb13.CMD) /\
   (mb15.ACT = 0 /\
    mb15.ACT = mb15.CMD) /\
   (mb20.ACT = 0 /\ mb20.ACT = mb20.CMD)) /\
  ((t10.MODE = 1) /\ (t20.MODE = 1) /\
   (t11.MODE = 1)) /\
  ((t20.D2U + t20.U2D = 0) /\
   (t11.S2PM + t11.P2S + t11.M2S = 0)) /\
  ((t10.D2U + t10.U2D = 0) \/ t10.D2U = 5) /\
  mb10.CMD = 1) /\
 ((r_3_.MODE = 3) =>
  (t11.POS = 0 /\ t11.POS = t11.CMD) /\
  ((mb10.ACT = 0 /\ mb10.ACT = mb10.CMD) /\
   (mb20.ACT = 0 /\ mb20.ACT = mb20.CMD)) /\
  ((t10.MODE = 1) /\ (t11.MODE = 1)) /\
  (t10.D2U + t10.U2D = 0) /\
  ((t11.S2PM + t11.P2S + t11.M2S = 0) \/ t11.P2S = 5) /\
  mb12.CMD = 1) /\
 ((r_4_.MODE = 3) =>
  (t13.POS = 0 /\ t13.POS = t13.CMD) /\
  ((mb15.ACT = 0 /\ mb15.ACT = mb15.CMD) /\
   (mb21.ACT = 0 /\ mb21.ACT = mb21.CMD)) /\
  ((t14.MODE = 1) /\ (t13.MODE = 1)) /\
  (t14.D2U + t14.U2D = 0) /\
  ((t13.S2PM + t13.P2S + t13.M2S = 0) \/ t13.P2S = 5) /\
  mb13.CMD = 1) /\
 ((r_5a.MODE = 3) =>
  ((t11.POS = 1 /\ t11.POS = t11.CMD) /\
   (t13.POS = 0 /\ t13.POS = t13.CMD)) /\
  ((mb13.ACT = 0 /\ mb13.ACT = mb13.CMD) /\
   (mb14.ACT = 0 /\ mb14.ACT = mb14.CMD) /\
   (mb21.ACT = 0 /\ mb21.ACT = mb21.CMD)) /\
  ((t12.MODE = 1) /\ (t14.MODE = 1) /\
   (t13.MODE = 1)) /\
  ((t12.D2U + t12.U2D = 0) /\
   (t13.S2PM + t13.P2S + t13.M2S = 0)) /\
  ((t14.D2U + t14.U2D = 0) \/ t14.U2D = 5) /\ mb15.CMD = 1) /\
 ((r_5b.MODE = 3) =>
  (t13.POS = 0 /\ t13.POS = t13.CMD) /\
  ((mb10.ACT = 0 /\ mb10.ACT = mb10.CMD) /\
   (mb13.ACT = 0 /\ mb13.ACT = mb13.CMD) /\
   (mb14.ACT = 0 /\ mb14.ACT = mb14.CMD) /\
   (mb20.ACT = 0 /\ mb20.ACT = mb20.CMD) /\
   (mb21.ACT = 0 /\ mb21.ACT = mb21.CMD)) /\
  ((t12.MODE = 1) /\ (t14.MODE = 1) /\ (t13.MODE = 1)) /\
  ((t12.D2U + t12.U2D = 0) /\
   (t13.S2PM + t13.P2S + t13.M2S = 0)) /\
  ((t14.D2U + t14.U2D = 0) \/ t14.U2D = 5) /\ mb15.CMD = 1) /\
 ((r_6a.MODE = 3) =>
  ((t11.POS = 0 /\ t11.POS = t11.CMD) /\
   (t13.POS = 1 /\ t13.POS = t13.CMD)) /\
  ((mb13.ACT = 0 /\ mb13.ACT = mb13.CMD) /\
   (mb14.ACT = 0 /\ mb14.ACT = mb14.CMD) /\
   (mb21.ACT = 0 /\ mb21.ACT = mb21.CMD)) /\
  ((t14.MODE = 1) /\ (t20.MODE = 1) /\ (t13.MODE = 1)) /\
  ((t20.D2U + t20.U2D = 0) /\
   (t13.S2PM + t13.P2S + t13.M2S = 0)) /\
  ((t14.D2U + t14.U2D = 0) \/ t14.U2D = 5) /\ mb15.CMD = 1) /\
 ((r_6b.MODE = 3) =>
  (t13.POS = 1 /\ t13.POS = t13.CMD) /\
  ((mb10.ACT = 0 /\ mb10.ACT = mb10.CMD) /\
   (mb12.ACT = 0 /\ mb12.ACT = mb12.CMD) /\
   (mb13.ACT = 0 /\ mb13.ACT = mb13.CMD) /\
   (mb14.ACT = 0 /\ mb14.ACT = mb14.CMD) /\
   (mb21.ACT = 0 /\ mb21.ACT = mb21.CMD)) /\
  ((t14.MODE = 1) /\ (t20.MODE = 1) /\ (t13.MODE = 1)) /\
  ((t20.D2U + t20.U2D = 0) /\ (t13.S2PM + t13.P2S + t13.M2S = 0)) /\
  ((t14.D2U + t14.U2D = 0) \/ t14.U2D = 5) /\ mb15.CMD = 1) /\
 ((r_7_.MODE = 3) =>
  (t11.POS = 1 /\ t11.POS = t11.CMD) /\
  ((mb10.ACT = 0 /\ mb10.ACT = mb10.CMD) /\
   (mb12.ACT = 0 /\ mb12.ACT = mb12.CMD)) /\
  ((t10.MODE = 1) /\ (t11.MODE = 1)) /\ (t10.D2U + t10.U2D = 0) /\
  ((t11.S2PM + t11.P2S + t11.M2S = 0) \/ t11.M2S = 5) /\ mb20.CMD = 1) /\
 ((r_8_.MODE = 3) =>
  (t13.POS = 1 /\ t13.POS = t13.CMD) /\
  ((mb13.ACT = 0 /\ mb13.ACT = mb13.CMD) /\
   (mb15.ACT = 0 /\ mb15.ACT = mb15.CMD)) /\
  ((t14.MODE = 1) /\ (t13.MODE = 1)) /\ (t14.D2U + t14.U2D = 0) /\
  ((t13.S2PM + t13.P2S + t13.M2S = 0) \/ t13.M2S = 5) /\ mb21.CMD = 1)),

[route_used_cnd_a]
((r_1a.MODE = 4 => (t12.MODE ~= 0)) /\
 (r_1b.MODE = 4 => (t12.MODE ~= 0)) /\
 (r_2a.MODE = 4 => (t20.MODE ~= 0)) /\
 (r_2b.MODE = 4 => (t20.MODE ~= 0)) /\
 (r_3_.MODE = 4 => (t10.MODE ~= 0)) /\
 (r_4_.MODE = 4 => (t14.MODE ~= 0)) /\
 (r_5a.MODE = 4 => (t12.MODE ~= 0)) /\
 (r_5b.MODE = 4 => (t12.MODE ~= 0)) /\
 (r_6a.MODE = 4 => (t20.MODE ~= 0)) /\
 (r_6b.MODE = 4 => (t20.MODE ~= 0)) /\ (r_7_.MODE = 4 => (t10.MODE ~= 0)) /\
 (r_8_.MODE = 4 => (t14.MODE ~= 0))),

[route_used_cnd_b]
((r_1a.MODE = 4 =>
  (((t12.D2U & 1) + (t11.POS = 0) /\
    ((t11.S2PM & 1) + (t10.D2U & 1))) \/
   t12.PREV /\ (t12.D2U + t12.U2D = 0))) /\
 (r_1b.MODE = 4 =>
  (((t12.D2U & 1) + (t11.POS = 0) /\
    ((t11.S2PM & 1) + (t10.D2U & 1))) \/
   t12.PREV /\ (t12.D2U + t12.U2D = 0))) /\
 (r_2a.MODE = 4 =>
  (((t20.D2U & 1) + (t11.POS = 1) /\
    ((t11.S2PM & 1) + (t10.D2U & 1))) \/
   t20.PREV /\ (t20.D2U + t20.U2D = 0))) /\
 (r_2b.MODE = 4 =>
  (((t20.D2U & 1) + (t11.POS = 1) /\
    ((t11.S2PM & 1) + (t10.D2U & 1))) \/
   t20.PREV /\ (t20.D2U + t20.U2D = 0))) /\
 (r_3_.MODE = 4 =>
  (((t10.U2D & 1) + (t11.POS = 0) /\ (t11.P2S & 1)) \/
   t10.PREV /\ (t10.D2U + t10.U2D = 0))) /\
 (r_4_.MODE = 4 =>
  (((t14.D2U & 1) + (t13.POS = 0) /\ (t13.P2S & 1)) \/
   t14.PREV /\ (t14.D2U + t14.U2D = 0))) /\
 (r_5a.MODE = 4 =>
  (((t12.U2D & 1) + (t13.POS = 0) /\
    ((t13.S2PM & 1) + (t14.U2D & 1))) \/
   t12.PREV /\ (t12.D2U + t12.U2D = 0))) /\
 (r_5b.MODE = 4 =>
  (((t12.U2D & 1) + (t13.POS = 0) /\
    ((t13.S2PM & 1) + (t14.U2D & 1))) \/
   t12.PREV /\ (t12.D2U + t12.U2D = 0))) /\
 (r_6a.MODE = 4 =>
  (((t20.U2D & 1) + (t13.POS = 1) /\
    ((t13.S2PM & 1) + (t14.U2D & 1))) \/
   t20.PREV /\ (t20.D2U + t20.U2D = 0))) /\
 (r_6b.MODE = 4 =>
  (((t20.U2D & 1) + (t13.POS = 1) /\
    ((t13.S2PM & 1) + (t14.U2D & 1))) \/
   t20.PREV /\ (t20.D2U + t20.U2D = 0))) /\
 (r_7_.MODE = 4 =>
  (((t10.U2D & 1) + (t11.POS = 1) /\ (t11.M2S & 1)) \/
   t10.PREV /\ (t10.D2U + t10.U2D = 0))) /\
 (r_8_.MODE = 4 =>
  (((t14.D2U & 1) + (t13.POS = 1) /\ (t13.M2S & 1)) \/
   t14.PREV /\ (t14.D2U + t14.U2D = 0)))),

[route_used_cnd_c]
((r_1a.MODE = 4 =>
  (((t11.S2PM & 1) + (t10.D2U & 1)) *
   ((t11.P2S & 1) + (t10.U2D & 1)) = 0)) /\
 (r_1b.MODE = 4 =>
  (((t11.S2PM & 1) + (t10.D2U & 1)) *
   ((t11.P2S & 1) + (t10.U2D & 1)) = 0)) /\
 (r_2a.MODE = 4 =>
  (((t11.S2PM & 1) + (t10.D2U & 1)) *
   ((t11.M2S & 1) + (t10.U2D & 1)) = 0)) /\
 (r_2b.MODE = 4 =>
  (((t11.S2PM & 1) + (t10.D2U & 1)) *
   ((t11.M2S & 1) + (t10.U2D & 1)) = 0)) /\
 (r_5a.MODE = 4 =>
  (((t13.S2PM & 1) + (t14.U2D & 1)) *
   ((t13.P2S & 1) + (t14.D2U & 1)) = 0)) /\
 (r_5b.MODE = 4 =>
  (((t13.S2PM & 1) + (t14.U2D & 1)) *
   ((t13.P2S & 1) + (t14.D2U & 1)) = 0)) /\
 (r_6a.MODE = 4 =>
  (((t13.S2PM & 1) + (t14.U2D & 1)) * ((t13.M2S & 1) + (t14.D2U & 1)) = 0)) /\
 (r_6b.MODE = 4 =>
  (((t13.S2PM & 1) + (t14.U2D & 1)) * ((t13.M2S & 1) + (t14.D2U & 1)) = 0))),

[route_in_use_last_sec_is_free_in_opposite_dir]
((r_1a.MODE = 4 => t12.U2D = 0) /\
 (r_1b.MODE = 4 => t12.U2D = 0) /\
 (r_2a.MODE = 4 => t20.U2D = 0) /\
 (r_2b.MODE = 4 => t20.U2D = 0) /\
 (r_3_.MODE = 4 => t10.D2U = 0) /\
 (r_4_.MODE = 4 => t14.U2D = 0) /\
 (r_5a.MODE = 4 => t12.D2U = 0) /\
 (r_5b.MODE = 4 => t12.D2U = 0) /\ (r_6a.MODE = 4 => t20.D2U = 0) /\
 (r_6b.MODE = 4 => t20.D2U = 0) /\ (r_7_.MODE = 4 => t10.D2U = 0) /\
 (r_8_.MODE = 4 => t14.U2D = 0)),

[routes_share_last_not_used_at_same_time]
((r_1a.MODE = 4 =>
  ((r_1b.MODE ~= 4) /\ (r_5a.MODE ~= 4) /\
   (r_5b.MODE ~= 4))) /\
 (r_1b.MODE = 4 =>
  ((r_1a.MODE ~= 4) /\ (r_5a.MODE ~= 4) /\
   (r_5b.MODE ~= 4))) /\
 (r_2a.MODE = 4 =>
  ((r_2b.MODE ~= 4) /\ (r_6a.MODE ~= 4) /\
   (r_6b.MODE ~= 4))) /\
 (r_2b.MODE = 4 =>
  ((r_2a.MODE ~= 4) /\ (r_6a.MODE ~= 4) /\
   (r_6b.MODE ~= 4))) /\
 (r_3_.MODE = 4 => (r_7_.MODE ~= 4)) /\
 (r_4_.MODE = 4 => (r_8_.MODE ~= 4)) /\
 (r_5a.MODE = 4 =>
  ((r_1a.MODE ~= 4) /\ (r_1b.MODE ~= 4) /\ (r_5b.MODE ~= 4))) /\
 (r_5b.MODE = 4 =>
  ((r_1a.MODE ~= 4) /\ (r_1b.MODE ~= 4) /\ (r_5a.MODE ~= 4))) /\
 (r_6a.MODE = 4 =>
  ((r_2a.MODE ~= 4) /\ (r_2b.MODE ~= 4) /\ (r_6b.MODE ~= 4))) /\
 (r_6b.MODE = 4 =>
  ((r_2a.MODE ~= 4) /\ (r_2b.MODE ~= 4) /\ (r_6a.MODE ~= 4))) /\
 (r_7_.MODE = 4 => (r_3_.MODE ~= 4)) /\ (r_8_.MODE = 4 => (r_4_.MODE ~= 4))),

[first_entry_cnd]
(~(~(t10.D2U + t10.U2D = 0) /\
  mb10.CMD = 1 /\ mb10.ACT = 0) /\
 ~(~(t10.D2U + t10.U2D = 0) /\ mb10.CMD = 1 /\
  mb10.ACT = 0) /\
 ~(~(t10.D2U + t10.U2D = 0) /\ mb10.CMD = 1 /\
  mb10.ACT = 0) /\
 ~(~(t10.D2U + t10.U2D = 0) /\ mb10.CMD = 1 /\
  mb10.ACT = 0) /\
 ~(~(t11.S2PM + t11.P2S + t11.M2S = 0) /\
  mb12.CMD = 1 /\ mb12.ACT = 0) /\
 ~(~(t13.S2PM + t13.P2S + t13.M2S = 0) /\ mb13.CMD = 1 /\
  mb13.ACT = 0) /\
 ~(~(t14.D2U + t14.U2D = 0) /\ mb15.CMD = 1 /\ mb15.ACT = 0) /\
 ~(~(t14.D2U + t14.U2D = 0) /\ mb15.CMD = 1 /\ mb15.ACT = 0) /\
 ~(~(t14.D2U + t14.U2D = 0) /\ mb15.CMD = 1 /\ mb15.ACT = 0) /\
 ~(~(t14.D2U + t14.U2D = 0) /\ mb15.CMD = 1 /\ mb15.ACT = 0) /\
 ~(~(t11.S2PM + t11.P2S + t11.M2S = 0) /\ mb20.CMD = 1 /\ mb20.ACT = 0) /\
 ~(~(t13.S2PM + t13.P2S + t13.M2S = 0) /\ mb21.CMD = 1 /\ mb21.ACT = 0)),

[entry_signal_closed_when_tail_in_first]
((((t10.D2U & 2) >> 1) => mb10.ACT = 0) /\
 (((t10.D2U & 2) >> 1) => mb10.ACT = 0) /\
 (((t10.D2U & 2) >> 1) => mb10.ACT = 0) /\
 (((t10.D2U & 2) >> 1) => mb10.ACT = 0) /\
 (((t11.P2S & 2) >> 1) => mb12.ACT = 0) /\
 (((t13.P2S & 2) >> 1) => mb13.ACT = 0) /\
 (((t14.U2D & 2) >> 1) => mb15.ACT = 0) /\
 (((t14.U2D & 2) >> 1) => mb15.ACT = 0) /\
 (((t14.U2D & 2) >> 1) => mb15.ACT = 0) /\
 (((t14.U2D & 2) >> 1) => mb15.ACT = 0) /\
 (((t11.M2S & 2) >> 1) => mb20.ACT = 0) /\
 (((t13.M2S & 2) >> 1) => mb21.ACT = 0)),

[signal_cmd_open_cnd]
((mb10.CMD = 1 =>
  (((r_1a.MODE = 3) + (r_1b.MODE = 3) + (r_2a.MODE = 3) +
    (r_2b.MODE = 3)) = 1)) /\
 (mb12.CMD = 1 => ((r_3_.MODE = 3) = 1)) /\
 (mb13.CMD = 1 => ((r_4_.MODE = 3) = 1)) /\
 (mb15.CMD = 1 =>
  (((r_5a.MODE = 3) + (r_5b.MODE = 3) + (r_6a.MODE = 3) +
    (r_6b.MODE = 3)) = 1)) /\ (mb20.CMD = 1 => ((r_7_.MODE = 3) = 1)) /\
 (mb21.CMD = 1 => ((r_8_.MODE = 3) = 1))),

[signal_act_open_cnd]
((mb10.ACT = 1 =>
  ((((r_1a.MODE = 3 /\
      (mb10.CMD = 1 \/
       (t10.D2U >> 2) ~= 0)) \/
     (r_1a.MODE = 4 /\ mb10.CMD = 0 /\
      (t10.D2U >> 2) ~= 0)) /\
    (((t12.D2U + t12.U2D = 0) /\
      t12.MODE = 1) /\
     ((t11.S2PM + t11.P2S + t11.M2S = 0) /\
      t11.MODE = 1)) +
    ((r_1b.MODE = 3 /\
      (mb10.CMD = 1 \/ (t10.D2U >> 2) ~= 0)) \/
     (r_1b.MODE = 4 /\ mb10.CMD = 0 /\
      (t10.D2U >> 2) ~= 0)) /\
    (((t12.D2U + t12.U2D = 0) /\ t12.MODE = 1) /\
     ((t11.S2PM + t11.P2S + t11.M2S = 0) /\
      t11.MODE = 1)) +
    ((r_2a.MODE = 3 /\
      (mb10.CMD = 1 \/ (t10.D2U >> 2) ~= 0)) \/
     (r_2a.MODE = 4 /\ mb10.CMD = 0 /\
      (t10.D2U >> 2) ~= 0)) /\
    (((t20.D2U + t20.U2D = 0) /\ t20.MODE = 1) /\
     ((t11.S2PM + t11.P2S + t11.M2S = 0) /\
      t11.MODE = 1)) +
    ((r_2b.MODE = 3 /\
      (mb10.CMD = 1 \/ (t10.D2U >> 2) ~= 0)) \/
     (r_2b.MODE = 4 /\ mb10.CMD = 0 /\
      (t10.D2U >> 2) ~= 0)) /\
    (((t20.D2U + t20.U2D = 0) /\ t20.MODE = 1) /\
     ((t11.S2PM + t11.P2S + t11.M2S = 0) /\ t11.MODE = 1))) =
   1)) /\
 (mb12.ACT = 1 =>
  (((r_3_.MODE = 3 /\
     (mb12.CMD = 1 \/ (t11.P2S >> 2) ~= 0)) \/
    (r_3_.MODE = 4 /\ mb12.CMD = 0 /\ (t11.P2S >> 2) ~= 0)) /\
   ((t10.D2U + t10.U2D = 0) /\ t10.MODE = 1) = 1)) /\
 (mb13.ACT = 1 =>
  (((r_4_.MODE = 3 /\ (mb13.CMD = 1 \/ (t13.P2S >> 2) ~= 0)) \/
    (r_4_.MODE = 4 /\ mb13.CMD = 0 /\ (t13.P2S >> 2) ~= 0)) /\
   ((t14.D2U + t14.U2D = 0) /\ t14.MODE = 1) = 1)) /\
 (mb15.ACT = 1 =>
  ((((r_5a.MODE = 3 /\
      (mb15.CMD = 1 \/ (t14.U2D >> 2) ~= 0)) \/
     (r_5a.MODE = 4 /\ mb15.CMD = 0 /\
      (t14.U2D >> 2) ~= 0)) /\
    (((t12.D2U + t12.U2D = 0) /\ t12.MODE = 1) /\
     ((t13.S2PM + t13.P2S + t13.M2S = 0) /\
      t13.MODE = 1)) +
    ((r_5b.MODE = 3 /\
      (mb15.CMD = 1 \/ (t14.U2D >> 2) ~= 0)) \/
     (r_5b.MODE = 4 /\ mb15.CMD = 0 /\
      (t14.U2D >> 2) ~= 0)) /\
    (((t12.D2U + t12.U2D = 0) /\ t12.MODE = 1) /\
     ((t13.S2PM + t13.P2S + t13.M2S = 0) /\ t13.MODE = 1)) +
    ((r_6a.MODE = 3 /\
      (mb15.CMD = 1 \/ (t14.U2D >> 2) ~= 0)) \/
     (r_6a.MODE = 4 /\ mb15.CMD = 0 /\ (t14.U2D >> 2) ~= 0)) /\
    (((t20.D2U + t20.U2D = 0) /\ t20.MODE = 1) /\
     ((t13.S2PM + t13.P2S + t13.M2S = 0) /\ t13.MODE = 1)) +
    ((r_6b.MODE = 3 /\
      (mb15.CMD = 1 \/ (t14.U2D >> 2) ~= 0)) \/
     (r_6b.MODE = 4 /\ mb15.CMD = 0 /\ (t14.U2D >> 2) ~= 0)) /\
    (((t20.D2U + t20.U2D = 0) /\ t20.MODE = 1) /\
     ((t13.S2PM + t13.P2S + t13.M2S = 0) /\ t13.MODE = 1))) = 1)) /\
 (mb20.ACT = 1 =>
  (((r_7_.MODE = 3 /\ (mb20.CMD = 1 \/ (t11.M2S >> 2) ~= 0)) \/
    (r_7_.MODE = 4 /\ mb20.CMD = 0 /\ (t11.M2S >> 2) ~= 0)) /\
   ((t10.D2U + t10.U2D = 0) /\ t10.MODE = 1) = 1)) /\
 (mb21.ACT = 1 =>
  (((r_8_.MODE = 3 /\ (mb21.CMD = 1 \/ (t13.M2S >> 2) ~= 0)) \/
    (r_8_.MODE = 4 /\ mb21.CMD = 0 /\ (t13.M2S >> 2) ~= 0)) /\
   ((t14.D2U + t14.U2D = 0) /\ t14.MODE = 1) = 1))),

[not_commanding_occupied_point_to_move]
(((~(t11.S2PM + t11.P2S + t11.M2S = 0) \/ t11.MODE = 2) =>
  t11.POS = t11.CMD) /\
 ((~(t13.S2PM + t13.P2S + t13.M2S = 0) \/ t13.MODE = 2) => t13.POS = t13.CMD)),

[point_only_cmd_when_alloc_a_route]
((t11.CMD ~= t11.POS =>
  (t11.MODE ~= 2 /\
   ((r_1a.MODE = 2) \/ (r_1b.MODE = 2) \/ (r_2a.MODE = 2) \/
    (r_2b.MODE = 2) \/ (r_3_.MODE = 2) \/ (r_5a.MODE = 2) \/
    (r_6a.MODE = 2) \/ (r_7_.MODE = 2)))) /\
 (t13.CMD ~= t13.POS =>
  (t13.MODE ~= 2 /\
   ((r_1a.MODE = 2) \/ (r_2a.MODE = 2) \/ (r_4_.MODE = 2) \/
    (r_5a.MODE = 2) \/ (r_5b.MODE = 2) \/ (r_6a.MODE = 2) \/
    (r_6b.MODE = 2) \/ (r_8_.MODE = 2))))),

[ground_unused_signal]
((mb11.ACT = 0 /\ mb11.CMD = 0) /\ (mb14.ACT = 0 /\ mb14.CMD = 0)),

[ground_unused_linear_to_down]
1,

[ground_unused_linear_to_up]
1,

[ground_unused_point_p]
1,

[ground_unused_point_m]
1,

[ground_unused_point_s]
1,

[ground_unused_boundary_linear]
((b10.U2D = 0 /\ b10.D2U = 0) /\ (b14.U2D = 0 /\ b14.D2U = 0)),

[element_prev_variable]
((t10.PREV = 1 => t10.MODE = 2) /\ (t12.PREV = 1 => t12.MODE = 2) /\
 (t14.PREV = 1 => t14.MODE = 2) /\ (t20.PREV = 1 => t20.MODE = 2) /\
 (t11.PREV = 1 => t11.MODE = 2) /\ (t13.PREV = 1 => t13.MODE = 2)),

[occupied_implies_exlck_or_used_point]
((~(t11.S2PM + t11.P2S + t11.M2S = 0) => (t11.MODE = 1 \/ t11.MODE = 2)) /\
 (~(t13.S2PM + t13.P2S + t13.M2S = 0) => (t13.MODE = 1 \/ t13.MODE = 2))),

[occupied_implies_exlck_or_used_linear]
1,

[point_chunk_cnd_stem_plus]
1,

[point_chunk_cnd_stem_minus]
1,

[hto_vs_mode]
((((t10.D2U = 1 =>
    t10.MODE = 2) /\
   (t10.D2U = 3 => t10.MODE = 2) /\
   (t10.D2U = 5 =>
    t10.MODE = 1 \/ t10.MODE = 2) /\
   (t10.D2U = 7 => t10.MODE = 2)) /\
  ((t11.S2PM = 1 => t11.MODE = 2) /\
   (t11.S2PM = 3 => t11.MODE = 2) /\
   (t11.S2PM = 5 =>
    t11.MODE = 1 \/ t11.MODE = 2) /\
   (t11.S2PM = 7 => t11.MODE = 2))) /\
 (((t10.D2U = 1 => t10.MODE = 2) /\
   (t10.D2U = 3 => t10.MODE = 2) /\
   (t10.D2U = 5 =>
    t10.MODE = 1 \/ t10.MODE = 2) /\
   (t10.D2U = 7 => t10.MODE = 2)) /\
  ((t11.S2PM = 1 => t11.MODE = 2) /\
   (t11.S2PM = 3 => t11.MODE = 2) /\
   (t11.S2PM = 5 =>
    t11.MODE = 1 \/ t11.MODE = 2) /\
   (t11.S2PM = 7 => t11.MODE = 2))) /\
 (((t10.D2U = 1 => t10.MODE = 2) /\
   (t10.D2U = 3 => t10.MODE = 2) /\
   (t10.D2U = 5 =>
    t10.MODE = 1 \/ t10.MODE = 2) /\
   (t10.D2U = 7 => t10.MODE = 2)) /\
  ((t11.S2PM = 1 => t11.MODE = 2) /\
   (t11.S2PM = 3 => t11.MODE = 2) /\
   (t11.S2PM = 5 =>
    t11.MODE = 1 \/ t11.MODE = 2) /\
   (t11.S2PM = 7 => t11.MODE = 2))) /\
 (((t10.D2U = 1 => t10.MODE = 2) /\
   (t10.D2U = 3 => t10.MODE = 2) /\
   (t10.D2U = 5 =>
    t10.MODE = 1 \/ t10.MODE = 2) /\
   (t10.D2U = 7 => t10.MODE = 2)) /\
  ((t11.S2PM = 1 => t11.MODE = 2) /\
   (t11.S2PM = 3 => t11.MODE = 2) /\
   (t11.S2PM = 5 => t11.MODE = 1 \/ t11.MODE = 2) /\
   (t11.S2PM = 7 => t11.MODE = 2))) /\
 ((t11.P2S = 1 => t11.MODE = 2) /\
  (t11.P2S = 3 => t11.MODE = 2) /\
  (t11.P2S = 5 => t11.MODE = 1 \/ t11.MODE = 2) /\
  (t11.P2S = 7 => t11.MODE = 2)) /\
 ((t13.P2S = 1 => t13.MODE = 2) /\
  (t13.P2S = 3 => t13.MODE = 2) /\
  (t13.P2S = 5 => t13.MODE = 1 \/ t13.MODE = 2) /\
  (t13.P2S = 7 => t13.MODE = 2)) /\
 (((t14.U2D = 1 => t14.MODE = 2) /\
   (t14.U2D = 3 => t14.MODE = 2) /\
   (t14.U2D = 5 => t14.MODE = 1 \/ t14.MODE = 2) /\
   (t14.U2D = 7 => t14.MODE = 2)) /\
  ((t13.S2PM = 1 => t13.MODE = 2) /\
   (t13.S2PM = 3 => t13.MODE = 2) /\
   (t13.S2PM = 5 => t13.MODE = 1 \/ t13.MODE = 2) /\
   (t13.S2PM = 7 => t13.MODE = 2))) /\
 (((t14.U2D = 1 => t14.MODE = 2) /\
   (t14.U2D = 3 => t14.MODE = 2) /\
   (t14.U2D = 5 => t14.MODE = 1 \/ t14.MODE = 2) /\
   (t14.U2D = 7 => t14.MODE = 2)) /\
  ((t13.S2PM = 1 => t13.MODE = 2) /\
   (t13.S2PM = 3 => t13.MODE = 2) /\
   (t13.S2PM = 5 => t13.MODE = 1 \/ t13.MODE = 2) /\
   (t13.S2PM = 7 => t13.MODE = 2))) /\
 (((t14.U2D = 1 => t14.MODE = 2) /\
   (t14.U2D = 3 => t14.MODE = 2) /\
   (t14.U2D = 5 => t14.MODE = 1 \/ t14.MODE = 2) /\
   (t14.U2D = 7 => t14.MODE = 2)) /\
  ((t13.S2PM = 1 => t13.MODE = 2) /\
   (t13.S2PM = 3 => t13.MODE = 2) /\
   (t13.S2PM = 5 => t13.MODE = 1 \/ t13.MODE = 2) /\
   (t13.S2PM = 7 => t13.MODE = 2))) /\
 (((t14.U2D = 1 => t14.MODE = 2) /\
   (t14.U2D = 3 => t14.MODE = 2) /\
   (t14.U2D = 5 => t14.MODE = 1 \/ t14.MODE = 2) /\
   (t14.U2D = 7 => t14.MODE = 2)) /\
  ((t13.S2PM = 1 => t13.MODE = 2) /\
   (t13.S2PM = 3 => t13.MODE = 2) /\
   (t13.S2PM = 5 => t13.MODE = 1 \/ t13.MODE = 2) /\
   (t13.S2PM = 7 => t13.MODE = 2))) /\
 ((t11.M2S = 1 => t11.MODE = 2) /\ (t11.M2S = 3 => t11.MODE = 2) /\
  (t11.M2S = 5 => t11.MODE = 1 \/ t11.MODE = 2) /\
  (t11.M2S = 7 => t11.MODE = 2)) /\
 ((t13.M2S = 1 => t13.MODE = 2) /\ (t13.M2S = 3 => t13.MODE = 2) /\
  (t13.M2S = 5 => t13.MODE = 1 \/ t13.MODE = 2) /\
  (t13.M2S = 7 => t13.MODE = 2))),

[hto_vs_mode_last_down]
(((t12.D2U = 1 => t12.MODE = 2) /\
  (t12.D2U = 3 => t12.MODE = 0 \/ t12.MODE = 2) /\
  (t12.D2U = 5 => t12.MODE = 1 \/ t12.MODE = 2) /\
  (t12.D2U = 7 => t12.MODE = 0 \/ t12.MODE = 2) /\
  ((r_1a.MODE = 4 /\ t12.MODE = 2 /\ t12.PREV = 1 /\
    t12.D2U = 0) =>
   (t12.U2D = 0 /\ ((t13.P2S & 2) >> 1) = 1))) /\
 ((t12.D2U = 1 => t12.MODE = 2) /\
  (t12.D2U = 3 => t12.MODE = 0 \/ t12.MODE = 2) /\
  (t12.D2U = 5 => t12.MODE = 1 \/ t12.MODE = 2) /\
  (t12.D2U = 7 => t12.MODE = 0 \/ t12.MODE = 2) /\
  ((r_1b.MODE = 4 /\ t12.MODE = 2 /\ t12.PREV = 1 /\
    t12.D2U = 0) =>
   (t12.U2D = 0 /\ ((t13.P2S & 2) >> 1) = 1))) /\
 ((t20.D2U = 1 => t20.MODE = 2) /\
  (t20.D2U = 3 => t20.MODE = 0 \/ t20.MODE = 2) /\
  (t20.D2U = 5 => t20.MODE = 1 \/ t20.MODE = 2) /\
  (t20.D2U = 7 => t20.MODE = 0 \/ t20.MODE = 2) /\
  ((r_2a.MODE = 4 /\ t20.MODE = 2 /\ t20.PREV = 1 /\
    t20.D2U = 0) => (t20.U2D = 0 /\ ((t13.M2S & 2) >> 1) = 1))) /\
 ((t20.D2U = 1 => t20.MODE = 2) /\
  (t20.D2U = 3 => t20.MODE = 0 \/ t20.MODE = 2) /\
  (t20.D2U = 5 => t20.MODE = 1 \/ t20.MODE = 2) /\
  (t20.D2U = 7 => t20.MODE = 0 \/ t20.MODE = 2) /\
  ((r_2b.MODE = 4 /\ t20.MODE = 2 /\ t20.PREV = 1 /\ t20.D2U = 0) =>
   (t20.U2D = 0 /\ ((t13.M2S & 2) >> 1) = 1))) /\
 ((t14.D2U = 1 => t14.MODE = 2) /\
  (t14.D2U = 3 => t14.MODE = 0 \/ t14.MODE = 2) /\
  (t14.D2U = 5 => t14.MODE = 1 \/ t14.MODE = 2) /\
  (t14.D2U = 7 => t14.MODE = 0 \/ t14.MODE = 2) /\
  ((r_4_.MODE = 4 /\ t14.MODE = 2 /\ t14.PREV = 1 /\ t14.D2U = 0) =>
   t14.U2D = 0)) /\
 ((t14.D2U = 1 => t14.MODE = 2) /\
  (t14.D2U = 3 => t14.MODE = 0 \/ t14.MODE = 2) /\
  (t14.D2U = 5 => t14.MODE = 1 \/ t14.MODE = 2) /\
  (t14.D2U = 7 => t14.MODE = 0 \/ t14.MODE = 2) /\
  ((r_8_.MODE = 4 /\ t14.MODE = 2 /\ t14.PREV = 1 /\ t14.D2U = 0) =>
   t14.U2D = 0))),

[hto_vs_mode_last_up]
(((t10.U2D = 1 => t10.MODE = 2) /\
  (t10.U2D = 3 => t10.MODE = 0 \/ t10.MODE = 2) /\
  (t10.U2D = 5 => t10.MODE = 1 \/ t10.MODE = 2) /\
  (t10.U2D = 7 => t10.MODE = 0 \/ t10.MODE = 2) /\
  ((r_3_.MODE = 4 /\ t10.MODE = 2 /\ t10.PREV = 1 /\
    t10.U2D = 0) => t10.D2U = 0)) /\
 ((t12.U2D = 1 => t12.MODE = 2) /\
  (t12.U2D = 3 => t12.MODE = 0 \/ t12.MODE = 2) /\
  (t12.U2D = 5 => t12.MODE = 1 \/ t12.MODE = 2) /\
  (t12.U2D = 7 => t12.MODE = 0 \/ t12.MODE = 2) /\
  ((r_5a.MODE = 4 /\ t12.MODE = 2 /\ t12.PREV = 1 /\
    t12.U2D = 0) =>
   (t12.D2U = 0 /\ ((t11.P2S & 2) >> 1) = 1))) /\
 ((t12.U2D = 1 => t12.MODE = 2) /\
  (t12.U2D = 3 => t12.MODE = 0 \/ t12.MODE = 2) /\
  (t12.U2D = 5 => t12.MODE = 1 \/ t12.MODE = 2) /\
  (t12.U2D = 7 => t12.MODE = 0 \/ t12.MODE = 2) /\
  ((r_5b.MODE = 4 /\ t12.MODE = 2 /\ t12.PREV = 1 /\
    t12.U2D = 0) => (t12.D2U = 0 /\ ((t11.P2S & 2) >> 1) = 1))) /\
 ((t20.U2D = 1 => t20.MODE = 2) /\
  (t20.U2D = 3 => t20.MODE = 0 \/ t20.MODE = 2) /\
  (t20.U2D = 5 => t20.MODE = 1 \/ t20.MODE = 2) /\
  (t20.U2D = 7 => t20.MODE = 0 \/ t20.MODE = 2) /\
  ((r_6a.MODE = 4 /\ t20.MODE = 2 /\ t20.PREV = 1 /\ t20.U2D = 0) =>
   (t20.D2U = 0 /\ ((t11.M2S & 2) >> 1) = 1))) /\
 ((t20.U2D = 1 => t20.MODE = 2) /\
  (t20.U2D = 3 => t20.MODE = 0 \/ t20.MODE = 2) /\
  (t20.U2D = 5 => t20.MODE = 1 \/ t20.MODE = 2) /\
  (t20.U2D = 7 => t20.MODE = 0 \/ t20.MODE = 2) /\
  ((r_6b.MODE = 4 /\ t20.MODE = 2 /\ t20.PREV = 1 /\ t20.U2D = 0) =>
   (t20.D2U = 0 /\ ((t11.M2S & 2) >> 1) = 1))) /\
 ((t10.U2D = 1 => t10.MODE = 2) /\
  (t10.U2D = 3 => t10.MODE = 0 \/ t10.MODE = 2) /\
  (t10.U2D = 5 => t10.MODE = 1 \/ t10.MODE = 2) /\
  (t10.U2D = 7 => t10.MODE = 0 \/ t10.MODE = 2) /\
  ((r_7_.MODE = 4 /\ t10.MODE = 2 /\ t10.PREV = 1 /\ t10.U2D = 0) =>
   t10.D2U = 0))),

[elem_locked_by_only_one_route]
((t10.MODE = 1 =>
  ((((r_1a.MODE = 2) \/ (r_1a.MODE = 3)) +
    ((r_1b.MODE = 2) \/ (r_1b.MODE = 3)) +
    ((r_2a.MODE = 2) \/ (r_2a.MODE = 3)) +
    ((r_2b.MODE = 2) \/ (r_2b.MODE = 3)) +
    ((r_3_.MODE = 2) \/ (r_3_.MODE = 3) \/
     (r_3_.MODE = 4 /\
      (t10.U2D = 5 /\ t11.MODE = 2 /\
       t11.POS = 0 /\ (t11.P2S & 5) = 1) \/
      ((t10.D2U + t10.U2D = 0) /\
       (t11.MODE = 1 \/ t11.MODE = 2) /\
       (t11.POS = 0 /\ t11.CMD = 0)))) +
    ((r_7_.MODE = 2) \/ (r_7_.MODE = 3) \/
     (r_7_.MODE = 4 /\
      (t10.U2D = 5 /\ t11.MODE = 2 /\ t11.POS = 1 /\
       (t11.M2S & 5) = 1) \/
      ((t10.D2U + t10.U2D = 0) /\
       (t11.MODE = 1 \/ t11.MODE = 2) /\
       (t11.POS = 1 /\ t11.CMD = 1))))) = 1)) /\
 (t12.MODE = 1 =>
  ((((r_1a.MODE = 2) \/ (r_1a.MODE = 3) \/
     (r_1a.MODE = 4 /\
      (t12.D2U = 5 /\ t11.MODE = 2 /\
       t11.POS = 0 /\ (t11.S2PM & 5) = 1) \/
      ((t12.D2U + t12.U2D = 0) /\
       (t11.MODE = 1 \/ t11.MODE = 2) /\
       (t11.POS = 0 /\ t11.CMD = 0)))) +
    ((r_1b.MODE = 2) \/ (r_1b.MODE = 3) \/
     (r_1b.MODE = 4 /\
      (t12.D2U = 5 /\ t11.MODE = 2 /\
       t11.POS = 0 /\ (t11.S2PM & 5) = 1) \/
      ((t12.D2U + t12.U2D = 0) /\
       (t11.MODE = 1 \/ t11.MODE = 2) /\
       (t11.POS = 0 /\ t11.CMD = 0)))) +
    ((r_5a.MODE = 2) \/ (r_5a.MODE = 3) \/
     (r_5a.MODE = 4 /\
      (t12.U2D = 5 /\ t13.MODE = 2 /\ t13.POS = 0 /\
       (t13.S2PM & 5) = 1) \/
      ((t12.D2U + t12.U2D = 0) /\
       (t13.MODE = 1 \/ t13.MODE = 2) /\
       (t13.POS = 0 /\ t13.CMD = 0)))) +
    ((r_5b.MODE = 2) \/ (r_5b.MODE = 3) \/
     (r_5b.MODE = 4 /\
      (t12.U2D = 5 /\ t13.MODE = 2 /\ t13.POS = 0 /\
       (t13.S2PM & 5) = 1) \/
      ((t12.D2U + t12.U2D = 0) /\
       (t13.MODE = 1 \/ t13.MODE = 2) /\
       (t13.POS = 0 /\ t13.CMD = 0))))) = 1)) /\
 (t14.MODE = 1 =>
  ((((r_4_.MODE = 2) \/ (r_4_.MODE = 3) \/
     (r_4_.MODE = 4 /\
      (t14.D2U = 5 /\ t13.MODE = 2 /\
       t13.POS = 0 /\ (t13.P2S & 5) = 1) \/
      ((t14.D2U + t14.U2D = 0) /\
       (t13.MODE = 1 \/ t13.MODE = 2) /\
       (t13.POS = 0 /\ t13.CMD = 0)))) +
    ((r_5a.MODE = 2) \/ (r_5a.MODE = 3)) +
    ((r_5b.MODE = 2) \/ (r_5b.MODE = 3)) +
    ((r_6a.MODE = 2) \/ (r_6a.MODE = 3)) +
    ((r_6b.MODE = 2) \/ (r_6b.MODE = 3)) +
    ((r_8_.MODE = 2) \/ (r_8_.MODE = 3) \/
     (r_8_.MODE = 4 /\
      (t14.D2U = 5 /\ t13.MODE = 2 /\ t13.POS = 1 /\
       (t13.M2S & 5) = 1) \/
      ((t14.D2U + t14.U2D = 0) /\
       (t13.MODE = 1 \/ t13.MODE = 2) /\
       (t13.POS = 1 /\ t13.CMD = 1))))) = 1)) /\
 (t20.MODE = 1 =>
  ((((r_2a.MODE = 2) \/ (r_2a.MODE = 3) \/
     (r_2a.MODE = 4 /\
      (t20.D2U = 5 /\ t11.MODE = 2 /\ t11.POS = 1 /\
       (t11.S2PM & 5) = 1) \/
      ((t20.D2U + t20.U2D = 0) /\
       (t11.MODE = 1 \/ t11.MODE = 2) /\
       (t11.POS = 1 /\ t11.CMD = 1)))) +
    ((r_2b.MODE = 2) \/ (r_2b.MODE = 3) \/
     (r_2b.MODE = 4 /\
      (t20.D2U = 5 /\ t11.MODE = 2 /\ t11.POS = 1 /\
       (t11.S2PM & 5) = 1) \/
      ((t20.D2U + t20.U2D = 0) /\
       (t11.MODE = 1 \/ t11.MODE = 2) /\
       (t11.POS = 1 /\ t11.CMD = 1)))) +
    ((r_6a.MODE = 2) \/ (r_6a.MODE = 3) \/
     (r_6a.MODE = 4 /\
      (t20.U2D = 5 /\ t13.MODE = 2 /\ t13.POS = 1 /\
       (t13.S2PM & 5) = 1) \/
      ((t20.D2U + t20.U2D = 0) /\
       (t13.MODE = 1 \/ t13.MODE = 2) /\
       (t13.POS = 1 /\ t13.CMD = 1)))) +
    ((r_6b.MODE = 2) \/ (r_6b.MODE = 3) \/
     (r_6b.MODE = 4 /\
      (t20.U2D = 5 /\ t13.MODE = 2 /\ t13.POS = 1 /\
       (t13.S2PM & 5) = 1) \/
      ((t20.D2U + t20.U2D = 0) /\
       (t13.MODE = 1 \/ t13.MODE = 2) /\
       (t13.POS = 1 /\ t13.CMD = 1))))) = 1)) /\
 (t11.MODE = 1 =>
  ((((r_1a.MODE = 2) \/ (r_1a.MODE = 3) \/
     (r_1a.MODE = 4 /\
      (t11.POS = 0 /\ t11.CMD = 0) /\
      (t12.MODE = 1 /\ (t12.D2U + t12.U2D = 0)) /\
      (t11.S2PM = 5 /\ t10.MODE = 2 /\
       (t10.D2U & 5) = 1) \/
      (t11.S2PM + t11.P2S + t11.M2S = 0) /\
      (t10.MODE = 1 \/ t10.MODE = 2))) +
    ((r_1b.MODE = 2) \/ (r_1b.MODE = 3) \/
     (r_1b.MODE = 4 /\ (t11.POS = 0 /\ t11.CMD = 0) /\
      (t12.MODE = 1 /\ (t12.D2U + t12.U2D = 0)) /\
      (t11.S2PM = 5 /\ t10.MODE = 2 /\ (t10.D2U & 5) = 1) \/
      (t11.S2PM + t11.P2S + t11.M2S = 0) /\
      (t10.MODE = 1 \/ t10.MODE = 2))) +
    ((r_2a.MODE = 2) \/ (r_2a.MODE = 3) \/
     (r_2a.MODE = 4 /\ (t11.POS = 1 /\ t11.CMD = 1) /\
      (t20.MODE = 1 /\ (t20.D2U + t20.U2D = 0)) /\
      (t11.S2PM = 5 /\ t10.MODE = 2 /\ (t10.D2U & 5) = 1) \/
      (t11.S2PM + t11.P2S + t11.M2S = 0) /\
      (t10.MODE = 1 \/ t10.MODE = 2))) +
    ((r_2b.MODE = 2) \/ (r_2b.MODE = 3) \/
     (r_2b.MODE = 4 /\ (t11.POS = 1 /\ t11.CMD = 1) /\
      (t20.MODE = 1 /\ (t20.D2U + t20.U2D = 0)) /\
      (t11.S2PM = 5 /\ t10.MODE = 2 /\ (t10.D2U & 5) = 1) \/
      (t11.S2PM + t11.P2S + t11.M2S = 0) /\
      (t10.MODE = 1 \/ t10.MODE = 2))) +
    ((r_3_.MODE = 2) \/ (r_3_.MODE = 3)) +
    ((r_7_.MODE = 2) \/ (r_7_.MODE = 3))) = 1)) /\
 (t13.MODE = 1 =>
  ((((r_4_.MODE = 2) \/ (r_4_.MODE = 3)) +
    ((r_5a.MODE = 2) \/ (r_5a.MODE = 3) \/
     (r_5a.MODE = 4 /\ (t13.POS = 0 /\ t13.CMD = 0) /\
      (t12.MODE = 1 /\ (t12.D2U + t12.U2D = 0)) /\
      (t13.S2PM = 5 /\ t14.MODE = 2 /\ (t14.U2D & 5) = 1) \/
      (t13.S2PM + t13.P2S + t13.M2S = 0) /\
      (t14.MODE = 1 \/ t14.MODE = 2))) +
    ((r_5b.MODE = 2) \/ (r_5b.MODE = 3) \/
     (r_5b.MODE = 4 /\ (t13.POS = 0 /\ t13.CMD = 0) /\
      (t12.MODE = 1 /\ (t12.D2U + t12.U2D = 0)) /\
      (t13.S2PM = 5 /\ t14.MODE = 2 /\ (t14.U2D & 5) = 1) \/
      (t13.S2PM + t13.P2S + t13.M2S = 0) /\
      (t14.MODE = 1 \/ t14.MODE = 2))) +
    ((r_6a.MODE = 2) \/ (r_6a.MODE = 3) \/
     (r_6a.MODE = 4 /\ (t13.POS = 1 /\ t13.CMD = 1) /\
      (t20.MODE = 1 /\ (t20.D2U + t20.U2D = 0)) /\
      (t13.S2PM = 5 /\ t14.MODE = 2 /\ (t14.U2D & 5) = 1) \/
      (t13.S2PM + t13.P2S + t13.M2S = 0) /\
      (t14.MODE = 1 \/ t14.MODE = 2))) +
    ((r_6b.MODE = 2) \/ (r_6b.MODE = 3) \/
     (r_6b.MODE = 4 /\ (t13.POS = 1 /\ t13.CMD = 1) /\
      (t20.MODE = 1 /\ (t20.D2U + t20.U2D = 0)) /\
      (t13.S2PM = 5 /\ t14.MODE = 2 /\ (t14.U2D & 5) = 1) \/
      (t13.S2PM + t13.P2S + t13.M2S = 0) /\
      (t14.MODE = 1 \/ t14.MODE = 2))) +
    ((r_8_.MODE = 2) \/ (r_8_.MODE = 3))) = 1))),

[elem_used_by_only_one_route]
((t10.MODE = 2 =>
  (((r_1a.MODE = 4 /\ ~t11.PREV /\
     (t11.POS = 0 /\ t11.CMD = 0) /\
     ((t11.MODE = 1 /\
       ((t11.S2PM = 5 /\
         (t10.D2U & 5) = 1) \/
        ((t11.S2PM + t11.P2S +
          t11.M2S = 0) /\
         (t10.D2U >> 2) = 1)) /\
       (t12.MODE = 1)) \/
      (t11.MODE = 2 /\
       (((t10.D2U & 5) = 1 /\
         (t11.S2PM & 3) = 1) \/
        (t10.D2U + t10.U2D = 0) /\
        ((t11.S2PM & 2) >> 1) = 1)))) +
    (r_1b.MODE = 4 /\ ~t11.PREV /\
     (t11.POS = 0 /\ t11.CMD = 0) /\
     ((t11.MODE = 1 /\
       ((t11.S2PM = 5 /\
         (t10.D2U & 5) = 1) \/
        ((t11.S2PM + t11.P2S +
          t11.M2S = 0) /\
         (t10.D2U >> 2) = 1)) /\
       (t12.MODE = 1)) \/
      (t11.MODE = 2 /\
       (((t10.D2U & 5) = 1 /\
         (t11.S2PM & 3) = 1) \/
        (t10.D2U + t10.U2D = 0) /\
        ((t11.S2PM & 2) >> 1) = 1)))) +
    (r_2a.MODE = 4 /\ ~t11.PREV /\
     (t11.POS = 1 /\ t11.CMD = 1) /\
     ((t11.MODE = 1 /\
       ((t11.S2PM = 5 /\
         (t10.D2U & 5) = 1) \/
        ((t11.S2PM + t11.P2S +
          t11.M2S = 0) /\
         (t10.D2U >> 2) = 1)) /\
       (t20.MODE = 1)) \/
      (t11.MODE = 2 /\
       (((t10.D2U & 5) = 1 /\
         (t11.S2PM & 3) = 1) \/
        (t10.D2U + t10.U2D = 0) /\
        ((t11.S2PM & 2) >> 1) = 1)))) +
    (r_2b.MODE = 4 /\ ~t11.PREV /\
     (t11.POS = 1 /\ t11.CMD = 1) /\
     ((t11.MODE = 1 /\
       ((t11.S2PM = 5 /\
         (t10.D2U & 5) = 1) \/
        ((t11.S2PM + t11.P2S +
          t11.M2S = 0) /\
         (t10.D2U >> 2) = 1)) /\
       (t20.MODE = 1)) \/
      (t11.MODE = 2 /\
       (((t10.D2U & 5) = 1 /\
         (t11.S2PM & 3) = 1) \/
        (t10.D2U + t10.U2D = 0) /\
        ((t11.S2PM & 2) >> 1) = 1)))) +
    (r_3_.MODE = 4 /\ t10.PREV \/
     (t11.POS = 0 /\ t11.MODE = 2 /\
      ((t11.P2S & 5) = 1 \/
       (t11.S2PM + t11.P2S + t11.M2S = 0) /\
       ((t10.U2D & 2) >> 1) = 1))) +
    (r_7_.MODE = 4 /\ t10.PREV \/
     (t11.POS = 1 /\ t11.MODE = 2 /\
      ((t11.M2S & 5) = 1 \/
       (t11.S2PM + t11.P2S + t11.M2S = 0) /\
       ((t10.U2D & 2) >> 1) = 1)))) = 1)) /\
 (t12.MODE = 2 =>
  (((r_1a.MODE = 4 /\ t12.PREV \/
     (t11.POS = 0 /\ t11.MODE = 2 /\
      ((t11.S2PM & 5) = 1 \/
       ((t11.S2PM + t11.P2S + t11.M2S = 0) /\
        ((t12.D2U & 2) >> 1) = 1 /\
        t11.PREV)))) +
    (r_1b.MODE = 4 /\ t12.PREV \/
     (t11.POS = 0 /\ t11.MODE = 2 /\
      ((t11.S2PM & 5) = 1 \/
       ((t11.S2PM + t11.P2S + t11.M2S = 0) /\
        ((t12.D2U & 2) >> 1) = 1 /\ t11.PREV)))) +
    (r_5a.MODE = 4 /\ t12.PREV \/
     (t13.POS = 0 /\ t13.MODE = 2 /\
      ((t13.S2PM & 5) = 1 \/
       ((t13.S2PM + t13.P2S + t13.M2S = 0) /\
        ((t12.U2D & 2) >> 1) = 1 /\ t13.PREV)))) +
    (r_5b.MODE = 4 /\ t12.PREV \/
     (t13.POS = 0 /\ t13.MODE = 2 /\
      ((t13.S2PM & 5) = 1 \/
       ((t13.S2PM + t13.P2S + t13.M2S = 0) /\
        ((t12.U2D & 2) >> 1) = 1 /\ t13.PREV))))) = 1)) /\
 (t14.MODE = 2 =>
  (((r_4_.MODE = 4 /\ t14.PREV \/
     (t13.POS = 0 /\ t13.MODE = 2 /\
      ((t13.P2S & 5) = 1 \/
       (t13.S2PM + t13.P2S + t13.M2S = 0) /\
       ((t14.D2U & 2) >> 1) = 1))) +
    (r_5a.MODE = 4 /\ ~t13.PREV /\
     (t13.POS = 0 /\ t13.CMD = 0) /\
     ((t13.MODE = 1 /\
       ((t13.S2PM = 5 /\ (t14.U2D & 5) = 1) \/
        ((t13.S2PM + t13.P2S + t13.M2S =
          0) /\ (t14.U2D >> 2) = 1)) /\
       (t12.MODE = 1)) \/
      (t13.MODE = 2 /\
       (((t14.U2D & 5) = 1 /\ (t13.S2PM & 3) = 1) \/
        (t14.D2U + t14.U2D = 0) /\
        ((t13.S2PM & 2) >> 1) = 1)))) +
    (r_5b.MODE = 4 /\ ~t13.PREV /\
     (t13.POS = 0 /\ t13.CMD = 0) /\
     ((t13.MODE = 1 /\
       ((t13.S2PM = 5 /\ (t14.U2D & 5) = 1) \/
        ((t13.S2PM + t13.P2S + t13.M2S = 0) /\
         (t14.U2D >> 2) = 1)) /\
       (t12.MODE = 1)) \/
      (t13.MODE = 2 /\
       (((t14.U2D & 5) = 1 /\ (t13.S2PM & 3) = 1) \/
        (t14.D2U + t14.U2D = 0) /\
        ((t13.S2PM & 2) >> 1) = 1)))) +
    (r_6a.MODE = 4 /\ ~t13.PREV /\
     (t13.POS = 1 /\ t13.CMD = 1) /\
     ((t13.MODE = 1 /\
       ((t13.S2PM = 5 /\ (t14.U2D & 5) = 1) \/
        ((t13.S2PM + t13.P2S + t13.M2S = 0) /\
         (t14.U2D >> 2) = 1)) /\
       (t20.MODE = 1)) \/
      (t13.MODE = 2 /\
       (((t14.U2D & 5) = 1 /\ (t13.S2PM & 3) = 1) \/
        (t14.D2U + t14.U2D = 0) /\
        ((t13.S2PM & 2) >> 1) = 1)))) +
    (r_6b.MODE = 4 /\ ~t13.PREV /\
     (t13.POS = 1 /\ t13.CMD = 1) /\
     ((t13.MODE = 1 /\
       ((t13.S2PM = 5 /\ (t14.U2D & 5) = 1) \/
        ((t13.S2PM + t13.P2S + t13.M2S = 0) /\
         (t14.U2D >> 2) = 1)) /\ (t20.MODE = 1)) \/
      (t13.MODE = 2 /\
       (((t14.U2D & 5) = 1 /\ (t13.S2PM & 3) = 1) \/
        (t14.D2U + t14.U2D = 0) /\
        ((t13.S2PM & 2) >> 1) = 1)))) +
    (r_8_.MODE = 4 /\ t14.PREV \/
     (t13.POS = 1 /\ t13.MODE = 2 /\
      ((t13.M2S & 5) = 1 \/
       (t13.S2PM + t13.P2S + t13.M2S = 0) /\
       ((t14.D2U & 2) >> 1) = 1)))) = 1)) /\
 (t20.MODE = 2 =>
  (((r_2a.MODE = 4 /\ t20.PREV \/
     (t11.POS = 1 /\ t11.MODE = 2 /\
      ((t11.S2PM & 5) = 1 \/
       ((t11.S2PM + t11.P2S + t11.M2S = 0) /\
        ((t20.D2U & 2) >> 1) = 1 /\ t11.PREV)))) +
    (r_2b.MODE = 4 /\ t20.PREV \/
     (t11.POS = 1 /\ t11.MODE = 2 /\
      ((t11.S2PM & 5) = 1 \/
       ((t11.S2PM + t11.P2S + t11.M2S = 0) /\
        ((t20.D2U & 2) >> 1) = 1 /\ t11.PREV)))) +
    (r_6a.MODE = 4 /\ t20.PREV \/
     (t13.POS = 1 /\ t13.MODE = 2 /\
      ((t13.S2PM & 5) = 1 \/
       ((t13.S2PM + t13.P2S + t13.M2S = 0) /\
        ((t20.U2D & 2) >> 1) = 1 /\ t13.PREV)))) +
    (r_6b.MODE = 4 /\ t20.PREV \/
     (t13.POS = 1 /\ t13.MODE = 2 /\
      ((t13.S2PM & 5) = 1 \/
       ((t13.S2PM + t13.P2S + t13.M2S = 0) /\
        ((t20.U2D & 2) >> 1) = 1 /\ t13.PREV))))) = 1)) /\
 (t11.MODE = 2 =>
  (((r_1a.MODE = 4 /\ t11.POS = 0 /\ t11.PREV \/
     (t10.MODE = 2 /\
      ((t10.D2U & 5) = 1 \/
       (t10.D2U + t10.U2D = 0) /\
       ((t11.S2PM & 2) >> 1) = 1)) /\ ~t12.PREV /\
     (t12.MODE = 1 /\
      ((t12.D2U = 5 /\ (t11.S2PM & 5) = 1) \/
       ((t12.D2U + t12.U2D = 0) /\
        (t11.S2PM >> 2) = 1)) \/
      (t12.MODE = 2 /\
       (((t11.S2PM & 5) = 1 /\ (t12.D2U & 3) = 1) \/
        ((t11.S2PM + t11.P2S + t11.M2S = 0) /\
         ((t12.D2U & 2) >> 1) = 1 /\ t11.PREV))))) +
    (r_1b.MODE = 4 /\ t11.POS = 0 /\ t11.PREV \/
     (t10.MODE = 2 /\
      ((t10.D2U & 5) = 1 \/
       (t10.D2U + t10.U2D = 0) /\
       ((t11.S2PM & 2) >> 1) = 1)) /\ ~t12.PREV /\
     (t12.MODE = 1 /\
      ((t12.D2U = 5 /\ (t11.S2PM & 5) = 1) \/
       ((t12.D2U + t12.U2D = 0) /\ (t11.S2PM >> 2) = 1)) \/
      (t12.MODE = 2 /\
       (((t11.S2PM & 5) = 1 /\ (t12.D2U & 3) = 1) \/
        ((t11.S2PM + t11.P2S + t11.M2S = 0) /\
         ((t12.D2U & 2) >> 1) = 1 /\ t11.PREV))))) +
    (r_2a.MODE = 4 /\ t11.POS = 1 /\ t11.PREV \/
     (t10.MODE = 2 /\
      ((t10.D2U & 5) = 1 \/
       (t10.D2U + t10.U2D = 0) /\
       ((t11.S2PM & 2) >> 1) = 1)) /\ ~t20.PREV /\
     (t20.MODE = 1 /\
      ((t20.D2U = 5 /\ (t11.S2PM & 5) = 1) \/
       ((t20.D2U + t20.U2D = 0) /\ (t11.S2PM >> 2) = 1)) \/
      (t20.MODE = 2 /\
       (((t11.S2PM & 5) = 1 /\ (t20.D2U & 3) = 1) \/
        ((t11.S2PM + t11.P2S + t11.M2S = 0) /\
         ((t20.D2U & 2) >> 1) = 1 /\ t11.PREV))))) +
    (r_2b.MODE = 4 /\ t11.POS = 1 /\ t11.PREV \/
     (t10.MODE = 2 /\
      ((t10.D2U & 5) = 1 \/
       (t10.D2U + t10.U2D = 0) /\
       ((t11.S2PM & 2) >> 1) = 1)) /\ ~t20.PREV /\
     (t20.MODE = 1 /\
      ((t20.D2U = 5 /\ (t11.S2PM & 5) = 1) \/
       ((t20.D2U + t20.U2D = 0) /\ (t11.S2PM >> 2) = 1)) \/
      (t20.MODE = 2 /\
       (((t11.S2PM & 5) = 1 /\ (t20.D2U & 3) = 1) \/
        ((t11.S2PM + t11.P2S + t11.M2S = 0) /\
         ((t20.D2U & 2) >> 1) = 1 /\ t11.PREV))))) +
    (r_3_.MODE = 4 /\ t11.POS = 0 /\ ~t10.PREV /\
     (t10.MODE = 1 /\
      ((t10.U2D = 5 /\ (t11.P2S & 5) = 1) \/
       ((t10.D2U + t10.U2D = 0) /\ (t11.P2S >> 2) = 1)) \/
      (t10.MODE = 2 /\
       (((t11.P2S & 5) = 1 /\ (t10.U2D & 3) = 1) \/
        (t11.S2PM + t11.P2S + t11.M2S = 0) /\
        ((t10.U2D & 2) >> 1) = 1)))) +
    (r_7_.MODE = 4 /\ t11.POS = 1 /\ ~t10.PREV /\
     (t10.MODE = 1 /\
      ((t10.U2D = 5 /\ (t11.M2S & 5) = 1) \/
       ((t10.D2U + t10.U2D = 0) /\ (t11.M2S >> 2) = 1)) \/
      (t10.MODE = 2 /\
       (((t11.M2S & 5) = 1 /\ (t10.U2D & 3) = 1) \/
        (t11.S2PM + t11.P2S + t11.M2S = 0) /\
        ((t10.U2D & 2) >> 1) = 1))))) = 1)) /\
 (t13.MODE = 2 =>
  (((r_4_.MODE = 4 /\ t13.POS = 0 /\ ~t14.PREV /\
     (t14.MODE = 1 /\
      ((t14.D2U = 5 /\ (t13.P2S & 5) = 1) \/
       ((t14.D2U + t14.U2D = 0) /\ (t13.P2S >> 2) = 1)) \/
      (t14.MODE = 2 /\
       (((t13.P2S & 5) = 1 /\ (t14.D2U & 3) = 1) \/
        (t13.S2PM + t13.P2S + t13.M2S = 0) /\
        ((t14.D2U & 2) >> 1) = 1)))) +
    (r_5a.MODE = 4 /\ t13.POS = 0 /\ t13.PREV \/
     (t14.MODE = 2 /\
      ((t14.U2D & 5) = 1 \/
       (t14.D2U + t14.U2D = 0) /\
       ((t13.S2PM & 2) >> 1) = 1)) /\ ~t12.PREV /\
     (t12.MODE = 1 /\
      ((t12.U2D = 5 /\ (t13.S2PM & 5) = 1) \/
       ((t12.D2U + t12.U2D = 0) /\ (t13.S2PM >> 2) = 1)) \/
      (t12.MODE = 2 /\
       (((t13.S2PM & 5) = 1 /\ (t12.U2D & 3) = 1) \/
        ((t13.S2PM + t13.P2S + t13.M2S = 0) /\
         ((t12.U2D & 2) >> 1) = 1 /\ t13.PREV))))) +
    (r_5b.MODE = 4 /\ t13.POS = 0 /\ t13.PREV \/
     (t14.MODE = 2 /\
      ((t14.U2D & 5) = 1 \/
       (t14.D2U + t14.U2D = 0) /\
       ((t13.S2PM & 2) >> 1) = 1)) /\ ~t12.PREV /\
     (t12.MODE = 1 /\
      ((t12.U2D = 5 /\ (t13.S2PM & 5) = 1) \/
       ((t12.D2U + t12.U2D = 0) /\ (t13.S2PM >> 2) = 1)) \/
      (t12.MODE = 2 /\
       (((t13.S2PM & 5) = 1 /\ (t12.U2D & 3) = 1) \/
        ((t13.S2PM + t13.P2S + t13.M2S = 0) /\
         ((t12.U2D & 2) >> 1) = 1 /\ t13.PREV))))) +
    (r_6a.MODE = 4 /\ t13.POS = 1 /\ t13.PREV \/
     (t14.MODE = 2 /\
      ((t14.U2D & 5) = 1 \/
       (t14.D2U + t14.U2D = 0) /\ ((t13.S2PM & 2) >> 1) = 1)) /\
     ~t20.PREV /\
     (t20.MODE = 1 /\
      ((t20.U2D = 5 /\ (t13.S2PM & 5) = 1) \/
       ((t20.D2U + t20.U2D = 0) /\ (t13.S2PM >> 2) = 1)) \/
      (t20.MODE = 2 /\
       (((t13.S2PM & 5) = 1 /\ (t20.U2D & 3) = 1) \/
        ((t13.S2PM + t13.P2S + t13.M2S = 0) /\
         ((t20.U2D & 2) >> 1) = 1 /\ t13.PREV))))) +
    (r_6b.MODE = 4 /\ t13.POS = 1 /\ t13.PREV \/
     (t14.MODE = 2 /\
      ((t14.U2D & 5) = 1 \/
       (t14.D2U + t14.U2D = 0) /\ ((t13.S2PM & 2) >> 1) = 1)) /\
     ~t20.PREV /\
     (t20.MODE = 1 /\
      ((t20.U2D = 5 /\ (t13.S2PM & 5) = 1) \/
       ((t20.D2U + t20.U2D = 0) /\ (t13.S2PM >> 2) = 1)) \/
      (t20.MODE = 2 /\
       (((t13.S2PM & 5) = 1 /\ (t20.U2D & 3) = 1) \/
        ((t13.S2PM + t13.P2S + t13.M2S = 0) /\
         ((t20.U2D & 2) >> 1) = 1 /\ t13.PREV))))) +
    (r_8_.MODE = 4 /\ t13.POS = 1 /\ ~t14.PREV /\
     (t14.MODE = 1 /\
      ((t14.D2U = 5 /\ (t13.M2S & 5) = 1) \/
       ((t14.D2U + t14.U2D = 0) /\ (t13.M2S >> 2) = 1)) \/
      (t14.MODE = 2 /\
       (((t13.M2S & 5) = 1 /\ (t14.D2U & 3) = 1) \/
        (t13.S2PM + t13.P2S + t13.M2S = 0) /\
        ((t14.D2U & 2) >> 1) = 1))))) = 1)))

end