--------------------------------------------------------------------------------
--
--  A railway crossing example
--
--  Author(s) : Willem Hagemann
--
--
--  fomc --flowpipe --noonion 
--       --configStringFlowpipe "max_steps=50000; step_width=1/30; \
--	 			 result_denominator=4096;"
--       --configStringFomc "flowpipeGCPreimage=false;"
--
-- This model was checked for different disturbtions
--------------------------------------------------------------------------------

DECL

    <stable> bool flow </stable>;

    -- state of drive
    <mode> [0,3] int d_mode </mode>;
    const [0,3] int braking = 0; 
    const [0,3] int normal = 1;
    const [0,3] int accel = 2;
    const [0,3] int emergency = 3; 
    
    -- phases of operation
    <mode> [0,4] int phases</mode>;
    const [0,4] int far = 0;
    const [0,4] int requesting = 1;
    const [0,4] int negotiation = 2;
    const [0,4] int correcting = 3;
    const [0,4] int passed = 4;
 
    -- desired velocity
    const real v_desired = 30.0;

    -- borders for the normal drive-mode
    const real v_max_normal = 45.0;
    const real v_min_normal = 20.0;

    -- borders for the braking drive-mode
    const real v_min_braking = 42.0;

    -- borders for the accel drive-mode
    const real v_max_accel = 22.0;

    -- Points of phase change
    const real ActivatedPoint = 400.0;			//activation point
    const real AcknowledgePoint = 450.0;		//receive acknowledge
    const real BrakingPoint = ActivatedPoint + 400.0; 	//braking point
    const real EOA = ActivatedPoint + 770.0;		//control point

    -- train length
    const real TL = 90.0;

    -- Global constraints for position and velocity
    [0.0, 60.0] real v;
    [0.0, EOA + 100.0] real p;

    -- EoA 
    
    bool newEoa;
    input bool i_newEoa;

    bool EoaFailure;
    
    -- Xing

    bool isXing;
    input bool i_isXing;

    bool XingAck;
    input bool i_XingAck;

    bool XingSafe;
    input bool i_XingSafe;

    bool XingReqLock;

    bool XingFailure;

    bool failure;
   
INIT
    
    EoaFailure = false;
    XingFailure = false;
    XingReqLock = false;
    failure = false;

    flow = true;

    p = TL;
    phases = far;

       (d_mode = normal and v >= v_min_normal and v <= v_max_normal)
    or (d_mode = accel and v >= 0.0 and v <= v_max_accel)
    or (d_mode = braking and v >= v_min_braking and v <= 50.0);

INVAR


JUMP

---DRIVE -----------------------------------

-- exits
  
  <c2d> d_mode = braking and v <= v_min_braking
  	-> flow' = false </c2d>;
  <c2d> d_mode = normal and v >= v_max_normal
  	-> flow' = false </c2d>;
  <c2d> d_mode = normal and v <= v_min_normal
  	-> flow' = false </c2d>;
  <c2d> d_mode = accel and v >= v_max_accel
  	-> flow' = false </c2d>;

-- entries

  <d2c> !(d_mode = emergency) and v >= v_max_normal
    	-> d_mode' = braking </d2c>;
  <d2c> !(d_mode = emergency) and v < v_max_normal and v > v_min_normal
   	-> d_mode' = normal </d2c>;
  <d2c> !(d_mode = emergency) and v <= v_min_normal
    	-> d_mode' = accel </d2c>;
  <d2c> d_mode = emergency
  	-> flow' = true </d2c>;


--- PHASE CTRL -----------------------------------


-- exits

  <c2d> phases = far and p >= ActivatedPoint
  	->  flow' = false and 
	    isXing' = i_isXing </c2d>;
  <c2d> phases = requesting and p >= AcknowledgePoint
  	->  flow' = false and
	    XingAck' = i_XingAck </c2d>;
  <c2d> phases = negotiation and p >= BrakingPoint
  	-> flow' = false and 
	   newEoa' = i_newEoa and
	   XingSafe' = i_XingSafe </c2d>;
  <c2d> phases = correcting and p >= EOA + TL
  	-> flow' = false </c2d>;

-- entries

  <d2c> !(phases = far) and p < ActivatedPoint 
      -> phases' = far </d2c>;
  <d2c> !(phases = requesting) and p >= ActivatedPoint and p < AcknowledgePoint
      -> phases' = requesting </d2c>;
  <d2c> !(phases = negotiation) and p >= AcknowledgePoint and p < BrakingPoint
      -> phases' = negotiation </d2c>;
  <d2c> !(phases = correcting) and p >= BrakingPoint and p < EOA + TL
      -> phases' = correcting </d2c>;
  <d2c> !(phases = passed) and p >= EOA + TL
      -> phases' = passed </d2c>;

  
-- XING PROTOCOL 

  <d> isXing and !XingReqLock 
      -> XingReqLock' = true </d>;
  <d> XingReqLock and p = AcknowledgePoint and !XingAck and !XingFailure 
      -> XingFailure' = true </d>;
  <d> isXing and p = BrakingPoint and !XingSafe and !XingFailure 
      -> XingFailure' = true </d>;


-- EOA PROTOCOL
  <d> p = BrakingPoint and !newEoa and !EoaFailure 
      -> EoaFailure' = true </d>;

-- ERROR CTRL
  <d> failure and !EoaFailure and !XingFailure 
      -> failure' = false </d>;
  <d> !failure and EoaFailure 
      -> failure' = true </d>;
  <d> !failure and XingFailure 
      -> failure' = true </d>;

  <d> !(d_mode = emergency) and failure
      -> d_mode' = emergency </d>;


FLOW
    d_mode = braking ->
    	   d/dt(v) = <disturb max = "0.001"> 
	   	       -1.5
		     </disturb>
       and d/dt(p) = v;

    d_mode = normal ->
    	   d/dt(v) = <disturb max = "0.001">
		       0.1*v_desired - 0.1*v
		     </disturb>
       and d/dt(p) = v;

    d_mode = accel ->
    	   d/dt(v) = <disturb max = "0.001"> 
	   	       1.0
		    </disturb>    	   
       and d/dt(p) = v;

    d_mode = emergency ->
           d/dt(v) = <disturb max = "0.1">  //0.1 is safe, 0.3 unsafe
		       -3.0
		     </disturb> 
       and d/dt(p) = v;

TARGET
-- MAIN TARGETS
     (d_mode = emergency) -> p <= EOA;  				//(1)
//    (d_mode = emergency or p <= EOA);					//(2)

//(1) safe: in case of emergency the train stops before end of authority
//(2) unsafe: in case of no emergency the train passes position EOA