(************************************************************
 *                      IMITATOR MODEL                      
 *
 *	IMITATOR JLR13-3tasks-npfp.imi -mode EF -incl -merge -output-cart
 *	IMITATOR JLR13-3tasks-npfp.imi JLR13-3tasks-npfp.v0 -mode cover -PRP -incl -merge -output-cart
 *
 * 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 [C1_BEST=10, b], C2 in [c, d], C3 in [C3_BEST, C3_WORST]
 * Source          : From "Integer Parameter Synthesis for Timed Automata" (2013) by A. Jovanovic, D. Lime and O.H. Roux; Section 6
 * Modeling        : Youcheng Sun
 * Input by        : Youcheng Sun, Étienne André
 *
 * Created         : xxxx (< 2015/10/28)
 * Last modified   : 2018/09/07
 *
 * IMITATOR version: 2.10.3
 ************************************************************)
 

var 
    p1, p2, p3, c1, c2, c3 : clock;
    
    a, b : parameter;
    
    d=28, c=18, C1_BEST = 10, C3_BEST=20, C3_WORST=28: 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
    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>=C1_BEST 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 >= C1_BEST 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>=C1_BEST 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 {c2 := 0} goto x2R;
    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>=C1_BEST 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 wait{}

end


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


init := 
	(*------------------------------------------------------------*)
	(* Initial location *)
	(*------------------------------------------------------------*)
        & loc[act1] = waiting1 
        & loc[act2] = waiting2
        & loc[act3] = waiting3 
        & loc[sched] = idle 
	(*------------------------------------------------------------*)
	(* Initial clock constraints *)
	(*------------------------------------------------------------*)
(*         & p1 >= 0 & p1 <= a & p2 >= 0 & p2 <=2*a & p3 >= 0 & p3 <= 3*a & c2 = 0 & c1 = 0 & c3 = 0 *)
        & p1 >= 0 & p1 <= a & p2 >= 0 & p2 <= 2*a & p3 >= 0 & p3 <= 3*a
        & c2 = 0 & c1 = 0 & c3 = 0
	(*------------------------------------------------------------*)
	(* Parameter constraints *)
	(*------------------------------------------------------------*)
	& a >= C1_BEST & b >= C1_BEST & a <= 50 & b <= 50
	;

(************************************************************)
(* Property specification *)
(************************************************************)
property := unreachable loc[sched] = error;

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