(************************************************************
 *                      IMITATOR MODEL                      
 *
 * Modeling of the circuit described in "Verification of timed circuits with symbolic delays" (Clariso -- Cortadella)
 *
 * Description     : A flip-flop circuit made of 4 gates. The environment is such that D raises, then CK raises then D falls, and then CK falls. No discrete variable.
 * Correctness     : Q should raise before CK falls
 * Source          : "Verification of timed circuits with symbolic delays" (Clariso -- Cortadella); Design Automation Conference, 2004. Proceedings of the ASP-DAC 2004. Asia and South Pacific; DOI: 10.1109/ASPDAC.2004.1337668
 * Author          : Roberto Clariso and Jordi Cortadella
 * Modeling        : Étienne André and Laurent Fribourg
 * Input by        : Étienne André
 *
 * Created         : 2007/11
 * Last modified   : 2020/01/06
 *
 * IMITATOR version: 3.0
 ************************************************************)

var 	s, ckG1, ckG2, ckG3, ckG4
		: clock;
(*
	tHI, tLO,
	tSetup, tHold,
	dG1_l, dG1_u,
	dG2_l, dG2_u,
	dG3_l, dG3_u,
	dG4_l, dG4_u
			: parameter; *)
			
	tHI    = 24,
	tLO    = 15,
	tSetup = 10,
	tHold  = 17,
	dG1_l  = 7,
	dG1_u  = 7,
	dG2_l  = 5,
	dG2_u  = 6,
	dG3_l  = 8,
	dG3_u, (*= 8 .. 30 -- 10*)
	dG4_l  = 3,
	dG4_u, (*= 3 .. 30 -- 7*)
	: parameter;


(************************************************************)
  automaton input
(************************************************************)
synclabs: dUp, dDown, ckUp, ckDown;

loc Input0: invariant s <= tLO - tSetup
	when s = tLO - tSetup sync dUp do {} goto Input1;

loc Input1: invariant s <= tLO
	when s = tLO sync ckUp do {} goto Input2;

loc Input2: invariant s <= tLO + tHold
	when s = tLO + tHold sync dDown do {} goto Input3;

loc Input3: invariant s <= tLO + tHI
	when s = tLO + tHI sync ckDown goto Input4;

urgent loc Input4: invariant True (* urgent: to blok time elapsing ckDown*)

end (* input *)


(************************************************************)
  automaton g1
(************************************************************)
(*Input : D, ck, qG2
Output : qG1*)

synclabs: dUp, dDown, ckUp, ckDown, qG2Up, qG2Down, qG1Up, qG1Down;

loc G10000: invariant ckG1 <= dG1_u
	when True sync dUp do {ckG1 := 0} goto G11000;
	when True sync ckUp do {ckG1 := 0} goto G10100;
	when True sync qG2Up do {ckG1 := 0} goto G10010;
	when ckG1 >= dG1_l sync qG1Up do {} goto G10001;

loc G10001: invariant ckG1 >= 0
	when True sync dUp do {} goto G11001;
	when True sync ckUp do {} goto G10101;
	when True sync qG2Up do {} goto G10011;

loc G10010: invariant ckG1 <= dG1_u
	when True sync dUp do {} goto G11010;
	when True sync ckUp do {} goto G10110;
	when True sync qG2Down do {ckG1 := 0} goto G10000;
	when ckG1 >= dG1_l sync qG1Up do {} goto G10011;

loc G10011: invariant ckG1 >= 0
	when True sync dUp do {ckG1 := 0} goto G11011;
	when True sync ckUp do {ckG1 := 0} goto G10111;
	when True sync qG2Down do {} goto G10001;

loc G10100: invariant ckG1 <= dG1_u
	when True sync dUp do {ckG1 := 0} goto G11100;
	when True sync ckDown do {ckG1 := 0} goto G10000;
	when True sync qG2Up do {} goto G10110;
	when ckG1 >= dG1_l sync qG1Up do {} goto G10101;

loc G10101: invariant ckG1 >= 0
	when True sync dUp do {} goto G11101;
	when True sync ckDown do {} goto G10001;
	when True sync qG2Up do {ckG1 := 0} goto G10111;

loc G10110: invariant ckG1 >= 0
	when True sync dUp do {} goto G11110;
	when True sync ckDown do {ckG1 := 0} goto G10010;
	when True sync qG2Down do {ckG1 := 0} goto G10100;

loc G10111: invariant ckG1 <= dG1_u
	when True sync dUp do {ckG1 := 0} goto G11111;
	when True sync ckDown do {} goto G10011;
	when True sync qG2Down do {} goto G10101;
	when ckG1 >= dG1_l sync qG1Down do {} goto G10110;

loc G11000: invariant ckG1 <= dG1_u
	when True sync dDown do {ckG1 := 0} goto G10000;
	when True sync ckUp do {ckG1 := 0} goto G11100;
	when True sync qG2Up do {} goto G11010;
	when ckG1 >= dG1_l sync qG1Up do {} goto G11001;

loc G11001: invariant ckG1 >= 0
	when True sync dDown do {} goto G10001;
	when True sync ckUp do {} goto G11101;
	when True sync qG2Up do {ckG1 := 0} goto G11011;

loc G11010: invariant ckG1 >= 0
	when True sync dDown do {ckG1 := 0} goto G10010;
	when True sync ckUp do {} goto G11110;
	when True sync qG2Down do {ckG1 := 0} goto G11000;

loc G11011: invariant ckG1 <= dG1_u
	when True sync dDown do {} goto G10011;
	when True sync ckUp do {ckG1 := 0} goto G11111;
	when True sync qG2Down do {} goto G11001;
	when ckG1 >= dG1_l sync qG1Down do {} goto G11010;

loc G11100: invariant ckG1 <= dG1_u
	when True sync dDown do {ckG1 := 0} goto G10100;
	when True sync ckDown do {ckG1 := 0} goto G11000;
	when True sync qG2Up do {} goto G11110;
	when ckG1 >= dG1_l sync qG1Up do {} goto G11101;

loc G11101: invariant ckG1 >= 0
	when True sync dDown do {} goto G10101;
	when True sync ckDown do {} goto G11001;
	when True sync qG2Up do {ckG1 := 0} goto G11111;

loc G11110: invariant ckG1 >= 0
	when True sync dDown do {} goto G10110;
	when True sync ckDown do {} goto G11010;
	when True sync qG2Down do {ckG1 := 0} goto G11100;

loc G11111: invariant ckG1 <= dG1_u
	when True sync dDown do {ckG1 := 0} goto G10111;
	when True sync ckDown do {ckG1 := 0} goto G11011;
	when True sync qG2Down do {} goto G11101;
	when ckG1 >= dG1_l sync qG1Down do {} goto G11110;
end (* g1 *)



(************************************************************)
  automaton g2
(************************************************************)
(*Input : qG1, ck
Output : qG2*)

synclabs: qG1Up, qG1Down, ckUp, ckDown, qG2Up, qG2Down;

loc G2001: invariant ckG2 >= 0
	when True sync qG1Up do {} goto G2101;
	when True sync ckUp do {} goto G2011;

loc G2000: invariant ckG2 <= dG2_u
	when True sync qG1Up do {ckG2 := 0} goto G2100;
	when True sync ckUp do {ckG2 := 0} goto G2010;
	when ckG2 >= dG2_l sync qG2Up do {} goto G2001;

loc G2011: invariant ckG2 >= 0
	when True sync qG1Up do {ckG2 := 0} goto G2111;
	when True sync ckDown do {} goto G2001;

loc G2010: invariant ckG2 <= dG2_u
	when True sync qG1Up do {} goto G2110;
	when True sync ckDown do {ckG2 := 0} goto G2000;
	when ckG2 >= dG2_l sync qG2Up do {} goto G2011;

loc G2101: invariant ckG2 >= 0
	when True sync qG1Down do {} goto G2001;
	when True sync ckUp do {ckG2 := 0} goto G2111;

loc G2100: invariant ckG2 <= dG2_u
	when True sync qG1Down do {ckG2 := 0} goto G2000;
	when True sync ckUp do {} goto G2110;
	when ckG2 >= dG2_l sync qG2Up do {} goto G2101;

loc G2111: invariant ckG2 <= dG2_u
	when True sync qG1Down do {} goto G2011;
	when True sync ckDown do {} goto G2101;
	when ckG2 >= dG2_l sync qG2Down do {} goto G2110;

loc G2110: invariant ckG2 >= 0
	when True sync qG1Down do {ckG2 := 0} goto G2010;
	when True sync ckDown do {ckG2 := 0} goto G2100;
end (* g2 *)



(************************************************************)
  automaton g3
(************************************************************)
(*Input : q, ck, qG2
Output : qG3*)

synclabs: qUp, qDown, ckUp, ckDown, qG2Up, qG2Down, qG3Up, qG3Down;

loc G30000: invariant ckG3 <= dG3_u
	when True sync qUp do {ckG3 := 0} goto G31000;
	when True sync ckUp do {ckG3 := 0} goto G30100;
	when True sync qG2Up do {ckG3 := 0} goto G30010;
	when ckG3 >= dG3_l sync qG3Up do {} goto G30001;

loc G30001: invariant ckG3 >= 0
	when True sync qUp do {} goto G31001;
	when True sync ckUp do {} goto G30101;
	when True sync qG2Up do {} goto G30011;

loc G30010: invariant ckG3 <= dG3_u
	when True sync qUp do {} goto G31010;
	when True sync ckUp do {} goto G30110;
	when True sync qG2Down do {ckG3 := 0} goto G30000;
	when ckG3 >= dG3_l sync qG3Up do {} goto G30011;

loc G30011: invariant ckG3 >= 0
	when True sync qUp do {ckG3 := 0} goto G31011;
	when True sync ckUp do {ckG3 := 0} goto G30111;
	when True sync qG2Down do {} goto G30001;

loc G30100: invariant ckG3 <= dG3_u
	when True sync qUp do {ckG3 := 0} goto G31100;
	when True sync ckDown do {ckG3 := 0} goto G30000;
	when True sync qG2Up do {} goto G30110;
	when ckG3 >= dG3_l sync qG3Up do {} goto G30101;

loc G30101: invariant ckG3 >= 0
	when True sync qUp do {} goto G31101;
	when True sync ckDown do {} goto G30001;
	when True sync qG2Up do {ckG3 := 0} goto G30111;

loc G30110: invariant ckG3 >= 0
	when True sync qUp do {} goto G31110;
	when True sync ckDown do {ckG3 := 0} goto G30010;
	when True sync qG2Down do {ckG3 := 0} goto G30100;

loc G30111: invariant ckG3 <= dG3_u
	when True sync qUp do {ckG3 := 0} goto G31111;
	when True sync ckDown do {} goto G30011;
	when True sync qG2Down do {} goto G30101;
	when ckG3 >= dG3_l sync qG3Down do {} goto G30110;

loc G31000: invariant ckG3 <= dG3_u
	when True sync qDown do {ckG3 := 0} goto G30000;
	when True sync ckUp do {ckG3 := 0} goto G31100;
	when True sync qG2Up do {} goto G31010;
	when ckG3 >= dG3_l sync qG3Up do {} goto G31001;

loc G31001: invariant ckG3 >= 0
	when True sync qDown do {} goto G30001;
	when True sync ckUp do {} goto G31101;
	when True sync qG2Up do {ckG3 := 0} goto G31011;

loc G31010: invariant ckG3 >= 0
	when True sync qDown do {ckG3 := 0} goto G30010;
	when True sync ckUp do {} goto G31110;
	when True sync qG2Down do {ckG3 := 0} goto G31000;

loc G31011: invariant ckG3 <= dG3_u
	when True sync qDown do {} goto G30011;
	when True sync ckUp do {ckG3 := 0} goto G31111;
	when True sync qG2Down do {} goto G31001;
	when ckG3 >= dG3_l sync qG3Down do {} goto G31010;

loc G31100: invariant ckG3 <= dG3_u
	when True sync qDown do {ckG3 := 0} goto G30100;
	when True sync ckDown do {ckG3 := 0} goto G31000;
	when True sync qG2Up do {} goto G31110;
	when ckG3 >= dG3_l sync qG3Up do {} goto G31101;

loc G31101: invariant ckG3 >= 0
	when True sync qDown do {} goto G30101;
	when True sync ckDown do {} goto G31001;
	when True sync qG2Up do {ckG3 := 0} goto G31111;

loc G31110: invariant ckG3 >= 0
	when True sync qDown do {} goto G30110;
	when True sync ckDown do {} goto G31010;
	when True sync qG2Down do {ckG3 := 0} goto G31100;

loc G31111: invariant ckG3 <= dG3_u
	when True sync qDown do {ckG3 := 0} goto G30111;
	when True sync ckDown do {ckG3 := 0} goto G31011;
	when True sync qG2Down do {} goto G31101;
	when ckG3 >= dG3_l sync qG3Down do {} goto G31110;
end (* g3 *)



(************************************************************)
  automaton g4
(************************************************************)
(*Input : qG3
Output : q*)

synclabs: qG3Up, qG3Down, qUp, qDown;

loc G401: invariant ckG4 >= 0
	when True sync qG3Up do {ckG4 := 0} goto G411;

loc G411: invariant ckG4 <= dG4_u
	when True sync qG3Down do {} goto G401;
	when ckG4 >= dG4_l sync qDown do {} goto G410;

loc G410: invariant ckG4 >= 0
	when True sync qG3Down do {ckG4 := 0} goto G400;

loc G400: invariant ckG4 <= dG4_u
	when True sync qG3Up do {} goto G410;
	when ckG4 >= dG4_l sync qUp do {} goto G401;
end (* g4 *)



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

init :=
	(*------------------------------------------------------------*)
	(* Initial location *)
	(*------------------------------------------------------------*)
	& loc[input] = Input0
	& loc[g1]    = G10011
	& loc[g2]    = G2101
	& loc[g3]    = G30011
	& loc[g4]    = G410

	(*------------------------------------------------------------*)
	(* Initial clock constraints *)
	(*------------------------------------------------------------*)
	& s = 0
	& ckG1 >= 0
	& ckG2 >= 0
	& ckG3 >= 0
	& ckG4 >= 0

	(*------------------------------------------------------------*)
	(* Parameter constraints *)
	(*------------------------------------------------------------*)

	& dG1_l >= 0
	& dG2_l >= 0
	& dG3_l >= 0
	& dG4_l >= 0

	& tHI  >= 0
	& tLO  >= 0
	& tSetup >= 0
	& tHold  >= 0

	& dG1_l <= dG1_u 
	& dG2_l <= dG2_u
	& dG3_l <= dG3_u
	& dG4_l <= dG4_u
	
	& tSetup <= tLO
	& tHold <= tHI
;


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