(*******************************************************************************
 *                                IMITATOR MODEL
 *
 * Title            : infinite loop
 * Description      : Toy benchmark for which there exists an infinite 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/01/21
 * Last modified    : 2021/01/21
 * Model version    :
 *
 * Computation      : Unsolvable
 *
 * IMITATOR version : 3
 ******************************************************************************)

property := #synth Cycle;