(*******************************************************************************
 *                                IMITATOR MODEL                               
 * 
 * Title            : SSLAF13_test2
 * Description      : Test Case 2 from [SSLAF13]. Note: might not be the final model of the paper (?)
 * Correctness      : system is schedulable
 * Scalable         : yes
 * Generated        : yes
 * Categories       : Protocol ; RTS
 * Source           : "Parametric Schedulability Analysis of Fixed Priority Real-Time Distributed Systems" (2013) by Youcheng Sun, Romain Soulat, Giuseppe Lipari, Etienne Andre and Laurent Fribourg; Test Case 2.
 * bibkey           : SSLAF13
 * Author           : Youcheng Sun, Romain Soulat, Giuseppe Lipari, Etienne Andre and Laurent Fribourg
 * Modeling         : Youcheng Sun, Romain Soulat, Giuseppe Lipari, Etienne Andre and Laurent Fribourg
 * Input by         : ?
 * License          : 
 * 
 * Created          : < 2015/10/30
 * Last modified    : 2018/08/20
 * Model version    : 
 * 
 * IMITATOR version : 3
 ******************************************************************************)



var 
	t_asap_1:clock;
	t_pipeline_1:clock;
	t_task_11:clock;
	Token_11:discrete;
	t_task_12:clock;
	Token_12:discrete;
	t_task_13:clock;
	Token_13:discrete;
	t_task_14:clock;
	Token_14:discrete;
	t_task_15:clock;
	Token_15:discrete;
	t_asap_2:clock;
	t_pipeline_2:clock;
	t_task_21:clock;
	Token_21:discrete;
	t_task_22:clock;
	Token_22:discrete;
	t_task_23:clock;
	Token_23:discrete;
	t_task_24:clock;
	Token_24:discrete;
	t_task_25:clock;
	Token_25:discrete;

	T_pipeline_1=31250,
	D_pipeline_1=200000,
	C_task_11,
	C_task_12=445,
	C_task_13=9091,
	C_task_14=445,
	C_task_15,
	T_pipeline_2=3000000,
	D_pipeline_2=1000000,
	C_task_21=90910,
	C_task_22=889,
	C_task_23=44248,
	C_task_24=889,
	C_task_25=22728,
		: parameter;

automaton pipeline_1
	synclabs:pipeline_restart_1,task_11_act,task_11_done,task_12_act,task_12_done,task_13_act,task_13_done,task_14_act,task_14_done,task_15_act,task_15_done;

	loc P1_1: invariant t_asap_1 <= 0
		 when t_asap_1=0 sync task_11_act goto P1_2;
	loc P1_2: invariant t_pipeline_1 <= D_pipeline_1
		 when t_pipeline_1 <= D_pipeline_1 sync task_11_done do {t_asap_1 := 0} goto P1_3;
	loc P1_3: invariant t_asap_1 <= 0
		 when t_asap_1=0 sync task_12_act goto P1_4;
	loc P1_4: invariant t_pipeline_1 <= D_pipeline_1
		 when t_pipeline_1 <= D_pipeline_1 sync task_12_done do {t_asap_1 := 0} goto P1_5;
	loc P1_5: invariant t_asap_1 <= 0
		 when t_asap_1=0 sync task_13_act goto P1_6;
	loc P1_6: invariant t_pipeline_1 <= D_pipeline_1
		 when t_pipeline_1 <= D_pipeline_1 sync task_13_done do {t_asap_1 := 0} goto P1_7;
	loc P1_7: invariant t_asap_1 <= 0
		 when t_asap_1=0 sync task_14_act goto P1_8;
	loc P1_8: invariant t_pipeline_1 <= D_pipeline_1
		 when t_pipeline_1 <= D_pipeline_1 sync task_14_done do {t_asap_1 := 0} goto P1_9;
	loc P1_9: invariant t_asap_1 <= 0
		 when t_asap_1=0 sync task_15_act goto P1_10;
	loc P1_10: invariant t_pipeline_1 <= D_pipeline_1
		 when t_pipeline_1 <= D_pipeline_1 sync task_15_done do {t_asap_1 := 0} goto P1_11;
	loc P1_11: invariant t_pipeline_1 <= T_pipeline_1
		 when t_pipeline_1 = T_pipeline_1 do {t_pipeline_1 := 0,t_asap_1 := 0} sync pipeline_restart_1 goto P1_1;
end

automaton pipeline_2
	synclabs:pipeline_restart_2,task_21_act,task_21_done,task_22_act,task_22_done,task_23_act,task_23_done,task_24_act,task_24_done,task_25_act,task_25_done;

	loc P2_1: invariant t_asap_2 <= 0
		 when t_asap_2=0 sync task_21_act goto P2_2;
	loc P2_2: invariant t_pipeline_2 <= D_pipeline_2
		 when t_pipeline_2 <= D_pipeline_2 sync task_21_done do {t_asap_2 := 0} goto P2_3;
	loc P2_3: invariant t_asap_2 <= 0
		 when t_asap_2=0 sync task_22_act goto P2_4;
	loc P2_4: invariant t_pipeline_2 <= D_pipeline_2
		 when t_pipeline_2 <= D_pipeline_2 sync task_22_done do {t_asap_2 := 0} goto P2_5;
	loc P2_5: invariant t_asap_2 <= 0
		 when t_asap_2=0 sync task_23_act goto P2_6;
	loc P2_6: invariant t_pipeline_2 <= D_pipeline_2
		 when t_pipeline_2 <= D_pipeline_2 sync task_23_done do {t_asap_2 := 0} goto P2_7;
	loc P2_7: invariant t_asap_2 <= 0
		 when t_asap_2=0 sync task_24_act goto P2_8;
	loc P2_8: invariant t_pipeline_2 <= D_pipeline_2
		 when t_pipeline_2 <= D_pipeline_2 sync task_24_done do {t_asap_2 := 0} goto P2_9;
	loc P2_9: invariant t_asap_2 <= 0
		 when t_asap_2=0 sync task_25_act goto P2_10;
	loc P2_10: invariant t_pipeline_2 <= D_pipeline_2
		 when t_pipeline_2 <= D_pipeline_2 sync task_25_done do {t_asap_2 := 0} goto P2_11;
	loc P2_11: invariant t_pipeline_2 <= T_pipeline_2
		 when t_pipeline_2 = T_pipeline_2 do {t_pipeline_2 := 0,t_asap_2 := 0} sync pipeline_restart_2 goto P2_1;
end

automaton proc_1
	 synclabs: DEADLINE_MISSED_1, task_11_act,task_11_done,task_15_act,task_15_done,task_25_act,task_25_done;

	loc DEADLINE_MISS: invariant True
	loc proc_1_000: invariant True stop {t_task_11,t_task_15,t_task_25}
		when True sync task_11_act do {t_task_11 := 0} goto proc_1_100;
		when True sync task_15_act do {t_task_15 := 0} goto proc_1_010;
		when True sync task_25_act do {t_task_25 := 0} goto proc_1_001;
	loc proc_1_100: invariant t_task_11 <= C_task_11 stop {t_task_15,t_task_25}
		when t_task_25 < C_task_25 & t_pipeline_1 = D_pipeline_1 sync DEADLINE_MISSED_1 goto DEADLINE_MISS;
		when t_task_25 < C_task_25 & t_pipeline_2 = D_pipeline_2 sync DEADLINE_MISSED_1 goto DEADLINE_MISS;
		when t_task_11 = C_task_11 sync task_11_done goto proc_1_000;
		when t_task_11 < C_task_11 sync task_15_act do {t_task_15 := 0} goto proc_1_110;
		when t_task_11 < C_task_11 sync task_25_act do {t_task_25 := 0} goto proc_1_101;
	loc proc_1_010: invariant t_task_15 <= C_task_15 stop {t_task_11,t_task_25}
		when t_task_25 < C_task_25 & t_pipeline_1 = D_pipeline_1 sync DEADLINE_MISSED_1 goto DEADLINE_MISS;
		when t_task_25 < C_task_25 & t_pipeline_2 = D_pipeline_2 sync DEADLINE_MISSED_1 goto DEADLINE_MISS;
		when t_task_15 < C_task_15 sync task_11_act do {t_task_11 := 0} goto proc_1_110;
		when t_task_15 = C_task_15 sync task_15_done goto proc_1_000;
		when t_task_15 < C_task_15 sync task_25_act do {t_task_25 := 0} goto proc_1_011;
	loc proc_1_001: invariant t_task_25 <= C_task_25 stop {t_task_11,t_task_15}
		when t_task_25 < C_task_25 & t_pipeline_1 = D_pipeline_1 sync DEADLINE_MISSED_1 goto DEADLINE_MISS;
		when t_task_25 < C_task_25 & t_pipeline_2 = D_pipeline_2 sync DEADLINE_MISSED_1 goto DEADLINE_MISS;
		when t_task_25 < C_task_25 sync task_11_act do {t_task_11 := 0} goto proc_1_101;
		when t_task_25 < C_task_25 sync task_15_act do {t_task_15 := 0} goto proc_1_011;
		when t_task_25 = C_task_25 sync task_25_done goto proc_1_000;
	loc proc_1_110: invariant t_task_11 <= C_task_11 stop {t_task_15,t_task_25}
		when t_task_25 < C_task_25 & t_pipeline_1 = D_pipeline_1 sync DEADLINE_MISSED_1 goto DEADLINE_MISS;
		when t_task_25 < C_task_25 & t_pipeline_2 = D_pipeline_2 sync DEADLINE_MISSED_1 goto DEADLINE_MISS;
		when t_task_11 = C_task_11 sync task_11_done goto proc_1_010;
		when t_task_15 = C_task_15 sync task_15_done goto proc_1_100;
		when t_task_11 < C_task_11 sync task_25_act do {t_task_25 := 0} goto proc_1_111;
	loc proc_1_101: invariant t_task_11 <= C_task_11 stop {t_task_15,t_task_25}
		when t_task_25 < C_task_25 & t_pipeline_1 = D_pipeline_1 sync DEADLINE_MISSED_1 goto DEADLINE_MISS;
		when t_task_25 < C_task_25 & t_pipeline_2 = D_pipeline_2 sync DEADLINE_MISSED_1 goto DEADLINE_MISS;
		when t_task_11 = C_task_11 sync task_11_done goto proc_1_001;
		when t_task_11 < C_task_11 sync task_15_act do {t_task_15 := 0} goto proc_1_111;
		when t_task_25 = C_task_25 sync task_25_done goto proc_1_100;
	loc proc_1_011: invariant t_task_15 <= C_task_15 stop {t_task_11,t_task_25}
		when t_task_25 < C_task_25 & t_pipeline_1 = D_pipeline_1 sync DEADLINE_MISSED_1 goto DEADLINE_MISS;
		when t_task_25 < C_task_25 & t_pipeline_2 = D_pipeline_2 sync DEADLINE_MISSED_1 goto DEADLINE_MISS;
		when t_task_15 < C_task_15 sync task_11_act do {t_task_11 := 0} goto proc_1_111;
		when t_task_15 = C_task_15 sync task_15_done goto proc_1_001;
		when t_task_25 = C_task_25 sync task_25_done goto proc_1_010;
	loc proc_1_111: invariant t_task_11 <= C_task_11 stop {t_task_15,t_task_25}
		when t_task_25 < C_task_25 & t_pipeline_1 = D_pipeline_1 sync DEADLINE_MISSED_1 goto DEADLINE_MISS;
		when t_task_25 < C_task_25 & t_pipeline_2 = D_pipeline_2 sync DEADLINE_MISSED_1 goto DEADLINE_MISS;
		when t_task_11 = C_task_11 sync task_11_done goto proc_1_011;
		when t_task_15 = C_task_15 sync task_15_done goto proc_1_101;
		when t_task_25 = C_task_25 sync task_25_done goto proc_1_110;
end

automaton proc_2
	 synclabs: DEADLINE_MISSED_2,task_12_act,task_12_done,task_14_act,task_14_done,task_22_act,task_22_done,task_24_act,task_24_done;

	 loc idle: invariant True stop{t_task_12,t_task_14,t_task_22,t_task_24}
		when True sync task_12_act do{Token_12 := 1}goto t_12_running;
		when True sync task_14_act do{Token_14 := 1}goto t_14_running;
		when True sync task_22_act do{Token_22 := 1}goto t_22_running;
		when True sync task_24_act do{Token_24 := 1}goto t_24_running;

	loc DEADLINE_MISS: invariant True
	loc t_12_running: invariant t_task_12 <= C_task_12 stop {t_task_14,t_task_22,t_task_24}
		when t_task_12 < C_task_12 & t_pipeline_1 = D_pipeline_1 sync DEADLINE_MISSED_2 goto DEADLINE_MISS;
		when t_task_12 < C_task_12 & t_pipeline_2 = D_pipeline_2 sync DEADLINE_MISSED_2 goto DEADLINE_MISS;
		 when t_task_12 <= 0 sync task_12_act do{Token_12 := 1}goto t_12_running;
		 when t_task_12 > 0 sync task_12_act do{Token_12 := 1}goto t_12_running;
		 when t_task_12 <= 0 sync task_14_act do{Token_14 := 1}goto t_12_running;
		 when t_task_12 > 0 sync task_14_act do{Token_14 := 1}goto t_12_running;
		 when t_task_12 <= 0 sync task_22_act do{Token_22 := 1}goto t_12_running;
		 when t_task_12 > 0 sync task_22_act do{Token_22 := 1}goto t_12_running;
		 when t_task_12 <= 0 sync task_24_act do{Token_24 := 1}goto t_12_running;
		 when t_task_12 > 0 sync task_24_act do{Token_24 := 1}goto t_12_running;
		when t_task_12 = C_task_12 & Token_14=0  & Token_22=0  & Token_24=0 sync task_12_done do{Token_12 := 0} goto idle;
		when t_task_12 = C_task_12 & Token_14=1  & Token_22=0  & Token_24=0 sync task_12_done do{t_task_14 := 0,Token_12 := 0} goto t_14_running;
		when t_task_12 = C_task_12 & Token_14=0  & Token_22=1  & Token_24=0 sync task_12_done do{t_task_22 := 0,Token_12 := 0} goto t_22_running;
		when t_task_12 = C_task_12 & Token_14=0  & Token_22=0  & Token_24=1 sync task_12_done do{t_task_24 := 0,Token_12 := 0} goto t_24_running;
		when t_task_12 = C_task_12 & Token_14=1  & Token_22=1  & Token_24=0 sync task_12_done do{t_task_14 := 0,Token_12 := 0} goto t_14_running;
		when t_task_12 = C_task_12 & Token_14=1  & Token_22=0  & Token_24=1 sync task_12_done do{t_task_14 := 0,Token_12 := 0} goto t_14_running;
		when t_task_12 = C_task_12 & Token_14=0  & Token_22=1  & Token_24=1 sync task_12_done do{t_task_22 := 0,Token_12 := 0} goto t_22_running;
		when t_task_12 = C_task_12 & Token_14=1  & Token_22=1  & Token_24=1 sync task_12_done do{t_task_14 := 0,Token_12 := 0} goto t_14_running;
	loc t_14_running: invariant t_task_14 <= C_task_14 stop {t_task_12,t_task_22,t_task_24}
		when t_task_14 < C_task_14 & t_pipeline_1 = D_pipeline_1 sync DEADLINE_MISSED_2 goto DEADLINE_MISS;
		when t_task_14 < C_task_14 & t_pipeline_2 = D_pipeline_2 sync DEADLINE_MISSED_2 goto DEADLINE_MISS;
		 when t_task_14 <= 0 sync task_12_act do{Token_12 := 1}goto t_12_running;
		 when t_task_14 > 0 sync task_12_act do{Token_12 := 1}goto t_14_running;
		 when t_task_14 <= 0 sync task_14_act do{Token_14 := 1}goto t_14_running;
		 when t_task_14 > 0 sync task_14_act do{Token_14 := 1}goto t_14_running;
		 when t_task_14 <= 0 sync task_22_act do{Token_22 := 1}goto t_14_running;
		 when t_task_14 > 0 sync task_22_act do{Token_22 := 1}goto t_14_running;
		 when t_task_14 <= 0 sync task_24_act do{Token_24 := 1}goto t_14_running;
		 when t_task_14 > 0 sync task_24_act do{Token_24 := 1}goto t_14_running;
		when t_task_14 = C_task_14 & Token_12=0  & Token_22=0  & Token_24=0 sync task_14_done do{Token_14 := 0} goto idle;
		when t_task_14 = C_task_14 & Token_12=1  & Token_22=0  & Token_24=0 sync task_14_done do{t_task_12 := 0,Token_14 := 0} goto t_12_running;
		when t_task_14 = C_task_14 & Token_12=0  & Token_22=1  & Token_24=0 sync task_14_done do{t_task_22 := 0,Token_14 := 0} goto t_22_running;
		when t_task_14 = C_task_14 & Token_12=0  & Token_22=0  & Token_24=1 sync task_14_done do{t_task_24 := 0,Token_14 := 0} goto t_24_running;
		when t_task_14 = C_task_14 & Token_12=1  & Token_22=1  & Token_24=0 sync task_14_done do{t_task_12 := 0,Token_14 := 0} goto t_12_running;
		when t_task_14 = C_task_14 & Token_12=1  & Token_22=0  & Token_24=1 sync task_14_done do{t_task_12 := 0,Token_14 := 0} goto t_12_running;
		when t_task_14 = C_task_14 & Token_12=0  & Token_22=1  & Token_24=1 sync task_14_done do{t_task_22 := 0,Token_14 := 0} goto t_22_running;
		when t_task_14 = C_task_14 & Token_12=1  & Token_22=1  & Token_24=1 sync task_14_done do{t_task_12 := 0,Token_14 := 0} goto t_12_running;
	loc t_22_running: invariant t_task_22 <= C_task_22 stop {t_task_12,t_task_14,t_task_24}
		when t_task_22 < C_task_22 & t_pipeline_1 = D_pipeline_1 sync DEADLINE_MISSED_2 goto DEADLINE_MISS;
		when t_task_22 < C_task_22 & t_pipeline_2 = D_pipeline_2 sync DEADLINE_MISSED_2 goto DEADLINE_MISS;
		 when t_task_22 <= 0 sync task_12_act do{Token_12 := 1}goto t_12_running;
		 when t_task_22 > 0 sync task_12_act do{Token_12 := 1}goto t_22_running;
		 when t_task_22 <= 0 sync task_14_act do{Token_14 := 1}goto t_14_running;
		 when t_task_22 > 0 sync task_14_act do{Token_14 := 1}goto t_22_running;
		 when t_task_22 <= 0 sync task_22_act do{Token_22 := 1}goto t_22_running;
		 when t_task_22 > 0 sync task_22_act do{Token_22 := 1}goto t_22_running;
		 when t_task_22 <= 0 sync task_24_act do{Token_24 := 1}goto t_22_running;
		 when t_task_22 > 0 sync task_24_act do{Token_24 := 1}goto t_22_running;
		when t_task_22 = C_task_22 & Token_12=0  & Token_14=0  & Token_24=0 sync task_22_done do{Token_22 := 0} goto idle;
		when t_task_22 = C_task_22 & Token_12=1  & Token_14=0  & Token_24=0 sync task_22_done do{t_task_12 := 0,Token_22 := 0} goto t_12_running;
		when t_task_22 = C_task_22 & Token_12=0  & Token_14=1  & Token_24=0 sync task_22_done do{t_task_14 := 0,Token_22 := 0} goto t_14_running;
		when t_task_22 = C_task_22 & Token_12=0  & Token_14=0  & Token_24=1 sync task_22_done do{t_task_24 := 0,Token_22 := 0} goto t_24_running;
		when t_task_22 = C_task_22 & Token_12=1  & Token_14=1  & Token_24=0 sync task_22_done do{t_task_12 := 0,Token_22 := 0} goto t_12_running;
		when t_task_22 = C_task_22 & Token_12=1  & Token_14=0  & Token_24=1 sync task_22_done do{t_task_12 := 0,Token_22 := 0} goto t_12_running;
		when t_task_22 = C_task_22 & Token_12=0  & Token_14=1  & Token_24=1 sync task_22_done do{t_task_14 := 0,Token_22 := 0} goto t_14_running;
		when t_task_22 = C_task_22 & Token_12=1  & Token_14=1  & Token_24=1 sync task_22_done do{t_task_12 := 0,Token_22 := 0} goto t_12_running;
	loc t_24_running: invariant t_task_24 <= C_task_24 stop {t_task_12,t_task_14,t_task_22}
		when t_task_24 < C_task_24 & t_pipeline_1 = D_pipeline_1 sync DEADLINE_MISSED_2 goto DEADLINE_MISS;
		when t_task_24 < C_task_24 & t_pipeline_2 = D_pipeline_2 sync DEADLINE_MISSED_2 goto DEADLINE_MISS;
		 when t_task_24 <= 0 sync task_12_act do{Token_12 := 1}goto t_12_running;
		 when t_task_24 > 0 sync task_12_act do{Token_12 := 1}goto t_24_running;
		 when t_task_24 <= 0 sync task_14_act do{Token_14 := 1}goto t_14_running;
		 when t_task_24 > 0 sync task_14_act do{Token_14 := 1}goto t_24_running;
		 when t_task_24 <= 0 sync task_22_act do{Token_22 := 1}goto t_22_running;
		 when t_task_24 > 0 sync task_22_act do{Token_22 := 1}goto t_24_running;
		 when t_task_24 <= 0 sync task_24_act do{Token_24 := 1}goto t_24_running;
		 when t_task_24 > 0 sync task_24_act do{Token_24 := 1}goto t_24_running;
		when t_task_24 = C_task_24 & Token_12=0  & Token_14=0  & Token_22=0 sync task_24_done do{Token_24 := 0} goto idle;
		when t_task_24 = C_task_24 & Token_12=1  & Token_14=0  & Token_22=0 sync task_24_done do{t_task_12 := 0,Token_24 := 0} goto t_12_running;
		when t_task_24 = C_task_24 & Token_12=0  & Token_14=1  & Token_22=0 sync task_24_done do{t_task_14 := 0,Token_24 := 0} goto t_14_running;
		when t_task_24 = C_task_24 & Token_12=0  & Token_14=0  & Token_22=1 sync task_24_done do{t_task_22 := 0,Token_24 := 0} goto t_22_running;
		when t_task_24 = C_task_24 & Token_12=1  & Token_14=1  & Token_22=0 sync task_24_done do{t_task_12 := 0,Token_24 := 0} goto t_12_running;
		when t_task_24 = C_task_24 & Token_12=1  & Token_14=0  & Token_22=1 sync task_24_done do{t_task_12 := 0,Token_24 := 0} goto t_12_running;
		when t_task_24 = C_task_24 & Token_12=0  & Token_14=1  & Token_22=1 sync task_24_done do{t_task_14 := 0,Token_24 := 0} goto t_14_running;
		when t_task_24 = C_task_24 & Token_12=1  & Token_14=1  & Token_22=1 sync task_24_done do{t_task_12 := 0,Token_24 := 0} goto t_12_running;
end

automaton proc_3
	 synclabs: DEADLINE_MISSED_3, task_23_act,task_23_done;

	loc DEADLINE_MISS: invariant True
	loc proc_3_0: invariant True stop {t_task_23}
		when True sync task_23_act do {t_task_23 := 0} goto proc_3_1;
	loc proc_3_1: invariant t_task_23 <= C_task_23 stop {}
		when t_task_23 < C_task_23 & t_pipeline_1 = D_pipeline_1 sync DEADLINE_MISSED_3 goto DEADLINE_MISS;
		when t_task_23 < C_task_23 & t_pipeline_2 = D_pipeline_2 sync DEADLINE_MISSED_3 goto DEADLINE_MISS;
		when t_task_23 = C_task_23 sync task_23_done goto proc_3_0;
end

automaton proc_4
	 synclabs: DEADLINE_MISSED_4, task_13_act,task_13_done,task_21_act,task_21_done;

	loc DEADLINE_MISS: invariant True
	loc proc_4_00: invariant True stop {t_task_13,t_task_21}
		when True sync task_13_act do {t_task_13 := 0} goto proc_4_10;
		when True sync task_21_act do {t_task_21 := 0} goto proc_4_01;
	loc proc_4_10: invariant t_task_13 <= C_task_13 stop {t_task_21}
		when t_task_21 < C_task_21 & t_pipeline_1 = D_pipeline_1 sync DEADLINE_MISSED_4 goto DEADLINE_MISS;
		when t_task_21 < C_task_21 & t_pipeline_2 = D_pipeline_2 sync DEADLINE_MISSED_4 goto DEADLINE_MISS;
		when t_task_13 = C_task_13 sync task_13_done goto proc_4_00;
		when t_task_13 < C_task_13 sync task_21_act do {t_task_21 := 0} goto proc_4_11;
	loc proc_4_01: invariant t_task_21 <= C_task_21 stop {t_task_13}
		when t_task_21 < C_task_21 & t_pipeline_1 = D_pipeline_1 sync DEADLINE_MISSED_4 goto DEADLINE_MISS;
		when t_task_21 < C_task_21 & t_pipeline_2 = D_pipeline_2 sync DEADLINE_MISSED_4 goto DEADLINE_MISS;
		when t_task_21 < C_task_21 sync task_13_act do {t_task_13 := 0} goto proc_4_11;
		when t_task_21 = C_task_21 sync task_21_done goto proc_4_00;
	loc proc_4_11: invariant t_task_13 <= C_task_13 stop {t_task_21}
		when t_task_21 < C_task_21 & t_pipeline_1 = D_pipeline_1 sync DEADLINE_MISSED_4 goto DEADLINE_MISS;
		when t_task_21 < C_task_21 & t_pipeline_2 = D_pipeline_2 sync DEADLINE_MISSED_4 goto DEADLINE_MISS;
		when t_task_13 = C_task_13 sync task_13_done goto proc_4_01;
		when t_task_21 = C_task_21 sync task_21_done goto proc_4_10;
end



init:= True &
	loc[proc_1]= proc_1_000 &
	loc[proc_2]= idle &
	loc[proc_3]= proc_3_0 &
	loc[proc_4]= proc_4_00 &
	loc[pipeline_1]=P1_1 &
	loc[pipeline_2]=P2_1 &
	t_asap_1 = 0 &
	t_pipeline_1 = 0 &
	t_task_11 = 0 & 
	t_task_12 = 0 & 
	t_task_13 = 0 & 
	t_task_14 = 0 & 
	t_task_15 = 0 & 
	t_asap_2 = 0 &
	t_pipeline_2 = 0 &
	t_task_21 = 0 & 
	t_task_22 = 0 & 
	t_task_23 = 0 & 
	t_task_24 = 0 & 
	t_task_25 = 0 & 
	Token_11 = 0 & 
	Token_12 = 0 & 
	Token_13 = 0 & 
	Token_14 = 0 & 
	Token_15 = 0 & 
	Token_21 = 0 & 
	Token_22 = 0 & 
	Token_23 = 0 & 
	Token_24 = 0 & 
	Token_25 = 0 & 
	True
	
	& T_pipeline_1 >= 0
	& D_pipeline_1 >= 0
	& C_task_11 >= 0
	& C_task_12>= 0
	& C_task_13 >= 0
	& C_task_14 >= 0
	& C_task_15 >= 0
	& T_pipeline_2 >= 0
	& D_pipeline_2 >= 0
	& C_task_21 >= 0
	& C_task_22 >= 0
	& C_task_23 >= 0
	& C_task_24 >= 0
	& C_task_25 >= 0
;

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