(************************************************************
 *                      IMITATOR MODEL                      
 *
 *	IMITATOR Sched2.100.2.imi -mode EF -incl -output-cart -merge
 *	IMITATOR Sched2.100.2.imi Sched2.100.0.pi0 -mode cover -PRP -incl -output-cart -merge
 *
 * Modeling of the uniprocessor Non-Preemptive Fixed-Priority scheduling of three periodic tasks
 *
 * Description     : Three periodic tasks run upon a uniprocessor by their fixed priorites, and the execution of a task cannot be preempted.
 *		     The priority order: tau_1 > tau_2 > tau_3.
 *		     Task periods T1 = a, T2 = 2a, T3 = 3a.
 *		     Execution Times: C1 in [e=10, b], C2 in [c, d], C3 in [C3_BEST, C3_WORST]
 *
 * Extension with a jitter J2=2
 *
 * References      : "Integer Parameter Synthesis for Timed Automata" (2013) by A. Jovanovic, D. Lime and O.H. Roux; Section 6
                     "Reachability Preservation Based Parameter Synthesis for Timed Automata" (2015) by Etienne Andre, Giuseppe Lipari, Hoang Gia Nguyen and Youcheng Sun; Sched2.100.2 
 * Modeling        : Youcheng Sun
 * Input by        : Youcheng Sun, Étienne André
 *
 * Created         : xxxx (< 2015/10/29)
 * Last modified   : 2020/08/18
 *
 * IMITATOR version: 3
 ************************************************************)

var 
    p1, p2, p3, c1, c2, c3 : clock;
    b, C3_WORST: parameter;
    e=10,a=100, c=18, d=28, C3_BEST=20, J2=2: constant;
    b_min = 10, b_max = 1000, C3_WORST_min = 20, C3_WORST_max = 1000: constant;


(************************************************************)
automaton act1
(************************************************************)
synclabs: r1;
loc waiting1 : invariant p1<=a
    when p1>=a sync r1 do {p1 := 0} goto waiting1;
end

(************************************************************)
automaton act2
(************************************************************)
synclabs: r2;
loc waiting2 : invariant p2<=2*a+J2
    when p2>=2*a sync r2 do {p2 := 0} goto waiting2;
end

(************************************************************)
automaton act3
(************************************************************)
synclabs: r3;
loc waiting3 : invariant p3<=3*a
    when p3>=3*a sync r3 do {p3 := 0} goto waiting3;
end


(************************************************************)
automaton sched
(************************************************************)
synclabs : r1, r2, r3;

loc idle : invariant True
    when True sync r1 do {c1 := 0} goto x1R;
    when True sync r2 do {c2 := 0} goto x2R;
    when True sync r3 do {c3 := 0} goto x3R;

loc x1R : invariant c1<=b
(*     when c1>=10 goto idle; *)
    when c1>=e goto idle;
    when c1<b sync r1 do{} goto error;
    when True sync r2 goto x1R2W;
    when True sync r3 goto x1R3W;

loc x2R : invariant c2<=d
    when c2>=c goto idle;
    when c2<d sync r2 goto error;
    when True sync r1 goto x1W2R;
    when True sync r3 goto x2R3W;

loc x3R : invariant c3 <= C3_WORST
    when c3>=C3_BEST goto idle;
    when c3<C3_WORST sync r3 goto error;
    when True sync r1 goto x1W3R;
    when True sync r2 goto x2W3R;

loc x1R2W : invariant c1<=b
    when c1 >= e do {c2 := 0} goto x2R;
    when c1 < b sync r1 goto error;
    when True sync r2 goto error;
    when True sync r3 goto x1R2W3W;

loc x1R3W : invariant c1<=b
    when c1>=e do {c3 := 0} goto x3R;
    when c1<b sync r1 goto error;
    when True sync r3 goto error;
    when True sync r2 goto x1R2W3W;

loc x1W2R : invariant c2<=d
    when c2 >= c do {c1 := 0} goto x1R;
    when c2<d sync r2 goto error;
    when True sync r1 goto error;
    when True sync r3 goto x1W2R3W;

loc x2R3W : invariant c2<=d
    when c2>=c do {c3 := 0} goto x3R;
    when c2<d sync r2 goto error;
    when True sync r3 goto error;
    when True sync r1 goto x1W2R3W;

loc x1W3R : invariant c3<=C3_WORST
    when c3 >= C3_BEST do {c1 := 0} goto x1R;
    when c3<C3_WORST sync r3 goto error;
    when True sync r1 goto error;
    when True sync r2 goto x1W2W3R;

loc x2W3R : invariant c3<=C3_WORST
    when c3 >= C3_BEST do {c1 := 0} goto x1R;
    when c3<C3_WORST sync r3 goto error;
    when True sync r2 goto error;
    when True sync r1 goto x1W2W3R;

loc x1R2W3W : invariant c1<=b
    when c1>=e do {c2 := 0} goto x2R3W;
    when c1<b sync r1 goto error;
    when True sync r2 goto error;
    when True sync r3 goto error;

loc x1W2R3W : invariant c2<=d
    when c2>=c do {c1 := 0} goto x1R3W;
    when c2<d sync r2 goto error;
    when True sync r1 goto error;
    when True sync r3 goto error;

loc x1W2W3R : invariant c3<=C3_WORST
    when c3>=C3_BEST do {c1 := 0} goto x1R2W;
    when c3<C3_WORST sync r3 goto error;
    when True sync r1 goto error;
    when True sync r2 goto error;

loc error : invariant True

end


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

init :=
	(*------------------------------------------------------------*)
	(* Initial location *)
	(*------------------------------------------------------------*)
	& loc[act1]=waiting1
	& loc[act2]=waiting2
	& loc[act3]=waiting3
	& loc[sched]=idle

	(*------------------------------------------------------------*)
	(* Initial clock constraints *)
	(*------------------------------------------------------------*)
	& p1 = 0
	& p2 = 0
	& p3 = 0
	& c2 = 0
	& c1 = 0
	& c3 = 0

	(*------------------------------------------------------------*)
	(* Parameter constraints *)
	(*------------------------------------------------------------*)
	& b >= b_min & b <= b_max
	& C3_WORST >= C3_WORST_min & C3_WORST <= C3_WORST_max
;



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