(************************************************************
 *                      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