/*
==========================================================
CASE: toy
--------
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_1] (r_1.MODE = 0) ==> (r_1.MODE' = 1)
 [=]
 
 [route_dispatching_r_2] (r_2.MODE = 0) ==> (r_2.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_allocating_r_1]
  (r_1.MODE = 1) /\
  ((r_2.MODE ~= 2 /\ r_2.MODE ~= 3) /\
   (r_3.MODE ~= 2 /\ r_3.MODE ~= 3) /\
   (r_4.MODE ~= 2 /\ r_4.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_1.MODE' = 2) /\ (t11.CMD' = 0) /\
  ((mb11.CMD' = 0) /\ (mb13.CMD' = 0) /\ (mb20.CMD' = 0)) /\
  ((t10.MODE' = 1) /\ (t12.MODE' = 1) /\ (t11.MODE' = 1))
  [=]
  
  [route_allocating_r_2]
  (r_2.MODE = 1) /\
  ((r_1.MODE ~= 2 /\ r_1.MODE ~= 3) /\
   (r_3.MODE ~= 2 /\ r_3.MODE ~= 3) /\
   (r_4.MODE ~= 2 /\ r_4.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_2.MODE' = 2) /\ (t11.CMD' = 0) /\
  ((mb10.CMD' = 0) /\ (mb12.CMD' = 0) /\ (mb20.CMD' = 0)) /\
  ((t10.MODE' = 1) /\ (t12.MODE' = 1) /\ (t11.MODE' = 1))
  [=]
  
  [route_allocating_r_3]
  (r_3.MODE = 1) /\
  ((r_1.MODE ~= 2 /\ r_1.MODE ~= 3) /\
   (r_2.MODE ~= 2 /\ r_2.MODE ~= 3) /\
   (r_4.MODE ~= 2 /\ r_4.MODE ~= 3)) /\
  ((t12.D2U + t12.U2D = 0) /\ (t20.D2U + t20.U2D = 0) /\
   (t11.S2PM + t11.P2S + t11.M2S = 0)) /\
  ((t12.MODE = 0) /\ (t20.MODE = 0) /\ (t11.MODE = 0))
  ==>
  (r_3.MODE' = 2) /\ (t11.CMD' = 1) /\
  ((mb10.CMD' = 0) /\ (mb12.CMD' = 0) /\ (mb20.CMD' = 0)) /\
  ((t12.MODE' = 1) /\ (t20.MODE' = 1) /\ (t11.MODE' = 1))
  [=]
  
  [route_allocating_r_4]
  (r_4.MODE = 1) /\
  ((r_1.MODE ~= 2 /\ r_1.MODE ~= 3) /\
   (r_2.MODE ~= 2 /\ r_2.MODE ~= 3) /\
   (r_3.MODE ~= 2 /\ r_3.MODE ~= 3)) /\
  ((t12.D2U + t12.U2D = 0) /\ (t20.D2U + t20.U2D = 0) /\
   (t11.S2PM + t11.P2S + t11.M2S = 0)) /\
  ((t12.MODE = 0) /\ (t20.MODE = 0) /\ (t11.MODE = 0))
  ==>
  (r_4.MODE' = 2) /\ (t11.CMD' = 1) /\
  ((mb10.CMD' = 0) /\ (mb13.CMD' = 0) /\ (mb21.CMD' = 0)) /\
  ((t12.MODE' = 1) /\ (t20.MODE' = 1) /\ (t11.MODE' = 1))
  [=]
  
  [route_lock_r_1]
  r_1.MODE = 2 /\
  ((mb11.ACT = 0) /\ (mb13.ACT = 0) /\ (mb20.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_1.MODE' = 3 /\ mb10.CMD' = 1
  [=]
  
  [route_lock_r_2]
  r_2.MODE = 2 /\
  ((mb10.ACT = 0) /\ (mb12.ACT = 0) /\ (mb20.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_2.MODE' = 3 /\ mb13.CMD' = 1
  [=]
  
  [route_lock_r_3]
  r_3.MODE = 2 /\
  ((mb10.ACT = 0) /\ (mb12.ACT = 0) /\ (mb20.ACT = 0)) /\
  (t11.POS = 1) /\
  ((t12.D2U + t12.U2D = 0) /\ (t20.D2U + t20.U2D = 0) /\
   (t11.S2PM + t11.P2S + t11.M2S = 0)) /\
  ((t12.MODE = 1) /\ (t20.MODE = 1) /\ (t11.MODE = 1))
  ==> r_3.MODE' = 3 /\ mb13.CMD' = 1
  [=]
  
  [route_lock_r_4]
  r_4.MODE = 2 /\
  ((mb10.ACT = 0) /\ (mb13.ACT = 0) /\ (mb21.ACT = 0)) /\
  (t11.POS = 1) /\
  ((t12.D2U + t12.U2D = 0) /\ (t20.D2U + t20.U2D = 0) /\
   (t11.S2PM + t11.P2S + t11.M2S = 0)) /\
  ((t12.MODE = 1) /\ (t20.MODE = 1) /\ (t11.MODE = 1))
  ==> r_4.MODE' = 3 /\ mb20.CMD' = 1
  [=]
  
  [route_in_use_r_1] r_1.MODE = 3 /\ ~(t10.D2U + t10.U2D = 0) ==>
  r_1.MODE' = 4 /\ mb10.CMD' = 0 /\ t10.MODE' = 2
  [=]
  
  [route_in_use_r_2] r_2.MODE = 3 /\ ~(t12.D2U + t12.U2D = 0) ==>
  r_2.MODE' = 4 /\ mb13.CMD' = 0 /\ t12.MODE' = 2
  [=]
  
  [route_in_use_r_3] r_3.MODE = 3 /\ ~(t12.D2U + t12.U2D = 0) ==>
  r_3.MODE' = 4 /\ mb13.CMD' = 0 /\ t12.MODE' = 2
  [=]
  
  [route_in_use_r_4] r_4.MODE = 3 /\ ~(t20.D2U + t20.U2D = 0) ==>
  r_4.MODE' = 4 /\ mb20.CMD' = 0 /\ t20.MODE' = 2
  [=]
  
  [element_in_use_r_1_t12]
  t11.MODE = 2 /\ r_1.MODE = 4 /\ t12.MODE = 1 /\ ~(t12.D2U + t12.U2D = 0)
  ==> t12.MODE' = 2
  [=]
  
  [element_in_use_r_1_t11]
  t10.MODE = 2 /\ r_1.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_2_t10]
  t11.MODE = 2 /\ r_2.MODE = 4 /\ t10.MODE = 1 /\ ~(t10.D2U + t10.U2D = 0)
  ==> t10.MODE' = 2
  [=]
  
  [element_in_use_r_2_t11]
  t12.MODE = 2 /\ r_2.MODE = 4 /\ t11.MODE = 1 /\
  ~(t11.S2PM + t11.P2S + t11.M2S = 0) /\ t11.POS = 0 /\ t10.MODE = 1
  ==> t11.MODE' = 2
  [=]
  
  [element_in_use_r_3_t20]
  t11.MODE = 2 /\ r_3.MODE = 4 /\ t20.MODE = 1 /\ ~(t20.D2U + t20.U2D = 0)
  ==> t20.MODE' = 2
  [=]
  
  [element_in_use_r_3_t11]
  t12.MODE = 2 /\ r_3.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_4_t12]
  t11.MODE = 2 /\ r_4.MODE = 4 /\ t12.MODE = 1 /\ ~(t12.D2U + t12.U2D = 0)
  ==> t12.MODE' = 2
  [=]
  
  [element_in_use_r_4_t11]
  t20.MODE = 2 /\ r_4.MODE = 4 /\ t11.MODE = 1 /\
  ~(t11.S2PM + t11.P2S + t11.M2S = 0) /\ t11.POS = 1 /\ t12.MODE = 1
  ==> t11.MODE' = 2
  [=]
  
  [sequential_release_e_r_1_t10]
  r_1.MODE = 4 /\ t10.MODE = 2 /\ (t10.D2U + t10.U2D = 0) /\
  t11.PREV = 0 /\ t11.MODE = 2 /\ (((t11.P2S & 2) >> 1) ~= 0) /\
  t11.POS = 0
  ==> t10.MODE' = 0 /\ t10.PREV' = 0 /\ t11.PREV' = 1
  [=]
  
  [sequential_release_e_r_1_t11]
  r_1.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_2_t12]
  r_2.MODE = 4 /\ t12.MODE = 2 /\ (t12.D2U + t12.U2D = 0) /\
  t11.PREV = 0 /\ t11.MODE = 2 /\ (((t11.S2PM & 2) >> 1) ~= 0) /\
  t11.POS = 0
  ==> t12.MODE' = 0 /\ t12.PREV' = 0 /\ t11.PREV' = 1
  [=]
  
  [sequential_release_e_r_2_t11]
  r_2.MODE = 4 /\ t11.MODE = 2 /\
  (t11.S2PM + t11.P2S + t11.M2S = 0) /\ t11.PREV = 1 /\
  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_3_t12]
  r_3.MODE = 4 /\ t12.MODE = 2 /\ (t12.D2U + t12.U2D = 0) /\
  t11.PREV = 0 /\ t11.MODE = 2 /\ (((t11.S2PM & 2) >> 1) ~= 0) /\
  t11.POS = 1
  ==> t12.MODE' = 0 /\ t12.PREV' = 0 /\ t11.PREV' = 1
  [=]
  
  [sequential_release_e_r_3_t11]
  r_3.MODE = 4 /\ t11.MODE = 2 /\
  (t11.S2PM + t11.P2S + t11.M2S = 0) /\ t11.PREV = 1 /\
  t20.PREV = 0 /\ t20.MODE = 2 /\ (((t20.U2D & 2) >> 1) ~= 0) /\
  t11.POS = 1
  ==> t11.MODE' = 0 /\ t11.PREV' = 0 /\ t20.PREV' = 1
  [=]
  
  [sequential_release_e_r_4_t20]
  r_4.MODE = 4 /\ t20.MODE = 2 /\ (t20.D2U + t20.U2D = 0) /\
  t11.PREV = 0 /\ t11.MODE = 2 /\ (((t11.M2S & 2) >> 1) ~= 0) /\
  t11.POS = 1
  ==> t20.MODE' = 0 /\ t20.PREV' = 0 /\ t11.PREV' = 1
  [=]
  
  [sequential_release_e_r_4_t11]
  r_4.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 = 1
  ==> t11.MODE' = 0 /\ t11.PREV' = 0 /\ t12.PREV' = 1
  [=]
  
  [sequential_release_last_elem_r_1]
  r_1.MODE = 4 /\ t12.MODE = 2 /\ (t12.D2U + t12.U2D = 0) /\ t12.PREV = 1
  ==> t12.MODE' = 0 /\ t12.PREV' = 0 /\ r_1.MODE' = 0
  [=]
  
  [sequential_release_last_elem_r_2]
  r_2.MODE = 4 /\ t10.MODE = 2 /\ (t10.D2U + t10.U2D = 0) /\ t10.PREV = 1
  ==> t10.MODE' = 0 /\ t10.PREV' = 0 /\ r_2.MODE' = 0
  [=]
  
  [sequential_release_last_elem_r_3]
  r_3.MODE = 4 /\ t20.MODE = 2 /\ (t20.D2U + t20.U2D = 0) /\ t20.PREV = 1
  ==> t20.MODE' = 0 /\ t20.PREV' = 0 /\ r_3.MODE' = 0
  [=]
  
  [sequential_release_last_elem_r_4]
  r_4.MODE = 4 /\ t12.MODE = 2 /\ (t12.D2U + t12.U2D = 0) /\ t12.PREV = 1
  ==> t12.MODE' = 0 /\ t12.PREV' = 0 /\ r_4.MODE' = 0
  [=]
  
  [release_last_elem_pseudo_timer_r_1]
  r_1.MODE = 4 /\ t12.MODE = 2 /\ t12.D2U = 0b111 /\ mb12.ACT = 0 /\
  t12.PREV = 1
  ==> t12.MODE' = 0 /\ t12.PREV' = 0 /\ r_1.MODE' = 0
  [=]
  
  [release_last_elem_pseudo_timer_r_2]
  r_2.MODE = 4 /\ t10.MODE = 2 /\ t10.U2D = 0b111 /\ mb11.ACT = 0 /\
  t10.PREV = 1
  ==> t10.MODE' = 0 /\ t10.PREV' = 0 /\ r_2.MODE' = 0
  [=]
  
  [release_last_elem_pseudo_timer_r_3]
  r_3.MODE = 4 /\ t20.MODE = 2 /\ t20.U2D = 0b111 /\ mb21.ACT = 0 /\
  t20.PREV = 1
  ==> t20.MODE' = 0 /\ t20.PREV' = 0 /\ r_3.MODE' = 0
  [=]
  
  [release_last_elem_pseudo_timer_r_4]
  r_4.MODE = 4 /\ t12.MODE = 2 /\ t12.D2U = 0b111 /\ mb12.ACT = 0 /\
  t12.PREV = 1
  ==> t12.MODE' = 0 /\ t12.PREV' = 0 /\ r_4.MODE' = 0)
 [>]
 
 ([point_switch_1_t11] t11.POS ~= t11.CMD /\ t11.POS ~= 2 ==> t11.POS' = 2
  [=]
  
  [point_switch_2_t11] t11.POS = 2 ==> t11.POS' = t11.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_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.P2S' = (t11.P2S ^ 5)
  [=]
  
  [head_movement_linear_up_t20] (t20.D2U & 5) = 5 ==>
  t20.D2U' = (t20.D2U ^ 4) /\ t11.M2S' = (t11.M2S ^ 5)
  [=]
  
  [head_movement_linear_down_t12] (t12.U2D & 5) = 5 ==>
  t12.U2D' = (t12.U2D ^ 4) /\ t11.S2PM' = (t11.S2PM ^ 5)
  [=]
  
  [tail_movement_linear_up_t10] t10.D2U = 3 ==>
  t10.D2U' = 0 /\ t11.P2S' = (t11.P2S ^ 2)
  [=]
  
  [tail_movement_linear_up_t20] t20.D2U = 3 ==>
  t20.D2U' = 0 /\ t11.M2S' = (t11.M2S ^ 2)
  [=]
  
  [tail_movement_linear_down_t12] t12.U2D = 3 ==>
  t12.U2D' = 0 /\ t11.S2PM' = (t11.S2PM ^ 2)
  [=]
  
  [head_movement_point_stem_to_plus_t11] (t11.S2PM & 5) = 5 /\ t11.POS = 0 ==>
  t11.S2PM' = (t11.S2PM ^ 4) /\ t10.U2D' = (t10.U2D ^ 5)
  [=]
  
  [head_movement_point_stem_to_minus_t11] (t11.S2PM & 5) = 5 /\ t11.POS = 1
  ==> t11.S2PM' = (t11.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) /\ t12.D2U' = (t12.D2U ^ 5)
  [=]
  
  [head_movement_point_minus_to_stem_t11] (t11.M2S & 5) = 5 /\ t11.POS = 1 ==>
  t11.M2S' = (t11.M2S ^ 4) /\ t12.D2U' = (t12.D2U ^ 5)
  [=]
  
  [tail_movement_point_stem_to_plus_t11] t11.S2PM = 3 /\ t11.POS = 0 ==>
  t11.S2PM' = 0 /\ t10.U2D' = (t10.U2D ^ 2)
  [=]
  
  [tail_movement_point_stem_to_minus_t11] t11.S2PM = 3 /\ t11.POS = 1 ==>
  t11.S2PM' = 0 /\ t20.U2D' = (t20.U2D ^ 2)
  [=]
  
  [tail_movement_point_plus_to_stem_t11] t11.P2S = 3 /\ t11.POS = 0 ==>
  t11.P2S' = 0 /\ t12.D2U' = (t12.D2U ^ 2)
  [=]
  
  [tail_movement_point_minus_to_stem_t11] t11.M2S = 3 /\ t11.POS = 1 ==>
  t11.M2S = 0 /\ t12.D2U' = (t12.D2U ^ 2)
  [=]
  
  [enter_interlocked_area_head_from_down_b10] mb10.ACT = 1 ==>
  t10.D2U' = (t10.D2U ^ 5)
  [=]
  
  [enter_interlocked_area_head_from_down_b20] mb20.ACT = 1 ==>
  t20.D2U' = (t20.D2U ^ 5)
  [=]
  
  [enter_interlocked_area_tail_from_down_b10] (t10.D2U & 3) = 1 ==>
  t10.D2U' = (t10.D2U ^ 2)
  [=]
  
  [enter_interlocked_area_tail_from_down_b20] (t20.D2U & 3) = 1 ==>
  t20.D2U' = (t20.D2U ^ 2)
  [=]
  
  [enter_interlocked_area_head_from_up_b12] mb13.ACT = 1 ==>
  t12.U2D' = (t12.U2D ^ 5)
  [=]
  
  [enter_interlocked_area_tail_from_up_b12] (t12.U2D & 3) = 1 ==>
  t12.U2D' = (t12.U2D ^ 2)
  [=]
  
  [leave_interlocked_area_head_to_down_b10] (t10.U2D & 5) = 5 ==>
  t10.U2D' = (t10.U2D ^ 4)
  [=]
  
  [leave_interlocked_area_head_to_down_b20] (t20.U2D & 5) = 5 ==>
  t20.U2D' = (t20.U2D ^ 4)
  [=]
  
  [leave_interlocked_area_tail_to_down_b10] t10.U2D = 3 ==> t10.U2D' = 0
  [=]
  
  [leave_interlocked_area_tail_to_down_b20] t20.U2D = 3 ==> t20.U2D' = 0
  [=]
  
  [leave_interlocked_area_head_to_up_b12] (t12.D2U & 5) = 5 ==>
  t12.D2U' = (t12.D2U ^ 4)
  [=]
  
  [leave_interlocked_area_tail_to_up_b12] t12.D2U = 3 ==> t12.D2U' = 0))

invariant

[no_head_to_head_collisions_linear]
((t10.D2U * t10.U2D = 0) /\ (t12.D2U * t12.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) /\
 (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),

[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),

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

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

[train_integrity_linear_down]
(((t12.U2D & 5) = 1 => (t11.S2PM & 3) = 1) /\
 ((t11.S2PM & 3) = 1 => (t12.U2D & 5) = 1)),

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

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

[conflicting_routes_are_not_set_together]
(((r_1.MODE = 2 \/ r_1.MODE = 3) =>
  ((r_2.MODE ~= 2 /\ r_2.MODE ~= 3) /\
   (r_3.MODE ~= 2 /\ r_3.MODE ~= 3) /\
   (r_4.MODE ~= 2 /\ r_4.MODE ~= 3))) /\
 ((r_2.MODE = 2 \/ r_2.MODE = 3) =>
  ((r_1.MODE ~= 2 /\ r_1.MODE ~= 3) /\
   (r_3.MODE ~= 2 /\ r_3.MODE ~= 3) /\
   (r_4.MODE ~= 2 /\ r_4.MODE ~= 3))) /\
 ((r_3.MODE = 2 \/ r_3.MODE = 3) =>
  ((r_1.MODE ~= 2 /\ r_1.MODE ~= 3) /\
   (r_2.MODE ~= 2 /\ r_2.MODE ~= 3) /\
   (r_4.MODE ~= 2 /\ r_4.MODE ~= 3))) /\
 ((r_4.MODE = 2 \/ r_4.MODE = 3) =>
  ((r_1.MODE ~= 2 /\ r_1.MODE ~= 3) /\ (r_2.MODE ~= 2 /\ r_2.MODE ~= 3) /\
   (r_3.MODE ~= 2 /\ r_3.MODE ~= 3)))),

[route_allocating_cnd]
(((r_1.MODE = 2) =>
  ((t11.CMD = 0) /\
   ((mb11.CMD = 0) /\ (mb13.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_2.MODE = 2) =>
  ((t11.CMD = 0) /\
   ((mb10.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_3.MODE = 2) =>
  ((t11.CMD = 1) /\
   ((mb10.CMD = 0) /\ (mb12.CMD = 0) /\ (mb20.CMD = 0)) /\
   ((t12.MODE = 1) /\ (t20.MODE = 1) /\ (t11.MODE = 1)) /\
   ((t12.D2U + t12.U2D = 0) /\ (t20.D2U + t20.U2D = 0) /\
    (t11.S2PM + t11.P2S + t11.M2S = 0)))) /\
 ((r_4.MODE = 2) =>
  ((t11.CMD = 1) /\
   ((mb10.CMD = 0) /\ (mb13.CMD = 0) /\ (mb21.CMD = 0)) /\
   ((t12.MODE = 1) /\ (t20.MODE = 1) /\ (t11.MODE = 1)) /\
   ((t12.D2U + t12.U2D = 0) /\ (t20.D2U + t20.U2D = 0) /\
    (t11.S2PM + t11.P2S + t11.M2S = 0))))),

[route_lock_cnd]
(((r_1.MODE = 3) =>
  (t11.POS = 0 /\ t11.POS = t11.CMD) /\
  ((mb11.ACT = 0 /\ mb11.ACT = mb11.CMD) /\
   (mb13.ACT = 0 /\ mb13.ACT = mb13.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_2.MODE = 3) =>
  (t11.POS = 0 /\ t11.POS = t11.CMD) /\
  ((mb10.ACT = 0 /\ mb10.ACT = mb10.CMD) /\
   (mb12.ACT = 0 /\ mb12.ACT = mb12.CMD) /\
   (mb20.ACT = 0 /\ mb20.ACT = mb20.CMD)) /\
  ((t10.MODE = 1) /\ (t12.MODE = 1) /\ (t11.MODE = 1)) /\
  ((t10.D2U + t10.U2D = 0) /\ (t11.S2PM + t11.P2S + t11.M2S = 0)) /\
  ((t12.D2U + t12.U2D = 0) \/ t12.U2D = 5) /\ mb13.CMD = 1) /\
 ((r_3.MODE = 3) =>
  (t11.POS = 1 /\ t11.POS = t11.CMD) /\
  ((mb10.ACT = 0 /\ mb10.ACT = mb10.CMD) /\
   (mb12.ACT = 0 /\ mb12.ACT = mb12.CMD) /\
   (mb20.ACT = 0 /\ mb20.ACT = mb20.CMD)) /\
  ((t12.MODE = 1) /\ (t20.MODE = 1) /\ (t11.MODE = 1)) /\
  ((t20.D2U + t20.U2D = 0) /\ (t11.S2PM + t11.P2S + t11.M2S = 0)) /\
  ((t12.D2U + t12.U2D = 0) \/ t12.U2D = 5) /\ mb13.CMD = 1) /\
 ((r_4.MODE = 3) =>
  (t11.POS = 1 /\ t11.POS = t11.CMD) /\
  ((mb10.ACT = 0 /\ mb10.ACT = mb10.CMD) /\
   (mb13.ACT = 0 /\ mb13.ACT = mb13.CMD) /\
   (mb21.ACT = 0 /\ mb21.ACT = mb21.CMD)) /\
  ((t12.MODE = 1) /\ (t20.MODE = 1) /\ (t11.MODE = 1)) /\
  ((t12.D2U + t12.U2D = 0) /\ (t11.S2PM + t11.P2S + t11.M2S = 0)) /\
  ((t20.D2U + t20.U2D = 0) \/ t20.D2U = 5) /\ mb20.CMD = 1)),

[route_used_cnd_a]
((r_1.MODE = 4 => (t12.MODE ~= 0)) /\ (r_2.MODE = 4 => (t10.MODE ~= 0)) /\
 (r_3.MODE = 4 => (t20.MODE ~= 0)) /\ (r_4.MODE = 4 => (t12.MODE ~= 0))),

[route_used_cnd_b]
((r_1.MODE = 4 =>
  (((t12.D2U & 1) + (t11.POS = 0) /\
    ((t11.P2S & 1) + (t10.D2U & 1))) \/
   t12.PREV /\ (t12.D2U + t12.U2D = 0))) /\
 (r_2.MODE = 4 =>
  (((t10.U2D & 1) + (t11.POS = 0) /\
    ((t11.S2PM & 1) + (t12.U2D & 1))) \/
   t10.PREV /\ (t10.D2U + t10.U2D = 0))) /\
 (r_3.MODE = 4 =>
  (((t20.U2D & 1) + (t11.POS = 1) /\ ((t11.S2PM & 1) + (t12.U2D & 1))) \/
   t20.PREV /\ (t20.D2U + t20.U2D = 0))) /\
 (r_4.MODE = 4 =>
  (((t12.D2U & 1) + (t11.POS = 1) /\ ((t11.M2S & 1) + (t20.D2U & 1))) \/
   t12.PREV /\ (t12.D2U + t12.U2D = 0)))),

[route_used_cnd_c]
((r_1.MODE = 4 =>
  (((t11.P2S & 1) + (t10.D2U & 1)) *
   ((t11.S2PM & 1) + (t10.U2D & 1)) = 0)) /\
 (r_2.MODE = 4 =>
  (((t11.S2PM & 1) + (t12.U2D & 1)) *
   ((t11.P2S & 1) + (t12.D2U & 1)) = 0)) /\
 (r_3.MODE = 4 =>
  (((t11.S2PM & 1) + (t12.U2D & 1)) * ((t11.M2S & 1) + (t12.D2U & 1)) = 0)) /\
 (r_4.MODE = 4 =>
  (((t11.M2S & 1) + (t20.D2U & 1)) * ((t11.S2PM & 1) + (t20.U2D & 1)) = 0))),

[route_in_use_last_sec_is_free_in_opposite_dir]
((r_1.MODE = 4 => t12.U2D = 0) /\ (r_2.MODE = 4 => t10.D2U = 0) /\
 (r_3.MODE = 4 => t20.D2U = 0) /\ (r_4.MODE = 4 => t12.U2D = 0)),

[routes_share_last_not_used_at_same_time]
((r_1.MODE = 4 => (r_4.MODE ~= 4)) /\ (r_4.MODE = 4 => (r_1.MODE ~= 4))),

[first_entry_cnd]
(~(~(t10.D2U + t10.U2D = 0) /\ mb10.CMD = 1 /\ mb10.ACT = 0) /\
 ~(~(t12.D2U + t12.U2D = 0) /\ mb13.CMD = 1 /\ mb13.ACT = 0) /\
 ~(~(t12.D2U + t12.U2D = 0) /\ mb13.CMD = 1 /\ mb13.ACT = 0) /\
 ~(~(t20.D2U + t20.U2D = 0) /\ mb20.CMD = 1 /\ mb20.ACT = 0)),

[entry_signal_closed_when_tail_in_first]
((((t10.D2U & 2) >> 1) => mb10.ACT = 0) /\
 (((t12.U2D & 2) >> 1) => mb13.ACT = 0) /\
 (((t12.U2D & 2) >> 1) => mb13.ACT = 0) /\
 (((t20.D2U & 2) >> 1) => mb20.ACT = 0)),

[signal_cmd_open_cnd]
(mb10.CMD = 1 => ((r_1.MODE = 3) = 1)) /\
(mb13.CMD = 1 => (((r_2.MODE = 3) + (r_3.MODE = 3)) = 1)) /\
(mb20.CMD = 1 => ((r_4.MODE = 3) = 1)),

[signal_act_open_cnd]
(mb10.ACT = 1 =>
 (((r_1.MODE = 3 /\ (mb10.CMD = 1 \/ (t10.D2U >> 2) ~= 0)) \/
   (r_1.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)) = 1)) /\
(mb13.ACT = 1 =>
 ((((r_2.MODE = 3 /\ (mb13.CMD = 1 \/ (t12.U2D >> 2) ~= 0)) \/
    (r_2.MODE = 4 /\ mb13.CMD = 0 /\ (t12.U2D >> 2) ~= 0)) /\
   (((t10.D2U + t10.U2D = 0) /\ t10.MODE = 1) /\
    ((t11.S2PM + t11.P2S + t11.M2S = 0) /\ t11.MODE = 1)) +
   ((r_3.MODE = 3 /\ (mb13.CMD = 1 \/ (t12.U2D >> 2) ~= 0)) \/
    (r_3.MODE = 4 /\ mb13.CMD = 0 /\ (t12.U2D >> 2) ~= 0)) /\
   (((t20.D2U + t20.U2D = 0) /\ t20.MODE = 1) /\
    ((t11.S2PM + t11.P2S + t11.M2S = 0) /\ t11.MODE = 1))) = 1)) /\
(mb20.ACT = 1 =>
 (((r_4.MODE = 3 /\ (mb20.CMD = 1 \/ (t20.D2U >> 2) ~= 0)) \/
   (r_4.MODE = 4 /\ mb20.CMD = 0 /\ (t20.D2U >> 2) ~= 0)) /\
  (((t12.D2U + t12.U2D = 0) /\ t12.MODE = 1) /\
   ((t11.S2PM + t11.P2S + t11.M2S = 0) /\ t11.MODE = 1)) = 1)),

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

[point_only_cmd_when_alloc_a_route]
(t11.CMD ~= t11.POS =>
 (t11.MODE ~= 2 /\
  ((r_1.MODE = 2) \/ (r_2.MODE = 2) \/ (r_3.MODE = 2) \/ (r_4.MODE = 2)))),

[ground_unused_signal]
((mb11.ACT = 0 /\ mb11.CMD = 0) /\ (mb12.ACT = 0 /\ mb12.CMD = 0) /\
 (mb21.ACT = 0 /\ mb21.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) /\ (b12.U2D = 0 /\ b12.D2U = 0) /\
 (b20.U2D = 0 /\ b20.D2U = 0)),

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

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

[occupied_implies_exlck_or_used_linear]
1,

[point_chunk_cnd_stem_plus]
((t11.POS = 0) =>
 ((t11.P2S + t12.D2U) * (t11.S2PM + t10.U2D * (~t10.PREV /\ t10.MODE = 2)) =
  0)),

[point_chunk_cnd_stem_minus]
((t11.POS = 1) =>
 ((t11.M2S + t12.D2U) * (t11.S2PM + t20.U2D * (~t20.PREV /\ t20.MODE = 2)) =
  0)),

[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.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))) /\
 (((t12.U2D = 1 => t12.MODE = 2) /\
   (t12.U2D = 3 => t12.MODE = 2) /\
   (t12.U2D = 5 => t12.MODE = 1 \/ t12.MODE = 2) /\
   (t12.U2D = 7 => t12.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))) /\
 (((t12.U2D = 1 => t12.MODE = 2) /\
   (t12.U2D = 3 => t12.MODE = 2) /\
   (t12.U2D = 5 => t12.MODE = 1 \/ t12.MODE = 2) /\
   (t12.U2D = 7 => t12.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))) /\
 (((t20.D2U = 1 => t20.MODE = 2) /\ (t20.D2U = 3 => t20.MODE = 2) /\
   (t20.D2U = 5 => t20.MODE = 1 \/ t20.MODE = 2) /\
   (t20.D2U = 7 => t20.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)))),

[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_1.MODE = 4 /\ t12.MODE = 2 /\ t12.PREV = 1 /\ t12.D2U = 0) =>
   t12.U2D = 0)) /\
 ((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_4.MODE = 4 /\ t12.MODE = 2 /\ t12.PREV = 1 /\ t12.D2U = 0) =>
   t12.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_2.MODE = 4 /\ t10.MODE = 2 /\ t10.PREV = 1 /\ t10.U2D = 0) =>
   t10.D2U = 0)) /\
 ((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_3.MODE = 4 /\ t20.MODE = 2 /\ t20.PREV = 1 /\ t20.U2D = 0) =>
   t20.D2U = 0))),

[elem_locked_by_only_one_route]
((t10.MODE = 1 =>
  ((((r_1.MODE = 2) \/ (r_1.MODE = 3)) +
    ((r_2.MODE = 2) \/ (r_2.MODE = 3) \/
     (r_2.MODE = 4 /\
      (t10.U2D = 5 /\ t11.MODE = 2 /\ t11.POS = 0 /\
       (t11.S2PM & 5) = 1) \/
      ((t10.D2U + t10.U2D = 0) /\
       (t11.MODE = 1 \/ t11.MODE = 2) /\
       (t11.POS = 0 /\ t11.CMD = 0))))) = 1)) /\
 (t12.MODE = 1 =>
  ((((r_1.MODE = 2) \/ (r_1.MODE = 3) \/
     (r_1.MODE = 4 /\
      (t12.D2U = 5 /\ t11.MODE = 2 /\ t11.POS = 0 /\
       (t11.P2S & 5) = 1) \/
      ((t12.D2U + t12.U2D = 0) /\
       (t11.MODE = 1 \/ t11.MODE = 2) /\
       (t11.POS = 0 /\ t11.CMD = 0)))) +
    ((r_2.MODE = 2) \/ (r_2.MODE = 3)) +
    ((r_3.MODE = 2) \/ (r_3.MODE = 3)) +
    ((r_4.MODE = 2) \/ (r_4.MODE = 3) \/
     (r_4.MODE = 4 /\
      (t12.D2U = 5 /\ t11.MODE = 2 /\ t11.POS = 1 /\
       (t11.M2S & 5) = 1) \/
      ((t12.D2U + t12.U2D = 0) /\
       (t11.MODE = 1 \/ t11.MODE = 2) /\
       (t11.POS = 1 /\ t11.CMD = 1))))) = 1)) /\
 (t20.MODE = 1 =>
  ((((r_3.MODE = 2) \/ (r_3.MODE = 3) \/
     (r_3.MODE = 4 /\
      (t20.U2D = 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_4.MODE = 2) \/ (r_4.MODE = 3))) = 1)) /\
 (t11.MODE = 1 =>
  ((((r_1.MODE = 2) \/ (r_1.MODE = 3) \/
     (r_1.MODE = 4 /\ (t11.POS = 0 /\ t11.CMD = 0) /\
      (t12.MODE = 1 /\ (t12.D2U + t12.U2D = 0)) /\
      (t11.P2S = 5 /\ t10.MODE = 2 /\ (t10.D2U & 5) = 1) \/
      (t11.S2PM + t11.P2S + t11.M2S = 0) /\
      (t10.MODE = 1 \/ t10.MODE = 2))) +
    ((r_2.MODE = 2) \/ (r_2.MODE = 3) \/
     (r_2.MODE = 4 /\ (t11.POS = 0 /\ t11.CMD = 0) /\
      (t10.MODE = 1 /\ (t10.D2U + t10.U2D = 0)) /\
      (t11.S2PM = 5 /\ t12.MODE = 2 /\ (t12.U2D & 5) = 1) \/
      (t11.S2PM + t11.P2S + t11.M2S = 0) /\
      (t12.MODE = 1 \/ t12.MODE = 2))) +
    ((r_3.MODE = 2) \/ (r_3.MODE = 3) \/
     (r_3.MODE = 4 /\ (t11.POS = 1 /\ t11.CMD = 1) /\
      (t20.MODE = 1 /\ (t20.D2U + t20.U2D = 0)) /\
      (t11.S2PM = 5 /\ t12.MODE = 2 /\ (t12.U2D & 5) = 1) \/
      (t11.S2PM + t11.P2S + t11.M2S = 0) /\
      (t12.MODE = 1 \/ t12.MODE = 2))) +
    ((r_4.MODE = 2) \/ (r_4.MODE = 3) \/
     (r_4.MODE = 4 /\ (t11.POS = 1 /\ t11.CMD = 1) /\
      (t12.MODE = 1 /\ (t12.D2U + t12.U2D = 0)) /\
      (t11.M2S = 5 /\ t20.MODE = 2 /\ (t20.D2U & 5) = 1) \/
      (t11.S2PM + t11.P2S + t11.M2S = 0) /\
      (t20.MODE = 1 \/ t20.MODE = 2)))) = 1))),

[elem_used_by_only_one_route]
((t10.MODE = 2 =>
  (((r_1.MODE = 4 /\ ~t11.PREV /\
     (t11.POS = 0 /\ t11.CMD = 0) /\
     ((t11.MODE = 1 /\
       ((t11.P2S = 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.P2S & 3) = 1) \/
        (t10.D2U + t10.U2D = 0) /\
        ((t11.P2S & 2) >> 1) = 1)))) +
    (r_2.MODE = 4 /\ t10.PREV \/
     (t11.POS = 0 /\ t11.MODE = 2 /\
      ((t11.S2PM & 5) = 1 \/
       ((t11.S2PM + t11.P2S + t11.M2S = 0) /\
        ((t10.U2D & 2) >> 1) = 1 /\ t11.PREV))))) = 1)) /\
 (t12.MODE = 2 =>
  (((r_1.MODE = 4 /\ t12.PREV \/
     (t11.POS = 0 /\ t11.MODE = 2 /\
      ((t11.P2S & 5) = 1 \/
       ((t11.S2PM + t11.P2S + t11.M2S = 0) /\
        ((t12.D2U & 2) >> 1) = 1 /\ t11.PREV)))) +
    (r_2.MODE = 4 /\ ~t11.PREV /\
     (t11.POS = 0 /\ t11.CMD = 0) /\
     ((t11.MODE = 1 /\
       ((t11.S2PM = 5 /\ (t12.U2D & 5) = 1) \/
        ((t11.S2PM + t11.P2S + t11.M2S = 0) /\
         (t12.U2D >> 2) = 1)) /\ (t10.MODE = 1)) \/
      (t11.MODE = 2 /\
       (((t12.U2D & 5) = 1 /\ (t11.S2PM & 3) = 1) \/
        (t12.D2U + t12.U2D = 0) /\
        ((t11.S2PM & 2) >> 1) = 1)))) +
    (r_3.MODE = 4 /\ ~t11.PREV /\
     (t11.POS = 1 /\ t11.CMD = 1) /\
     ((t11.MODE = 1 /\
       ((t11.S2PM = 5 /\ (t12.U2D & 5) = 1) \/
        ((t11.S2PM + t11.P2S + t11.M2S = 0) /\
         (t12.U2D >> 2) = 1)) /\ (t20.MODE = 1)) \/
      (t11.MODE = 2 /\
       (((t12.U2D & 5) = 1 /\ (t11.S2PM & 3) = 1) \/
        (t12.D2U + t12.U2D = 0) /\ ((t11.S2PM & 2) >> 1) = 1)))) +
    (r_4.MODE = 4 /\ t12.PREV \/
     (t11.POS = 1 /\ t11.MODE = 2 /\
      ((t11.M2S & 5) = 1 \/
       ((t11.S2PM + t11.P2S + t11.M2S = 0) /\
        ((t12.D2U & 2) >> 1) = 1 /\ t11.PREV))))) = 1)) /\
 (t20.MODE = 2 =>
  (((r_3.MODE = 4 /\ t20.PREV \/
     (t11.POS = 1 /\ t11.MODE = 2 /\
      ((t11.S2PM & 5) = 1 \/
       ((t11.S2PM + t11.P2S + t11.M2S = 0) /\
        ((t20.U2D & 2) >> 1) = 1 /\ t11.PREV)))) +
    (r_4.MODE = 4 /\ ~t11.PREV /\ (t11.POS = 1 /\ t11.CMD = 1) /\
     ((t11.MODE = 1 /\
       ((t11.M2S = 5 /\ (t20.D2U & 5) = 1) \/
        ((t11.S2PM + t11.P2S + t11.M2S = 0) /\
         (t20.D2U >> 2) = 1)) /\ (t12.MODE = 1)) \/
      (t11.MODE = 2 /\
       (((t20.D2U & 5) = 1 /\ (t11.M2S & 3) = 1) \/
        (t20.D2U + t20.U2D = 0) /\ ((t11.M2S & 2) >> 1) = 1))))) = 1)) /\
 (t11.MODE = 2 =>
  (((r_1.MODE = 4 /\ t11.POS = 0 /\ t11.PREV \/
     (t10.MODE = 2 /\
      ((t10.D2U & 5) = 1 \/
       (t10.D2U + t10.U2D = 0) /\ ((t11.P2S & 2) >> 1) = 1)) /\
     ~t12.PREV /\
     (t12.MODE = 1 /\
      ((t12.D2U = 5 /\ (t11.P2S & 5) = 1) \/
       ((t12.D2U + t12.U2D = 0) /\ (t11.P2S >> 2) = 1)) \/
      (t12.MODE = 2 /\
       (((t11.P2S & 5) = 1 /\ (t12.D2U & 3) = 1) \/
        ((t11.S2PM + t11.P2S + t11.M2S = 0) /\
         ((t12.D2U & 2) >> 1) = 1 /\ t11.PREV))))) +
    (r_2.MODE = 4 /\ t11.POS = 0 /\ t11.PREV \/
     (t12.MODE = 2 /\
      ((t12.U2D & 5) = 1 \/
       (t12.D2U + t12.U2D = 0) /\ ((t11.S2PM & 2) >> 1) = 1)) /\
     ~t10.PREV /\
     (t10.MODE = 1 /\
      ((t10.U2D = 5 /\ (t11.S2PM & 5) = 1) \/
       ((t10.D2U + t10.U2D = 0) /\ (t11.S2PM >> 2) = 1)) \/
      (t10.MODE = 2 /\
       (((t11.S2PM & 5) = 1 /\ (t10.U2D & 3) = 1) \/
        ((t11.S2PM + t11.P2S + t11.M2S = 0) /\
         ((t10.U2D & 2) >> 1) = 1 /\ t11.PREV))))) +
    (r_3.MODE = 4 /\ t11.POS = 1 /\ t11.PREV \/
     (t12.MODE = 2 /\
      ((t12.U2D & 5) = 1 \/
       (t12.D2U + t12.U2D = 0) /\ ((t11.S2PM & 2) >> 1) = 1)) /\
     ~t20.PREV /\
     (t20.MODE = 1 /\
      ((t20.U2D = 5 /\ (t11.S2PM & 5) = 1) \/
       ((t20.D2U + t20.U2D = 0) /\ (t11.S2PM >> 2) = 1)) \/
      (t20.MODE = 2 /\
       (((t11.S2PM & 5) = 1 /\ (t20.U2D & 3) = 1) \/
        ((t11.S2PM + t11.P2S + t11.M2S = 0) /\
         ((t20.U2D & 2) >> 1) = 1 /\ t11.PREV))))) +
    (r_4.MODE = 4 /\ t11.POS = 1 /\ t11.PREV \/
     (t20.MODE = 2 /\
      ((t20.D2U & 5) = 1 \/
       (t20.D2U + t20.U2D = 0) /\ ((t11.M2S & 2) >> 1) = 1)) /\
     ~t12.PREV /\
     (t12.MODE = 1 /\
      ((t12.D2U = 5 /\ (t11.M2S & 5) = 1) \/
       ((t12.D2U + t12.U2D = 0) /\ (t11.M2S >> 2) = 1)) \/
      (t12.MODE = 2 /\
       (((t11.M2S & 5) = 1 /\ (t12.D2U & 3) = 1) \/
        ((t11.S2PM + t11.P2S + t11.M2S = 0) /\
         ((t12.D2U & 2) >> 1) = 1 /\ t11.PREV)))))) = 1)))

end