(************************************************************ * IMITATOR MODEL * * IMITATOR Sched1.imi Sched1.pi0 -mode cover -PRP -incl -merge * IMITATOR Sched1.imi -mode EF -incl -merge * * Model derived from the "idle scheduler" in the SynCop 2014 paper with 3 tasks. * Tasks have implicit deadlines; that is, for a task, its period and deadline are the same in the model. * Model automatically generated from some script * Author: Giuseppe Lipari * Date: January 2014 * References: ''Reachability Preservation Based Parameter Synthesis for Timed Automata'' (2015) by * Etienne Andre, Giuseppe Lipari, Hoang Gia Nguyen and Youcheng Sun; Sched1 * ''Toward Parametric Timed Interfaces for Real-Time Components'' (2014) by * Youcheng Sun, Giuseppe Lipari, Etienne Andre and Laurent Fribourg * Created: < 2015/10/30 * Last modified: 2018/09/07 * IMITATOR version: 2.10.3 ************************************************************) var t1_c, t1_d, t1_urgent, t1_arr_x, t2_c, t2_d, t2_urgent, t2_arr_x, t3_c, t3_d, t3_urgent, t3_arr_x, CPU1_urgent : clock; t1_inst, t2_inst, t3_inst, max_inst=5: discrete; t1_D = 40, t1_arr_P=40, t2_D , t2_arr_P , t3_D = 100, t3_arr_P=100 : parameter; automaton Task_t1 synclabs : 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_D stop { t1_c } when True sync t1_dis goto t1_loc_exe; when t1_d >= t1_D sync t1_miss goto t1_loc_miss; when t1_inst< max_inst sync t1_arr_event do { t1_inst := t1_inst+1 , t1_d := 0 } goto t1_loc_act; when t1_inst= max_inst sync t1_arr_event goto t1_loc_miss; when t1_inst< max_inst sync t1_arr_event goto t1_loc_act; loc t1_loc_exe : invariant t1_d <= t1_D & t1_c <= 5 * t1_inst when t1_c<5*t1_inst sync t1_pre goto t1_loc_act; when t1_d >= t1_D & t1_c < 5 * t1_inst sync t1_miss goto t1_loc_miss; when t1_inst< max_inst sync t1_arr_event do { t1_inst := t1_inst+1 , t1_d := 0 } goto t1_loc_exe; when t1_inst= max_inst sync t1_arr_event goto t1_loc_miss; when t1_inst< max_inst sync t1_arr_event goto t1_loc_exe; when t1_c = 5*t1_inst sync t1_end goto t1_loc_idle; loc t1_loc_miss : invariant True end automaton Periodic_t1_arr synclabs : 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 synclabs : 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_D stop { t2_c } when True sync t2_dis goto t2_loc_exe; when t2_d >= t2_D sync t2_miss goto t2_loc_miss; when t2_inst< max_inst sync t2_arr_event do { t2_inst := t2_inst+1 , t2_d := 0 } goto t2_loc_act; when t2_inst= max_inst sync t2_arr_event goto t2_loc_miss; when t2_inst< max_inst sync t2_arr_event goto t2_loc_act; loc t2_loc_exe : invariant t2_d <= t2_D & t2_c <= 20 * t2_inst when t2_c<20*t2_inst sync t2_pre goto t2_loc_act; when t2_d >= t2_D & t2_c < 20 * t2_inst sync t2_miss goto t2_loc_miss; when t2_inst< max_inst sync t2_arr_event do { t2_inst := t2_inst+1 , t2_d := 0 } goto t2_loc_exe; when t2_inst= max_inst sync t2_arr_event goto t2_loc_miss; when t2_inst< max_inst sync t2_arr_event goto t2_loc_exe; when t2_c = 20*t2_inst sync t2_end goto t2_loc_idle; loc t2_loc_miss : invariant True end automaton Periodic_t2_arr synclabs : 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 Task_t3 synclabs : t3_arr_event , t3_arr , t3_dis , t3_pre , t3_end , t3_miss; loc t3_loc_idle : invariant True when True sync t3_arr_event do { t3_urgent := 0 } goto t3_loc_act_event; loc t3_loc_act_event : invariant t3_urgent <= 0 when t3_urgent = 0 sync t3_arr do { t3_c := 0 , t3_d := 0 , t3_inst := 1 } goto t3_loc_act; loc t3_loc_act : invariant t3_d <= t3_D stop { t3_c } when True sync t3_dis goto t3_loc_exe; when t3_d >= t3_D sync t3_miss goto t3_loc_miss; when t3_inst< max_inst sync t3_arr_event do { t3_inst := t3_inst+1 , t3_d := 0 } goto t3_loc_act; when t3_inst= max_inst sync t3_arr_event goto t3_loc_miss; when t3_inst< max_inst sync t3_arr_event goto t3_loc_act; loc t3_loc_exe : invariant t3_d <= t3_D & t3_c <= 30 * t3_inst when t3_c<30*t3_inst sync t3_pre goto t3_loc_act; when t3_d >= t3_D & t3_c < 30 * t3_inst sync t3_miss goto t3_loc_miss; when t3_inst< max_inst sync t3_arr_event do { t3_inst := t3_inst+1 , t3_d := 0 } goto t3_loc_exe; when t3_inst= max_inst sync t3_arr_event goto t3_loc_miss; when t3_inst< max_inst sync t3_arr_event goto t3_loc_exe; when t3_c = 30*t3_inst sync t3_end goto t3_loc_idle; loc t3_loc_miss : invariant True end automaton Periodic_t3_arr synclabs : t3_arr_event; loc t3_arr_loc_arr : invariant t3_arr_x<=t3_arr_P when t3_arr_x=t3_arr_P sync t3_arr_event do { t3_arr_x := 0 } goto t3_arr_loc_arr; end automaton sched_CPU1 synclabs : t1_arr, t1_dis, t1_pre, t1_end, t2_arr, t2_dis, t2_pre, t2_end, t3_arr, t3_dis, t3_pre, t3_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; when True sync t3_arr do {CPU1_urgent := 0} goto CPU1_loc_At3; loc CPU1_loc_At1 : invariant CPU1_urgent <= 0 wait when CPU1_urgent = 0 sync t1_dis goto CPU1_loc_Rt1; loc CPU1_loc_At2 : invariant CPU1_urgent <= 0 wait when CPU1_urgent = 0 sync t2_dis goto CPU1_loc_Rt2; loc CPU1_loc_At3 : invariant CPU1_urgent <= 0 wait when CPU1_urgent = 0 sync t3_dis goto CPU1_loc_Rt3; loc CPU1_loc_Rt3 : invariant True when True sync t1_arr do {CPU1_urgent := 0} goto CPU1_loc_At1Rt3; when True sync t2_arr do {CPU1_urgent := 0} goto CPU1_loc_At2Rt3; when True sync t3_end do { CPU1_urgent := 0 } goto CPU1_loc_Et3; loc CPU1_loc_Et3 : invariant CPU1_urgent <= 0 wait when CPU1_urgent = 0 goto CPU1_loc_stop; loc CPU1_loc_At1Rt3 : invariant CPU1_urgent <= 0 wait when CPU1_urgent = 0 sync t3_pre goto CPU1_loc_At1Wt3; loc CPU1_loc_At1Wt3 : invariant CPU1_urgent <= 0 wait when CPU1_urgent = 0 sync t1_dis goto CPU1_loc_Rt1Wt3; loc CPU1_loc_At2Rt3 : invariant CPU1_urgent <= 0 wait when CPU1_urgent = 0 sync t3_pre goto CPU1_loc_At2Wt3; loc CPU1_loc_At2Wt3 : invariant CPU1_urgent <= 0 wait when CPU1_urgent = 0 sync t2_dis goto CPU1_loc_Rt2Wt3; loc CPU1_loc_Rt2 : invariant True when True sync t1_arr do {CPU1_urgent := 0} goto CPU1_loc_At1Rt2; when True sync t3_arr do {CPU1_urgent := 0} goto CPU1_loc_Rt2Wt3; when True sync t2_end do { CPU1_urgent := 0 } goto CPU1_loc_Et2; loc CPU1_loc_Et2 : invariant CPU1_urgent <= 0 wait when CPU1_urgent = 0 goto CPU1_loc_stop; loc CPU1_loc_At1Rt2 : invariant CPU1_urgent <= 0 wait when CPU1_urgent = 0 sync t2_pre goto CPU1_loc_At1Wt2; loc CPU1_loc_At1Wt2 : invariant CPU1_urgent <= 0 wait when CPU1_urgent = 0 sync t1_dis goto CPU1_loc_Rt1Wt2; loc CPU1_loc_Rt2Wt3 : invariant True when True sync t1_arr do {CPU1_urgent := 0} goto CPU1_loc_At1Rt2Wt3; when True sync t2_end do { CPU1_urgent := 0 } goto CPU1_loc_Et2Wt3; loc CPU1_loc_Et2Wt3 : invariant CPU1_urgent <= 0 wait when CPU1_urgent = 0 sync t3_dis goto CPU1_loc_Rt3; loc CPU1_loc_At1Rt2Wt3 : invariant CPU1_urgent <= 0 wait when CPU1_urgent = 0 sync t2_pre goto CPU1_loc_At1Wt2Wt3; loc CPU1_loc_At1Wt2Wt3 : invariant CPU1_urgent <= 0 wait when CPU1_urgent = 0 sync t1_dis goto CPU1_loc_Rt1Wt2Wt3; loc CPU1_loc_Rt1 : invariant True when True sync t2_arr do {CPU1_urgent := 0} goto CPU1_loc_Rt1Wt2; when True sync t3_arr do {CPU1_urgent := 0} goto CPU1_loc_Rt1Wt3; when True sync t1_end do { CPU1_urgent := 0 } goto CPU1_loc_Et1; loc CPU1_loc_Et1 : invariant CPU1_urgent <= 0 wait when CPU1_urgent = 0 goto CPU1_loc_stop; loc CPU1_loc_Rt1Wt3 : invariant True when True sync t2_arr do {CPU1_urgent := 0} goto CPU1_loc_Rt1Wt2Wt3; when True sync t1_end do { CPU1_urgent := 0 } goto CPU1_loc_Et1Wt3; loc CPU1_loc_Et1Wt3 : invariant CPU1_urgent <= 0 wait when CPU1_urgent = 0 sync t3_dis goto CPU1_loc_Rt3; loc CPU1_loc_Rt1Wt2 : invariant True when True sync t3_arr do {CPU1_urgent := 0} goto CPU1_loc_Rt1Wt2Wt3; when True sync t1_end do { CPU1_urgent := 0 } goto CPU1_loc_Et1Wt2; loc CPU1_loc_Et1Wt2 : invariant CPU1_urgent <= 0 wait when CPU1_urgent = 0 sync t2_dis goto CPU1_loc_Rt2; loc CPU1_loc_Rt1Wt2Wt3 : invariant True when True sync t1_end do { CPU1_urgent := 0 } goto CPU1_loc_Et1Wt2Wt3; loc CPU1_loc_Et1Wt2Wt3 : invariant CPU1_urgent <= 0 wait when CPU1_urgent = 0 sync t2_dis goto CPU1_loc_Rt2Wt3; loc CPU1_loc_stop : invariant True end automaton OBS_dline synclabs : t1_miss , t2_miss , t3_miss; loc dline_loc_nomiss : invariant True when True sync t1_miss goto dline_loc_miss; when True sync t2_miss goto dline_loc_miss; when True sync t3_miss goto dline_loc_miss; loc dline_loc_miss : invariant True end init := loc[Task_t1] = t1_loc_idle & t1_urgent = 0 & t1_c = 0 & t1_d = 0& t1_inst = 0 & t1_D >= 0 & loc[Periodic_t1_arr] = t1_arr_loc_arr & t1_arr_x = t1_arr_P & loc[Task_t2] = t2_loc_idle & t2_urgent = 0 & t2_c = 0 & t2_d = 0& t2_inst = 0 & t2_D >= 0 & loc[Periodic_t2_arr] = t2_arr_loc_arr & t2_arr_x = t2_arr_P & loc[Task_t3] = t3_loc_idle & t3_urgent = 0 & t3_c = 0 & t3_d = 0& t3_inst = 0 & t3_D >= 0 & loc[Periodic_t3_arr] = t3_arr_loc_arr & t3_arr_x = t3_arr_P & loc[sched_CPU1] = CPU1_loc_ & CPU1_urgent = 0 & loc[OBS_dline] = dline_loc_nomiss & t2_arr_P>=20 & t2_arr_P<=100 & t2_D>=20 & t2_D<=100 & True; property := unreachable loc[OBS_dline] = dline_loc_miss