(************************************************************
 *                      IMITATOR MODEL                      
 *
 * Wireless fire alarm system
 *
 * Description     : wireless fire alarm system. Note that [BBLS15] only synthesize point valuations, and not the most general constraint satisfying correctness.
 * Correctness     : No failure and no timeout (safety property)
 *
 * Source          : "Language Emptiness of Continuous-Time Parametric Timed Automata" by Nikola Benes, Peter Bezdek, Kim G. Larsen, and Jiri Srba (the model was described in Sergio Feo-Arenis, Bernd Westphal, Daniel Dietsch, Marco Mun ̃iz, and Siyar Andisha. The wireless fire alarm system: Ensuring conformance to industrial standards through formal verification. In FM'14, volume 8442 of LNCS, pages 658–672. Springer, 2014.)
 * URL             : http://arxiv.org/abs/1504.07838v1
 * Author          : cf. above
 * Input by        : Étienne André
 *
 * Created         : 2015/05/13
 * Last modified   : 2018/09/10
 *
 * IMITATOR version: 2.10.4
 ************************************************************)

var

(* Clocks *)
 	x1, x2, x, y
		: clock;

(* Parameters *)
	p1, p2
		: parameter;



(************************************************************)
  automaton sensor1
(************************************************************)
synclabs: result1, wakeup1;

loc idle: invariant True
	when True sync wakeup1 do {x1 := 0} goto awake;

loc awake: invariant x1 < 3
	when True sync wakeup1 goto awake;
	when x1 > 2 & x1 < 3 sync result1 goto idle;
end (* sensor1 *)



(************************************************************)
  automaton sensor2
(************************************************************)
synclabs: result2, wakeup2;

loc idle: invariant True
	when True sync wakeup2 do {x2 := 0} goto awake;

loc awake: invariant x2 < 17
	when True sync wakeup2 goto awake;
	when x2 > 2 & x2 < 3 sync result2 goto idle;
	when x2 > 16 & x2 < 17 sync result2 goto idle;
end (* sensor2 *)


(************************************************************)
  automaton controller
(************************************************************)
synclabs: result1, wakeup1, result2, wakeup2;

loc cont_1: invariant x < 2 & y <= 20
	when True sync result1 goto fail;
	when True sync result2 goto fail;
	when x < 2 sync wakeup1 goto cont_2;
	when y = 20 goto timeout;

loc cont_2: invariant x <= p1 & y <= 20
	when True sync result2 goto fail;
	when x = p1 do {x := 0} goto cont_3;
	when x < p1 sync result1 do {x := 0} goto cont_3;
	when y = 20 goto timeout;

loc cont_3: invariant x < 2 & y <= 20
	when True sync result1 goto fail;
	when True sync result2 goto fail;
	when x < 2 sync wakeup2 goto cont_4;
	when y = 20 goto timeout;

loc cont_4: invariant x <= p2 & y <= 20
	when True sync result1 goto fail;
		(* BUG in the paper? I replaced 'x < p2' with 'x = p2' *)
	when x = p2 do {x := 0, y := 0} goto cont_1;
	when x < p2 sync result2 do {x := 0, y := 0} goto cont_1;
	when y = 20 goto timeout;

loc fail: invariant True

loc timeout: invariant True

end (* controller *)


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

init := True
	(*------------------------------------------------------------
	   INITIAL LOCATION
	  ------------------------------------------------------------*)
	& loc[sensor1] = idle
	& loc[sensor2] = idle
	& loc[controller] = cont_1

	(*------------------------------------------------------------
	   INITIAL CLOCKS
	  ------------------------------------------------------------*)
	& x1 = 0
	& x2 = 0
	& x = 0
	& y = 0


	(*------------------------------------------------------------
	   PARAMETER CONSTRAINTS
	  ------------------------------------------------------------*)
	& p1 >= 0
	& p2 >= 0
	
(*	& p1 <= 50
	& p2 <= 50*)
	
(* 	& 0 < p1 & p1 < 5 *)
(* 	& p1 > 2 *)

	(*------------------------------------------------------------
	   PARAMETER VALUATIONS
	  ------------------------------------------------------------*)
	(* Valuation 1 from [BBLS15]: not satisfactory because, although fail is unreachable, timeout is reachable *)
(*	& p1 = 5
	& p2 = 19*)
	(* Valuation 2 from [BBLS15]: satisfactory *)
(*	& p1 = 5
	& p2 = 9*)
;


(************************************************************)
(* Analysis *)
(************************************************************)

property := unreachable loc[controller] = fail or loc[controller] = timeout;

end