(*******************************************************************************
 *                                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    : 2021/08/30
 * Model version    : 
 * 
 * IMITATOR version : 3.1
 ******************************************************************************)





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
actions: r1;

loc waiting1 : invariant p1<=a
    when p1>=a sync r1 do {p1 := 0} goto waiting1;
end

automaton act2
actions: r2;
loc waiting2 : invariant p2<=2*a
    when p2>=2*a sync r2 do {p2 := 0} goto waiting2;
end

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


automaton sched
actions : 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 := {
  discrete =
  	(*------------------------------------------------------------*)
  	(* Initial location *)
  	(*------------------------------------------------------------*)
          loc[act1]  := waiting1,
          loc[act2]  := waiting2,
          loc[act3]  := waiting3,
          loc[sched] := idle,
    ;

    continuous =
  	(*------------------------------------------------------------*)
  	(* 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 *)
(************************************************************)