(************************************************************
 *                      IMITATOR MODEL                      
 *
 * Small problem with a nuclear plant that may explode
 *
 * Description     : Toy example of a nuclear plant that may explode
 * Correctness     : The nuclear plant must not blow up
 * Source          : "SITH" course final examination at Institut Galilée, Université Paris 13 (2013-2014)
 * Author          : Étienne André
 * Modeling        : Étienne André
 * Input by        : Étienne André
 *
 * Created         : 2014/03/21
 * Last modified   : 2020/08/13
 *
 * IMITATOR version: 3
 ************************************************************)


var 	x1, x2
		: clock;
		
	p1, (* Min duration between heating start and explosion *)
	p2, (* Exact duration between heating start and alarm triggering *)
	p3, (* Exact duration between alarm triggering and watering start *)
	p4  (* Max duration between watering start and watering end *)
		: parameter;




(************************************************************)
  automaton plant
(************************************************************)
synclabs: startHeating, tooHot, triggerAlarm, startWatering, endWatering, restart;
initially normal;

loc normal: invariant True
	when True do {x1 := 0, x2 := 0} sync startHeating goto heating;

loc heating: invariant x1 <= p1 & x2 <= p2
	when x1 >= p1 sync tooHot goto boom;
	when x2 = p2 do{x2 := 0} sync triggerAlarm goto ringing;

loc ringing: invariant x1 <= p1 & x2 <= p3
	when x1 >= p1 sync tooHot goto boom;
	when x2 = p3 do{x2 := 0} sync startWatering goto watering;

loc watering: invariant x1 <= p1 & x2 <= p4
	when x1 >= p1 sync tooHot goto boom;
	when x2 <= p4 do {x1 := 0, x2 := 0} sync endWatering goto stopped;
		(* reset to try to reduce state space *)

loc stopped: invariant True
	when True do {x1 := 0, x2 := 0} sync restart goto normal;
		(* reset to try to reduce state space *)

loc boom: invariant True

end (* plant *)



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

init := 
	(*------------------------------------------------------------*)
	(*   INITIAL LOCATION *)
	(*------------------------------------------------------------*)
	& loc[plant] = normal

	(*------------------------------------------------------------*)
	(*   INITIAL CLOCKS *)
	(*------------------------------------------------------------*)
	& x1 = 0
	& x2 = 0
	
	(*------------------------------------------------------------*)
	(*   PARAMETER CONSTRAINTS *)
	(*------------------------------------------------------------*)
	& p1 >= 0
	& p2 >= 0
	& p3 >= 0
	& p4 >= 0
	
	
(* 	& p3 > 0 & p1 > p2 & p4 = 0 *)
(* 	& p3 = 0 & p1 = 2 & p2 = 2 & p4 = 0 *)
(* 	& p2 >= p1 & p2 >=p2 + p3 *)
(* 	& p1 < p2+p3 *)
(* 	& p1 < p3 *)
(*	& p1 = 10
	& p2 = 12
	& p3 = 14
	& p4 = 15*)

(*	& p2 + p3 >= p1
	& p1 = p2
	& p3 = 0*)



	(*------------------------------------------------------------*)
	(*   Parameter valuation to ensure not EF boom *)
	(*------------------------------------------------------------*)
(*	& p1 = 10
	& p2 = 2
	& p3 = 3
	& p4 = 4*)

	(*------------------------------------------------------------*)
	(*   Parameter valuation to ensure AF boom *)
	(*------------------------------------------------------------*)
(*
	& p1 = 2
	& p2 = 2
	& p3 = 3
	& p4 = 4
*)


;



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