(******************************************************************************* * IMITATOR MODEL * * Title : TrainAHV93 * Description : Classical Railroad Gate Controller * Correctness : "Whenever the train is inside the gate, the gate should be closed" * Scalable : * Generated : * Categories : Academic * Source : Model described in "Parametric Real-Time Reasoning" (fig. 2); Alur, Henzinger, Vardi (STOC 1993) * bibkey : AHV93 * Author : Alur, Henzinger, Vardi * Modeling : Alur, Henzinger, Vardi * Input by : Étienne André * License : * * Created : 2011/11/25 * Last modified : 2020/08/19 * Model version : * * IMITATOR version : 3 ******************************************************************************) 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 ; (************************************************************) (* The end *) (************************************************************) end