(*******************************************************************************
 *                                IMITATOR MODEL                               
 * 
 * Title            : uniproc_fp_sched_no_termination
 * Description      : 
 * Correctness      : 
 * Scalable         : 
 * Generated        : 
 * Categories       : 
 * Source           : ''Toward Parametric Timed Interfaces for Real-Time Components'' (2014) by Youcheng Sun, Giuseppe Lipari, Étienne André and Laurent Fribourg
 * bibkey           : 
 * Author           : Giuseppe Lipari
 * Modeling         : 
 * Input by         : 
 * License          : 
 * 
 * Created          : 2020/08/18
 * Last modified    : 2020/08/18
 * Model version    : 
 * 
 * IMITATOR version : 3
 ******************************************************************************)

var
    t1_c, t1_d, t1_urgent, t1_arr_x, t2_c, t2_d, t2_urgent, t2_arr_x, CPU1_urgent : clock;
    t1_inst, t2_inst: rational;
    stop_flag : bool;
    t1_arr_P, t2_arr_P: parameter;


automaton Task_t1
actions : t1_arr_event , t1_arr , t1_dis , t1_pre , t1_end , t1_miss;
loc t1_loc_idle : invariant True
    when True sync t1_arr_event do { t1_urgent := 0 } goto t1_loc_act_event;
loc t1_loc_act_event : invariant t1_urgent <= 0
    when t1_urgent = 0 sync t1_arr do { t1_c := 0 , t1_d := 0 , t1_inst := 1 } goto t1_loc_act;
loc t1_loc_act : invariant t1_d <= t1_arr_P stop { t1_c }
    when True sync t1_dis  goto t1_loc_exe;
    when t1_d  >=  t1_arr_P sync t1_miss  goto t1_loc_miss;
    when True sync t1_arr_event do { t1_inst := t1_inst+1 , t1_d := 0 } goto t1_loc_act;
    when True sync t1_arr_event  goto t1_loc_act;
loc t1_loc_exe : invariant t1_d <= t1_arr_P & t1_c <= 2 * t1_inst
    when True sync t1_pre  goto t1_loc_act;
    when t1_d >= t1_arr_P & t1_c < 2 * t1_inst sync t1_miss  goto t1_loc_miss;
    when True sync t1_arr_event do { t1_inst := t1_inst+1 , t1_d := 0 } goto t1_loc_exe;
    when True sync t1_arr_event  goto t1_loc_exe;
    when t1_c = 2*t1_inst sync t1_end  goto t1_loc_idle;
loc t1_loc_miss : invariant True
end



automaton Periodic_t1_arr
actions : t1_arr_event;
loc t1_arr_loc_arr : invariant t1_arr_x<=t1_arr_P
    when t1_arr_x=t1_arr_P sync t1_arr_event do { t1_arr_x :=  0 } goto t1_arr_loc_arr;
end


automaton Task_t2
actions : t2_arr_event , t2_arr , t2_dis , t2_pre , t2_end , t2_miss;
loc t2_loc_idle : invariant True
    when True sync t2_arr_event do { t2_urgent := 0 } goto t2_loc_act_event;
loc t2_loc_act_event : invariant t2_urgent <= 0
    when t2_urgent = 0 sync t2_arr do { t2_c := 0 , t2_d := 0 , t2_inst := 1 } goto t2_loc_act;
loc t2_loc_act : invariant t2_d <= t2_arr_P stop { t2_c }
    when True sync t2_dis  goto t2_loc_exe;
    when t2_d  >=  t2_arr_P sync t2_miss  goto t2_loc_miss;
    when True sync t2_arr_event do { t2_inst := t2_inst+1 , t2_d := 0 } goto t2_loc_act;
    when True sync t2_arr_event  goto t2_loc_act;
loc t2_loc_exe : invariant t2_d <= t2_arr_P & t2_c <= 2 * t2_inst
    when True sync t2_pre  goto t2_loc_act;
    when t2_d >= t2_arr_P & t2_c < 2 * t2_inst sync t2_miss  goto t2_loc_miss;
    when True sync t2_arr_event do { t2_inst := t2_inst+1 , t2_d := 0 } goto t2_loc_exe;
    when True sync t2_arr_event  goto t2_loc_exe;
    when t2_c = 2*t2_inst sync t2_end  goto t2_loc_idle;
loc t2_loc_miss : invariant True
end



automaton Periodic_t2_arr
actions : t2_arr_event;
loc t2_arr_loc_arr : invariant t2_arr_x<=t2_arr_P
    when t2_arr_x=t2_arr_P sync t2_arr_event do { t2_arr_x :=  0 } goto t2_arr_loc_arr;
end


automaton sched_CPU1
actions : t1_arr, t1_dis, t1_pre, t1_end, t2_arr, t2_dis, t2_pre, t2_end;
loc CPU1_loc_ : invariant True
    when True sync t1_arr do {CPU1_urgent := 0} goto CPU1_loc_At1;
    when True sync t2_arr do {CPU1_urgent := 0} goto CPU1_loc_At2;
loc CPU1_loc_At1 : invariant CPU1_urgent <= 0
    when CPU1_urgent = 0 sync t1_dis goto CPU1_loc_Rt1;
loc CPU1_loc_At2 : invariant CPU1_urgent <= 0
    when CPU1_urgent = 0 sync t2_dis goto CPU1_loc_Rt2;

loc CPU1_loc_Rt2 : invariant True
    when True sync t1_arr do {CPU1_urgent := 0} goto CPU1_loc_At1Rt2;
    when True sync t2_end do { CPU1_urgent := 0 } goto CPU1_loc_Et2;
loc CPU1_loc_Et2 : invariant CPU1_urgent <= 0
    when CPU1_urgent = 0   goto CPU1_loc_;
loc CPU1_loc_At1Rt2 : invariant CPU1_urgent <= 0
    when CPU1_urgent = 0 sync t2_pre goto CPU1_loc_At1Wt2;
loc CPU1_loc_At1Wt2 : invariant CPU1_urgent <= 0
    when CPU1_urgent = 0 sync t1_dis goto CPU1_loc_Rt1Wt2;

loc CPU1_loc_Rt1 : invariant True
    when True sync t2_arr do {CPU1_urgent := 0} goto CPU1_loc_Rt1Wt2;
    when True sync t1_end do { CPU1_urgent := 0 } goto CPU1_loc_Et1;
loc CPU1_loc_Et1 : invariant CPU1_urgent <= 0
    when CPU1_urgent = 0   goto CPU1_loc_;

loc CPU1_loc_Rt1Wt2 : invariant True
    when True sync t1_end do { CPU1_urgent := 0 } goto CPU1_loc_Et1Wt2;
loc CPU1_loc_Et1Wt2 : invariant CPU1_urgent <= 0
    when CPU1_urgent = 0 sync t2_dis  goto CPU1_loc_Rt2;

loc CPU1_loc_stop : invariant True
end



automaton OBS_dline
actions : t1_miss , t2_miss;
loc dline_loc_nomiss : invariant True
    when True sync t1_miss do { stop_flag := True } goto dline_loc_miss;
    when True sync t2_miss do { stop_flag := True } goto dline_loc_miss;
loc dline_loc_miss : invariant True
end


init := {

	discrete =
		(*------------------------------------------------------------*)
		(* Initial location *)
		(*------------------------------------------------------------*)
		loc[Task_t1] := t1_loc_idle,
		loc[Periodic_t1_arr] := t1_arr_loc_arr,
		loc[Task_t2] := t2_loc_idle,
		loc[Periodic_t2_arr] := t2_arr_loc_arr,
		loc[sched_CPU1] := CPU1_loc_,
		loc[OBS_dline] := dline_loc_nomiss,
		(*------------------------------------------------------------*)
		(* Initial discrete variables assignments *)
		(*------------------------------------------------------------*)
		t1_inst := 0,
		t2_inst := 0,
		stop_flag := False,
	;

	(*------------------------------------------------------------*)
	(* Initial continuous constraint *)
	(*------------------------------------------------------------*)
	continuous =
		&  t2_arr_P >= 0
    & t1_arr_P >= 0
    & t2_d = 0
    & t2_c = 0
    & t1_arr_P = t1_arr_x
    & t1_urgent = 0
    & t1_d = 0
    & t1_c = 0
    & t2_arr_P = t2_arr_x
    & t2_urgent = 0
    & CPU1_urgent = 0
	;

}

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