(*******************************************************************************
 *                                IMITATOR MODEL                               
 * 
 * Title            : train_intruder-converted_parameters
 * Description      : Railway crossing with an intruder that can disable some sensor (preventing the gate do detect that the train is approaching), possibly provoking a crash. Simple model with few symbolic states reachable.
 * Correctness      : "Crash" cannot happen
 * Scalable         : 
 * Generated        : 
 * Categories       : 
 * Source           : Own work
 * bibkey           : 
 * Author           : Étienne André, Michał Knapik
 * Modeling         : Étienne André
 * Input by         : Étienne André
 * License          : 
 * 
 * Created          : 2015/09/24
 * Last modified    : 2021/07/09
 * Model version    : 
 * 
 * IMITATOR version : 
 ******************************************************************************)

var

(* Clocks *)
 	x_train,
 	x_gate,
 	x_intruder,
		: clock;

(* Boolean discrete variables *)
	gate_down,     (* (Boolean) encoding whether the gate is down *)
	sensors_active,(* (Boolean) encoding whether the sensor is active *)
		: bool;

(* Train parameters *)
	p_far,         (* time between being far and approaching *)
	p_approaching, (* time between the approach and the passing *)
	
(* Gate parameters *)
	p_waiting,     (* time from the sensor activation until starting lowering the gate *)
	p_lowering,    (* time to lower the gate *)
	
(* Intruder parameters *)
	p_walking_sensor, (* time to walk to (and disable) the sensor *)

(* Action parameters *)
p_sensor_far, p_pass, p_start_lowering, p_end_lowering, p_break_sensor
		: parameter;

(* Constants *)
	ACTIVE = 0,
		: rational;


(************************************************************)
  automaton train
(************************************************************)
actions: sensor_far, pass;

loc far: invariant x_train <= p_far
	(* Normal mode: sensors are on *)
	when x_train = p_far & sensors_active & p_sensor_far = ACTIVE sync sensor_far do {x_train := 0} goto approaching;
	(* Failure: sensors are off *)
	when x_train = p_far & not(sensors_active) do {x_train := 0} goto approaching;

loc approaching: invariant x_train <= p_approaching
	(* Normal situation *)
	when x_train = p_approaching & gate_down & p_pass = ACTIVE  do {x_train := 0} sync pass goto gone;
	(* Gate not closed! *)
	when x_train = p_approaching & not(gate_down) & p_pass = ACTIVE do {x_train := 0} sync pass goto crash;
	
(** HACK: stop time to reduce state space *)
loc gone: invariant x_train <= 0

(** HACK: stop time to reduce state space *)
loc crash: invariant x_train <= 0


end (* train *)


(************************************************************)
  automaton gate
(************************************************************)
actions: pass, sensor_far, start_lowering, end_lowering;

loc up: invariant True
	when True sync sensor_far do {x_gate := 0} goto waiting;
	(* Gate is reinitialized whenever the train passes *)
	when p_pass = ACTIVE sync pass do {x_gate := 0} goto up;

loc waiting: invariant x_gate <= p_waiting
	when x_gate = p_waiting sync start_lowering do {x_gate := 0} goto lowering;
	(* Gate is reinitialized whenever the train passes *)
	when p_pass = ACTIVE sync pass do {x_gate := 0} goto up;

loc lowering: invariant x_gate <= p_lowering
	when x_gate = p_lowering & p_end_lowering = ACTIVE sync end_lowering do {x_gate := 0, gate_down := True} goto down;
	(* Gate is reinitialized whenever the train passes *)
	when p_pass = ACTIVE sync pass do {x_gate := 0} goto up;

loc down: invariant True
	(* Gate is reinitialized whenever the train passes *)
	when p_pass = ACTIVE sync pass do {x_gate := 0} goto up;

end (* gate *)


(************************************************************)
  automaton intruder
(************************************************************)
actions: break_sensor;

loc walking_sensor: invariant x_intruder <= p_walking_sensor
	when x_intruder = p_walking_sensor & p_break_sensor = ACTIVE sync break_sensor do {sensors_active := False, x_intruder := 0} goto intruder_done;

loc intruder_done: invariant True

end (* intruder *)



(************************************************************)
(* Initial state *)
(************************************************************)
init := {
	
    discrete =
		(*------------------------------------------------------------*)
		(* Initial location *)
		(*------------------------------------------------------------*)
		loc[train]     := far,
		loc[gate]      := up,
		loc[intruder]  := walking_sensor,

		(*------------------------------------------------------------*)
		(* Initial discrete variables assignments *)
		(*------------------------------------------------------------*)
		gate_down      := False,
		sensors_active := True,
    ;

    continuous =        
		(*------------------------------------------------------------*)
		(* Initial clock constraints *)
		(*------------------------------------------------------------*)
		& x_train    = 0
		& x_gate     >= 0
		& x_intruder = 0

		(*------------------------------------------------------------*)
		(* Parameter constraints *)
		(*------------------------------------------------------------*)
		& p_far            >= 0
		& p_approaching    >= 0
		& p_waiting        >= 0
		& p_lowering       >= 0
		& p_walking_sensor >= 0
		
		& p_sensor_far >= 0
		& p_pass >= 0
		& p_start_lowering >= 0
		& p_end_lowering >= 0
		& p_break_sensor >= 0
	;
}


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