(*******************************************************************************
 *                                IMITATOR MODEL                               
 * 
 * Title            : synthpN
 * Description      : Toy benchmark for which the result is "p2 = i*p1 | i \in N" but IMITATOR cannot find it because the accumulated constraints grow forever
 * Correctness      : Reachability
 * Scalable         : no
 * Generated        : no
 * Categories       : Academic ; Toy ; Unsolvable
 * Source           : Own work
 * bibkey           : 
 * Author           : Étienne André
 * Modeling         : Dylan Marinho
 * Input by         : Dylan Marinho
 * License          : Creative Commons Attribution-ShareAlike 4.0 International (CC BY-SA 4.0)
 * 
 * Created          : 2021/01/21
 * Last modified    : 2021/08/31
 * Model version    : 
 * 
 * IMITATOR version : 3.1
 ******************************************************************************)

var

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

(* Parameters *)
	p1, p2
		: parameter;



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

loc l1: invariant x <= 1
	when x = p1 do {x := 0} goto l1;
	when x = 0 & y = p2 do {x := 0, y := 0} goto lGoal;

loc lGoal: invariant True

end (* pta *)



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

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

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

  	(*------------------------------------------------------------*)
  	(* Parameter constraints *)
  	(*------------------------------------------------------------*)
  	& p1 >= 0
    & p2 >= 0
  ;
}

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