/*************************************************** * File automatically generated by IMITATOR 2.5.0 for model 'examples/Scheduling/am02.imi' * The following pi0 was considered: wcet_m2_job2 = 5 & wcet_m1_job1 = 3 & wcet_m2_job1 = 2 & wcet_m3_job1 = 4 * 53 states and 70 transitions * Program terminated after 0.091 second ***************************************************/ DESCRIPTION OF THE STATES STATE 0: checker: nop, job1: m1_begin, job2: m2_begin ==> & wcet_m2_job2 + wcet_m1_job1 + wcet_m2_job1 >= 10 & wcet_m2_job2 + wcet_m2_job1 + wcet_m3_job1 >= 10 & c1 >= 0 & 10 >= c1 & c2 = 0 & c1 = time STATE 1: checker: error, job1: m1_begin, job2: m2_begin ==> & wcet_m2_job2 + wcet_m1_job1 + wcet_m2_job1 >= 10 & wcet_m2_job2 + wcet_m2_job1 + wcet_m3_job1 >= 10 & c2 = 0 & c1 = 10 & time = 10 STATE 2: checker: nop, job1: m1_running, job2: m2_begin ==> & wcet_m2_job2 + wcet_m1_job1 + wcet_m2_job1 >= 10 & wcet_m2_job2 + wcet_m2_job1 + wcet_m3_job1 >= 10 & wcet_m1_job1 >= c1 & c1 >= 0 & c1 + 10 > time & 10 >= time & time >= c1 & c2 = 0 STATE 3: checker: nop, job1: m1_begin, job2: m2_running ==> & wcet_m2_job2 + wcet_m1_job1 + wcet_m2_job1 >= 10 & wcet_m2_job2 + wcet_m2_job1 + wcet_m3_job1 >= 10 & wcet_m2_job2 >= c2 & c2 >= 0 & c2 + 10 > c1 & 10 >= c1 & c1 >= c2 & c1 = time STATE 4: checker: error, job1: m1_running, job2: m2_begin ==> & wcet_m2_job2 + wcet_m1_job1 + wcet_m2_job1 >= 10 & wcet_m2_job2 + wcet_m2_job1 + wcet_m3_job1 >= 10 & wcet_m1_job1 >= c1 & c1 > 0 & 10 >= c1 & c2 = 0 & time = 10 STATE 5: checker: nop, job1: m2_begin, job2: m2_begin ==> & wcet_m2_job2 + wcet_m1_job1 + wcet_m2_job1 >= 10 & wcet_m2_job2 + wcet_m2_job1 + wcet_m3_job1 >= 10 & wcet_m1_job1 >= 0 & 10 >= time & time >= wcet_m1_job1 & 10 > wcet_m1_job1 & c2 = 0 & wcet_m1_job1 = c1 STATE 6: checker: nop, job1: m1_running, job2: m2_running ==> & wcet_m2_job2 + wcet_m1_job1 + wcet_m2_job1 >= 10 & wcet_m2_job2 + wcet_m2_job1 + wcet_m3_job1 >= 10 & wcet_m2_job2 >= c2 & wcet_m1_job1 >= c1 & c2 >= 0 & c2 + 10 > time & c1 >= 0 & c1 + 10 > time & 10 >= time & time >= c1 & time >= c2 STATE 7: checker: error, job1: m1_begin, job2: m2_running ==> & wcet_m2_job2 + wcet_m1_job1 + wcet_m2_job1 >= 10 & wcet_m2_job2 + wcet_m2_job1 + wcet_m3_job1 >= 10 & wcet_m2_job2 >= c2 & c2 > 0 & 10 >= c2 & c1 = 10 & time = 10 STATE 8: checker: nop_1, job1: m1_begin, job2: finished ==> & wcet_m2_job2 + wcet_m1_job1 + wcet_m2_job1 >= 10 & wcet_m2_job2 + wcet_m2_job1 + wcet_m3_job1 >= 10 & wcet_m2_job2 >= 0 & 10 >= c1 & c1 >= wcet_m2_job2 & 10 > wcet_m2_job2 & wcet_m2_job2 = c2 & c1 = time STATE 10: checker: error, job1: m1_running, job2: m2_running ==> & wcet_m2_job2 + wcet_m1_job1 + wcet_m2_job1 >= 10 & wcet_m2_job2 + wcet_m2_job1 + wcet_m3_job1 >= 10 & wcet_m2_job2 >= c2 & wcet_m1_job1 >= c1 & c2 > 0 & c1 > 0 & 10 >= c1 & 10 >= c2 & time = 10 STATE 11: checker: nop_1, job1: m1_running, job2: finished ==> & wcet_m2_job2 + wcet_m1_job1 + wcet_m2_job1 >= 10 & wcet_m2_job2 + wcet_m2_job1 + wcet_m3_job1 >= 10 & wcet_m2_job2 >= 0 & wcet_m1_job1 >= c1 & c1 >= 0 & c1 + 10 > time & 10 >= time & time >= c1 & time >= wcet_m2_job2 & 10 > wcet_m2_job2 & wcet_m2_job2 = c2 STATE 13: checker: error, job1: m2_begin, job2: m2_begin ==> & wcet_m2_job2 + wcet_m1_job1 + wcet_m2_job1 >= 10 & wcet_m2_job2 + wcet_m2_job1 + wcet_m3_job1 >= 10 & wcet_m1_job1 >= 0 & 10 > wcet_m1_job1 & c2 = 0 & wcet_m1_job1 = c1 & time = 10 STATE 14: checker: nop, job1: m2_running, job2: m2_begin ==> & wcet_m2_job2 + wcet_m1_job1 + wcet_m2_job1 >= 10 & wcet_m2_job2 + wcet_m2_job1 + wcet_m3_job1 >= 10 & wcet_m1_job1 >= 0 & wcet_m2_job1 >= c1 & c1 >= 0 & c1 + 10 > time & 10 >= time & time >= wcet_m1_job1 + c1 & c2 = 0 STATE 15: checker: nop, job1: m2_begin, job2: m2_running ==> & wcet_m2_job2 + wcet_m1_job1 + wcet_m2_job1 >= 10 & wcet_m2_job2 + wcet_m2_job1 + wcet_m3_job1 >= 10 & wcet_m2_job2 >= c2 & wcet_m1_job1 >= 0 & c2 >= 0 & c2 + 10 > time & 10 >= time & time >= c2 & time >= wcet_m1_job1 & 10 > wcet_m1_job1 & wcet_m1_job1 = c1 STATE 16: checker: error, job1: m1_begin, job2: finished ==> & wcet_m2_job2 + wcet_m1_job1 + wcet_m2_job1 >= 10 & wcet_m2_job2 + wcet_m2_job1 + wcet_m3_job1 >= 10 & wcet_m2_job2 >= 0 & 10 > wcet_m2_job2 & wcet_m2_job2 = c2 & c1 = 10 & time = 10 STATE 18: checker: error, job1: m2_begin, job2: m2_running ==> & wcet_m2_job2 + wcet_m1_job1 + wcet_m2_job1 >= 10 & wcet_m2_job2 + wcet_m2_job1 + wcet_m3_job1 >= 10 & wcet_m2_job2 >= c2 & wcet_m1_job1 >= 0 & c2 > 0 & 10 >= c2 & 10 > wcet_m1_job1 & wcet_m1_job1 = c1 & time = 10 STATE 19: checker: nop_1, job1: m2_begin, job2: finished ==> & wcet_m2_job2 + wcet_m1_job1 + wcet_m2_job1 >= 10 & wcet_m2_job2 + wcet_m2_job1 + wcet_m3_job1 >= 10 & wcet_m2_job2 >= 0 & wcet_m1_job1 >= 0 & 10 >= time & time >= wcet_m1_job1 & 10 > wcet_m1_job1 & time >= wcet_m2_job2 & 10 > wcet_m2_job2 & wcet_m2_job2 = c2 & wcet_m1_job1 = c1 STATE 21: checker: error, job1: m2_running, job2: m2_begin ==> & wcet_m2_job2 + wcet_m1_job1 + wcet_m2_job1 >= 10 & wcet_m2_job2 + wcet_m2_job1 + wcet_m3_job1 >= 10 & wcet_m1_job1 >= 0 & wcet_m2_job1 >= c1 & c1 > 0 & 10 >= wcet_m1_job1 + c1 & c2 = 0 & time = 10 STATE 22: checker: nop, job1: m3_begin, job2: m2_begin ==> & wcet_m2_job2 + wcet_m1_job1 + wcet_m2_job1 >= 10 & wcet_m2_job2 + wcet_m2_job1 + wcet_m3_job1 >= 10 & wcet_m1_job1 >= 0 & wcet_m2_job1 >= 0 & 10 >= time & time >= wcet_m1_job1 + wcet_m2_job1 & 10 > wcet_m1_job1 + wcet_m2_job1 & c2 = 0 & wcet_m2_job1 = c1 STATE 23: checker: nop, job1: m2_preempted, job2: m2_running ==> & wcet_m2_job2 + wcet_m1_job1 + wcet_m2_job1 >= 10 & wcet_m2_job2 + wcet_m2_job1 + wcet_m3_job1 >= 10 & wcet_m2_job2 >= c2 & wcet_m1_job1 >= 0 & wcet_m2_job1 > c1 & c2 >= 0 & c2 + 10 > time & c1 >= 0 & 10 >= time & time >= wcet_m1_job1 + c2 + c1 STATE 24: checker: error, job1: m1_running, job2: finished ==> & wcet_m2_job2 + wcet_m1_job1 + wcet_m2_job1 >= 10 & wcet_m2_job2 + wcet_m2_job1 + wcet_m3_job1 >= 10 & wcet_m2_job2 >= 0 & wcet_m1_job1 >= c1 & c1 > 0 & 10 >= c1 & 10 > wcet_m2_job2 & wcet_m2_job2 = c2 & time = 10 STATE 25: checker: error, job1: m2_running, job2: m2_preempted ==> & wcet_m2_job2 + wcet_m2_job1 + wcet_m3_job1 >= 10 & wcet_m2_job2 + wcet_m1_job1 + wcet_m2_job1 >= 10 & wcet_m2_job2 > c2 & wcet_m1_job1 >= 0 & wcet_m2_job1 >= c1 & c2 >= 0 & c1 > 0 & 10 >= c2 + c1 & 10 >= wcet_m1_job1 + c1 & time = 10 STATE 26: checker: nop, job1: m3_begin, job2: m2_preempted ==> & wcet_m2_job2 + wcet_m2_job1 + wcet_m3_job1 >= 10 & wcet_m2_job2 + wcet_m1_job1 + wcet_m2_job1 >= 10 & wcet_m2_job2 > c2 & wcet_m1_job1 >= 0 & wcet_m2_job1 >= 0 & c2 >= 0 & 10 >= time & time >= wcet_m2_job1 + c2 & 10 > wcet_m2_job1 + c2 & time >= wcet_m1_job1 + wcet_m2_job1 & 10 > wcet_m1_job1 + wcet_m2_job1 & wcet_m2_job1 = c1 STATE 27: checker: nop, job1: m2_preempted, job2: m2_running ==> & wcet_m2_job2 + wcet_m2_job1 + wcet_m3_job1 >= 10 & wcet_m2_job2 + wcet_m1_job1 + wcet_m2_job1 >= 10 & wcet_m2_job2 > 0 & wcet_m2_job2 >= c2 & wcet_m2_job2 + time > wcet_m1_job1 + c2 + c1 & wcet_m1_job1 >= 0 & wcet_m2_job1 > c1 & c2 >= 0 & c2 + 10 > time & c1 >= 0 & 10 >= time & time >= c2 + c1 & time >= wcet_m1_job1 + c1 & 10 > wcet_m1_job1 + c1 STATE 28: checker: error, job1: m2_begin, job2: finished ==> & wcet_m2_job2 + wcet_m1_job1 + wcet_m2_job1 >= 10 & wcet_m2_job2 + wcet_m2_job1 + wcet_m3_job1 >= 10 & wcet_m2_job2 >= 0 & wcet_m1_job1 >= 0 & 10 > wcet_m1_job1 & 10 > wcet_m2_job2 & wcet_m2_job2 = c2 & wcet_m1_job1 = c1 & time = 10 STATE 30: checker: error, job1: m3_begin, job2: m2_begin ==> & wcet_m2_job2 + wcet_m1_job1 + wcet_m2_job1 >= 10 & wcet_m2_job2 + wcet_m2_job1 + wcet_m3_job1 >= 10 & wcet_m1_job1 >= 0 & wcet_m2_job1 >= 0 & 10 > wcet_m1_job1 + wcet_m2_job1 & c2 = 0 & wcet_m2_job1 = c1 & time = 10 STATE 31: checker: nop, job1: m3_running, job2: m2_begin ==> & wcet_m2_job2 + wcet_m1_job1 + wcet_m2_job1 >= 10 & wcet_m2_job2 + wcet_m2_job1 + wcet_m3_job1 >= 10 & wcet_m1_job1 >= 0 & wcet_m2_job1 >= 0 & wcet_m3_job1 >= c1 & c1 >= 0 & c1 + 10 > time & 10 >= time & time >= wcet_m1_job1 + wcet_m2_job1 + c1 & c2 = 0 STATE 34: checker: nop_1, job1: m2_preempted, job2: finished ==> & wcet_m2_job2 + wcet_m2_job1 + wcet_m3_job1 >= 10 & wcet_m2_job2 + wcet_m1_job1 + wcet_m2_job1 >= 10 & wcet_m2_job2 >= 0 & wcet_m1_job1 >= 0 & c1 >= 0 & 10 >= time & time >= wcet_m2_job2 + wcet_m1_job1 + c1 & 10 > wcet_m2_job2 + wcet_m1_job1 + c1 & wcet_m2_job2 = c2 STATE 38: checker: error, job1: m3_running, job2: m2_begin ==> & wcet_m2_job2 + wcet_m2_job1 + wcet_m3_job1 >= 10 & wcet_m2_job2 + wcet_m1_job1 + wcet_m2_job1 >= 10 & wcet_m1_job1 >= 0 & wcet_m2_job1 >= 0 & wcet_m3_job1 >= c1 & c1 > 0 & 10 >= wcet_m1_job1 + wcet_m2_job1 + c1 & c2 = 0 & time = 10 STATE 39: checker: nop_1, job1: finished, job2: m2_begin ==> & wcet_m2_job2 + wcet_m2_job1 + wcet_m3_job1 >= 10 & wcet_m2_job2 + wcet_m1_job1 + wcet_m2_job1 >= 10 & wcet_m1_job1 >= 0 & wcet_m2_job1 >= 0 & wcet_m3_job1 >= 0 & 10 >= time & time >= wcet_m1_job1 + wcet_m2_job1 + wcet_m3_job1 & 10 > wcet_m1_job1 + wcet_m2_job1 + wcet_m3_job1 & c2 = 0 & wcet_m3_job1 = c1 STATE 41: checker: error, job1: m2_preempted, job2: m2_running ==> & wcet_m2_job2 + wcet_m2_job1 + wcet_m3_job1 >= 10 & wcet_m2_job2 + wcet_m1_job1 + wcet_m2_job1 >= 10 & wcet_m2_job2 >= c2 & wcet_m1_job1 >= 0 & wcet_m2_job1 > c1 & c2 > 0 & c1 >= 0 & 10 >= c2 + c1 & 10 > wcet_m1_job1 + c1 & time = 10 STATE 42: checker: nop_1, job1: m2_preempted, job2: finished ==> & wcet_m2_job2 + wcet_m2_job1 + wcet_m3_job1 >= 10 & wcet_m2_job2 + wcet_m1_job1 + wcet_m2_job1 >= 10 & wcet_m2_job2 > 0 & wcet_m1_job1 >= 0 & wcet_m2_job1 > c1 & c1 >= 0 & 10 >= time & time > wcet_m1_job1 + c1 & 10 > wcet_m1_job1 + c1 & time >= wcet_m2_job2 + c1 & 10 > wcet_m2_job2 + c1 & wcet_m2_job2 = c2 STATE 43: checker: nop, job1: m2_running, job2: m2_preempted ==> & wcet_m2_job2 + wcet_m2_job1 + wcet_m3_job1 >= 10 & wcet_m2_job2 + wcet_m1_job1 + wcet_m2_job1 >= 10 & wcet_m2_job2 > c2 & wcet_m1_job1 >= 0 & wcet_m2_job1 >= c1 & c2 >= 0 & c1 >= 0 & c1 + 10 > time & 10 >= time & time >= c2 + c1 & time >= wcet_m1_job1 + c1 STATE 44: checker: error, job1: m3_begin, job2: m2_preempted ==> & wcet_m2_job2 + wcet_m2_job1 + wcet_m3_job1 >= 10 & wcet_m2_job2 + wcet_m1_job1 + wcet_m2_job1 >= 10 & wcet_m2_job2 > c2 & wcet_m1_job1 >= 0 & wcet_m2_job1 >= 0 & c2 >= 0 & 10 > wcet_m2_job1 + c2 & 10 > wcet_m1_job1 + wcet_m2_job1 & wcet_m2_job1 = c1 & time = 10 STATE 45: checker: nop, job1: m3_running, job2: m2_preempted ==> & wcet_m2_job2 + wcet_m2_job1 + wcet_m3_job1 >= 10 & wcet_m2_job2 + wcet_m1_job1 + wcet_m2_job1 >= 10 & wcet_m2_job2 > c2 & wcet_m1_job1 >= 0 & wcet_m2_job1 >= 0 & wcet_m3_job1 >= c1 & c2 >= 0 & c1 >= 0 & c1 + 10 > time & 10 >= time & time >= wcet_m2_job1 + c2 + c1 & time >= wcet_m1_job1 + wcet_m2_job1 + c1 STATE 46: checker: nop, job1: m3_begin, job2: m2_running ==> & wcet_m2_job2 + wcet_m2_job1 + wcet_m3_job1 >= 10 & wcet_m2_job2 + wcet_m1_job1 + wcet_m2_job1 >= 10 & wcet_m2_job2 >= c2 & wcet_m2_job2 + time > wcet_m1_job1 + wcet_m2_job1 + c2 & wcet_m1_job1 >= 0 & wcet_m2_job1 >= 0 & c2 >= 0 & c2 + 10 > time & 10 >= time & time >= wcet_m2_job1 + c2 & time >= wcet_m1_job1 + wcet_m2_job1 & 10 > wcet_m1_job1 + wcet_m2_job1 & wcet_m2_job1 = c1 STATE 47: checker: error, job1: m2_running, job2: finished ==> & wcet_m2_job2 + wcet_m2_job1 + wcet_m3_job1 >= 10 & wcet_m2_job2 + wcet_m1_job1 + wcet_m2_job1 >= 10 & wcet_m2_job2 >= 0 & wcet_m1_job1 >= 0 & wcet_m2_job1 >= c1 & c1 > 0 & 10 >= wcet_m1_job1 + c1 & 10 >= wcet_m2_job2 + c1 & wcet_m2_job2 = c2 & time = 10 STATE 51: checker: error, job1: m3_begin, job2: finished ==> & wcet_m2_job2 + wcet_m2_job1 + wcet_m3_job1 >= 10 & wcet_m2_job2 + wcet_m1_job1 + wcet_m2_job1 >= 10 & wcet_m2_job1 >= 0 & 10 > wcet_m1_job1 + wcet_m2_job1 & 10 > wcet_m2_job2 + wcet_m2_job1 & wcet_m2_job2 = c2 & wcet_m2_job1 = c1 & time = 10 STATE 53: checker: error, job1: m2_preempted, job2: finished ==> & wcet_m2_job2 + wcet_m2_job1 + wcet_m3_job1 >= 10 & wcet_m2_job2 + wcet_m1_job1 + wcet_m2_job1 >= 10 & wcet_m2_job2 >= 0 & wcet_m1_job1 >= 0 & wcet_m2_job1 > c1 & c1 >= 0 & 10 > wcet_m1_job1 + c1 & 10 > wcet_m2_job2 + c1 & 100 > wcet_m2_job2 + 9*wcet_m1_job1 + 9*c1 & wcet_m2_job2 = c2 & time = 10 STATE 54: checker: nop_1, job1: m2_running, job2: finished ==> & wcet_m2_job2 + wcet_m2_job1 + wcet_m3_job1 >= 10 & wcet_m2_job2 + wcet_m1_job1 + wcet_m2_job1 >= 10 & wcet_m2_job2 >= 0 & wcet_m1_job1 >= 0 & wcet_m2_job1 >= c1 & c1 >= 0 & c1 + 10 > time & 10 >= time & time >= wcet_m1_job1 + c1 & time >= wcet_m2_job2 + c1 & wcet_m2_job2 = c2 STATE 57: checker: error, job1: finished, job2: m2_begin ==> & wcet_m2_job2 + wcet_m2_job1 + wcet_m3_job1 >= 10 & wcet_m2_job2 + wcet_m1_job1 + wcet_m2_job1 >= 10 & wcet_m1_job1 >= 0 & wcet_m2_job1 >= 0 & wcet_m3_job1 >= 0 & 10 > wcet_m1_job1 + wcet_m2_job1 + wcet_m3_job1 & c2 = 0 & wcet_m3_job1 = c1 & time = 10 STATE 59: checker: error, job1: m3_running, job2: m2_preempted ==> & wcet_m2_job2 + wcet_m2_job1 + wcet_m3_job1 >= 10 & wcet_m2_job2 + wcet_m1_job1 + wcet_m2_job1 >= 10 & wcet_m2_job2 > c2 & wcet_m1_job1 >= 0 & wcet_m2_job1 >= 0 & wcet_m3_job1 >= c1 & c2 >= 0 & c1 > 0 & 10 >= wcet_m2_job1 + c2 + c1 & 10 >= wcet_m1_job1 + wcet_m2_job1 + c1 & time = 10 STATE 60: checker: nop_1, job1: finished, job2: m2_preempted ==> & wcet_m2_job2 + wcet_m1_job1 + wcet_m2_job1 >= 10 & wcet_m2_job2 + wcet_m2_job1 + wcet_m3_job1 >= 10 & wcet_m1_job1 >= 0 & wcet_m2_job1 >= 0 & wcet_m3_job1 >= 0 & c2 >= 0 & 10 >= time & time >= wcet_m2_job1 + wcet_m3_job1 + c2 & 10 > wcet_m2_job1 + wcet_m3_job1 + c2 & time >= wcet_m1_job1 + wcet_m2_job1 + wcet_m3_job1 & 10 > wcet_m1_job1 + wcet_m2_job1 + wcet_m3_job1 & wcet_m3_job1 = c1 STATE 61: checker: nop, job1: m3_running, job2: m2_running ==> & wcet_m2_job2 + wcet_m2_job1 + wcet_m3_job1 >= 10 & wcet_m2_job2 + wcet_m1_job1 + wcet_m2_job1 >= 10 & wcet_m2_job2 >= c2 & wcet_m2_job2 + time > wcet_m1_job1 + wcet_m2_job1 + c2 & wcet_m1_job1 >= 0 & wcet_m2_job1 >= 0 & wcet_m3_job1 >= c1 & c2 >= 0 & c2 + 10 > time & c1 >= 0 & c1 + 10 > time & 10 >= time & time >= wcet_m2_job1 + c2 & time >= wcet_m1_job1 + wcet_m2_job1 + c1 STATE 62: checker: error, job1: m3_begin, job2: m2_running ==> & wcet_m2_job2 + wcet_m2_job1 + wcet_m3_job1 >= 10 & wcet_m2_job2 + wcet_m1_job1 + wcet_m2_job1 >= 10 & wcet_m2_job2 >= c2 & wcet_m1_job1 >= 0 & wcet_m2_job1 >= 0 & c2 > 0 & 10 >= wcet_m2_job1 + c2 & 10 > wcet_m1_job1 + wcet_m2_job1 & wcet_m2_job1 = c1 & time = 10 STATE 63: checker: nop_1, job1: m3_begin, job2: finished ==> & wcet_m2_job2 + wcet_m2_job1 + wcet_m3_job1 >= 10 & wcet_m2_job2 + wcet_m1_job1 + wcet_m2_job1 >= 10 & wcet_m2_job1 >= 0 & 10 >= time & time >= wcet_m1_job1 + wcet_m2_job1 & 10 > wcet_m1_job1 + wcet_m2_job1 & time >= wcet_m2_job2 + wcet_m2_job1 & 10 > wcet_m2_job2 + wcet_m2_job1 & wcet_m2_job2 = c2 & wcet_m2_job1 = c1 STATE 65: checker: error, job1: m3_running, job2: m2_running ==> & wcet_m2_job2 + wcet_m2_job1 + wcet_m3_job1 >= 10 & wcet_m2_job2 + wcet_m1_job1 + wcet_m2_job1 >= 10 & wcet_m2_job2 >= c2 & wcet_m1_job1 >= 0 & wcet_m2_job1 >= 0 & wcet_m3_job1 >= c1 & c2 > 0 & c1 > 0 & 10 >= wcet_m2_job1 + c2 & 10 >= wcet_m1_job1 + wcet_m2_job1 + c1 & time = 10 STATE 66: checker: nop_1, job1: finished, job2: m2_running ==> & wcet_m2_job2 + wcet_m1_job1 + wcet_m2_job1 >= 10 & wcet_m2_job2 >= c2 & wcet_m2_job2 + wcet_m2_job1 + wcet_m3_job1 >= 10 & wcet_m1_job1 >= 0 & wcet_m2_job1 >= 0 & wcet_m3_job1 >= 0 & c2 >= 0 & c2 + 10 > time & 10 >= time & time >= wcet_m2_job1 + c2 & time >= wcet_m1_job1 + wcet_m2_job1 + wcet_m3_job1 & 10 > wcet_m1_job1 + wcet_m2_job1 + wcet_m3_job1 & wcet_m3_job1 = c1 STATE 67: checker: nop_1, job1: m3_running, job2: finished ==> & 10 >= time & wcet_m2_job2 + wcet_m1_job1 + wcet_m2_job1 >= 10 & wcet_m3_job1 >= c1 & 10 > wcet_m2_job2 + wcet_m2_job1 & wcet_m3_job1 + 10 > wcet_m1_job1 + wcet_m2_job1 + c1 & c1 + 10 > time & 20 > wcet_m1_job1 + wcet_m2_job1 + time & time >= wcet_m2_job2 + wcet_m2_job1 & wcet_m2_job1 >= 0 & wcet_m2_job2 + wcet_m2_job1 + wcet_m3_job1 >= 10 & c1 >= 0 & time >= wcet_m1_job1 + wcet_m2_job1 + c1 & wcet_m2_job2 = c2 STATE 68: checker: error, job1: finished, job2: m2_preempted ==> & wcet_m2_job2 + wcet_m1_job1 + wcet_m2_job1 >= 10 & wcet_m2_job2 + wcet_m2_job1 + wcet_m3_job1 >= 10 & wcet_m1_job1 >= 0 & wcet_m2_job1 >= 0 & wcet_m3_job1 >= 0 & c2 >= 0 & 10 > wcet_m2_job1 + wcet_m3_job1 + c2 & 10 > wcet_m1_job1 + wcet_m2_job1 + wcet_m3_job1 & wcet_m3_job1 = c1 & time = 10 STATE 72: checker: error, job1: m3_running, job2: finished ==> & wcet_m2_job2 + wcet_m1_job1 + wcet_m2_job1 >= 10 & wcet_m2_job2 + wcet_m2_job1 + wcet_m3_job1 >= 10 & wcet_m2_job1 >= 0 & wcet_m3_job1 >= c1 & c1 > 0 & 10 > wcet_m2_job2 + wcet_m2_job1 & 10 > wcet_m1_job1 + wcet_m2_job1 & 10 >= wcet_m1_job1 + wcet_m2_job1 + c1 & wcet_m2_job2 = c2 & time = 10 STATE 73: checker: finished, job1: finished, job2: finished ==> & 10 >= time & wcet_m2_job2 + wcet_m1_job1 + wcet_m2_job1 >= 10 & wcet_m2_job2 + wcet_m2_job1 + wcet_m3_job1 >= 10 & wcet_m2_job1 >= 0 & time >= wcet_m1_job1 + wcet_m2_job1 + wcet_m3_job1 & 10 > wcet_m1_job1 + wcet_m2_job1 + wcet_m3_job1 & time >= wcet_m2_job2 + wcet_m2_job1 & 10 > wcet_m2_job2 + wcet_m2_job1 & wcet_m2_job2 = c2 & wcet_m3_job1 = c1 STATE 74: checker: error, job1: finished, job2: m2_running ==> & wcet_m2_job2 + wcet_m1_job1 + wcet_m2_job1 >= 10 & wcet_m2_job2 + wcet_m2_job1 + wcet_m3_job1 >= 10 & wcet_m2_job2 >= c2 & wcet_m1_job1 >= 0 & wcet_m2_job1 >= 0 & wcet_m3_job1 >= 0 & c2 > 0 & 10 > wcet_m1_job1 + wcet_m2_job1 + wcet_m3_job1 & 10 >= wcet_m2_job1 + c2 & wcet_m3_job1 = c1 & time = 10 DESCRIPTION OF THE TRANSITIONS s_0 -> s_1 via "DEADLINE" s_2 -> s_4 via "DEADLINE" s_3 -> s_7 via "DEADLINE" s_5 -> s_13 via "DEADLINE" s_6 -> s_10 via "DEADLINE" s_8 -> s_16 via "DEADLINE" s_11 -> s_24 via "DEADLINE" s_14 -> s_21 via "DEADLINE" s_15 -> s_18 via "DEADLINE" s_19 -> s_28 via "DEADLINE" s_22 -> s_30 via "DEADLINE" s_23 -> s_41 via "DEADLINE" s_26 -> s_44 via "DEADLINE" s_27 -> s_41 via "DEADLINE" s_31 -> s_38 via "DEADLINE" s_34 -> s_53 via "DEADLINE" s_39 -> s_57 via "DEADLINE" s_42 -> s_53 via "DEADLINE" s_43 -> s_25 via "DEADLINE" s_45 -> s_59 via "DEADLINE" s_46 -> s_62 via "DEADLINE" s_54 -> s_47 via "DEADLINE" s_60 -> s_68 via "DEADLINE" s_61 -> s_65 via "DEADLINE" s_63 -> s_51 via "DEADLINE" s_66 -> s_74 via "DEADLINE" s_67 -> s_72 via "DEADLINE" s_0 -> s_2 via "m1_j1_begin" s_3 -> s_6 via "m1_j1_begin" s_8 -> s_11 via "m1_j1_begin" s_14 -> s_22 via "m2_j1_finished" s_43 -> s_26 via "m2_j1_finished" s_54 -> s_63 via "m2_j1_finished" s_31 -> s_39 via "m3_j1_finished" s_45 -> s_60 via "m3_j1_finished" s_61 -> s_66 via "m3_j1_finished" s_67 -> s_73 via "m3_j1_finished" s_2 -> s_5 via "m1_j1_finished" s_6 -> s_15 via "m1_j1_finished" s_11 -> s_19 via "m1_j1_finished" s_22 -> s_31 via "m3_j1_begin" s_26 -> s_45 via "m3_j1_begin" s_46 -> s_61 via "m3_j1_begin" s_63 -> s_67 via "m3_j1_begin" s_3 -> s_8 via "m2_j2_finished" s_6 -> s_11 via "m2_j2_finished" s_15 -> s_19 via "m2_j2_finished" s_23 -> s_34 via "m2_j2_finished" s_27 -> s_42 via "m2_j2_finished" s_46 -> s_63 via "m2_j2_finished" s_61 -> s_67 via "m2_j2_finished" s_66 -> s_73 via "m2_j2_finished" s_5 -> s_14 via "m2_j1_begin" s_15 -> s_43 via "m2_j1_begin" s_19 -> s_54 via "m2_j1_begin" s_23 -> s_43 via "m2_j1_begin" s_27 -> s_43 via "m2_j1_begin" s_34 -> s_54 via "m2_j1_begin" s_42 -> s_54 via "m2_j1_begin" s_0 -> s_3 via "m2_j2_begin" s_2 -> s_6 via "m2_j2_begin" s_5 -> s_15 via "m2_j2_begin" s_14 -> s_23 via "m2_j2_begin" s_22 -> s_46 via "m2_j2_begin" s_26 -> s_46 via "m2_j2_begin" s_31 -> s_61 via "m2_j2_begin" s_39 -> s_66 via "m2_j2_begin" s_43 -> s_27 via "m2_j2_begin" s_45 -> s_61 via "m2_j2_begin" s_60 -> s_66 via "m2_j2_begin"