(*******************************************************************************
 *                                IMITATOR MODEL                               
 * 
 * Title            : JLR13_3tasks_npfp-50_2
 * 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           : 
 * bibkey           : JLR13
 * Author           : 
 * Modeling         : Youcheng Sun
 * Input by         : Youcheng Sun, Étienne André
 * License          : 
 * 
 * Created          : xxxx (< 2015/10/30)
 * Last modified    : 2020/08/18
 * Model version    : 
 * 
 * IMITATOR version : 3
 ******************************************************************************)




var 
    p1, p2, p3, c1, c2, c3 : clock;
    b,C3_WORST: parameter;
    e=10,a=50, c=18, d=28, C3_BEST=20, J2=2: constant;
    b_min = 10, b_max = 50, C3_WORST_min = 20, C3_WORST_max = 100: 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