(******************************************************************************* * IMITATOR MODEL * * Title : infinite-5_6 * Description : Toy benchmark for which there exists an infinite accepting run for p>=6 but not detecting if the algorithm diverges on the infinite p>=5 path * Correctness : * Scalable : no * Generated : no * Categories : Academic ; Toy ; Unsolvable * Source : Iterative Bounded Synthesis for Efficient Cycle Detection in Parametric Timed Automata, Fig. 6 * 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/01/21 * Model version : * * IMITATOR version : 3 ******************************************************************************) var (* Clocks *) x, y, : clock; (* Parameters *) p, : parameter; (************************************************************) automaton pta (************************************************************) synclabs: a; loc l0: invariant y <= p when x >= 5 do {y := 0} goto l0; when y >= 6 do {x := 0} goto l1; accepting loc l1: invariant True when True goto l1; end (* pta *) (************************************************************) (* Initial state *) (************************************************************) init := (*------------------------------------------------------------*) (* Initial location *) (*------------------------------------------------------------*) & loc[pta] = l0 (*------------------------------------------------------------*) (* Initial clock constraints *) (*------------------------------------------------------------*) & x = 0 & y = 0 (*------------------------------------------------------------*) (* Parameter constraints *) (*------------------------------------------------------------*) & p >= 0 ; (************************************************************) (* The end *) (************************************************************) end