(*******************************************************************************
 *                                IMITATOR MODEL                               
 * 
 * Title            : fig1_DCLXZL18-fixed
 * Description      : An ATM modeled using a PTA. Version fixed by changing incompatible constraints.
 * Correctness      : N/A
 * Scalable         : no
 * Generated        : no
 * Categories       : Academic ; Toy
 * Source           : Fig.1, "Parameter Synthesis Problems for one parametric clock Timed Automata" (https://arxiv.org/abs/1809.07177)
 * bibkey           : DCL18
 * Author           : Liyun Dai, Taolue Chen, Zhiming Liu, Bican Xia, Naijun Zhan, Kim G. Larsen
 * Modeling         : Liyun Dai, Taolue Chen, Zhiming Liu, Bican Xia, Naijun Zhan, Kim G. Larsen + Étienne André
 * Input by         : Jawher Jerray, Étienne André
 * License          : unclear ("Non-exclusive license to distribute" on arxiv: https://arxiv.org/licenses/nonexclusive-distrib/1.0/license.html)
 * 
 * Created          : 2018/09/23
 * Last modified    : 2021/02/09
 * Model version    : 
 * 
 * IMITATOR version : 3
 ******************************************************************************)

var

(* Clocks *)
 	x,
	y,
	z,
		: clock;

(* Parameters *)
	p1,
	p2,
	p3,
		: parameter;

(************************************************************)
  automaton pta
(************************************************************)
synclabs: ;

loc Idle: invariant True
	when True do {x := 0 , y := 0 , z := 0} goto Start;

loc Start: invariant z <= p1
	when z = p1 goto Idle;
	when z <= p1 do { y := 0 } goto Login;

loc Login: invariant y <= p2 && z <= p1
	when z = p1 goto Idle;
	when True do {x := 0} goto Withdrawals;
	when y = p2 goto Start;
	when True do {x := 0} goto Check;

loc Withdrawals: invariant x <= p3
	when True goto Login;

loc Check: invariant x <= p3
	when True goto Login;

end (* pta *)

(************************************************************)
(* Initial state *)
(************************************************************)

init :=
	(*------------------------------------------------------------*)
	(* Initial location *)
	(*------------------------------------------------------------*)
	& loc[pta] = Idle

	(*------------------------------------------------------------*)
	(* Initial discrete assignments *)
	(*------------------------------------------------------------*)

	(*------------------------------------------------------------*)
	(* Initial clock constraints *)
	(*------------------------------------------------------------*)
	& x = 0
	& y = 0
	& z = 0

	(*------------------------------------------------------------*)
	(* Parameter constraints *)
	(*------------------------------------------------------------*)
	& p1 >= 0
	& p2 >= 0
	& p3 >= 0
;


(************************************************************)
(* The end *)
(************************************************************)
end