(************************************************************
 *                      IMITATOR MODEL                      
 *
 * Wireless fire alarm system
 *
 * Description     : wireless fire alarm system
 * Correctness     : TODO
 *
 * 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 An- disha. The wireless fire alarm system: Ensuring conformance to industrial stan- dards through formal verification. In FM'14, volume 8442 of LNCS, pages 658–672. Springer, 2014.)
 * URL             : http://arxiv.org/abs/1504.07838v1
 * Author          : Input by Étienne André
 *
 * Created         : 2015/05/14
 * Last modified   : 2015/05/14
 *
 * IMITATOR version: 2.7-beta2
 ************************************************************)

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