(******************************************************************************* * IMITATOR MODEL * * Title : infinite-notFiniteDisjunction * Description : Toy benchmark for which there exists an infinite accepting run for a not finite disjunction of parameters (p in N) * Correctness : * Scalable : no * Generated : no * Categories : Academic ; Toy ; Unsolvable * Source : Iterative Bounded Synthesis for Efficient Cycle Detection in Parametric Timed Automata, Fig. 5 * bibkey : [AAPP21] * Author : Étienne André, Jaime Arias, Laure Petrucci, Jaco van de Pol * 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/03/12 * Model version : * * IMITATOR version : 3 ******************************************************************************) var (* Clocks *) x, y, : clock; (* Parameters *) p, : parameter; (************************************************************) automaton pta (************************************************************) synclabs: a; loc l0: invariant x <= 1 when x >= 1 do {x := 0} goto l0; when x = 1 & y = p do {x := 0, y := 0} goto lGoal; accepting loc lGoal: invariant True when True do {x := 0, y:= 0} goto lGoal; end (* pta *) (************************************************************) (* Initial state *) (************************************************************) init := (*------------------------------------------------------------*) (* Initial location *) (*------------------------------------------------------------*) & loc[pta] = l0 (*------------------------------------------------------------*) (* Initial clock constraints *) (*------------------------------------------------------------*) & x = 0 & y = 0 (*------------------------------------------------------------*) (* Parameter constraints *) (*------------------------------------------------------------*) & p >= 0 ; (************************************************************) (* The end *) (************************************************************) end