(************************************************************
 *                      IMITATOR MODEL                      
 *
 * Model of a small acyclic asynchronous circuit
 *
 * Description     : Model of a small acyclic asynchronous circuit
 * Correctness     : Q must not rise
 * Source          : "Preserving Partial Order Runs in Parametric Time Petri Nets"  (ACSD 2015), Fig. 7
 * Author          : Étienne André, Thomas Chatain, César Rodríguez
 * Modeling        : Étienne André, Thomas Chatain, César Rodríguez
 * Input by        : Étienne André
 *
 * Created         : 2015/01/29
 * Last modified   : 2020/08/13
 *
 * IMITATOR version: 3
 ************************************************************)


property := #synth IM(
	(*------------------------------------------------------------
	   PARAMETER VALUATION: stable
	  ------------------------------------------------------------*)
	& dNot1_l	= 8
	& dNot1_u	= 10
	& dNot2_l	= 4
	& dNot2_u	= 5
	& dNot3_l	= 2
	& dNot3_u	= 8
	& dAnd_l	= 3
	& dAnd_u	= 4
	& di_l		= 1
	& di_u		= 2

	
	(*------------------------------------------------------------
	   PARAMETER VALUATION: loop
	  ------------------------------------------------------------*)
(*	& dNot1_l	= 1
	& dNot1_u	= 5
	& dNot2_l	= 4
	& dNot2_u	= 5
	& dNot3_l	= 2
	& dNot3_u	= 8
	& dAnd_l	= 3
	& dAnd_u	= 4
	& di_l		= 1
	& di_u		= 2*)
);