(************************************************************
 *                      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. 1
 * Author          : Etienne Andre, Thomas Chatain, Cesar Rodriguez
 * Modeling        : Etienne Andre, Thomas Chatain, Cesar Rodriguez
 * Input by        : Etienne Andre
 *
 * Created         : 2015/01/29
 * Last modified   : 2015/07/30
 *
 * IMITATOR version: 2.7.1
 ************************************************************)

var 	ckNot1, ckNot2, ckAnd, ckEnv1, ckEnv2
		: clock;

	di1_l = 0, di1_u = 1,
	di2_l = 0, di2_u = 1,
	dNot1_l, dNot1_u,
	dNot2_l, dNot2_u,
	dAnd_l, dAnd_u
			: parameter;


(************************************************************)
  automaton Not1Gate
(************************************************************)
synclabs: i1Up, i1Down, n1Up, n1Down;

(* Unstable *)
loc Not100: while ckNot1 <= dNot1_u wait {}
	when True sync i1Up do {} goto Not110;
	when ckNot1 >= dNot1_l sync n1Up do {} goto Not101;

(* Stable *)
loc Not101: while True wait {}
	when True sync i1Up do {ckNot1' = 0} goto Not111;

(* Stable *)
loc Not110: while True wait {}
	when True sync i1Down do {ckNot1' = 0} goto Not100;

(* Unstable *)
loc Not111: while ckNot1 <= dNot1_u wait {}
	when True sync i1Down goto Not101;
	when ckNot1 >= dNot1_l sync n1Down goto Not110;

end (*Not1Gate*)



(************************************************************)
  automaton Not2Gate
(************************************************************)
synclabs: i2Up, i2Down, n2Up, n2Down;

(* Unstable *)
loc Not200: while ckNot2 <= dNot2_u wait {}
	when True sync i2Up do {} goto Not210;
	when ckNot2 >= dNot2_l sync n2Up do {} goto Not201;

(* Stable *)
loc Not201: while True wait {}
	when True sync i2Up do {ckNot2' = 0} goto Not211;

(* Stable *)
loc Not210: while True wait {}
	when True sync i2Down do {ckNot2' = 0} goto Not200;

(* Unstable *)
loc Not211: while ckNot2 <= dNot2_u wait {}
	when True sync i2Down goto Not201;
	when ckNot2 >= dNot2_l sync n2Down goto Not210;

end (*Not2Gate*)



(************************************************************)
  automaton AndGate
(************************************************************)
synclabs: n1Up, n1Down, n2Up, n2Down, qUp, qDown;

(* Stable *)
loc And000: while True wait {}
	when True sync n1Up do {} goto And100;
	when True sync n2Up do {} goto And010;

(* Untable *)
loc And001: while ckAnd <= dAnd_u wait {}
	when True sync n1Up do {ckAnd' = 0} goto And101;
	when True sync n2Up do {ckAnd' = 0} goto And011;
	when ckAnd >= dAnd_l sync qDown do {} goto And000;

(* Stable *)
loc And010: while True wait {}
	when True sync n1Up do {ckAnd' = 0} goto And110;
	when True sync n2Down do {} goto And000;

(* Untable *)
loc And011: while ckAnd <= dAnd_u wait {}
	when True sync n1Up do {} goto And111;
	when True sync n2Down do {ckAnd' = 0} goto And001;
	when ckAnd >= dAnd_l sync qDown do {} goto And010;

(* Stable *)
loc And100: while True wait {}
	when True sync n1Down do {} goto And000;
	when True sync n2Up do {ckAnd' = 0} goto And110;

(* Untable *)
loc And101: while ckAnd <= dAnd_u wait {}
	when True sync n1Down do {ckAnd' = 0} goto And001;
	when True sync n2Up do {} goto And111;
	when ckAnd >= dAnd_l sync qDown do {} goto And100;

(* Untable *)
loc And110: while ckAnd <= dAnd_u  wait {}
	when True sync n1Down do {} goto And010;
	when True sync n2Down do {} goto And100;
	when ckAnd >= dAnd_l sync qUp do {} goto And111;

(* Stable *)
loc And111: while True wait {}
	when True sync n1Down do {ckAnd' = 0} goto And011;
	when True sync n2Down do {ckAnd' = 0} goto And101;

end (*AndGate*)



(************************************************************)
  automaton EnvI1
(************************************************************)
synclabs: i1Up, i1Down;

(* Unstable *)
loc EnvI11: while ckEnv1 <= di1_u wait {}
	when ckEnv1 >= di1_u sync i1Down do {} goto EnvI10;

(* Stable *)
loc EnvI10: while True wait {}

end (*EnvI1*)



(************************************************************)
  automaton EnvI2
(************************************************************)
synclabs: i2Up, i2Down;

(* Unstable *)
loc EnvI20: while ckEnv2 <= di2_u wait {}
	when ckEnv2 >= di2_u sync i2Up do {} goto EnvI21;

(* Stable *)
loc EnvI21: while True wait {}

end (*EnvI2*)



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

init := True
	(*------------------------------------------------------------
	   INITIAL LOCATION
	  ------------------------------------------------------------*)
	 (*
		I1  = 1
		I2  = 0
		N1 = 0
		N2 = 1
		Q  = 0
	 *)
	  
	& loc[EnvI1]	= EnvI11
	& loc[EnvI2]	= EnvI20
	& loc[Not1Gate]	= Not110
	& loc[Not2Gate]	= Not201
	& loc[AndGate]	= And010

	(*------------------------------------------------------------
	   INITIAL CLOCKS
	  ------------------------------------------------------------*)
	& ckNot1 = 0
	& ckNot2 = 0
	& ckAnd = 0
	& ckEnv1 = 0
	& ckEnv2 = 0

	(*------------------------------------------------------------
	   PARAMETER CONSTRAINTS
	  ------------------------------------------------------------*)
	& dNot1_l >= 0
	& dNot1_l <= dNot1_u
	& dNot2_l >= 0
	& dNot2_l <= dNot2_u
	& dAnd_l >= 0
	& dAnd_l <= dAnd_u
	& di1_l >= 0
	& di1_l <= di1_u
	& di2_l >= 0
	& di2_l <= di2_u
	
	(*------------------------------------------------------------
	   PARAMETER VALUATION
	  ------------------------------------------------------------*)
	  
(*(*	& dNot1_l	= 6
	& dNot1_u	= 7
	& dNot2_l	= 1
	& dNot2_u	= 2
	& dAnd_l	= 1
	& dAnd_u	= 2*)*)

(*	& dNot2_l  = 0.1
	& dNot2_u = 0.3
	& dNot1_l  = 0.4
	& dNot1_u = 0.4*)
	
;


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

property := unreachable loc[AndGate] = And111;


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