(************************************************************
 *                      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          : É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
 ************************************************************)

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: invariant ckNot1 <= dNot1_u
	when True sync i1Up do {} goto Not110;
	when ckNot1 >= dNot1_l sync n1Up do {} goto Not101;

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

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

(* Unstable *)
loc Not111: invariant ckNot1 <= dNot1_u
	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: invariant ckNot2 <= dNot2_u
	when True sync i2Up do {} goto Not210;
	when ckNot2 >= dNot2_l sync n2Up do {} goto Not201;

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

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

(* Unstable *)
loc Not211: invariant ckNot2 <= dNot2_u
	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: invariant True
	when True sync n1Up do {} goto And100;
	when True sync n2Up do {} goto And010;

(* Untable *)
loc And001: invariant ckAnd <= dAnd_u
	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: invariant True
	when True sync n1Up do {ckAnd := 0} goto And110;
	when True sync n2Down do {} goto And000;

(* Untable *)
loc And011: invariant ckAnd <= dAnd_u
	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: invariant True
	when True sync n1Down do {} goto And000;
	when True sync n2Up do {ckAnd := 0} goto And110;

(* Untable *)
loc And101: invariant ckAnd <= dAnd_u
	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: invariant ckAnd <= dAnd_u 
	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: invariant True
	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: invariant ckEnv1 <= di1_u
	when ckEnv1 >= di1_u sync i1Down do {} goto EnvI10;

(* Stable *)
loc EnvI10: invariant True

end (*EnvI1*)



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

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

(* Stable *)
loc EnvI21: invariant True

end (*EnvI2*)



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

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*)
	
;


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