(************************************************************ * IMITATOR MODEL * * Railroad Gate Controller * * Description : Classical Railroad Gate Controller * Correctness : "Whenever the train is inside the gate, the gate should be closed" * Source : Model described in "Parametric Real-Time Reasoning" (fig. 2); Alur, Henzinger, Vardi (STOC 1993) * Author : Alur, Henzinger, Vardi * Modeling : Alur, Henzinger, Vardi * Input by : Etienne Andre * * Created : 2011/11/25 * Last modified : 2015/07/31 * * IMITATOR version: 2.7.2 ************************************************************) var x, y, z : clock; a, b, c, d, e, f : parameter; (************************************************************) automaton train (************************************************************) synclabs: approach, inn, out, exit; loc train0: invariant True when True sync approach do {x := 0} goto train1; loc train1: invariant True when x > a sync inn goto train2; loc train2: invariant True when True sync out goto train3; loc train3: invariant True when x < b sync exit goto train0; end (*train*) (************************************************************) automaton gate (************************************************************) synclabs: lower, up, down, raise; (* Gate is open *) loc gate0: invariant True when True sync lower do {y := 0} goto gate1; loc gate1: invariant True when c < y & y < d sync down goto gate2; (* Gate is closed *) loc gate2: invariant True when True sync raise do {y := 0} goto gate3; loc gate3: invariant True when c < y & y < d sync up goto gate0; end (*gate*) (************************************************************) automaton controller (************************************************************) synclabs: approach, lower, exit, raise; loc controller0: invariant True when True sync approach do {z := 0} goto controller1; loc controller1: invariant True when e < z & z < f sync lower goto controller2; loc controller2: invariant True when True sync exit do {z := 0} goto controller3; loc controller3: invariant True when e < z & z < f sync raise goto controller0; end (*controller*) (************************************************************) (* Initial state *) (************************************************************) init := (*------------------------------------------------------------*) (* Initial location *) (*------------------------------------------------------------*) & loc[train] = train0 & loc[gate] = gate0 & loc[controller] = controller0 (*------------------------------------------------------------*) (* Initial clock constraints *) (*------------------------------------------------------------*) & x >= 0 & y >= 0 & z >= 0 (*------------------------------------------------------------*) (* Parameter constraints *) (*------------------------------------------------------------*) & a >= 0 & a <= b & c >= 0 & c <= d & e >= 0 & e <= f ; (************************************************************) (* Property specification *) (************************************************************) property := unreachable (* IMITATOR still misses the "<>", hence we need to enumerate other locations of gate *) loc[train] = train2 & loc[gate] = gate0 or loc[train] = train2 & loc[gate] = gate1 or loc[train] = train2 & loc[gate] = gate3 ; (************************************************************) (* The end *) (************************************************************) end