(*******************************************************************************
 *                                IMITATOR MODEL                               
 * 
 * Title            : BlT09_fig1
 * Description      : TODO
 * Correctness      : infinite run visiting infinitely often location 3
 * Scalable         : no
 * Generated        : no
 * Categories       : Toy
 * Source           : Laura Bozzelli, Salvatore La Torre: Decision problems for lower/upper bound parametric timed automata. Formal Methods in System Design 35(2): 121-151 (2009), Fig1
 * bibkey           : BT09
 * Author           : Laura Bozzelli, Salvatore La Torre
 * Modeling         : Laura Bozzelli, Salvatore La Torre
 * Input by         : Étienne André
 * License          : 
 * 
 * Created          : 2015/11/17
 * Last modified    : 2021/08/30
 * Model version    : 
 * 
 * IMITATOR version : 3.1
 ******************************************************************************)

var

(* Clocks *)
 	x, y
		: clock;

(* Parameters *)
	l, u
		: parameter;



(************************************************************)
  automaton pta
(************************************************************)
(* actions: a; *)

loc l0: invariant True
	when True goto l0;
	when True do {x := 0, y := 0} goto l1;

loc l1: invariant True
	when True goto l1;
	when -y < 2 - l goto l2;


loc l2: invariant True
	when True goto l2;
	when x < u goto l3;

loc l3: invariant True
	when True goto l3;

end (* pta *)



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

init := {
  discrete =
  	(*------------------------------------------------------------*)
  	(* Initial location *)
  	(*------------------------------------------------------------*)
  	loc[pta] := l0,
  ;

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

  	(*------------------------------------------------------------*)
  	(* Parameter constraints *)
  	(*------------------------------------------------------------*)
  	& l >= 0
  	& u >= 0
  ;
}

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