(*******************************************************************************
 *                                IMITATOR MODEL                               
 * 
 * Title            : JLR15_Fig6
 * Description      : Example from [Figure 6, JLR15]
 * Correctness      : l2 is reachable
 * Scalable         : no
 * Generated        : no
 * Categories       : Toy ; Unsolvable
 * Source           : "Integer Parameter Synthesis for Real-time Systems" (used to be Figure 1 in "Integer Parameter Synthesis for Timed Automata" in [TACAS, 2013])
 * bibkey           : JLR15
 * Author           : Aleksandra Jovanović, Didier Lime, Olivier H. Roux
 * Modeling         : Aleksandra Jovanović, Didier Lime, Olivier H. Roux
 * Input by         : Étienne André
 * License          : Creative Commons Attribution-ShareAlike 4.0 International (CC BY-SA 4.0)
 * 
 * Created          : 2013/11/13
 * Last modified    : 2021/07/09
 * Model version    : 
 * 
 * IMITATOR version : 3.1
 ******************************************************************************)

var

(* Clocks *)
 	x, y,
		: clock;

(* Parameters *)
	a, b,
		: parameter;



(************************************************************)
  automaton aa
(************************************************************)
synclabs: ;

loc l1: invariant x <= b
	when x >= a do {x := 0} goto l1;
	when y >= 2 goto l2;

loc l2: invariant True

end (* pta *)



(************************************************************)
(* Initial state *)
(************************************************************)
init := {
	
    discrete =
		(*------------------------------------------------------------*)
		(* Initial location *)
		(*------------------------------------------------------------*)
		loc[aa] := l1,

		(*------------------------------------------------------------*)
		(* Initial discrete variables assignments *)
		(*------------------------------------------------------------*)
    ;

    continuous =        
		(*------------------------------------------------------------*)
		(* Initial clock constraints *)
		(*------------------------------------------------------------*)
		& x = 0
		& y = 0

		(*------------------------------------------------------------*)
		(* Parameter constraints *)
		(*------------------------------------------------------------*)
		& 0 <= a & a <= 10
		& 0 <= b & b <= 10
	;
}


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