(******************************************************************************* * IMITATOR MODEL * * Title : untimedLanguage * Description : Toy benchmark for which the associated language is untimed (a^n.b^n.c^n) * Correctness : Reachability * Scalable : no * Generated : no * Categories : Academic ; Toy ; Unsolvable * Source : André É., Lime D., Roux O.H. (2016) On the Expressiveness of Parametric Timed Automata. In: Fränzle M., Markey N. (eds) Formal Modeling and Analysis of Timed Systems. FORMATS 2016. Lecture Notes in Computer Science, vol 9884. Springer, Cham. https://doi.org/10.1007/978-3-319-44878-7_2. Fig 2 * bibkey : ALR16 * 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/22 * Last modified : 2021/01/22 * Model version : * * IMITATOR version : 3 ******************************************************************************) var (* Clocks *) x, y, : clock; (* Parameters *) p, : parameter; (************************************************************) automaton pta (************************************************************) synclabs: a, b, c; loc l1: invariant x <= 1 & y <= p when x = 1 sync a do {x := 0} goto l1; when x = 1 & y = p sync a do {x := 0, y := 0} goto l2; loc l2: invariant x <= 1 & y <= p when x = 1 sync b do {x := 0} goto l2; when x = 1 & y = p sync b do {x := 0, y := 0} goto l3; loc l3: invariant x <= 1 & y <= p when x = 1 sync c do {x := 0} goto l3; when x = 1 & y = p sync c do {x := 0, y := 0} goto l4; accepting loc l4: invariant True end (* pta *) (************************************************************) (* Initial state *) (************************************************************) init := (*------------------------------------------------------------*) (* Initial location *) (*------------------------------------------------------------*) & loc[pta] = l1 (*------------------------------------------------------------*) (* Initial clock constraints *) (*------------------------------------------------------------*) & x = 0 & y = 0 (*------------------------------------------------------------*) (* Parameter constraints *) (*------------------------------------------------------------*) & p >= 0 ; (************************************************************) (* The end *) (************************************************************) end