(*******************************************************************************
 *                                IMITATOR MODEL                               
 * 
 * Title            : JLR13_3tasks_npfp
 * Description      : Three periodic tasks run upon a uniprocessor by their fixed priorites, and the execution of a task cannot be preempted.
 * Correctness      : 
 * Scalable         : 
 * Generated        : 
 * Categories       : Academic ; Protocol ; RTS
 * Source           : From "Integer Parameter Synthesis for Timed Automata" (2013) by A. Jovanovic, D. Lime and O.H. Roux; Section 6
 * bibkey           : JLR13
 * Author           : 
 * Modeling         : Youcheng Sun
 * Input by         : Youcheng Sun, Étienne André
 * License          : 
 * 
 * Created          : xxxx (< 2015/10/28)
 * Last modified    : 2020/08/18
 * Model version    : 
 * 
 * IMITATOR version : 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

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
	;

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