/* =======================================================
 *     File: $Name: dk_interlocking.kr $
 *  Created: $Date: 2014-04-10 12:22:23 $
 *   Author: $Author: Linh H. Vu<lvho@dtu.dk> $
 * =======================================================
 * Description: Generic behavioral model of the forthcoming
 * Danish interlocking systems
 * =======================================================
 * Route states:
 * ============
 * 0 : FREE
 * 1 : MARKED
 * 2 : ALLOCATING
 * 3 : LOCKED
 * 4 : OCCUPIED
 * Signals aspect:
 * ==============
 * 0 : CLOSED
 * 1 : OPEN
 * Point positions:
 * ===============
 * 0 : PLUS
 * 1 : MINUS
 * 2 : INTER
 * Element modes:
 * =============
 * 0 : AVAIL
 * 1 : EXLCK
 * 2 : USED
 */
kripke dk_interlocking

encoding

/**
 * D2U: occupancy status for direction from down to up
 * U2D: occupancy status for direction from up to down
 * MODE: current mode of the element
 * PREV: whether the previous element in the same route has been
 * released
 */
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],
/**
 * S2PM: occupancy status for direction from stem to plus/minus
 * P2S: occupancy status for direction from plus to stem
 * M2S: occupancy status for direction from minus to stem
 * CMD: commanded position of the point
 * POS: actual position of the point
 * MODE: current mode of the element
 * PREV: whether the previous element in the same route has been
 * released
 */
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],
/**
 * ACT: actual aspect of the signal
 * CMD: commanded aspect of the signal
 */
Signal::
  ACT -> [INPUT,"unsigned int",0,0,1]
  CMD -> [OUTPUT,"unsigned int",0,0,1],
/**
 * MODE: current mode of the route (internal)
 */
Route::
  MODE -> [LOCAL,"unsigned int",0,0,4]

// init
// /**
//  * Linear sections are vacant and available, their PREV variables are unset
//  */
// [initial_state_linear]
// (all l : Linear :- vacant(l) /\ l.MODE = AVAIL /\ l.PREV = PENDING),
// /**
//  * Points are vacant and available, their PREV variables are unset, and their
//  * positions are PLUS
//  */
// [initial_state_point]
// (all p : Linear :-
//  (vacant(p) /\ p.MODE = AVAIL /\ p.PREV = PENDING) /\
//  (p.CMD = PLUS /\ p.POS = PLUS)),
// /**
//  * Signals are CLOSED
//  */
// [initial_state_signal]
// (all s : Signal :- s.CMD = CLOSED /\ s.ACT = CLOSED),
// /**
//  * Routes are FREE and no pending commands
//  */
// [initial_state_route]
// (all r : Route :- r.MODE = FREE)
/**
 * =======================================
 * TRANSITION RELATION OF THE WHOLE SYSTEM
 * =======================================
 */
transrel

[DP] [=] ([SUT] [>] [ET] [>] [TM])

/**
 * =============================
 * ROUTE DISPATCHING TRANSITIONS
 * =============================
 */
module DP

([=] r : Route :- [route_dispatching] (r.MODE = FREE) ==> (r.MODE' = MARKED))

/**
 * ========================
 * INTERLOCKING TRANSITIONS
 * ========================
 */
/*@\label{kr:SUT}@*/
module SUT

/*
 * ROUTE ALLOCATING
 * ================
 */
([=] r : Route :-
 [route_allocating]
 (r.MODE = MARKED) /\
 /* none of the conflicting routes in ALLOCATING(2) or LOCKED(3) modes
  */
 (all cr : Route :-
  (cr isin conflicts(r)) => (cr.MODE ~= ALLOCATING /\ cr.MODE ~= LOCKED)) /\
 /* all detection sections in the path and overlap are vacant */
 (all e : Section :-
  e isin (elems path(r) union elems overlap(r)) => vacant(e)) /\
 /* all elements in route's path are in AVAIL mode */
 (all e : Section :- e isin path(r) => (e.MODE = AVAIL)) /\
 /* all elements in route's overlap are not in USED mode */
 (all e : Section :- e isin overlap(r) => (e.MODE ~= USED)) /\
 /* all protecting points are in AVAIL mode,
  * or are already in the correct position */
 (all e : Point :-
  e isin (dom points(r) \ elems path(r)) =>
  (e.MODE = AVAIL \/ e.POS = req(r,e)))
 ==>
 (r.MODE' = ALLOCATING) /\
 /* command points */
 (all p : Point :- p isin points(r) => (p.CMD' = req(r,p))) /\
 /* command signals */
 (all s : Signal :- s isin signals(r) => (s.CMD' = CLOSED)) /\
 /* lock exclusively all elements in the route's path */
 (all e : Section :- e isin path(r) => (e.MODE' = EXLCK)))
[=]

/**
 * ROUTE LOCKING
 * =============
 */
([=] r : Route :-
 [route_lock]
 r.MODE = ALLOCATING /\
 /* protecting signals' actual aspects are as required */
 (all s : Signal :- s isin signals(r) => (s.ACT = CLOSED)) /\
 /* points' actual positions are as required */
 (all p : Point :- p isin points(r) => (p.POS = req(r,p))) /\
 /* all detection sections in the path and overlap are vacant */
 (all e : Section :-
  e isin (elems path(r) union elems overlap(r)) => vacant(e)) /\
 /* all elements in the route's path are locked exclusively */
 (all e : Section :- e isin path(r) => (e.MODE = EXLCK))
 ==> r.MODE' = LOCKED /\ src(r).CMD' = OPEN)
[=]

/**
 * ROUTE IN USE + FIRST ELEMENT IN USE
 * ===================================
 */
([=] r : Route :-
 [route_in_use]
 /* the first element of the route is occupied */
 let e = first(r) in
   r.MODE = LOCKED /\ ~vacant(e)
 end
 ==> r.MODE' = OCCUPIED /\ src(r).CMD' = CLOSED /\ first(r).MODE' = USED)
[=]

/**
 * ELEMENT IN USE
 * ==============
 * Excluding the first element
 */
([=] r : Route :-
 ([=] e : Section :-
  [element_in_use]
  e isin path(r) /\ e ~= first(r) /\ prev(r,e).MODE = USED /\
  r.MODE = OCCUPIED /\ e.MODE = EXLCK /\ not vacant(e) /\
  ((e isin Point) => e.POS = req(r,e)) /\
  (e ~= last(r) => next(r,e).MODE = EXLCK)
  ==> e.MODE' = USED))
[=]

/**
 * SEQUENTIAL RELEASE OF ELEMENTS
 * ==============================
 * Except the last element
 */
([=] r : Route :-
 ([=] e : Section :-
  [sequential_release_e]
  e isin path(r) /\ e ~= last(r) /\ r.MODE = OCCUPIED /\
  e.MODE = USED /\ vacant(e) /\ (e ~= first(r) => e.PREV = RELEASED) /\
  let nx = next(r,e) in
    nx.PREV = PENDING /\ nx.MODE = USED /\ (_T_(hto(nx,r,0)) ~= 0) /\
    ((nx isin Point) => nx.POS = req(r,nx))
  end /\ ((e isin Point) => e.POS = req(r,e))
  ==> e.MODE' = FREE /\ e.PREV' = PENDING /\ next(r,e).PREV' = RELEASED))
[=]

/**
 * SEQUENTIAL RELEASE OF THE LAST ELEMENT + ROUTE
 * ==============================================
 * - It is the last element, release the route
 */
([=] r : Route :-
 [sequential_release_last_elem]
 r.MODE = OCCUPIED /\
 let e = last(r) in
   e.MODE = USED /\ vacant(e) /\ (e ~= first(r) => e.PREV = RELEASED) /\
   ((e isin Point) => e.POS = req(r,e))
 end
 ==> last(r).MODE' = AVAIL /\ last(r).PREV' = PENDING /\ r.MODE' = FREE)
[=]

/**
 * RELEASE THE LAST ELEMENT AND THE ROUTE
 * ======================================
 */
([=] r : Route :-
 [release_last_elem_pseudo_timer]
 r.MODE = OCCUPIED /\
 let e = last(r) in
   e.MODE = USED /\ hto(e,r,0) = 0b111 /\ dst(r).ACT = CLOSED /\
   (e ~= first(r) => e.PREV = RELEASED)
 end
 ==> last(r).MODE' = AVAIL /\ last(r).PREV' = PENDING /\ r.MODE' = FREE)

/**
 * =========================
 * TRACK ELEMENT TRANSITIONS
 * =========================
 */
/*@\label{kr:ET}@*/
module ET

/**
 * POINT SWITCHING
 * ===============
 */
/* Start switching */
([=] p : Point :-
 [point_switch_1] p.POS ~= p.CMD /\ p.POS ~= INTER ==> p.POS' = INTER)
[=]

/* Move in the commanded position */
([=] p : Point :- [point_switch_2] p.POS = INTER ==> p.POS' = p.CMD)
[=]

/**
 * COMMUNICATE SIGNAL ASPECTS TO TRAINS
 * ====================================
 */
([=] s : Signal :-
 [communicate_signal_aspect] s.ACT ~= s.CMD ==> s.ACT' = s.CMD)

/**
 * ==========================
 * TRAIN MOVEMENT TRANSITIONS
 * ==========================
 */
/*@\label{kr:TM}@*/
module TM

/**
 * HEAD MOVEMENT ON LINEAR SECTIONS
 * ================================
 */
/* from down to up */
([=] l : Linear :-
 [head_movement_linear_up]
 up(l) /\ ~is_boundary_sec_up(up(l)) /\ ~is_boundary_sec_down(l) /\
 occupied_with_head(l.D2U) /\ (~up_sig(l) \/ up_sig(l).ACT = OPEN)
 ==> head_leaves(l.D2U,l.D2U') /\ head_enters_next(up(l),l))
[=]

/* from up to down */
([=] l : Linear :-
 [head_movement_linear_down]
 down(l) /\ ~is_boundary_sec_down(down(l)) /\ ~is_boundary_sec_up(l) /\
 occupied_with_head(l.U2D) /\ (~down_sig(l) \/ down_sig(l).ACT = OPEN)
 ==> head_leaves(l.U2D,l.U2D') /\ head_enters_next(down(l),l))
[=]

/**
 * TAIL MOVEMENT ON LINEAR SECTIONS
 * ================================
 */
/* from down to up */
([=] l : Linear :-
 [tail_movement_linear_up]
 up(l) /\ ~is_boundary_sec_up(up(l)) /\ ~is_boundary_sec_down(l) /\
 occupied_with_only_tail(l.D2U)
 ==> tail_leaves(l.D2U,l.D2U') /\ tail_enters_next(up(l),l))
[=]

/* from up to down */
([=] l : Linear :-
 [tail_movement_linear_down]
 down(l) /\ ~is_boundary_sec_down(down(l)) /\ ~is_boundary_sec_up(l) /\
 occupied_with_only_tail(l.U2D)
 ==> tail_leaves(l.U2D,l.U2D') /\ tail_enters_next(down(l),l))
[=]

/**
 * HEAD MOVEMENT ON POINT SECTIONS
 * ===============================
 */
/* from stem toward plus */
([=] p : Point :-
 [head_movement_point_stem_to_plus] occupied_with_head(p.S2PM) /\ p.POS = PLUS
 ==> head_leaves(p.S2PM,p.S2PM') /\ head_enters_next(plus(p),p))
[=]

/* from stem toward minus */
([=] p : Point :-
 [head_movement_point_stem_to_minus]
 occupied_with_head(p.S2PM) /\ p.POS = MINUS
 ==> head_leaves(p.S2PM,p.S2PM') /\ head_enters_next(minus(p),p))
[=]

/* from plus toward stem */
([=] p : Point :-
 [head_movement_point_plus_to_stem] occupied_with_head(p.P2S) /\ p.POS = PLUS
 ==> head_leaves(p.P2S,p.P2S') /\ head_enters_next(stem(p),p))
[=]

/* from minus toward stem */
([=] p : Point :-
 [head_movement_point_minus_to_stem]
 occupied_with_head(p.M2S) /\ p.POS = MINUS
 ==> head_leaves(p.M2S,p.M2S') /\ head_enters_next(stem(p),p))
[=]

/**
 * TAIL MOVEMENT ON POINT SECTIONS
 * ===============================
 */
/* from stem toward plus */
([=] p : Point :-
 [tail_movement_point_stem_to_plus]
 occupied_with_only_tail(p.S2PM) /\ p.POS = PLUS
 ==> tail_leaves(p.S2PM,p.S2PM') /\ tail_enters_next(plus(p),p))
[=]

/* from stem toward minus */
([=] p : Point :-
 [tail_movement_point_stem_to_minus]
 occupied_with_only_tail(p.S2PM) /\ p.POS = MINUS
 ==> tail_leaves(p.S2PM,p.S2PM') /\ tail_enters_next(minus(p),p))
[=]

/* from plus toward stem */
([=] p : Point :-
 [tail_movement_point_plus_to_stem]
 occupied_with_only_tail(p.P2S) /\ p.POS = PLUS
 ==> tail_leaves(p.P2S,p.P2S') /\ tail_enters_next(stem(p),p))
[=]

/* from minus toward stem */
([=] p : Point :-
 [tail_movement_point_minus_to_stem]
 occupied_with_only_tail(p.M2S) /\ p.POS = MINUS
 ==> tail_leaves(p.M2S,p.M2S) /\ tail_enters_next(stem(p),p))
[=]

/**
 * CHANGE DIRECTION (ONLY ON LINEAR SECTIONS)
 * ==========================================
 */
/* change direction from going upward to downward */
([=] l : Linear :-
 [change_direction_up_to_down]
 down_sig(l) /\ up_sig(l) /\ l.D2U = 0b111 /\ up_sig(l).ACT = CLOSED
 ==> swap_up_down_vars(l))
[=]

/* change direction from going downward to upward */
([=] l : Linear :-
 [change_direction_down_to_up]
 down_sig(l) /\ up_sig(l) /\ l.U2D = 0b111 /\ down_sig(l).ACT = CLOSED
 ==> swap_up_down_vars(l))
[=]

/**
 * ENTER INTERLOCKED AREA (ONLY ON LINEAR SECTIONS)
 * ================================================
 */
/**
 * from the down side if down is the border of interlocked area
 * <-- down       up -->
 * ////------|--||------
 *       l   []    up(l)
 *           sig
 */
/* head enters */
([=] l : Linear :-
 [enter_interlocked_area_head_from_down]
 is_boundary_sec_down(l) /\ up_sig(l).ACT = OPEN
 ==>
 let e = up(l) in
   head_enters(e.D2U,e.D2U')
 end)
[=]

/* tail enters */
([=] l : Linear :-
 [enter_interlocked_area_tail_from_down]
 is_boundary_sec_down(l) /\
 let e = up(l) in
   occupied_without_tail(e.D2U)
 end
 ==>
 let e = up(l) in
   tail_enters(e.D2U,e.D2U')
 end)
[=]

/**
 * from the up if the up is the border of interlocked area
 * <-- down         up -->
 *           sig
 * down(l)    []   l
 * --------||--|------////
 */
/* head enters */
([=] l : Linear :-
 [enter_interlocked_area_head_from_up]
 is_boundary_sec_up(l) /\ down_sig(l).ACT = OPEN
 ==>
 let e = down(l) in
   head_enters(e.U2D,e.U2D')
 end)
[=]

/* tail enters */
([=] l : Linear :-
 [enter_interlocked_area_tail_from_up]
 is_boundary_sec_up(l) /\
 let e = down(l) in
   occupied_without_tail(e.U2D)
 end
 ==>
 let e = down(l) in
   tail_enters(e.U2D,e.U2D')
 end)
[=]

/**
 * LEAVE INTERLOCKED AREA (ONLY ON LINEAR SECTIONS)
 * ================================================
 * We don't care the aspect of the exit signal since the exiting signal
 * is not controled by this interlocking
 */
/**
 * leave downward if the down is border
 * <-- down      up -->
 * ////--------||------
 *       l       up(l)
 */
/* head leaves */
([=] l : Linear :-
 [leave_interlocked_area_head_to_down]
 is_boundary_sec_down(l) /\
 let e = up(l) in
   occupied_with_head(e.U2D)
 end
 ==>
 let e = up(l) in
   head_leaves(e.U2D,e.U2D')
 end)
[=]

/* tail leaves */
([=] l : Linear :-
 [leave_interlocked_area_tail_to_down]
 is_boundary_sec_down(l) /\
 let e = up(l) in
   occupied_with_only_tail(e.U2D)
 end
 ==>
 let e = up(l) in
   tail_leaves(e.U2D,e.U2D')
 end)
[=]

/**
 * leave upward if the up is border
 * <-- down       up -->
 * down(l)       l
 * --------||-------////
 */
/* head leaves */
([=] l : Linear :-
 [leave_interlocked_area_head_to_up]
 is_boundary_sec_up(l) /\
 let e = down(l) in
   occupied_with_head(e.D2U)
 end
 ==>
 let e = down(l) in
   head_leaves(e.D2U,e.D2U')
 end)
[=]

/* tail leaves */
([=] l : Linear :-
 [leave_interlocked_area_tail_to_up]
 is_boundary_sec_up(l) /\
 let e = down(l) in
   occupied_with_only_tail(e.D2U)
 end
 ==>
 let e = down(l) in
   tail_leaves(e.D2U,e.D2U')
 end)

invariant

/**
 * ============================
 * HIGH-LEVEL SAFETY PROPERTIES
 * ============================
 */
[no_head_to_head_collisions_linear]
(all l : Linear :- (~is_boundary_sec(l)) => (l.D2U * l.U2D = 0)),

[no_head_to_tail_collisions_linear]
(all l : Linear :-
 (~is_boundary_sec(l)) =>
 (l.D2U * (1 - (l.D2U & 1)) + l.U2D * (1 - (l.U2D & 1)) = 0)),

[no_head_to_head_collisions_point]
(all p : Point :- p.M2S * p.S2PM + p.P2S * p.S2PM + p.P2S * p.M2S = 0),

[no_head_to_tail_collisions_point]
(all p : Point :-
 p.S2PM * (1 - (p.S2PM & 1)) + p.P2S * (1 - (p.P2S & 1)) +
 p.M2S * (1 - (p.M2S & 1)) = 0),

[no_derailments]
(all p : Point :-
 p.POS * p.P2S + (1 - (p.POS & 1)) * p.M2S + (p.POS >> 1) * p.S2PM = 0),

/**
 *
 * ========================
 * STRENGTHENING INVARIANTS
 * ========================
 */
/**
 * TRAIN INTEGRITY CONDITIONS
 * ==========================
 */
/* linear section, up direction */
[train_integrity_linear_up]
(all l : Linear :-
 (up(l) /\ ~is_boundary_sec_up(up(l)) /\ ~is_boundary_sec_down(l)) =>
 ((occupied_without_head(l.D2U) => occupied_without_tail(hto(up(l),l))) /\
  (occupied_without_tail(hto(up(l),l)) => occupied_without_head(l.D2U)))),

/* linear section, down direction */
[train_integrity_linear_down]
(all l : Linear :-
 (down(l) /\ ~is_boundary_sec_down(down(l)) /\ ~is_boundary_sec_up(l)) =>
 ((occupied_without_head(l.U2D) => occupied_without_tail(hto(down(l),l))) /\
  (occupied_without_tail(hto(down(l),l)) => occupied_without_head(l.U2D)))),

/* point section, from stem toward plus/minus */
[train_integrity_point_stem_to_plusminus]
(all p : Point :-
 (occupied_without_head(p.S2PM) =>
  ((occupied_without_tail(hto(plus(p),p)) /\ p.POS = PLUS) xor
   (occupied_without_tail(hto(minus(p),p)) /\ p.POS = MINUS))) /\
 (occupied_without_tail(hto(plus(p),p)) =>
  (occupied_without_head(p.S2PM) /\ p.POS = PLUS)) /\
 (occupied_without_tail(hto(minus(p),p)) =>
  (occupied_without_head(p.S2PM) /\ p.POS = MINUS)) /\
 ~(occupied_without_tail(hto(plus(p),p)) /\
  occupied_without_tail(hto(minus(p),p)))),

/* point section, from plus/minus toward stem */
[train_integrity_point_plusminus_to_stem]
(all p : Point :-
 (occupied_without_head(p.P2S) =>
  (occupied_without_tail(hto(stem(p),p)) /\ p.POS = PLUS)) /\
 (occupied_without_head(p.M2S) =>
  (occupied_without_tail(hto(stem(p),p)) /\ p.POS = MINUS)) /\
 (occupied_without_tail(hto(stem(p),p)) =>
  ((occupied_without_head(p.P2S) /\ p.POS = PLUS) xor
   (occupied_without_head(p.M2S) /\ p.POS = MINUS)))),

/* \ ~ (occupied_without_head(p.P2S) /\ occupied_without_head(p.M2S))), ->
 * covered by point
 * safety prop */
/**
 * CONDITIONS ON ROUTES
 * ====================
 */
[conflicting_routes_are_not_set_together]
(all r : Route :-
 (r.MODE = ALLOCATING \/ r.MODE = LOCKED) =>
 (all cr : Route :-
  cr isin conflicts(r) => (cr.MODE ~= ALLOCATING /\ cr.MODE ~= LOCKED))),

[route_allocating_cnd]
(all r : Route :-
 (r.MODE = ALLOCATING) =>
 /* points are commanded in correct positions */
 ((all p : Point :- p isin points(r) => (p.CMD = req(r,p))) /\
  /* protecting signals are commanded in correct aspects */
  (all s : Signal :- s isin signals(r) => (s.CMD = CLOSED)) /\
  /* all lockable elements in the path are EXLCK(1) */
  (all e : Section :- e isin path(r) => (e.MODE = EXLCK)) /\
  /* all sections have to be vacant */
  (all e : Section :-
   e isin (elems path(r) union elems overlap(r)) => vacant(e)))),

[route_lock_cnd]
(all r : Route :-
 (r.MODE = LOCKED) =>
 let fst = first(r) in
   /* points are in correct positions */
   (all p : Point :-
    p isin points(r) => (p.POS = req(r,p) /\ p.POS = p.CMD)) /\
   /* protecting signals are in correct aspects */
   (all s : Signal :-
    s isin signals(r) => (s.ACT = CLOSED /\ s.ACT = s.CMD)) /\
   /* all lockable elements in the path are EXLCK(1) */
   (all e : Section :- e isin path(r) => (e.MODE = EXLCK)) /\
   /* all sections except the first one have to be vacant */
   (all e : Section :-
    (e ~= fst /\ e isin (elems path(r) union elems overlap(r))) =>
    vacant(e)) /\
   /* first section is vacant or occupied by head of the train */
   (vacant(fst) \/ hto(fst,r) = 5) /\
   /* entry signal is commanded to be open */
   src(r).CMD = OPEN
 end),

[route_used_cnd_a]
(all r : Route :- r.MODE = OCCUPIED => (last(r).MODE ~= AVAIL)),

[route_used_cnd_b]
(all r : Route :-
 r.MODE = OCCUPIED =>
 (count_fwd___O(r) \/
  let fst = first(r),
      lst = last(r) in
    ((lst ~= fst) ? lst.PREV : (lst.MODE = USED)) /\ vacant(last(r))
  end)),

[route_used_cnd_c]
(all r : Route :- r.MODE = OCCUPIED => linear_chunk_cnd(r,last(r))),

[route_in_use_last_sec_is_free_in_opposite_dir]
(all r : Route :- r.MODE = OCCUPIED => bwd_hto(last(r),r,0) = 0),

[routes_share_last_not_used_at_same_time]
(all r : Route :-
 r.MODE = OCCUPIED =>
 (all opr : Route :-
  (opr ~= r /\ last(r) = last(opr)) => (opr.MODE ~= OCCUPIED))),

[first_entry_cnd]
(all r : Route :-
 ~(~vacant(first(r)) /\ src(r).CMD = OPEN /\ src(r).ACT = CLOSED)),

/**
 * CONDITIONS ON SIGNALS
 * =====================
 */
[entry_signal_closed_when_tail_in_first]
(all r : Route :- _T_(hto(first(r),r)) => src(r).ACT = CLOSED),

[signal_cmd_open_cnd]
(all s : Signal :-
 (exists r : Route :- s = src(r)) =>
 (s.CMD = OPEN => (exists! r : Route :- src(r) = s /\ r.MODE = LOCKED))),

[signal_act_open_cnd]
(all s : Signal :-
 (exists r : Route :- s = src(r)) =>
 (s.ACT = OPEN =>
  (exists! r : Route :-
   (src(r) = s) /\
   (((r.MODE = LOCKED /\
      (s.CMD = OPEN \/ H__(hto(first(r),r)) ~= 0)) \/
     (r.MODE = OCCUPIED /\ s.CMD = CLOSED /\
      H__(hto(first(r),r)) ~= 0)) /\
    (all e : Section :-
     (e isin path(r) /\ e ~= first(r)) => (vacant(e) /\ e.MODE = EXLCK)) /\
    (all e : Section :- e isin overlap(r) => vacant(e)))))),

/**
 * POINT SWITCHING CONDITIONS
 * ==========================
 */
[not_commanding_occupied_point_to_move]
(all p : Point :- (~vacant(p) \/ p.MODE = USED) => p.POS = p.CMD),

/* protecting point can be in FREE mode */
[point_only_cmd_when_alloc_a_route]
(all e : Point :-
 (exists r : Route :- e isin points(r)) =>
 (e.CMD ~= e.POS =>
  (e.MODE ~= USED /\
   (exists r : Route :- e isin points(r) /\ r.MODE = ALLOCATING)))),

/**
 * GROUND UNOCCUPIED ELEMENTS
 * ======================
 */
/* if a signal is not an entry signal of any route, then it is always
 * CLOSED */
[ground_unused_signal]
(all s : Signal :-
 (all r : Route :- src(r) ~= s) => (s.ACT = CLOSED /\ s.CMD = CLOSED)),

/* ground unused segments */
[ground_unused_linear_to_down]
(all l : Linear :-
 /* a section is not used by any routes in the direction up */
 (~is_boundary_sec(l) /\
  (all r : Route :- l isin path(r) => entry(r,l) ~= UP) /\
  /* trains cannot turn around here */
  ~(can_turn_around_at(l) /\
   (exists r : Route :- l isin path(r) /\ entry(r,l) = DOWN))) =>
 (l.U2D = 0)),

[ground_unused_linear_to_up]
(all l : Linear :-
 /* a section is not used by any routes in the up direction up */
 (~is_boundary_sec(l) /\
  (all r : Route :- l isin path(r) => entry(r,l) ~= DOWN) /\
  /* trains cannot turn around here */
  ~(can_turn_around_at(l) /\
   (exists r : Route :- l isin path(r) /\ entry(r,l) = UP))) => (l.D2U = 0)),

[ground_unused_point_p]
(all p : Point :-
 (~(exists r : Route :-
   p isin (dom points(r) inter elems path(r)) /\ entry(r,p) = PLUS)) =>
 (p.P2S = 0)),

[ground_unused_point_m]
(all p : Point :-
 (~(exists r : Route :-
   p isin (dom points(r) inter elems path(r)) /\ entry(r,p) = MINUS)) =>
 (p.M2S = 0)),

[ground_unused_point_s]
(all p : Point :-
 (~(exists r : Route :-
   p isin (dom points(r) inter elems path(r)) /\ entry(r,p) = STEM)) =>
 (p.S2PM = 0)),

/**
 * Ground boundary sections
 */
[ground_unused_boundary_linear]
(all l : Linear :- is_boundary_sec(l) => (l.U2D = 0 /\ l.D2U = 0)),

/**
 * CONDITIONS ON ELEMENTS
 * ======================
 */
[element_prev_variable]
(all e : Section :- is_boundary_sec(e) \/ (e.PREV = RELEASED => e.MODE = USED)),

[occupied_implies_exlck_or_used_point]
(all e : Point :-
 (all r : Route :- e ~= last(r)) =>
 (~vacant(e) => (e.MODE = EXLCK \/ e.MODE = USED))),

[occupied_implies_exlck_or_used_linear]
(all e : Linear :-
 ((all r : Route :- e ~= last(r)) /\ down(e) /\ up(e)) =>
 (~vacant(e) => (e.MODE = EXLCK \/ e.MODE = USED))),

[point_chunk_cnd_stem_plus]
(all e : Point :-
 let s = stem(e),
     p = plus(e),
     s_b = hto(stem(e),e,0),
     p_b = hto(plus(e),e,0),
     s_t = e.S2PM,
     p_t = e.P2S in
   (~can_turn_around_at(s) /\ ~can_turn_around_at(p)) =>
   ((e.POS = PLUS) =>
    ((p_t + s_b) * (s_t + p_b * (~p.PREV /\ p.MODE = USED)) = 0))
 end),

[point_chunk_cnd_stem_minus]
(all e : Point :-
 let s = stem(e),
     m = minus(e),
     s_b = hto(stem(e),e,0),
     m_b = hto(minus(e),e,0),
     s_t = e.S2PM,
     m_t = e.M2S in
   (~can_turn_around_at(s) /\ ~can_turn_around_at(m)) =>
   ((e.POS = MINUS) =>
    ((m_t + s_b) * (s_t + m_b * (~m.PREV /\ m.MODE = USED)) = 0))
 end),

[hto_vs_mode]
(all r : Route :-
 (all e : Section :-
  (e isin path(r) /\ e ~= last(r)) =>
  ((hto(e,r,0) = 1 => e.MODE = USED) /\
   (hto(e,r,0) = 3 => e.MODE = USED) /\
   (hto(e,r,0) = 5 => e.MODE = EXLCK \/ e.MODE = USED) /\
   (hto(e,r,0) = 7 => e.MODE = USED)))),

[hto_vs_mode_last_down]
(all r : Route :-
 (entry(r,last(r)) = 0) =>
 let e = last(r) in
   (e.D2U = 1 => e.MODE = USED) /\
   (e.D2U = 3 => e.MODE = AVAIL \/ e.MODE = USED) /\
   (e.D2U = 5 => e.MODE = EXLCK \/ e.MODE = USED) /\
   (e.D2U = 7 => e.MODE = AVAIL \/ e.MODE = USED) /\
   ((r.MODE = OCCUPIED /\ e.MODE = USED /\ e.PREV = RELEASED /\ e.D2U = 0) =>
    (e.U2D = 0 /\
     (~up(e) \/ is_boundary_sec_up(up(e)) \/ _T_(hto(up(e),e)) = 1)))
 end),

[hto_vs_mode_last_up]
(all r : Route :-
 (entry(r,last(r)) = 1) =>
 let e = last(r) in
   (e.U2D = 1 => e.MODE = USED) /\
   (e.U2D = 3 => e.MODE = AVAIL \/ e.MODE = USED) /\
   (e.U2D = 5 => e.MODE = EXLCK \/ e.MODE = USED) /\
   (e.U2D = 7 => e.MODE = AVAIL \/ e.MODE = USED) /\
   ((r.MODE = OCCUPIED /\ e.MODE = USED /\ e.PREV = RELEASED /\ e.U2D = 0) =>
    (e.D2U = 0 /\
     (~down(e) \/ is_boundary_sec_down(down(e)) \/ _T_(hto(down(e),e)) = 1)))
 end),

[elem_locked_by_only_one_route]
(all e : Section :-
 (exists r : Route :- e isin path(r)) =>
 (e.MODE = EXLCK =>
  (exists! r : Route :-
   e isin path(r) /\
   let lst = last(r),
       fst = first(r) in
     /* route is allocating, imply all elems locked */
     ((r.MODE = ALLOCATING) \/
      /* route is locked, imply all elems locked */
      (r.MODE = LOCKED) \/
      /* route in use, the 1st elem is never locked when
       * the route is in use */
      ((e ~= fst) /\ r.MODE = OCCUPIED /\
       ((e isin Point) => (e.POS = req(r,e) /\ e.CMD = req(r,e))) /\
       /* next elems in the same route are locked and vacant */
       (all ne : Section :-
        ne isin nexts(r,e) =>
        (ne.MODE = EXLCK /\ vacant(ne) /\
         ((ne isin Point) =>
          (ne.POS = req(r,ne) /\ ne.CMD = req(r,ne))))) /\
       /* the head of the train is in e
        * then prev is occupied without a head
        * we have e ~= fst, thus pv always exists */
       let pv = prev(r,e) in
         (hto(e,r) = 5 /\ pv.MODE = USED /\
          ((pv isin Point) => pv.POS = req(r,pv)) /\
          occupied_without_head(hto(pv,r))) \/
         /* e is vacant, then the prev is locked or used */
         (vacant(e) /\ (pv.MODE = EXLCK \/ pv.MODE = USED) /\
          ((pv isin Point) => (pv.POS = req(r,pv) /\ pv.CMD = req(r,pv))))
       end))
   end))),

[elem_used_by_only_one_route]
(all e : Section :-
 (exists r : Route :- e isin path(r)) =>
 (e.MODE = USED =>
  (exists! r : Route :-
   e isin path(r) /\
   let fst = first(r),
       lst = last(r) in
     r.MODE = OCCUPIED /\ ((e isin Point) => e.POS = req(r,e)) /\
     (e ~= fst =>
      let pv = prev(r,e) in
        /* the prev has been released */
        e.PREV \/
        /* the prev is used without a head
         * or is going to be released */
        (((pv isin Point) => pv.POS = req(r,pv)) /\ pv.MODE = USED /\
         (occupied_without_head(hto(pv,r)) \/
          (vacant(pv) /\ _T_(hto(e,r)) = 1 /\ (pv ~= fst => pv.PREV))))
      end) /\
     (e ~= lst =>
      let nx = next(r,e) in
        ~nx.PREV /\
        /* this includes nx */
        (all p : Point :-
         p isin nexts(r,e) => (p.POS = req(r,p) /\ p.CMD = req(r,p))) /\
        ((nx.MODE = EXLCK /\
          ((hto(nx,r) = 5 /\ occupied_without_head(hto(e,r))) \/
           (vacant(nx) /\ H__(hto(e,r)) = 1)) /\
          (all ne : Section :-
           (ne ~= nx /\ ne isin nexts(r,e)) => (ne.MODE = EXLCK))) \/
         (nx.MODE = USED /\
          ((occupied_without_head(hto(e,r)) /\
            occupied_without_tail(hto(nx,r))) \/
           (vacant(e) /\ _T_(hto(nx,r)) = 1 /\ (e ~= fst => e.PREV)))))
      end)
   end)))

macro

/**
 * NAMED CONSTANTS
 */
/* control modes */
def NOCMD = 0,

def DISPATCH = 1,

def CANCEL = 2,

/* Route modes */
def FREE = 0,

def MARKED = 1,

def ALLOCATING = 2,

def LOCKED = 3,

def OCCUPIED = 4,

/* Signals aspect */
def CLOSED = 0,

def OPEN = 1,

/* Point positions and neighbor sides */
def PLUS = 0,

def MINUS = 1,

def STEM = 2,

def INTER = 2,

/* Element modes */
def AVAIL = 0,

def EXLCK = 1,

def USED = 2,

/* prev variable values */
def PENDING = 0,

def RELEASED = 1,

/* DIRECTION */
def DOWN = 0,

def UP = 1,

/*
 * Perform function f on a linear section
 * e: the linear element
 * p: the neighbor end
 * 0: down end
 * 1: up end
 * f: function to perform, takes two parameters: current value, next
 * value
 */
def do_linear(e,p,f) =
case p of
  DOWN -> f(e.D2U,e.D2U'),
  UP -> f(e.U2D,e.U2D')
end,

/*
 * Perform function f on a point section
 * e: the point element
 * p: the neighbor end
 * 0: plus end
 * 1: minus end
 * 2: stem end
 * f: function to perform, takes two parameters: current value, next
 * value
 */
def do_point(e,p,f) =
case p of
  PLUS -> f(e.P2S,e.P2S'),
  MINUS -> f(e.M2S,e.M2S'),
  STEM -> f(e.S2PM,e.S2PM')
end,

/*
 * Perform function f on a section. The function will decide whether to
 * perform
 * do_linear or do_point based on the type of e.
 * e: the linear element
 * p: the neighbor end
 * f: function to perform, takes two parameters: current value, next
 * value
 */
def do_sec(e,p,f) =
(e isin Linear) ? do_linear(e,p,f) : do_point(e,p,f),

/*
 * A function returns HTO variable at version 0
 */
def _hto0(v0,v1) =
v0,

/*
 * A function returns HTO variable at version 0
 */
def _hto1(v0,v1) =
v1,

/*
 * Return the HTO variable of the element e in the direction that the route r
 * enters e
 */
/*@\label{kr:route-entry-hto}@*/
def route_entry_hto(e,r,v) =
case v of
  0 -> do_sec(e,entry(r,e),_hto0),
  1 -> do_sec(e,entry(r,e),_hto1)
end,

def bwd_hto(e,r,v) =
case v of
  0 -> do_sec(e,exit(r,e),_hto0),
  1 -> do_sec(e,exit(r,e),_hto1)
end,

/*
 * return the HTO variable of e which encodes traffic coming from n
 */
/*@\label{kr:neighbor-hto}@*/
def neighbor_hto(e,n,v) =
case v of
  0 -> do_sec(e,conn_end(e,n),_hto0),
  1 -> do_sec(e,conn_end(e,n),_hto1)
end,

/*
 * Return the HTO variable of the element e based on either:
 * - the end that neighbor x is connected to e
 * - the direction that route x enters e
 */
/*@\label{kr:hto}@*/
def hto(e,x,v) =
(x isin Route) ? route_entry_hto(e,x,v) : neighbor_hto(e,x,v),

/*
 * An overload of hto(x,e,v), returns HTO variable at version 0
 */
def hto(e,x) =
hto(e,x,0),

/*
 * Return H bit of a HTO variable
 */
/*@\label{kr:h}@*/
def H__(hto) =
(hto >> 2),

/*
 * Return T bit of HTO variable
 */
/*@\label{kr:t}@*/
def _T_(hto) =
((hto & 2) >> 1),

/*
 * Return O bit of HTO variable
 */
/*@\label{kr:o}@*/
def __O(hto) =
(hto & 1),

/*
 * A formula encodes whether a linear section l is vacant
 */
def vacant_linear(l) =
(l.D2U + l.U2D = 0),

/*
 * A formula encodes whether a point section p is vacant
 */
/*@\label{kr:vacant-point}@*/
def vacant_point(p) =
(p.S2PM + p.P2S + p.M2S = 0),

/*
 * A formula encodes whether a section e is vacant
 */
/*@\label{kr:vacant}@*/
def vacant(e) =
(e isin Linear) ? vacant_linear(e) : vacant_point(e),

/*
 * Toggle the H and O bit of a section
 */
/*@\label{kr:head-enters}@*/
def head_enters(hto0,hto1) =
hto1 = (hto0 ^ 5),

/*@\label{kr:head-enters-next}@*/
def head_enters_next(nx,curr) =
let hto0 = hto(nx,curr,0),
    hto1 = hto(nx,curr,1) in
  head_enters(hto0,hto1)
end,

/*
 * Toggle the H bit of a section
 */
/*@\label{kr:head-leaves}@*/
def head_leaves(hto0,hto1) =
hto1 = (hto0 ^ 4),

/*
 * Toggle the T bit of a section
 */
/*@\label{kr:tail-enters}@*/
def tail_enters(hto0,hto1) =
hto1 = (hto0 ^ 2),

/*@\label{kr:tail-enters-next}@*/
def tail_enters_next(nx,curr) =
let hto0 = hto(nx,curr,0),
    hto1 = hto(nx,curr,1) in
  tail_enters(hto0,hto1)
end,

/*
 * Tail leaves
 */
/*@\label{kr:tail-leaves}@*/
def tail_leaves(hto0,hto1) =
hto1 = 0,

/**
 * Swap values of occupancy status variables in a linear section
 */
/*@\label{kr:swap-up-down-vars}@*/
def swap_up_down_vars(l) =
l.D2U' = l.U2D /\ l.U2D' = l.D2U,

/**
 * ==================================
 * Macros for strenthening properties
 * ==================================
 */
/*
 * These macros are used for specifying strengthening invariants
 */
/*
 * Occupied without a tail: 101 001
 */
/*@\label{kr:occupied-without-tail}@*/
def occupied_without_tail(hto) =
(hto & 3) = 1,

/*
 * Occupied without a head: 001 011
 */
/*@\label{kr:occupied-without-head}@*/
def occupied_without_head(hto) =
(hto & 5) = 1,

/*
 * Occupied with a head: 111 101
 */
/*@\label{kr:occupied-with-head}@*/
def occupied_with_head(hto) =
(hto & 5) = 5,

/*
 * Occupied with only the tail: 011
 */
/*@\label{kr:occupied-with-only-tail}@*/
def occupied_with_only_tail(hto) =
hto = 3,

/*
 * If trains can change direction at a section
 */
/*@\label{kr:can-turn-around-at}@*/
def can_turn_around_at(e) =
(e isin Linear) /\ down_sig(e) /\ up_sig(e),

/* Apply function f to HTO variables (in the same direction as r's) of elements
 * in the path of r, start from the last section toward the first section,
 * until a point which has different position than required by r is met
 */
def count_fwd_bit(r,f) =
count_fwd_bit(r,last(r),f),

/*
 * Apply function f to HTO variables (in the same direction as r's) of elements
 * in the path of r, start from e toward the first section, until a point which
 * has different position than required by r is met
 */
def count_fwd_bit(r,e,f) =
let fst = first(r) in
  if (e isin Linear)
  then
    (e = fst) ? f(hto(e,r,0)) : (f(hto(e,r,0)) + count_fwd_bit(r,prev(r,e),f))
  else
    (e.POS = req(r,e)) /\
    ((e = fst) ? f(hto(e,r,0))
     : (f(hto(e,r,0)) + count_fwd_bit(r,prev(r,e),f)))
  end
end,

/*
 * Apply function f to HTO variables (in the opposite direction of r's) of
 * elements in the path of r, start from the last section toward the first
 * section, until a point which has different position than required by r is
 * met
 */
def count_bwd_bit(r,f) =
count_bwd_bit(r,last(r),f),

/*
 * Apply function f to HTO variables (in the opposite direction of r's) of
 * elements in the path of r, start from e toward the first section, until a
 * point which has different position than required by r is met
 */
def count_bwd_bit(r,e,f) =
let fst = first(r) in
  if (e isin Linear)
  then
    let val = (entry(r,e) = DOWN) ? f(e.U2D) : f(e.D2U) in
      (e = fst) ? val : (val + count_bwd_bit(r,prev(r,e),f))
    end
  else
    (e.POS = req(r,e)) /\
    let val = (entry(r,e) ~= STEM) ? f(e.S2PM)
              : ((req(r,e) = PLUS) ? f(e.P2S) : f(e.M2S)) in
      (e = fst) ? val : (val + count_bwd_bit(r,prev(r,e),f))
    end
  end
end,

/*
 * Search backward from e for a point
 */
def check_point(r,e) =
let fst = first(r) in
  if (e = fst)
  then
    e
  else
    let pv = prev(r,e) in
      (pv isin Point) ? e : check_point(r,pv)
    end
  end
end,

/*
 * This formula ensures each chunk of linear sections between two points of a
 * route only is occupied in one direction at a time
 */
def linear_chunk_cnd(r,e) =
let fst = first(r),
    cp = check_point(r,e) in
  ((cp = e) ? 1
   : (count_chunk_fwd_bit(r,e,cp,__O) * count_chunk_bwd_bit(r,e,cp,__O) =
      0)) /\ ((cp ~= fst) => linear_chunk_cnd(r,prev(r,cp)))
end,

/*
 * Apply function f to HTO variables (in the same direction of r's) of elements
 * in the path of r, start from e toward stop
 */
def count_chunk_fwd_bit(r,e,stop,f) =
(e = stop) ? f(hto(e,r,0))
: (f(hto(e,r,0)) + count_chunk_fwd_bit(r,prev(r,e),stop,f)),

/*
 * Apply function f to HTO variables (in the opposite direction of r's) of
 * elements in the path of r, start from e toward stop
 */
def count_chunk_bwd_bit(r,e,stop,f) =
if (e isin Linear)
then
  let val = (entry(r,e) = DOWN) ? f(e.U2D) : f(e.D2U) in
    (e = stop) ? val : (val + count_chunk_bwd_bit(r,prev(r,e),stop,f))
  end
else
  let val = (entry(r,e) ~= STEM) ? f(e.S2PM)
            : ((req(r,e) = PLUS) ? f(e.P2S) : f(e.M2S)) in
    (e = stop) ? val : (val + count_chunk_bwd_bit(r,prev(r,e),stop,f))
  end
end,

/*
 * Count O bit of forward HTO variables
 */
def count_fwd___O(r) =
count_fwd_bit(r,__O),

/* check if e is a boundary section */
def is_boundary_sec(e) =
(is_boundary_sec_down(e) \/ is_boundary_sec_up(e)),

/* check if e is a boundary section in the downward direction */
/*@\label{kr:is-boundary-sec-down}@*/
def is_boundary_sec_down(e) =
(e isin Linear) /\ ~down(e) /\ up_sig(e) /\ ~down_sig(e) /\
let us = up(e) in
  (us isin Linear) /\ down_sig(us)
end,

/* check if e is a boundary section in the upward direction */
/*@\label{kr:is-boundary-sec-up}@*/
def is_boundary_sec_up(e) =
(e isin Linear) /\ ~up(e) /\ down_sig(e) /\ ~up_sig(e) /\
let ds = down(e) in
  (ds isin Linear) /\ up_sig(ds)
end

end