(******************************************************************************* * IMITATOR MODEL * * Title : BlT09_fig1 * Description : TODO * Correctness : infinite run visiting infinitely often location 3 * Scalable : no * Generated : no * Categories : Toy * Source : Laura Bozzelli, Salvatore La Torre: Decision problems for lower/upper bound parametric timed automata. Formal Methods in System Design 35(2): 121-151 (2009), Fig1 * bibkey : BT09 * Author : Laura Bozzelli, Salvatore La Torre * Modeling : Laura Bozzelli, Salvatore La Torre * Input by : Étienne André * License : * * Created : 2015/11/17 * Last modified : 2020/08/13 * Model version : * * IMITATOR version : 3 ******************************************************************************) var (* Clocks *) x, y : clock; (* Parameters *) l, u : parameter; (************************************************************) automaton pta (************************************************************) (* synclabs: a; *) loc l0: invariant True when True goto l0; when True do {x := 0, y := 0} goto l1; loc l1: invariant True when True goto l1; when -y < 2 - l goto l2; loc l2: invariant True when True goto l2; when x < u goto l3; loc l3: invariant True when True goto l3; end (* pta *) (************************************************************) (* Initial state *) (************************************************************) init := (*------------------------------------------------------------*) (* Initial location *) (*------------------------------------------------------------*) & loc[pta] = l0 (*------------------------------------------------------------*) (* Initial clock constraints *) (*------------------------------------------------------------*) & x = 0 & y = 0 (*------------------------------------------------------------*) (* Parameter constraints *) (*------------------------------------------------------------*) & l >= 0 & u >= 0 ; (************************************************************) (* The end *) (************************************************************) end