(******************************************************************************* * 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 : 2021/10/07 * Model version : * * IMITATOR version : 3.1 ******************************************************************************) var t_asap_1:clock; t_pipeline_1:clock; t_task_11:clock; (* Token_11:discrete; *) t_task_12:clock; Token_12:bool; t_task_13:clock; (* Token_13:discrete; *) t_task_14:clock; Token_14:bool; 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:bool; t_task_23:clock; (* Token_23:discrete; *) t_task_24:clock; Token_24:bool; 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 actions: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 actions: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 actions: 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 actions: 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 := True}goto t_12_running; when True sync task_14_act do{Token_14 := True}goto t_14_running; when True sync task_22_act do{Token_22 := True}goto t_22_running; when True sync task_24_act do{Token_24 := True}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 := True}goto t_12_running; when t_task_12 > 0 sync task_12_act do{Token_12 := True}goto t_12_running; when t_task_12 <= 0 sync task_14_act do{Token_14 := True}goto t_12_running; when t_task_12 > 0 sync task_14_act do{Token_14 := True}goto t_12_running; when t_task_12 <= 0 sync task_22_act do{Token_22 := True}goto t_12_running; when t_task_12 > 0 sync task_22_act do{Token_22 := True}goto t_12_running; when t_task_12 <= 0 sync task_24_act do{Token_24 := True}goto t_12_running; when t_task_12 > 0 sync task_24_act do{Token_24 := True}goto t_12_running; when t_task_12 = C_task_12 & not(Token_14) & not(Token_22) & not(Token_24) sync task_12_done do{Token_12 := False} goto idle; when t_task_12 = C_task_12 & Token_14 & not(Token_22) & not(Token_24) sync task_12_done do{t_task_14 := 0,Token_12 := False} goto t_14_running; when t_task_12 = C_task_12 & not(Token_14) & Token_22 & not(Token_24) sync task_12_done do{t_task_22 := 0,Token_12 := False} goto t_22_running; when t_task_12 = C_task_12 & not(Token_14) & not(Token_22) & Token_24 sync task_12_done do{t_task_24 := 0,Token_12 := False} goto t_24_running; when t_task_12 = C_task_12 & Token_14 & Token_22 & not(Token_24) sync task_12_done do{t_task_14 := 0,Token_12 := False} goto t_14_running; when t_task_12 = C_task_12 & Token_14 & not(Token_22) & Token_24 sync task_12_done do{t_task_14 := 0,Token_12 := False} goto t_14_running; when t_task_12 = C_task_12 & not(Token_14) & Token_22 & Token_24 sync task_12_done do{t_task_22 := 0,Token_12 := False} goto t_22_running; when t_task_12 = C_task_12 & Token_14 & Token_22 & Token_24 sync task_12_done do{t_task_14 := 0,Token_12 := False} 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 := True}goto t_12_running; when t_task_14 > 0 sync task_12_act do{Token_12 := True}goto t_14_running; when t_task_14 <= 0 sync task_14_act do{Token_14 := True}goto t_14_running; when t_task_14 > 0 sync task_14_act do{Token_14 := True}goto t_14_running; when t_task_14 <= 0 sync task_22_act do{Token_22 := True}goto t_14_running; when t_task_14 > 0 sync task_22_act do{Token_22 := True}goto t_14_running; when t_task_14 <= 0 sync task_24_act do{Token_24 := True}goto t_14_running; when t_task_14 > 0 sync task_24_act do{Token_24 := True}goto t_14_running; when t_task_14 = C_task_14 & not(Token_12) & not(Token_22) & not(Token_24) sync task_14_done do{Token_14 := False} goto idle; when t_task_14 = C_task_14 & Token_12 & not(Token_22) & not(Token_24) sync task_14_done do{t_task_12 := 0,Token_14 := False} goto t_12_running; when t_task_14 = C_task_14 & not(Token_12) & Token_22 & not(Token_24) sync task_14_done do{t_task_22 := 0,Token_14 := False} goto t_22_running; when t_task_14 = C_task_14 & not(Token_12) & not(Token_22) & Token_24 sync task_14_done do{t_task_24 := 0,Token_14 := False} goto t_24_running; when t_task_14 = C_task_14 & Token_12 & Token_22 & not(Token_24) sync task_14_done do{t_task_12 := 0,Token_14 := False} goto t_12_running; when t_task_14 = C_task_14 & Token_12 & not(Token_22) & Token_24 sync task_14_done do{t_task_12 := 0,Token_14 := False} goto t_12_running; when t_task_14 = C_task_14 & not(Token_12) & Token_22 & Token_24 sync task_14_done do{t_task_22 := 0,Token_14 := False} goto t_22_running; when t_task_14 = C_task_14 & Token_12 & Token_22 & Token_24 sync task_14_done do{t_task_12 := 0,Token_14 := False} 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 := True}goto t_12_running; when t_task_22 > 0 sync task_12_act do{Token_12 := True}goto t_22_running; when t_task_22 <= 0 sync task_14_act do{Token_14 := True}goto t_14_running; when t_task_22 > 0 sync task_14_act do{Token_14 := True}goto t_22_running; when t_task_22 <= 0 sync task_22_act do{Token_22 := True}goto t_22_running; when t_task_22 > 0 sync task_22_act do{Token_22 := True}goto t_22_running; when t_task_22 <= 0 sync task_24_act do{Token_24 := True}goto t_22_running; when t_task_22 > 0 sync task_24_act do{Token_24 := True}goto t_22_running; when t_task_22 = C_task_22 & not(Token_12) & not(Token_14) & not(Token_24) sync task_22_done do{Token_22 := False} goto idle; when t_task_22 = C_task_22 & Token_12 & not(Token_14) & not(Token_24) sync task_22_done do{t_task_12 := 0,Token_22 := False} goto t_12_running; when t_task_22 = C_task_22 & not(Token_12) & Token_14 & not(Token_24) sync task_22_done do{t_task_14 := 0,Token_22 := False} goto t_14_running; when t_task_22 = C_task_22 & not(Token_12) & not(Token_14) & Token_24 sync task_22_done do{t_task_24 := 0,Token_22 := False} goto t_24_running; when t_task_22 = C_task_22 & Token_12 & Token_14 & not(Token_24) sync task_22_done do{t_task_12 := 0,Token_22 := False} goto t_12_running; when t_task_22 = C_task_22 & Token_12 & not(Token_14) & Token_24 sync task_22_done do{t_task_12 := 0,Token_22 := False} goto t_12_running; when t_task_22 = C_task_22 & not(Token_12) & Token_14 & Token_24 sync task_22_done do{t_task_14 := 0,Token_22 := False} goto t_14_running; when t_task_22 = C_task_22 & Token_12 & Token_14 & Token_24 sync task_22_done do{t_task_12 := 0,Token_22 := False} 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 := True}goto t_12_running; when t_task_24 > 0 sync task_12_act do{Token_12 := True}goto t_24_running; when t_task_24 <= 0 sync task_14_act do{Token_14 := True}goto t_14_running; when t_task_24 > 0 sync task_14_act do{Token_14 := True}goto t_24_running; when t_task_24 <= 0 sync task_22_act do{Token_22 := True}goto t_22_running; when t_task_24 > 0 sync task_22_act do{Token_22 := True}goto t_24_running; when t_task_24 <= 0 sync task_24_act do{Token_24 := True}goto t_24_running; when t_task_24 > 0 sync task_24_act do{Token_24 := True}goto t_24_running; when t_task_24 = C_task_24 & not(Token_12) & not(Token_14) & not(Token_22) sync task_24_done do{Token_24 := False} goto idle; when t_task_24 = C_task_24 & Token_12 & not(Token_14) & not(Token_22) sync task_24_done do{t_task_12 := 0,Token_24 := False} goto t_12_running; when t_task_24 = C_task_24 & not(Token_12) & Token_14 & not(Token_22) sync task_24_done do{t_task_14 := 0,Token_24 := False} goto t_14_running; when t_task_24 = C_task_24 & not(Token_12) & not(Token_14) & Token_22 sync task_24_done do{t_task_22 := 0,Token_24 := False} goto t_22_running; when t_task_24 = C_task_24 & Token_12 & Token_14 & not(Token_22) sync task_24_done do{t_task_12 := 0,Token_24 := False} goto t_12_running; when t_task_24 = C_task_24 & Token_12 & not(Token_14) & Token_22 sync task_24_done do{t_task_12 := 0,Token_24 := False} goto t_12_running; when t_task_24 = C_task_24 & not(Token_12) & Token_14 & Token_22 sync task_24_done do{t_task_14 := 0,Token_24 := False} goto t_14_running; when t_task_24 = C_task_24 & Token_12 & Token_14 & Token_22 sync task_24_done do{t_task_12 := 0,Token_24 := False} goto t_12_running; end automaton proc_3 actions: 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 actions: 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:= { discrete = 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, (* Token_11 := 0, *) Token_12 := False, (* Token_13 := 0, *) Token_14 := False, (* Token_15 := 0, *) (* Token_21 := 0, *) Token_22 := False, (* Token_23 := 0, *) Token_24 := False, (* Token_25 := 0, *) ; continuous = 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 & 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