90 lines
2.6 KiB
Plaintext
90 lines
2.6 KiB
Plaintext
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); |