automaton checker

var
	time: clock;
	deadline: parameter;

synclabs: m_0_job_1_beginning, m_0_job_1_finishing, m_3_job_1_beginning, m_3_job_1_finishing, m_1_job_1_beginning, m_1_job_1_finishing, m_4_job_1_beginning, m_4_job_1_finishing, m_2_job_1_beginning, m_2_job_1_finishing,m_4_job_2_beginning, m_4_job_2_finishing, m_2_job_2_beginning, m_2_job_2_finishing, m_0_job_2_beginning, m_0_job_2_finishing, m_1_job_2_beginning, m_1_job_2_finishing, m_3_job_2_beginning, m_3_job_2_finishing, DEADLINE;


loc check_1: while time <= deadline wait {}
	when True sync m_0_job_1_beginning goto check_1;
	when True sync m_0_job_1_finishing goto check_1;
	when True sync m_1_job_1_beginning goto check_1;
	when True sync m_1_job_1_finishing goto check_1;
	when True sync m_2_job_1_beginning goto check_1;
	when True sync m_2_job_1_finishing goto check_2;
	when True sync m_3_job_1_beginning goto check_1;
	when True sync m_3_job_1_finishing goto check_1;
	when True sync m_4_job_1_beginning goto check_1;
	when True sync m_4_job_1_finishing goto check_1;

	when True sync m_0_job_2_beginning goto check_1;
	when True sync m_0_job_2_finishing goto check_1;
	when True sync m_1_job_2_beginning goto check_1;
	when True sync m_1_job_2_finishing goto check_1;
	when True sync m_2_job_2_beginning goto check_1;
	when True sync m_2_job_2_finishing goto check_1;
	when True sync m_3_job_2_beginning goto check_1;
	when True sync m_3_job_2_finishing goto check_2;
	when True sync m_4_job_2_beginning goto check_1;
	when True sync m_4_job_2_finishing goto check_1;

	when time = deadline sync DEADLINE goto error;

loc check_2: while time <= deadline wait {}
	when True sync m_0_job_1_beginning goto check_2;
	when True sync m_0_job_1_finishing goto check_2;
	when True sync m_1_job_1_beginning goto check_2;
	when True sync m_1_job_1_finishing goto check_2;
	when True sync m_2_job_1_beginning goto check_2;
	when True sync m_2_job_1_finishing goto success;
	when True sync m_3_job_1_beginning goto check_2;
	when True sync m_3_job_1_finishing goto check_2;
	when True sync m_4_job_1_beginning goto check_2;
	when True sync m_4_job_1_finishing goto check_2;

	when True sync m_0_job_2_beginning goto check_2;
	when True sync m_0_job_2_finishing goto check_2;
	when True sync m_1_job_2_beginning goto check_2;
	when True sync m_1_job_2_finishing goto check_2;
	when True sync m_2_job_2_beginning goto check_2;
	when True sync m_2_job_2_finishing goto check_2;
	when True sync m_3_job_2_beginning goto check_2;
	when True sync m_3_job_2_finishing goto success;
	when True sync m_4_job_2_beginning goto check_2;
	when True sync m_4_job_2_finishing goto check_2;

	when time = deadline sync DEADLINE goto error;

loc success: while time <= deadline wait {}

loc error: while time <= deadline wait {}

end

automaton job_1

var
	c_1:analog;
	wcet_m_0_job_1, wcet_m_3_job_1, wcet_m_1_job_1, wcet_m_4_job_1, wcet_m_2_job_1:parameter;


synclabs: m_0_job_1_beginning, m_0_job_1_finishing, m_3_job_1_beginning, m_3_job_1_finishing, m_1_job_1_beginning, m_1_job_1_finishing, m_4_job_1_beginning, m_4_job_1_finishing, m_2_job_1_beginning, m_2_job_1_finishing, m_4_job_2_beginning, m_2_job_2_beginning, m_0_job_2_beginning, m_1_job_2_beginning, m_3_job_2_beginning;

-- TASK 1 --

loc m_0_waiting: while True wait {c_1'=0}
	when True sync m_0_job_1_beginning do {c_1'=0} goto m_0_running;
	when True sync m_4_job_2_beginning do {c_1'=c_1} goto m_0_waiting;
	when True sync m_2_job_2_beginning do {c_1'=c_1} goto m_0_waiting;
	when True sync m_0_job_2_beginning do {c_1'=c_1} goto m_0_waiting;
	when True sync m_1_job_2_beginning do {c_1'=c_1} goto m_0_waiting;
	when True sync m_3_job_2_beginning do {c_1'=c_1} goto m_0_waiting;

loc m_0_running: while c_1 <= wcet_m_0_job_1 wait {c_1'=1}
	when c_1 = wcet_m_0_job_1 sync m_0_job_1_finishing do {c_1'=c_1} goto m_3_waiting;
	when c_1 < wcet_m_0_job_1 sync m_0_job_2_beginning do {c_1'=c_1} goto m_0_preempted;
	when c_1 < wcet_m_0_job_1 sync m_4_job_2_beginning do {c_1'=c_1} goto m_0_running;
	when c_1 < wcet_m_0_job_1 sync m_2_job_2_beginning do {c_1'=c_1} goto m_0_running;
	when c_1 < wcet_m_0_job_1 sync m_1_job_2_beginning do {c_1'=c_1} goto m_0_running;
	when c_1 < wcet_m_0_job_1 sync m_3_job_2_beginning do {c_1'=c_1} goto m_0_running;


loc m_0_preempted: while True wait {c_1'=0}
	when True sync m_0_job_1_beginning do {c_1'=c_1} goto m_0_running;
	when True sync m_4_job_2_beginning do {c_1'=c_1} goto m_0_preempted;
	when True sync m_1_job_2_beginning do {c_1'=c_1} goto m_0_preempted;
	when True sync m_2_job_2_beginning do {c_1'=c_1} goto m_0_preempted;
	when True sync m_3_job_2_beginning do {c_1'=c_1} goto m_0_preempted;
	when True sync m_0_job_2_beginning do {c_1'=c_1} goto m_0_preempted;

-- TASK 2 --

loc m_3_waiting: while True wait {c_1'=0}
	when True sync m_3_job_1_beginning do {c_1'=0} goto m_3_running;
	when True sync m_4_job_2_beginning do {c_1'=c_1} goto m_3_waiting;
	when True sync m_1_job_2_beginning do {c_1'=c_1} goto m_3_waiting;
	when True sync m_2_job_2_beginning do {c_1'=c_1} goto m_3_waiting;
	when True sync m_3_job_2_beginning do {c_1'=c_1} goto m_3_waiting;
	when True sync m_0_job_2_beginning do {c_1'=c_1} goto m_3_waiting;

loc m_3_running: while c_1 <= wcet_m_3_job_1 wait {c_1'=1}
	when c_1 = wcet_m_3_job_1 sync m_3_job_1_finishing do {c_1'=c_1} goto m_1_waiting;
	when c_1 < wcet_m_3_job_1 sync m_3_job_2_beginning do {c_1'=c_1} goto m_3_preempted;
	when c_1 < wcet_m_3_job_1 sync m_4_job_2_beginning do {c_1'=c_1} goto m_3_running;
	when c_1 < wcet_m_3_job_1 sync m_1_job_2_beginning do {c_1'=c_1} goto m_3_running;
	when c_1 < wcet_m_3_job_1 sync m_2_job_2_beginning do {c_1'=c_1} goto m_3_running;
	when c_1 < wcet_m_3_job_1 sync m_0_job_2_beginning do {c_1'=c_1} goto m_3_running;

loc m_3_preempted: while True wait {c_1'=0}
	when True sync m_3_job_1_beginning do {c_1'=c_1} goto m_3_running;
	when True sync m_4_job_2_beginning do {c_1'=c_1} goto m_3_preempted;
	when True sync m_1_job_2_beginning do {c_1'=c_1} goto m_3_preempted;
	when True sync m_2_job_2_beginning do {c_1'=c_1} goto m_3_preempted;
	when True sync m_3_job_2_beginning do {c_1'=c_1} goto m_3_preempted;
	when True sync m_0_job_2_beginning do {c_1'=c_1} goto m_3_preempted;

-- TASK 3 --

loc m_1_waiting: while True wait {c_1'=0}
	when True sync m_1_job_1_beginning do {c_1'=0} goto m_1_running;
	when True sync m_4_job_2_beginning do {c_1'=c_1} goto m_1_waiting;
	when True sync m_1_job_2_beginning do {c_1'=c_1} goto m_1_waiting;
	when True sync m_2_job_2_beginning do {c_1'=c_1} goto m_1_waiting;
	when True sync m_3_job_2_beginning do {c_1'=c_1} goto m_1_waiting;
	when True sync m_0_job_2_beginning do {c_1'=c_1} goto m_1_waiting;

loc m_1_running: while c_1 <= wcet_m_1_job_1 wait {c_1'=1}
	when c_1 = wcet_m_1_job_1 sync m_1_job_1_finishing do {c_1'=c_1} goto m_4_waiting;
	when c_1 < wcet_m_1_job_1 sync m_1_job_2_beginning do {c_1'=c_1} goto m_1_preempted;
	when c_1 < wcet_m_1_job_1 sync m_4_job_2_beginning do {c_1'=c_1} goto m_1_running;
	when c_1 < wcet_m_1_job_1 sync m_2_job_2_beginning do {c_1'=c_1} goto m_1_running;
	when c_1 < wcet_m_1_job_1 sync m_3_job_2_beginning do {c_1'=c_1} goto m_1_running;
	when c_1 < wcet_m_1_job_1 sync m_0_job_2_beginning do {c_1'=c_1} goto m_1_running;

loc m_1_preempted: while True wait {c_1'=0}
	when True sync m_1_job_1_beginning do {c_1'=c_1} goto m_1_running;
	when True sync m_4_job_2_beginning do {c_1'=c_1} goto m_1_preempted;
	when True sync m_1_job_2_beginning do {c_1'=c_1} goto m_1_preempted;
	when True sync m_2_job_2_beginning do {c_1'=c_1} goto m_1_preempted;
	when True sync m_3_job_2_beginning do {c_1'=c_1} goto m_1_preempted;
	when True sync m_0_job_2_beginning do {c_1'=c_1} goto m_1_preempted;

-- TASK 4 --

loc m_4_waiting: while True wait {c_1'=0}
	when True sync m_4_job_1_beginning do {c_1'=0} goto m_4_running;
	when True sync m_4_job_2_beginning do {c_1'=c_1} goto m_4_waiting;
	when True sync m_1_job_2_beginning do {c_1'=c_1} goto m_4_waiting;
	when True sync m_2_job_2_beginning do {c_1'=c_1} goto m_4_waiting;
	when True sync m_3_job_2_beginning do {c_1'=c_1} goto m_4_waiting;
	when True sync m_0_job_2_beginning do {c_1'=c_1} goto m_4_waiting;

loc m_4_running: while c_1 <= wcet_m_4_job_1 wait {c_1'=1}
	when c_1 = wcet_m_4_job_1 sync m_4_job_1_finishing do {c_1'=c_1} goto m_2_waiting;
	when c_1 < wcet_m_4_job_1 sync m_4_job_2_beginning do {c_1'=c_1} goto m_4_preempted;
	when c_1 < wcet_m_4_job_1 sync m_1_job_2_beginning do {c_1'=c_1} goto m_4_running;
	when c_1 < wcet_m_4_job_1 sync m_2_job_2_beginning do {c_1'=c_1} goto m_4_running;
	when c_1 < wcet_m_4_job_1 sync m_3_job_2_beginning do {c_1'=c_1} goto m_4_running;
	when c_1 < wcet_m_4_job_1 sync m_0_job_2_beginning do {c_1'=c_1} goto m_4_running;

loc m_4_preempted: while True wait {c_1'=0}
	when True sync m_4_job_1_beginning do {c_1'=c_1} goto m_4_running;
	when True sync m_4_job_2_beginning do {c_1'=c_1} goto m_4_preempted;
	when True sync m_1_job_2_beginning do {c_1'=c_1} goto m_4_preempted;
	when True sync m_2_job_2_beginning do {c_1'=c_1} goto m_4_preempted;
	when True sync m_3_job_2_beginning do {c_1'=c_1} goto m_4_preempted;
	when True sync m_0_job_2_beginning do {c_1'=c_1} goto m_4_preempted;

-- TASK 5 --

loc m_2_waiting: while True wait {c_1'=0}
	when True sync m_2_job_1_beginning do {c_1'=0} goto m_2_running;
	when True sync m_4_job_2_beginning do {c_1'=c_1} goto m_2_waiting;
	when True sync m_1_job_2_beginning do {c_1'=c_1} goto m_2_waiting;
	when True sync m_2_job_2_beginning do {c_1'=c_1} goto m_2_waiting;
	when True sync m_3_job_2_beginning do {c_1'=c_1} goto m_2_waiting;
	when True sync m_0_job_2_beginning do {c_1'=c_1} goto m_2_waiting;

loc m_2_running: while c_1 <= wcet_m_2_job_1 wait {c_1'=1}
	when c_1 = wcet_m_2_job_1 sync m_2_job_1_finishing do {c_1'=c_1} goto success;
	when c_1 < wcet_m_2_job_1 sync m_2_job_2_beginning do {c_1'=c_1} goto m_2_preempted;
	when c_1 < wcet_m_2_job_1 sync m_4_job_2_beginning do {c_1'=c_1} goto m_2_running;
	when c_1 < wcet_m_2_job_1 sync m_1_job_2_beginning do {c_1'=c_1} goto m_2_running;
	when c_1 < wcet_m_2_job_1 sync m_3_job_2_beginning do {c_1'=c_1} goto m_2_running;
	when c_1 < wcet_m_2_job_1 sync m_0_job_2_beginning do {c_1'=c_1} goto m_2_running;

loc m_2_preempted: while True wait {c_1'=0}
	when True sync m_2_job_1_beginning do {c_1'=c_1} goto m_2_running;
	when True sync m_4_job_2_beginning do {c_1'=c_1} goto m_2_preempted;
	when True sync m_1_job_2_beginning do {c_1'=c_1} goto m_2_preempted;
	when True sync m_2_job_2_beginning do {c_1'=c_1} goto m_2_preempted;
	when True sync m_3_job_2_beginning do {c_1'=c_1} goto m_2_preempted;
	when True sync m_0_job_2_beginning do {c_1'=c_1} goto m_2_preempted;

-- END --

loc success : while True wait {}

end


automaton job_2

var
	c_2:analog;
	wcet_m_4_job_2, wcet_m_2_job_2, wcet_m_0_job_2, wcet_m_1_job_2, wcet_m_3_job_2:parameter;


synclabs: m_4_job_2_beginning, m_4_job_2_finishing, m_2_job_2_beginning, m_2_job_2_finishing, m_0_job_2_beginning, m_0_job_2_finishing, m_1_job_2_beginning, m_1_job_2_finishing, m_3_job_2_beginning, m_3_job_2_finishing, m_0_job_1_beginning, m_3_job_1_beginning, m_1_job_1_beginning, m_4_job_1_beginning, m_2_job_1_beginning;

-- TASK 1 --

loc m_4_waiting: while True wait {c_2'=0}
	when True sync m_4_job_2_beginning do {c_2'=0} goto m_4_running;
	when True sync m_0_job_1_beginning do {c_2'=c_2} goto m_4_waiting;
	when True sync m_3_job_1_beginning do {c_2'=c_2} goto m_4_waiting;
	when True sync m_1_job_1_beginning do {c_2'=c_2} goto m_4_waiting;
	when True sync m_4_job_1_beginning do {c_2'=c_2} goto m_4_waiting;
	when True sync m_2_job_1_beginning do {c_2'=c_2} goto m_4_waiting;

loc m_4_running: while c_2 <= wcet_m_4_job_2 wait {c_2'=1}
	when c_2 = wcet_m_4_job_2 sync m_4_job_2_finishing do {c_2'=c_2} goto m_2_waiting;
	when c_2 < wcet_m_4_job_2 sync m_4_job_1_beginning do {c_2'=c_2} goto m_4_preempted;
	when c_2 < wcet_m_4_job_2 sync m_0_job_1_beginning do {c_2'=c_2} goto m_4_running;
	when c_2 < wcet_m_4_job_2 sync m_3_job_1_beginning do {c_2'=c_2} goto m_4_running;
	when c_2 < wcet_m_4_job_2 sync m_1_job_1_beginning do {c_2'=c_2} goto m_4_running;
	when c_2 < wcet_m_4_job_2 sync m_2_job_1_beginning do {c_2'=c_2} goto m_4_running;


loc m_4_preempted: while True wait {c_2'=0}
	when True sync m_4_job_2_beginning do {c_2'=c_2} goto m_4_running;
	when True sync m_0_job_1_beginning do {c_2'=c_2} goto m_4_preempted;
	when True sync m_3_job_1_beginning do {c_2'=c_2} goto m_4_preempted;
	when True sync m_1_job_1_beginning do {c_2'=c_2} goto m_4_preempted;
	when True sync m_4_job_1_beginning do {c_2'=c_2} goto m_4_preempted;
	when True sync m_2_job_1_beginning do {c_2'=c_2} goto m_4_preempted;

-- TASK 2 --

loc m_2_waiting: while True wait {c_2'=0}
	when True sync m_2_job_2_beginning do {c_2'=0} goto m_2_running;
	when True sync m_0_job_1_beginning do {c_2'=c_2} goto m_2_waiting;
	when True sync m_3_job_1_beginning do {c_2'=c_2} goto m_2_waiting;
	when True sync m_1_job_1_beginning do {c_2'=c_2} goto m_2_waiting;
	when True sync m_4_job_1_beginning do {c_2'=c_2} goto m_2_waiting;
	when True sync m_2_job_1_beginning do {c_2'=c_2} goto m_2_waiting;

loc m_2_running: while c_2 <= wcet_m_2_job_2 wait {c_2'=1}
	when c_2 = wcet_m_2_job_2 sync m_2_job_2_finishing do {c_2'=c_2} goto m_0_waiting;
	when c_2 < wcet_m_2_job_2 sync m_2_job_1_beginning do {c_2'=c_2} goto m_2_preempted;
	when c_2 < wcet_m_2_job_2 sync m_0_job_1_beginning do {c_2'=c_2} goto m_2_running;
	when c_2 < wcet_m_2_job_2 sync m_3_job_1_beginning do {c_2'=c_2} goto m_2_running;
	when c_2 < wcet_m_2_job_2 sync m_1_job_1_beginning do {c_2'=c_2} goto m_2_running;
	when c_2 < wcet_m_2_job_2 sync m_4_job_1_beginning do {c_2'=c_2} goto m_2_running;

loc m_2_preempted: while True wait {c_2'=0}
	when True sync m_2_job_2_beginning do {c_2'=c_2} goto m_2_running;
	when True sync m_0_job_1_beginning do {c_2'=c_2} goto m_2_preempted;
	when True sync m_3_job_1_beginning do {c_2'=c_2} goto m_2_preempted;
	when True sync m_1_job_1_beginning do {c_2'=c_2} goto m_2_preempted;
	when True sync m_4_job_1_beginning do {c_2'=c_2} goto m_2_preempted;
	when True sync m_2_job_1_beginning do {c_2'=c_2} goto m_2_preempted;

-- TASK 3 --

loc m_0_waiting: while True wait {c_2'=0}
	when True sync m_0_job_2_beginning do {c_2'=0} goto m_0_running;
	when True sync m_0_job_1_beginning do {c_2'=c_2} goto m_0_waiting;
	when True sync m_3_job_1_beginning do {c_2'=c_2} goto m_0_waiting;
	when True sync m_1_job_1_beginning do {c_2'=c_2} goto m_0_waiting;
	when True sync m_4_job_1_beginning do {c_2'=c_2} goto m_0_waiting;
	when True sync m_2_job_1_beginning do {c_2'=c_2} goto m_0_waiting;

loc m_0_running: while c_2 <= wcet_m_0_job_2 wait {c_2'=1}
	when c_2 = wcet_m_0_job_2 sync m_0_job_2_finishing do {c_2'=c_2} goto m_1_waiting;
	when c_2 < wcet_m_0_job_2 sync m_0_job_1_beginning do {c_2'=c_2} goto m_0_preempted;
	when c_2 < wcet_m_0_job_2 sync m_3_job_1_beginning do {c_2'=c_2} goto m_0_running;
	when c_2 < wcet_m_0_job_2 sync m_1_job_1_beginning do {c_2'=c_2} goto m_0_running;
	when c_2 < wcet_m_0_job_2 sync m_4_job_1_beginning do {c_2'=c_2} goto m_0_running;
	when c_2 < wcet_m_0_job_2 sync m_2_job_1_beginning do {c_2'=c_2} goto m_0_running;

loc m_0_preempted: while True wait {c_2'=0}
	when True sync m_0_job_2_beginning do {c_2'=c_2} goto m_0_running;
	when True sync m_0_job_1_beginning do {c_2'=c_2} goto m_0_preempted;
	when True sync m_3_job_1_beginning do {c_2'=c_2} goto m_0_preempted;
	when True sync m_1_job_1_beginning do {c_2'=c_2} goto m_0_preempted;
	when True sync m_4_job_1_beginning do {c_2'=c_2} goto m_0_preempted;
	when True sync m_2_job_1_beginning do {c_2'=c_2} goto m_0_preempted;

-- TASK 4 --

loc m_1_waiting: while True wait {c_2'=0}
	when True sync m_1_job_2_beginning do {c_2'=0} goto m_1_running;
	when True sync m_0_job_1_beginning do {c_2'=c_2} goto m_1_waiting;
	when True sync m_3_job_1_beginning do {c_2'=c_2} goto m_1_waiting;
	when True sync m_1_job_1_beginning do {c_2'=c_2} goto m_1_waiting;
	when True sync m_4_job_1_beginning do {c_2'=c_2} goto m_1_waiting;
	when True sync m_2_job_1_beginning do {c_2'=c_2} goto m_1_waiting;

loc m_1_running: while c_2 <= wcet_m_1_job_2 wait {c_2'=1}
	when c_2 = wcet_m_1_job_2 sync m_1_job_2_finishing do {c_2'=c_2} goto m_3_running;
	when c_2 < wcet_m_1_job_2 sync m_1_job_1_beginning do {c_2'=c_2} goto m_1_preempted;
	when c_2 < wcet_m_1_job_2 sync m_0_job_1_beginning do {c_2'=c_2} goto m_1_running;
	when c_2 < wcet_m_1_job_2 sync m_3_job_1_beginning do {c_2'=c_2} goto m_1_running;
	when c_2 < wcet_m_1_job_2 sync m_4_job_1_beginning do {c_2'=c_2} goto m_1_running;
	when c_2 < wcet_m_1_job_2 sync m_2_job_1_beginning do {c_2'=c_2} goto m_1_running;

loc m_1_preempted: while True wait {c_2'=0}
	when True sync m_1_job_2_beginning do {c_2'=c_2} goto m_1_running;
	when True sync m_0_job_1_beginning do {c_2'=c_2} goto m_1_preempted;
	when True sync m_3_job_1_beginning do {c_2'=c_2} goto m_1_preempted;
	when True sync m_1_job_1_beginning do {c_2'=c_2} goto m_1_preempted;
	when True sync m_4_job_1_beginning do {c_2'=c_2} goto m_1_preempted;
	when True sync m_2_job_1_beginning do {c_2'=c_2} goto m_1_preempted;

-- TASK 5 --

loc m_3_waiting: while True wait {c_2'=0}
	when True sync m_3_job_2_beginning do {c_2'=0} goto m_3_running;
	when True sync m_0_job_1_beginning do {c_2'=c_2} goto m_3_waiting;
	when True sync m_3_job_1_beginning do {c_2'=c_2} goto m_3_waiting;
	when True sync m_1_job_1_beginning do {c_2'=c_2} goto m_3_waiting;
	when True sync m_4_job_1_beginning do {c_2'=c_2} goto m_3_waiting;
	when True sync m_2_job_1_beginning do {c_2'=c_2} goto m_3_waiting;

loc m_3_running: while c_2 <= wcet_m_3_job_2 wait {c_2'=1}
	when c_2 = wcet_m_3_job_2 sync m_3_job_2_finishing do {c_2'=c_2} goto success;
	when c_2 < wcet_m_3_job_2 sync m_3_job_1_beginning do {c_2'=c_2} goto m_3_preempted;
	when c_2 < wcet_m_3_job_2 sync m_0_job_1_beginning do {c_2'=c_2} goto m_3_running;
	when c_2 < wcet_m_3_job_2 sync m_1_job_1_beginning do {c_2'=c_2} goto m_3_running;
	when c_2 < wcet_m_3_job_2 sync m_4_job_1_beginning do {c_2'=c_2} goto m_3_running;
	when c_2 < wcet_m_3_job_2 sync m_2_job_1_beginning do {c_2'=c_2} goto m_3_running;

loc m_3_preempted: while True wait {c_2'=0}
	when True sync m_3_job_2_beginning do {c_2'=c_2} goto m_3_running;
	when True sync m_0_job_1_beginning do {c_2'=c_2} goto m_3_preempted;
	when True sync m_3_job_1_beginning do {c_2'=c_2} goto m_3_preempted;
	when True sync m_1_job_1_beginning do {c_2'=c_2} goto m_3_preempted;
	when True sync m_4_job_1_beginning do {c_2'=c_2} goto m_3_preempted;
	when True sync m_2_job_1_beginning do {c_2'=c_2} goto m_3_preempted;

-- END --

loc success : while True wait {}

end

var init: region;

init:= 	loc[checker] = check_1 &
			loc[job_1] = m_0_waiting &
			loc[job_2] = m_4_waiting &
			c_1 = 0 &
			c_2 = 0 &
			time = 0 &

			wcet_m_0_job_1 = 20 &
			wcet_m_1_job_1 = 31 &
			wcet_m_2_job_1 = 17 &
			wcet_m_3_job_1 = 87 &			
			wcet_m_4_job_1 = 76 &
--			wcet_m_0_job_2 = 24 &
--			wcet_m_1_job_2 = 18 &
--			wcet_m_2_job_2 = 32 &
--			wcet_m_3_job_2 = 81 &			
--			wcet_m_4_job_2 = 25 &
			deadline = 231 &
			True
;