(************************************************************
 *                      IMITATOR MODEL                      
 *
 * Railroad Gate Controller
 *
 * Description     : Simple model with 1 PTA only
 * Correctness     : "Crash" cannot happen
 * Source          : Own work
 * Author          : Étienne André
 * Modeling        : Étienne André
 * Input by        : Étienne André
 *
 * Created         : 2012/03/13
 * Last modified   : 2017/06/29
 *
 * IMITATOR version: 2.9
 ************************************************************)

var

(* Clocks *)
 	x, y
		: clock;

(* Parameters *)
	dApproach,  (* Time between the approach and the passing *)
	dStartDown, (* Time between the approach and the gate starting to go down *)
	dGetDown,   (* Time between the gate starts to lower, and the gate is closed *)
		: parameter;



(************************************************************)
  automaton system
(************************************************************)
synclabs: approach, startDown, endDown, pass;

loc Far: invariant True
	when True sync approach do {x := 0} goto Approaching;

loc Approaching: invariant x <= dApproach & x <= dStartDown
	when x = dStartDown sync startDown do {y := 0} goto Lowering;
	when x = dApproach sync pass goto Crash;

loc Crash: invariant True

loc Lowering: invariant x <= dApproach & y <= dGetDown
	when x = dApproach sync pass goto Crash;
	when y = dGetDown sync endDown goto Safe;

loc Safe: invariant x <= dApproach
	when x = dApproach sync pass do {x := 0, y := 0} goto Far;
end (* system *)



(************************************************************)
(* Initial state *)
(************************************************************)

init :=
	(*------------------------------------------------------------*)
	(* Initial location *)
	(*------------------------------------------------------------*)
	  loc[system]      = Far

	(*------------------------------------------------------------*)
	(* Initial clock constraints *)
	(*------------------------------------------------------------*)
	& x = 0
	& y = 0

	(*------------------------------------------------------------*)
	(* Parameter constraints *)
	(*------------------------------------------------------------*)
	& dApproach >= 0
	& dStartDown >= 0
	& dGetDown >= 0
;


(************************************************************)
(* Property specification *)
(************************************************************)

property := unreachable loc[system] = Crash;


(************************************************************)
(* The end *)
(************************************************************)
end