/*
==========================================================
CASE: tiny
--------
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_allocating_r_1]
  (r_1.MODE = 1) /\ (r_2.MODE ~= 2 /\ r_2.MODE ~= 3) /\ (t.D2U + t.U2D = 0) /\
  (t.MODE = 0)
  ==> (r_1.MODE' = 2) /\ ((mb02.CMD' = 0) /\ (mb04.CMD' = 0)) /\ (t.MODE' = 1)
  [=]
  
  [route_allocating_r_2]
  (r_2.MODE = 1) /\ (r_1.MODE ~= 2 /\ r_1.MODE ~= 3) /\ (t.D2U + t.U2D = 0) /\
  (t.MODE = 0)
  ==> (r_2.MODE' = 2) /\ ((mb01.CMD' = 0) /\ (mb03.CMD' = 0)) /\ (t.MODE' = 1)
  [=]
  
  [route_lock_r_1]
  r_1.MODE = 2 /\ ((mb02.ACT = 0) /\ (mb04.ACT = 0)) /\ (t.D2U + t.U2D = 0) /\
  (t.MODE = 1)
  ==> r_1.MODE' = 3 /\ mb01.CMD' = 1
  [=]
  
  [route_lock_r_2]
  r_2.MODE = 2 /\ ((mb01.ACT = 0) /\ (mb03.ACT = 0)) /\ (t.D2U + t.U2D = 0) /\
  (t.MODE = 1)
  ==> r_2.MODE' = 3 /\ mb04.CMD' = 1
  [=]
  
  [route_in_use_r_1] r_1.MODE = 3 /\ ~(t.D2U + t.U2D = 0) ==>
  r_1.MODE' = 4 /\ mb01.CMD' = 0 /\ t.MODE' = 2
  [=]
  
  [route_in_use_r_2] r_2.MODE = 3 /\ ~(t.D2U + t.U2D = 0) ==>
  r_2.MODE' = 4 /\ mb04.CMD' = 0 /\ t.MODE' = 2
  [=]
  
  [route_in_use_r_1] r_1.MODE = 3 /\ ~(t.D2U + t.U2D = 0) ==>
  r_1.MODE' = 4 /\ mb01.CMD' = 0 /\ t.MODE' = 2
  [=]
  
  [route_in_use_r_2] r_2.MODE = 3 /\ ~(t.D2U + t.U2D = 0) ==>
  r_2.MODE' = 4 /\ mb04.CMD' = 0 /\ t.MODE' = 2
  [=]
  
  [route_in_use_r_1] r_1.MODE = 3 /\ ~(t.D2U + t.U2D = 0) ==>
  r_1.MODE' = 4 /\ mb01.CMD' = 0 /\ t.MODE' = 2
  [=]
  
  [route_in_use_r_2] r_2.MODE = 3 /\ ~(t.D2U + t.U2D = 0) ==>
  r_2.MODE' = 4 /\ mb04.CMD' = 0 /\ t.MODE' = 2
  [=]
  
  [sequential_release_last_elem_r_1]
  r_1.MODE = 4 /\ t.MODE = 2 /\ (t.D2U + t.U2D = 0)
  ==> t.MODE' = 0 /\ t.PREV' = 0 /\ r_1.MODE' = 0
  [=]
  
  [sequential_release_last_elem_r_2]
  r_2.MODE = 4 /\ t.MODE = 2 /\ (t.D2U + t.U2D = 0)
  ==> t.MODE' = 0 /\ t.PREV' = 0 /\ r_2.MODE' = 0
  [=]
  
  [release_last_elem_pseudo_timer_r_1]
  r_1.MODE = 4 /\ t.MODE = 2 /\ t.D2U = 0b111 /\ mb03.ACT = 0
  ==> t.MODE' = 0 /\ t.PREV' = 0 /\ r_1.MODE' = 0
  [=]
  
  [release_last_elem_pseudo_timer_r_2]
  r_2.MODE = 4 /\ t.MODE = 2 /\ t.U2D = 0b111 /\ mb02.ACT = 0
  ==> t.MODE' = 0 /\ t.PREV' = 0 /\ r_2.MODE' = 0)
 [>]
 
 ([communicate_signal_aspect_mb01] mb01.ACT ~= mb01.CMD ==>
  mb01.ACT' = mb01.CMD
  [=]
  
  [communicate_signal_aspect_mb02] mb02.ACT ~= mb02.CMD ==>
  mb02.ACT' = mb02.CMD
  [=]
  
  [communicate_signal_aspect_mb03] mb03.ACT ~= mb03.CMD ==>
  mb03.ACT' = mb03.CMD
  [=]
  
  [communicate_signal_aspect_mb04] mb04.ACT ~= mb04.CMD ==>
  mb04.ACT' = mb04.CMD)
 [>]
 
 ([change_direction_up_to_down_t] t.D2U = 0b111 /\ mb03.ACT = 0 ==>
  t.D2U' = t.U2D /\ t.U2D' = t.D2U
  [=]
  
  [change_direction_down_to_up_t] t.U2D = 0b111 /\ mb02.ACT = 0 ==>
  t.D2U' = t.U2D /\ t.U2D' = t.D2U
  [=]
  
  [enter_interlocked_area_head_from_down_bd] mb01.ACT = 1 ==>
  t.D2U' = (t.D2U ^ 5)
  [=]
  
  [enter_interlocked_area_tail_from_down_bd] (t.D2U & 3) = 1 ==>
  t.D2U' = (t.D2U ^ 2)
  [=]
  
  [enter_interlocked_area_head_from_up_bu] mb04.ACT = 1 ==>
  t.U2D' = (t.U2D ^ 5)
  [=]
  
  [enter_interlocked_area_tail_from_up_bu] (t.U2D & 3) = 1 ==>
  t.U2D' = (t.U2D ^ 2)
  [=]
  
  [leave_interlocked_area_head_to_down_bd] (t.U2D & 5) = 5 ==>
  t.U2D' = (t.U2D ^ 4)
  [=]
  
  [leave_interlocked_area_tail_to_down_bd] t.U2D = 3 ==> t.U2D' = 0
  [=]
  
  [leave_interlocked_area_head_to_up_bu] (t.D2U & 5) = 5 ==>
  t.D2U' = (t.D2U ^ 4)
  [=]
  
  [leave_interlocked_area_tail_to_up_bu] t.D2U = 3 ==> t.D2U' = 0))

invariant

[no_head_to_head_collisions_linear]
(t.D2U * t.U2D = 0),

[no_head_to_tail_collisions_linear]
(t.D2U * (1 - (t.D2U & 1)) + t.U2D * (1 - (t.U2D & 1)) = 0),

[no_head_to_head_collisions_point]
1,

[no_head_to_tail_collisions_point]
1,

[no_derailments]
1,

[train_integrity_linear_up]
1,

[train_integrity_linear_down]
1,

[train_integrity_point_stem_to_plusminus]
1,

[train_integrity_point_plusminus_to_stem]
1,

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

[route_allocating_cnd]
(((r_1.MODE = 2) =>
  (((mb02.CMD = 0) /\ (mb04.CMD = 0)) /\ (t.MODE = 1) /\
   (t.D2U + t.U2D = 0))) /\
 ((r_2.MODE = 2) =>
  (((mb01.CMD = 0) /\ (mb03.CMD = 0)) /\ (t.MODE = 1) /\ (t.D2U + t.U2D = 0)))),

[route_lock_cnd]
(((r_1.MODE = 3) =>
  ((mb02.ACT = 0 /\ mb02.ACT = mb02.CMD) /\
   (mb04.ACT = 0 /\ mb04.ACT = mb04.CMD)) /\ (t.MODE = 1) /\
  ((t.D2U + t.U2D = 0) \/ t.D2U = 5) /\ mb01.CMD = 1) /\
 ((r_2.MODE = 3) =>
  ((mb01.ACT = 0 /\ mb01.ACT = mb01.CMD) /\
   (mb03.ACT = 0 /\ mb03.ACT = mb03.CMD)) /\ (t.MODE = 1) /\
  ((t.D2U + t.U2D = 0) \/ t.U2D = 5) /\ mb04.CMD = 1)),

[route_used_cnd_a]
((r_1.MODE = 4 => (t.MODE ~= 0)) /\ (r_2.MODE = 4 => (t.MODE ~= 0))),

[route_used_cnd_b]
((r_1.MODE = 4 => ((t.D2U & 1) \/ (t.MODE = 2) /\ (t.D2U + t.U2D = 0))) /\
 (r_2.MODE = 4 => ((t.U2D & 1) \/ (t.MODE = 2) /\ (t.D2U + t.U2D = 0)))),

[route_used_cnd_c]
1,

[route_in_use_last_sec_is_free_in_opposite_dir]
((r_1.MODE = 4 => t.U2D = 0) /\ (r_2.MODE = 4 => t.D2U = 0)),

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

[first_entry_cnd]
(~(~(t.D2U + t.U2D = 0) /\ mb01.CMD = 1 /\ mb01.ACT = 0) /\
 ~(~(t.D2U + t.U2D = 0) /\ mb04.CMD = 1 /\ mb04.ACT = 0)),

[entry_signal_closed_when_tail_in_first]
((((t.D2U & 2) >> 1) => mb01.ACT = 0) /\ (((t.U2D & 2) >> 1) => mb04.ACT = 0)),

[signal_cmd_open_cnd]
((mb01.CMD = 1 => ((r_1.MODE = 3) = 1)) /\
 (mb04.CMD = 1 => ((r_2.MODE = 3) = 1))),

[signal_act_open_cnd]
((mb01.ACT = 1 =>
  (((r_1.MODE = 3 /\ (mb01.CMD = 1 \/ (t.D2U >> 2) ~= 0)) \/
    (r_1.MODE = 4 /\ mb01.CMD = 0 /\ (t.D2U >> 2) ~= 0)) = 1)) /\
 (mb04.ACT = 1 =>
  (((r_2.MODE = 3 /\ (mb04.CMD = 1 \/ (t.U2D >> 2) ~= 0)) \/
    (r_2.MODE = 4 /\ mb04.CMD = 0 /\ (t.U2D >> 2) ~= 0)) = 1))),

[not_commanding_occupied_point_to_move]
1,

[point_only_cmd_when_alloc_a_route]
1,

[ground_unused_signal]
((mb02.ACT = 0 /\ mb02.CMD = 0) /\ (mb03.ACT = 0 /\ mb03.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]
((bd.U2D = 0 /\ bd.D2U = 0) /\ (bu.U2D = 0 /\ bu.D2U = 0)),

[element_prev_variable]
(t.PREV = 1 => t.MODE = 2),

[occupied_implies_exlck_or_used_point]
1,

[occupied_implies_exlck_or_used_linear]
1,

[point_chunk_cnd_stem_plus]
1,

[point_chunk_cnd_stem_minus]
1,

[hto_vs_mode]
1,

[hto_vs_mode_last_down]
((t.D2U = 1 => t.MODE = 2) /\ (t.D2U = 3 => t.MODE = 0 \/ t.MODE = 2) /\
 (t.D2U = 5 => t.MODE = 1 \/ t.MODE = 2) /\
 (t.D2U = 7 => t.MODE = 0 \/ t.MODE = 2) /\
 ((r_1.MODE = 4 /\ t.MODE = 2 /\ t.PREV = 1 /\ t.D2U = 0) => t.U2D = 0)),

[hto_vs_mode_last_up]
((t.U2D = 1 => t.MODE = 2) /\ (t.U2D = 3 => t.MODE = 0 \/ t.MODE = 2) /\
 (t.U2D = 5 => t.MODE = 1 \/ t.MODE = 2) /\
 (t.U2D = 7 => t.MODE = 0 \/ t.MODE = 2) /\
 ((r_2.MODE = 4 /\ t.MODE = 2 /\ t.PREV = 1 /\ t.U2D = 0) => t.D2U = 0)),

[elem_locked_by_only_one_route]
(t.MODE = 1 =>
 ((((r_1.MODE = 2) \/ (r_1.MODE = 3)) + ((r_2.MODE = 2) \/ (r_2.MODE = 3))) =
  1)),

[elem_used_by_only_one_route]
(t.MODE = 2 => (((r_1.MODE = 4) + (r_2.MODE = 4)) = 1))

end