--------------------------------------------------------------------------------
--
--  'Railroad Crossing' from Henzinger's HyTech Suite.
--
--  Author : Christian Herde
--
--  Last Modified :
--              Tue Nov 29 11:22:05 CET 2005
--
--------------------------------------------------------------------------------


DECL
    -- Global definitions and declarations.
    boole jump;                     -- true iff system engages in a global jump
    boole app, exit, lower, raise;  -- syncronisation labels (local variables)
    float [0.0, 1000.0] dt;         -- duration of a flow

    -- Declarations for TRAIN automaton.
    float [-5000.0, 5000.0] x;      -- position of the train
    boole far, near, past;

    -- Declarations for CONTROLLER automaton.
    define alpha = 9.8;             -- time delay of controller
    float [0.0, 1000.0] t;          -- timer of controller automaton
    boole idle, about_to_lower, about_to_raise;

    -- Declarations for GATE automaton.
    float [0, 90] g;                -- angle of gate
    boole open, closed, raising, lowering;


INIT
    -- Start with a flow.
    !jump;

    -- Initial state of TRAIN automaton.
    far and !near and !past;
    x >= 2000.0;

    -- Initial state of TRAIN automaton.
    idle and !about_to_lower and !about_to_raise;
    t = 0.0;

    -- Initial state of GATE automaton.
    open and !closed and !lowering and !raising;
    g = 90.0;


TRANS
    -- Global stuff.
     jump <-> !jump';
     jump -> dt = 0.0;
    !jump -> dt > 0.0;


    -- TRAIN automaton.
    --   Jumps
    (jump and app and far) -> near';
    (jump and far and near') ->
        (app
        and !exit  -- CONTROLLER must not do exit transition
        and x = 1000.0 and x' = 1000.0);

    (jump and near and past') ->
        (!app
        and !exit -- CONTROLLER must not do app or exit transition
        and x = 0.0 and x' = 0.0);

    (jump and exit and past) -> far';
    (jump and past and far') ->
        (exit
        and !app  -- CONTROLLER must not do app transition
        and x = 100.0 and x' >= 2000);

    --  Stutter jumps.
    (jump and far and far') ->
        (!app and !exit -- A stutter jump must not be misused by another
                        -- component to do a 'synchronous' transition.
        and x' = x);

    (jump and near and near') ->
        (!app and !exit
        and x' = x);

    (jump and past and past') ->
        (!app and !exit
        and x' = x);

    --  Flows
    (!jump and far) ->
        (far' and x - 50.0 * dt <= x' and x' <= x - 40.0 and x' >= 1000.0);

    (!jump and near) ->
        (near' and x - 50.0 * dt <= x' and x' <= x - 30.0 and x' >= 0.0);

    (!jump and past) ->
        (past' and x + 30.0 * dt <= x' and x' <= x + 50.0 and x' <= 100.0);

    -- Exclude unwanted transitions.
    far -> (far' or near');
    near -> (near' or past');
    past -> (past' or far');

    -- Exactly in one location.
    far' + near' + past' = 1;


    -- CONTROLLER automaton.
    --  Jumps
    (jump and idle and idle') -> --stutter jump
        (!app and !exit and !raise and !lower
        and t' = t);

    (jump and app and idle) -> about_to_lower';
    (jump and idle and about_to_lower') ->
        (app
        and !exit               -- CONTROLLER must not do exit transition
        and !raise and !lower   -- GATE must not do raise or lower transition
        and t' = 0.0);

    (jump and lower and about_to_lower) -> idle';
    (jump and about_to_lower and idle') ->
        (lower
        and !raise              -- GATE must not do raise transition
        and !app and !exit      -- CONTROLLER must not do app or exit transition
        and t' = t);

    (jump and exit and idle) -> about_to_raise';
    (jump and idle and about_to_raise') ->
        (exit
        and !app
        and !raise and !lower
        and t' = 0.0);

    (jump and raise and about_to_raise) -> idle';
    (jump and about_to_raise and idle') ->
        (raise
        and !lower
        and !app and !exit
        and t' = t);

    (jump and app and about_to_lower) -> about_to_lower';
    (jump and about_to_lower and about_to_lower') ->
        [(app
          and !exit
          and !raise and !lower
          and t' = t)
        or -- stutter jump
         (!app and !exit and !raise and !lower
         and t' = t)
        ];

    (jump and exit and about_to_raise) -> about_to_raise';
    (jump and about_to_raise and about_to_raise') ->
        [(exit
          and !app
          and !raise and !lower
          and t' = t)
        or -- stutter jump
         (!app and !exit and !raise and !lower
         and t' = t)
        ];

    (jump and exit and about_to_lower) -> about_to_raise';
    (jump and about_to_lower and about_to_raise') ->
        (exit
        and !app
        and !raise and !lower
        and t' = 0.0);

    (jump and app and about_to_raise) -> about_to_lower';
    (jump and about_to_raise and about_to_lower') ->
        (app
        and !exit
        and !raise and !lower
        and t' = 0.0);

    --  Flows
    (!jump and idle) ->
        (idle' and t' = t);

    (!jump and about_to_lower) ->
        (about_to_lower' and t' = t + dt and t' <= alpha);

    (!jump and about_to_raise) ->
        (about_to_raise' and t' = t + dt and t' <= alpha);

    -- Exclude unwanted transitions.
    -- (empty)

    -- Exactly in one location.
    idle' + about_to_lower' + about_to_raise' = 1;


    -- GATE automaton
    --   Jumps
    (jump and lower and open) -> lowering';
    (jump and open and lowering') ->
        (lower
        and !raise  -- CONTROLLER must not do raise transition
        and g' = 90.0);

    (jump and raise and open) -> open';
    (jump and open and open') ->
        [(raise
          and !lower
          and g' = 90.0)
        or  -- stutter jump
         (!raise and !lower
          and g' = 90.0)
        ];

    (jump and raise and closed) -> raising';
    (jump and closed and raising') ->
        (raise
        and !lower
        and g' = 0.0);

    (jump and lower and closed) -> closed';
    (jump and closed and closed') ->
        [(lower
          and !raise
          and g' = 0.0)
        or -- stutter jump
         (!raise and !lower
          and g' = 90.0)
        ];

    (jump and raise and raising) -> raising';
    (jump and raising and raising') ->
        [(raise
          and !lower
          and g' = g)
        or -- stutter jump
         (!raise and !lower
         and g' = g)
        ];

    (jump and raising and open') ->
        (g = 90.0 and g' = 90.0);

    (jump and lower and raising) -> lowering';
    (jump and raising and lowering') ->
        (lower
        and !raise
        and g' = g);

    (jump and lower and lowering) -> lowering';
    (jump and lowering and lowering') ->
        [(lower
          and !raise
          and g' = g)
        or -- stutter jump
          (!raise and !lower
          and g' = g)
        ];

    (jump and lowering and closed') ->
        (g = 0.0 and g' = 0.0);

    (jump and raise and lowering) -> raising';
    (jump and lowering and raising') ->
        (raise
        and !lower
        and g' = g);

    --  Flows
    (!jump and open) ->
        (open' and g' = 90.0);

    (!jump and closed) ->
        (closed' and g' = 0.0);

    (!jump and raising) ->
        (raising' and g' = g + 9.0 * dt);

    (!jump and lowering) ->
        (lowering' and g' = g - 9.0 * dt);

    -- Exclude unwanted transitions.
    open -> (open' or lowering');
    closed -> (closed' or raising');
    raising -> (raising' or open' or lowering');
    lowering -> (lowering' or closed' or raising');

    -- Exactly in one location.
    open' + closed' + raising' + lowering' = 1;


TARGET
    -- We are looking for a violation of the following property: "When
    -- the train is within 10 meters to the gate, the gate is always
    -- fully closed." Violations are possible for alpha >= 49/5 = 9.8.
    -- Trace has length 5.
    near and x <= 10.0 and !closed;