MODULE train(signal)
    -- Model of the train
    VAR
        mode : {away, wait, bridge};
        out : {none, arrive, leave};
    ASSIGN
        init(mode) := away;
        out := case
            mode = away     : {none, arrive};
            mode = bridge   : {none, leave};
            TRUE            : none;
        esac;
        next(mode) := case
            mode = away & out = arrive      : wait;
            mode = wait & signal = green    : bridge;
            mode = bridge & out = leave     : away;
            TRUE                            : mode;
        esac;

MODULE controller(out_w, out_e)
    -- First model of the controller
    VAR
        west    : {green, red};
        east    : {green, red};
        nearw   : {0, 1};
        neare   : {0, 1};
    ASSIGN
        init(west)  := red;
        init(east)  := red;
        init(nearw) := 0;
        init(neare) := 0;
        
        next(neare) := case
            out_e = arrive  : 1;
            out_e = leave   : 0;
            TRUE            : neare;
        esac;

        next(nearw) := case
            out_w = arrive  : 1;
            out_w = leave   : 0;    
            TRUE            : nearw;
        esac;
        
        next(east) := case
            neare = 0                              : red;
            neare = 1 & west = red                 : green;
            TRUE                                   : east;
        esac;
        
        next(west) := case
            nearw = 0                               : red;
            nearw = 1 & east = red & neare != 1     : green;
            TRUE                                    : west;
        esac;
    DEFINE
        signal_w := west;
        signal_e := east;


-- to test
MODULE WestTrainMonitor(out_w, out_e, signal_w)
    VAR 
        state : {0,1,2,3};
    ASSIGN
        init(state) := 0;
        next(state) := case
            state = 0 & out_w = arrive : 1;
            -- state = 0 : 0;
            state = 1 & signal_w != green & out_e = leave : 2;
            state = 1 & signal_w = green : 0;
            -- state = 1 : 1;
            state = 2 & signal_w != green & out_e = leave : 3;
            state = 2 & signal_w = green : 0;
            -- state = 2 : 2;
            -- state = 3 : 3;
            TRUE : state;
        esac;


MODULE main
    -- Composition of train_W, train_E and controller
    VAR
        train_w : train(contr.signal_w);
        train_e : train(contr.signal_e);
        contr   : controller(train_w.out, train_e.out);
        wtm     : WestTrainMonitor(train_w.out, train_e.out, contr.signal_w);
        
INVARSPEC !(train_w.mode = bridge & train_e.mode = bridge);
INVARSPEC !(wtm.state = 3);