(************************************************************
 *                      IMITATOR MODEL                      
 *
 * References: ''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
              
 * Note: might not be the final model of the paper (?)
 
 * Last modified: 2015/10/30
 ************************************************************)

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: while t_asap_1 <= 0 wait
		 when t_asap_1=0 sync task_11_act goto P1_2;
	loc P1_2: while t_pipeline_1 <= D_pipeline_1 wait
		 when t_pipeline_1 <= D_pipeline_1 sync task_11_done do {t_asap_1'=0} goto P1_3;
	loc P1_3: while t_asap_1 <= 0 wait
		 when t_asap_1=0 sync task_12_act goto P1_4;
	loc P1_4: while t_pipeline_1 <= D_pipeline_1 wait
		 when t_pipeline_1 <= D_pipeline_1 sync task_12_done do {t_asap_1'=0} goto P1_5;
	loc P1_5: while t_asap_1 <= 0 wait
		 when t_asap_1=0 sync task_13_act goto P1_6;
	loc P1_6: while t_pipeline_1 <= D_pipeline_1 wait
		 when t_pipeline_1 <= D_pipeline_1 sync task_13_done do {t_asap_1'=0} goto P1_7;
	loc P1_7: while t_asap_1 <= 0 wait
		 when t_asap_1=0 sync task_14_act goto P1_8;
	loc P1_8: while t_pipeline_1 <= D_pipeline_1 wait
		 when t_pipeline_1 <= D_pipeline_1 sync task_14_done do {t_asap_1'=0} goto P1_9;
	loc P1_9: while t_asap_1 <= 0 wait
		 when t_asap_1=0 sync task_15_act goto P1_10;
	loc P1_10: while t_pipeline_1 <= D_pipeline_1 wait
		 when t_pipeline_1 <= D_pipeline_1 sync task_15_done do {t_asap_1'=0} goto P1_11;
	loc P1_11: while t_pipeline_1 <= T_pipeline_1 wait
		 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: while t_asap_2 <= 0 wait
		 when t_asap_2=0 sync task_21_act goto P2_2;
	loc P2_2: while t_pipeline_2 <= D_pipeline_2 wait
		 when t_pipeline_2 <= D_pipeline_2 sync task_21_done do {t_asap_2'=0} goto P2_3;
	loc P2_3: while t_asap_2 <= 0 wait
		 when t_asap_2=0 sync task_22_act goto P2_4;
	loc P2_4: while t_pipeline_2 <= D_pipeline_2 wait
		 when t_pipeline_2 <= D_pipeline_2 sync task_22_done do {t_asap_2'=0} goto P2_5;
	loc P2_5: while t_asap_2 <= 0 wait
		 when t_asap_2=0 sync task_23_act goto P2_6;
	loc P2_6: while t_pipeline_2 <= D_pipeline_2 wait
		 when t_pipeline_2 <= D_pipeline_2 sync task_23_done do {t_asap_2'=0} goto P2_7;
	loc P2_7: while t_asap_2 <= 0 wait
		 when t_asap_2=0 sync task_24_act goto P2_8;
	loc P2_8: while t_pipeline_2 <= D_pipeline_2 wait
		 when t_pipeline_2 <= D_pipeline_2 sync task_24_done do {t_asap_2'=0} goto P2_9;
	loc P2_9: while t_asap_2 <= 0 wait
		 when t_asap_2=0 sync task_25_act goto P2_10;
	loc P2_10: while t_pipeline_2 <= D_pipeline_2 wait
		 when t_pipeline_2 <= D_pipeline_2 sync task_25_done do {t_asap_2'=0} goto P2_11;
	loc P2_11: while t_pipeline_2 <= T_pipeline_2 wait
		 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: while True wait
	loc proc_1_000: while True stop {t_task_11,t_task_15,t_task_25} wait
		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: while t_task_11 <= C_task_11 stop {t_task_15,t_task_25} wait
		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: while t_task_15 <= C_task_15 stop {t_task_11,t_task_25} wait
		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: while t_task_25 <= C_task_25 stop {t_task_11,t_task_15} wait
		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: while t_task_11 <= C_task_11 stop {t_task_15,t_task_25} wait
		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: while t_task_11 <= C_task_11 stop {t_task_15,t_task_25} wait
		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: while t_task_15 <= C_task_15 stop {t_task_11,t_task_25} wait
		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: while t_task_11 <= C_task_11 stop {t_task_15,t_task_25} wait
		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: while True stop{t_task_12,t_task_14,t_task_22,t_task_24} wait
		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: while True wait
	loc t_12_running: while t_task_12 <= C_task_12 stop {t_task_14,t_task_22,t_task_24} wait
		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: while t_task_14 <= C_task_14 stop {t_task_12,t_task_22,t_task_24} wait
		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: while t_task_22 <= C_task_22 stop {t_task_12,t_task_14,t_task_24} wait
		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: while t_task_24 <= C_task_24 stop {t_task_12,t_task_14,t_task_22} wait
		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: while True wait
	loc proc_3_0: while True stop {t_task_23} wait
		when True sync task_23_act do {t_task_23'=0} goto proc_3_1;
	loc proc_3_1: while t_task_23 <= C_task_23 stop {} wait
		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: while True wait
	loc proc_4_00: while True stop {t_task_13,t_task_21} wait
		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: while t_task_13 <= C_task_13 stop {t_task_21} wait
		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: while t_task_21 <= C_task_21 stop {t_task_13} wait
		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: while t_task_13 <= C_task_13 stop {t_task_21} wait
		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

var init:region;
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
;

property := unreachable(loc[proc_1] = DEADLINE_MISS)
	or
	(loc[proc_2] = DEADLINE_MISS)
	or
	(loc[proc_3] = DEADLINE_MISS)
;