(******************************************************************************* * IMITATOR MODEL * * Title : infinite accepting loop * Description : Toy benchmark for which there exists an infinite accepting run * Categories : Academic ; Unsolvable * Source : Iterative Bounded Synthesis for Efficient Cycle Detection in Parametric Timed Automata, Fig. 1 * Author : Étienne André, Jaime Arias, Laure Petrucci, Jaco van de Pol * Modeling : Dylan Marinho * Input by : Dylan Marinho * License : * * Created : 2021/03/11 * Last modified : 2021/03/11 * Model version : * * Computation : Unsolvable * * IMITATOR version : 3 ******************************************************************************) property := #synth CycleThrough(accepting);