-----------------------------------------------------------------------------
-- COMP424-06A - U-Turn Section
-----------------------------------------------------------------------------
-- At an underground terminus, there is a special U-turn section to let
-- trains change tracks and return in the opposite direction. The U-turn
-- section consists of three track sections, A, B, and C, connected by a
-- switch. Trains enter from A and leave via C. In order to transfer
-- safely, they must wait for the switch to connect A and B, proceed to B,
-- and wait once more for the switch to connect B and C before leaving.
--
-- The U-turn section is controlled by an automated underground
-- management system (UMS). The UMS uses sensors detect_A, detect_B, and
-- detect_C to detect the presence of a train on each track section.
-- Trains are controlled by light signals grant_access and grant_exit at
-- sections A and B, respectively. The switch is driven by a signal
-- switch_toggle which causes it to shift from one state to the other.
-- 
-- Since several trains may be involved, collisions are possible and have to
-- be avoided. Furthermore, the switch is unsafe, so trains may derail when
-- crossing it while it is changing its position, or when travelling from 
-- A and B with the switch in the wrong position.
-----------------------------------------------------------------------------


-----------------------------------------------------------------------------
-- Plant model of a railway switch
-----------------------------------------------------------------------------
-- Inputs:
--   toggle - set to true to change the switch state
-----------------------------------------------------------------------------
-- Internal:
--   state  - the position of the switch:
--              straight = the switch connects tracks A and B
--              curved   = the switch connects tracks B and C
-----------------------------------------------------------------------------
-- When the actuator toggle is set, the switch will change to the other
-- position in the next step. When this happens, it is considered unsafe,
-- and trains travelling on the switch while toggle is set may derail.
-- This is not checked by the switch---it is the responsibility of the
-- controller to avoid this condition.
-----------------------------------------------------------------------------

MODULE switch(toggle)

VAR
  state:       {straight, curved};

ASSIGN
  init(state) := straight;
  next(state) := case
    !toggle:                   state;
    toggle & state = straight: curved;
    toggle & state = curved:   straight;
  esac;


-----------------------------------------------------------------------------
-- Plant model of a train
-----------------------------------------------------------------------------
-- Inputs:
--   grant_access - true if the signal allows trains to exit section A
--                  towards section B.
--   grant_exit   - true if the signal allows trains to exit from section B.
--   switch_state - state state of the switch that connects the track
--                  sections A, B, and C; it is either straight or curved.
--   ok_to_enter  - an internal flag to model the assumption that only one
--                  train enters track section A at a time;
--                  trains will only enter if this is true.
-----------------------------------------------------------------------------
-- Internal:
--   pos          - the position of the train:
--                    travelling = this train is outside of the U-turn section.
--                    on_A =       this train is completely and safely on track
--                                 section A.
--                    on_B =       this train is completely and safely on track
--                                 section B.
--                    on_C =       this train is completely and safely on track
--                                 section C.
--                    transit_AB = this train is moving from track section A
--                                 towards track section B.
--                    transit_BA = this train is moving from track section B
--                                 towards track section A.
--                    transit_BC = this train is moving from track section B
--                                 towards track section C.
--   slow         - a boolean flag used to model that the speed of
--                  trains is unpredictable.
--                  The slow flag changes its value at random,
--                  and the train will only move if it is false.
-----------------------------------------------------------------------------
-- Trains take some unpredictable amount of time to cross the switch and
-- transfer from one track section to another. This is modelled by the
-- states transit_AB, transit_BA, and transit_BC. While in transit, trains
-- may partially occupy the origin and destination track sections, so it
-- needs to be ensured that no other trains are there. Again,
-- this is the responsibility of the controller and not checked in the
-- train module.
-- The number of steps spent in transit is not determined. It changes
-- randomly depending on the slow variable. The only guarantee is that
-- the train will eventually reach its destination.
-----------------------------------------------------------------------------

MODULE train(grant_access, grant_exit, switch_state, ok_to_enter)

VAR
  pos:         {travelling,
	        on_A, on_B, on_C,
                transit_AB, transit_BA, transit_BC};
  slow:        boolean;

DEFINE
  -- Auxiliary flags: this train may partially occupy a track section.
  near_A := pos = on_A | pos = transit_AB | pos = transit_BA;
  near_B := pos = on_B | pos = transit_AB | pos = transit_BA |
            pos = transit_BC;
  near_C := pos = on_C | pos = transit_BC;

ASSIGN
  -- This is the model of train movement:
  init(pos) := travelling;
  next(pos) := case
    -- do not move if slow ...
    slow:                                                   pos;
    -- if travelling, only enter when ok_to_enter is set ...
    pos = travelling & !ok_to_enter:                        travelling;
    pos = travelling & ok_to_enter:                         {travelling, on_A};
    -- transfer from A to B ...
    pos = on_A & !grant_access:                             on_A;
    pos = on_A & grant_access & switch_state = straight:    transit_AB;
    pos = transit_AB & switch_state = straight:             on_B;
    -- transfer from B to A or C depending on switch ...
    pos = on_B & !grant_exit:                               on_B;
    pos = on_B & grant_exit & switch_state = straight:      transit_BA;
    pos = on_B & grant_exit & switch_state = curved:        transit_BC;
    pos = transit_BA & switch_state = straight:             on_A;
    pos = transit_BC & switch_state = curved:               on_C;
    -- leave from C ...
    pos = on_C:                                             travelling;
    -- chaos in all other cases ...
    1:     {travelling, on_A, on_B, on_C, transit_AB, transit_BA, transit_BC};
  esac;

JUSTICE
  -- Fairness assumption: slow will not be true all the time.
  !slow

-- Every train that enters track section A evetually reaches C.
SPEC
  AG (pos = on_A -> A [pos != travelling U pos = on_C])

-- Some consistency checks:
-- Trains always can enter track section A.
SPEC
  AG EF pos = on_A

-- Trains can always get back to the travelling state.
SPEC
  AG EF pos = travelling


-----------------------------------------------------------------------------
-- Plant model
-----------------------------------------------------------------------------
-- This models the complete U-turn section consisting of the switch,
-- the two signals, and two trains.
-----------------------------------------------------------------------------
-- Actuators:
--   switch_toggle - set to true to change the state of the switch;
--                   when it is set, the switch will change to the
--                   opposite state.
--   grant_access  - true if the signal allows trains to exit section A
--                   towards section B.
--   grant_exit    - true if the signal allows trains to exit from section B.
-----------------------------------------------------------------------------
-- Sensors:
--   detect_A      - there is a train safely positioned on track section A.
--   detect_B      - there is a train safely positioned on track section B.
--   detect_C      - there is a train safely positioned on track section C.
-- NOTE:
--   Trains take some time to cross the switch and transfer between different
--   track sections, and during this time may still partially occupy the
--   track sections of their origin and destination. The sensors detect_A,
--   etc., are only set if a train is positioned completely and safely on
--   the corresponding track section.
-----------------------------------------------------------------------------
-- Internal:
--   entering_1    - train 1 may enter track section A
--   entering_2    - train 2 may enter track section A
-- NOTE:
--   These variables CANNOT be accessed by the controller.
-----------------------------------------------------------------------------

MODULE uturn_section(grant_access, grant_exit, switch_toggle)

VAR
  entering_1:  boolean;
  entering_2:  boolean;

  switch_ABC:  switch(switch_toggle);
  train_1:     train(grant_access, grant_exit, switch_ABC.state, entering_1);
  train_2:     train(grant_access, grant_exit, switch_ABC.state, entering_2);

DEFINE
  -- Definition of the sensors.
  -- detect_A, e.g., is only signalled if a train has safely reached track
  -- section A and does not occupy parts of any other track section.
  detect_A := train_1.pos = on_A | train_2.pos = on_A;
  detect_B := train_1.pos = on_B | train_2.pos = on_B;
  detect_C := train_1.pos = on_C | train_2.pos = on_C;

  -- Auxiliary flags: there may be a train partially occupying a track section.
  near_A := train_1.near_A | train_2.near_A;
  near_B := train_1.near_B | train_2.near_B;
  near_C := train_1.near_C | train_2.near_C;

ASSIGN
  -- The model of the assumption that only one train enters the U-turn section
  -- section at a time. The two flags entering_1 and entering_2 will only be
  -- true if there is no train that partially occupies track section A,
  -- and only one of these flags can be true at a time. The train module uses
  -- these flags to make sure that trains only enter the U-turn section
  -- when their entering flag is set.
  entering_1 := case
    !near_A:     {0, 1};
    1:           0;
  esac;
  entering_2 := case
    entering_1:  0;
    !near_A:     {0, 1};
    1:           0;
  esac;


-- No collisions.
SPEC
  AG (train_1.near_A + train_2.near_A <= 1)
SPEC
  AG (train_1.near_B + train_2.near_B <= 1)
SPEC
  AG (train_1.near_C + train_2.near_C <= 1)

-- No derailments I:
-- the switch is not operated when trains may be crossing it.
SPEC
  AG (train_1.pos = transit_AB | train_2.pos = transit_AB -> !switch_toggle)
SPEC
  AG (train_1.pos = transit_BA | train_2.pos = transit_BA -> !switch_toggle)
SPEC
  AG (train_1.pos = transit_BC | train_2.pos = transit_BC -> !switch_toggle)
SPEC
  AG ((train_1.pos = on_A | train_2.pos = on_A) & grant_access ->
         !switch_toggle)
SPEC
  AG ((train_1.pos = on_B | train_2.pos = on_B) & grant_exit ->
         !switch_toggle)

-- No derailments II:
-- the switch connects A and B when a train is entering from A.
SPEC
  AG (train_1.pos = transit_AB | train_2.pos = transit_AB ->
      switch_ABC.state = straight)
SPEC
  AG ((train_1.pos = on_A | train_2.pos = on_A) & grant_access ->
         switch_ABC.state = straight)


-----------------------------------------------------------------------------
-- UMS --- the control program for U-turn section
-----------------------------------------------------------------------------
-- Inputs:
--   detect_A      - there is a train safely positioned on track section A.
--   detect_B      - there is a train safely positioned on track section B.
--   detect_C      - there is a train safely positioned on track section C.
-- Outputs:
--   switch_toggle - set to true to change the state of the switch;
--                   when it is set, the switch will change to the
--                   opposite state.
--   grant_access  - true if the signal allows trains to exit section A
--                   towards section B.
--   grant_exit    - true if the signal allows trains to exit from section B.
-----------------------------------------------------------------------------
-- Internal:
--   estimated_switch_state - the controller's estimate of the switch state.
--                     AB = the switch connects tracks A and B.
--                     BC = the switch connects tracks B and C.
--                   Since the plant does not provide a sensor to report
--                   the state of the switch, the controller uses this
--                   internal variable to calculate the switch state based
--                   on the known initial state (A and B connected) and
--                   the number of switch_toggle signals sent.
--   transit - the controller's estimate of whether a train is crossing the
--                   switch.
--                     AB = a train is crossing from section A to B.
--                     BC = a train is crossing from section B to C.
--                     none = no train on the switch.
--   prev_grant_access, prev_grant_exit, prev_transit - the values of
--                   the indicated variables in the previous state.
-----------------------------------------------------------------------------

MODULE ums(detect_A, detect_B, detect_C)

VAR
  switch_toggle:                                  boolean;
  grant_access:                                   boolean;
  grant_exit:                                     boolean;

VAR
  estimated_switch_state:                         {AB, BC};

  prev_grant_access:                              boolean;
  prev_grant_exit:                                boolean;
  prev_transit:                                   {AB, BC, none};

DEFINE
  transit := case
    prev_transit = AB & detect_B:                 none;
    prev_transit = BC & detect_C:                 none;
    prev_grant_access & !detect_A:                AB;
    prev_grant_exit & !detect_B:                  BC;
    1:                                            prev_transit;
  esac;

ASSIGN
  init(estimated_switch_state) := AB;
  next(estimated_switch_state) := case
    estimated_switch_state = AB & switch_toggle:  BC;
    estimated_switch_state = BC & switch_toggle:  AB;
    1:                                            estimated_switch_state;
  esac;

  init(prev_grant_access) := 0;
  next(prev_grant_access) := grant_access;
  init(prev_grant_exit) := 0;
  next(prev_grant_exit) := grant_exit;
  init(prev_transit) := none;
  next(prev_transit) := transit;

  switch_toggle := case
    transit != none:                              0;
    detect_B:                                     estimated_switch_state = AB;
    1:                                            estimated_switch_state = BC;
  esac;

  grant_access := 
    transit = none & detect_A & !detect_B & estimated_switch_state = AB;

  grant_exit := 
    transit = none & detect_B & !detect_C & estimated_switch_state = BC;


-----------------------------------------------------------------------------
-- Putting it all together
-----------------------------------------------------------------------------
-- The obligatory main module to link the plant and controller.
-----------------------------------------------------------------------------

MODULE main

VAR
  plant:       uturn_section(controller.grant_access,
			     controller.grant_exit,
		 	     controller.switch_toggle);
  controller:  ums(plant.detect_A, plant.detect_B, plant.detect_C);


-- Some consistency checks:
-- The controller estimates the switch state correctly.
SPEC
  AG (plant.switch_ABC.state = straight <->
      controller.estimated_switch_state = AB)

-- The controller correctly predicts that a train is crossing the switch.
SPEC
  AG ((plant.train_1.pos = transit_AB | plant.train_2.pos = transit_AB) <->
      controller.transit = AB)
SPEC
  AG ((plant.train_1.pos = transit_BC | plant.train_2.pos = transit_BC) <->
      controller.transit = BC)