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