(*******************************************************************************
 *                                IMITATOR MODEL                               
 * 
 * Title            : infinite-noSolution
 * Description      : Toy benchmark for which the PZG has an infinite path but where the PTA infinite path is infeasible, i.e., there not exists any infinite accepting run for any value of p. NOTE: principle similar to `exU-noloop.imi`
 * Correctness      : 
 * Scalable         : no
 * Generated        : no
 * Categories       : Academic ; Toy ; Unsolvable
 * Source           : Étienne André, Jaime Arias, Laure Petrucci, Jaco van de Pol. "Iterative Bounded Synthesis for Efficient Cycle Detection in Parametric Timed Automata", TACAS 2021. Fig. 4
 * bibkey           : [AAPP21]
 * Author           : Jaco van de Pol
 * Modeling         : Jaco van de Pol
 * Input by         : Dylan Marinho
 * License          : Creative Commons Attribution-ShareAlike 4.0 International (CC BY-SA 4.0)
 * 
 * Created          : 2021/01/21
 * Last modified    : 2021/01/21
 * Model version    : 
 * 
 * IMITATOR version : 3
 ******************************************************************************)

var

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

(* Parameters *)
	p,
		: parameter;



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

accepting loc l0: invariant x <= 1 & y <= p
    when x >= 1 do {x := 0} goto l0;

end (* pta *)



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

init :=
	(*------------------------------------------------------------*)
	(* Initial location *)
	(*------------------------------------------------------------*)
	& loc[pta] = l0

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

	(*------------------------------------------------------------*)
	(* Parameter constraints *)
	(*------------------------------------------------------------*)
	& p >= 0
;


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