-----------------------------------------
-- STOPPER Used for Analysis Only		--
-----------------------------------------
automaton stopper
var time :clock;
	  deadlineBasic: parameter;

synclabs: done1, require2, done2;

loc f_1_r: while time<= deadlineBasic wait {}	
	when True sync done1 goto f_2_r;
	when True sync require2 goto f_1_r;
	when True sync done2 goto f_1_r;

loc f_2_r: while time<= deadlineBasic wait {}	
	when True sync done1 goto f_3_r;
	when True sync require2 goto f_2_r;
	when True sync done2 goto f_2_r;

loc f_3_r: while time<= deadlineBasic wait {}	
	when True sync done1 goto f_4_r;
	when True sync require2 goto f_3_r;
	when True sync done2 goto f_3_r;

loc f_4_r: while time<= deadlineBasic wait {}	
	when True sync done1 goto f_5_r;
	when True sync require2 goto f_4_r;
	when True sync done2 goto f_4_r;

loc f_5_r: while time<= deadlineBasic wait {}	
	when True sync done1 goto f_6_r;
	when True sync require2 goto f_5_r;
	when True sync done2 goto f_5_r;

loc f_6_r: while time<= deadlineBasic wait {}	
	when True sync done1 goto f_7_r;
	when True sync require2 goto f_6_r;
	when True sync done2 goto f_6_r;

loc f_7_r: while time<= deadlineBasic wait {}	
	when True sync done1 goto f_8_r;
	when True sync require2 goto f_7_r;
	when True sync done2 goto f_7_r;

loc f_8_r: while time<= deadlineBasic wait {}	
	when True sync done1 goto f_9_r;
	when True sync require2 goto f_8_r;
	when True sync done2 goto f_8_r;

loc f_9_r: while time<= deadlineBasic wait {}	
	when True sync done1 goto f_10_r;
	when True sync require2 goto f_9_r;
	when True sync done2 goto f_9_r;

loc f_10_r: while time<= deadlineBasic wait {}	
	when True sync done1 goto f_10;
	when True sync require2 goto f_10_r;
	when True sync done2 goto f_10_r;

loc f_10: while time <= deadlineBasic wait {}
	when True sync require2 goto g_r;

loc g_r: while time <= deadlineBasic wait {}
	when True sync done2 goto lf_r;
	when True sync done1 goto g_r;

loc lf_r: while time <= deadlineBasic wait {}
	when True sync done1 goto end_flow;

loc end_flow: while time <= deadlineBasic wait {}

end

automaton scheduler_EDF

var
	x1,x2,x3: analog;
	d1,d2,d3: clock;
	WCET1, WCET2, WCET3, D1, D2, D3:parameter;

synclabs:require1, require2, require3, done1, done2, done3;

initially non1_non2_non3;

loc non1_non2_non3: while True wait {x1'=0 & x2'=0 & x3'=0}
	when True sync require1 do {x1'=x1, x2'=x2, x3'=x3, d1'=0} goto ok1_non2_non3;
	when True sync require2 do {x1'=x1, x2'=x2, x3'=x3, d2'=0} goto non1_ok2_non3;
	when True sync require3 do {x1'=x1, x2'=x2, x3'=x3, d3'=0} goto non1_non2_ok3;

loc ok1_non2_non3: while x1 <= WCET1 wait {x1'=1 & x2'=0 & x3'=0}
	when x1 = WCET1 sync done1 do {x1'=0, x2'=x2, x3'=x3} goto non1_non2_non3;
	when x1 < WCET1 & d1 < D1 - D2 sync require2 do {x1'=x1, x2'=x2, x3'=x3, d2'=0} goto w1_ok2_non3;
	when x1 < WCET1 & d1 >= D1 - D2 sync require2 do {x1'=x1, x2'=x2, x3'=x3, d2'=0} goto ok1_w2_non3;
	when x1 < WCET1 & d1 < D1 - D3 sync require3 do {x1'=x1, x2'=x2, x3'=x3, d3'=0} goto w1_non2_ok3;
	when x1 < WCET1 & d1 >= D1 - D3 sync require3 do {x1'=x1, x2'=x2, x3'=x3, d3'=0} goto ok1_non2_w3;

loc non1_ok2_non3: while x2 <= WCET2 wait {x1'=0 & x2'=1 & x3'=0}
	when x2 = WCET2 sync done2 do {x1'=x1, x2'=0, x3'=x3} goto non1_non2_non3;
	when x2 < WCET2 & d2 < D2 - D1 sync require1 do {x1'=x1, x2'=x2, x3'=x3, d1'=0} goto ok1_w2_non3;
	when x2 < WCET2 & d2 >= D2 - D1 sync require1 do {x1'=x1, x2'=x2, x3'=x3, d1'=0} goto w1_ok2_non3;
	when x2 < WCET2 & d2 < D2 - D3 sync require3 do {x1'=x1, x2'=x2, x3'=x3, d3'=0} goto non1_w2_ok3;
	when x2 < WCET2 & d2 >= D2 - D3 sync require3 do {x1'=x1, x2'=x2, x3'=x3, d3'=0} goto non1_ok2_w3;

loc non1_non2_ok3: while x3 <= WCET3 wait {x1'=0 & x2'=0 & x3'=1}
	when x3 = WCET3 sync done3 do {x1'=x1, x2'=x2, x3'=0} goto non1_non2_non3;
	when x3 < WCET3 & d3 < D3 - D1 sync require1 do {x1'=x1, x2'=x2, x3'=x3, d1'=0} goto ok1_non2_w3;
	when x3 < WCET3 & d3 >= D3 - D1 sync require1 do {x1'=x1, x2'=x2, x3'=x3, d1'=0} goto w1_non2_ok3;
	when x3 < WCET3 & d3 < D3 - D2 sync require2 do {x1'=x1, x2'=x2, x3'=x3, d2'=0} goto non1_ok2_w3;
	when x3 < WCET3 & d3 >= D3 - D2 sync require2 do {x1'=x1, x2'=x2, x3'=x3, d2'=0} goto non1_w2_ok3;

loc ok1_w2_non3: while x1 <= WCET1 wait {x1'=1 & x2'=0 & x3'=0}
	when x1 = WCET1 sync done1 do {x1'=0, x2'=x2, x3'=x3} goto non1_ok2_non3;
	when x1 < WCET1 & d1 < D1 - D3 sync require3 do {x1'=x1, x2'=x2, x3'=x3, d3'=0} goto w1_w2_ok3;
	when x1 < WCET1 & d1 >= D1 - D3 sync require3 do {x1'=x1, x2'=x2, x3'=x3, d3'=0} goto ok1_w2_w3;

loc w1_ok2_non3: while x2 <= WCET2 wait {x1'=0 & x2'=1 & x3'=0}
	when x2 = WCET2 sync done2 do {x1'=x1, x2'=0, x3'=x3} goto ok1_non2_non3;
	when x2 < WCET2 & d2 < D2 - D3 sync require3 do {x1'=x1, x2'=x2, x3'=x3, d3'=0} goto w1_w2_ok3;
	when x2 < WCET2 & d2 >= D2 - D3 sync require3 do {x1'=x1, x2'=x2, x3'=x3, d3'=0} goto w1_ok2_w3;

loc ok1_non2_w3: while x1 <= WCET1 wait {x1'=1 & x2'=0 & x3'=0}
	when x1 = WCET1 sync done1 do {x1'=0, x2'=x2, x3'=x3} goto non1_non2_ok3;
	when x1 < WCET1 & d1 < D1 - D2 sync require2 do {x1'=x1, x2'=x2, x3'=x3, d2'=0} goto w1_ok2_w3;
	when x1 < WCET1 & d1 >= D1 - D2 sync require2 do {x1'=x1, x2'=x2, x3'=x3, d2'=0} goto ok1_w2_w3;

loc w1_non2_ok3: while x3 <= WCET3 wait {x1'=0 & x2'=0 & x3'=1}
	when x3 = WCET3 sync done3 do {x1'=x1, x2'=x2', x3'=0} goto ok1_non2_non3;
	when x3 < WCET3 & d3 < D3 - D2 sync require2 do {x1'=x1, x2'=x2, x3'=x3, d2'=0} goto w1_ok2_w3;
	when x3 < WCET3 & d3 >= D3 - D2 sync require2 do {x1'=x1, x2'=x2, x3'=x3, d2'=0} goto w1_w2_ok3;

loc non1_ok2_w3: while x2 <= WCET2 wait {x1'=0 & x2'=1 & x3'=0}
	when x2 = WCET2 sync done2 do {x1'=x1', x2'=0, x3'=x3} goto non1_non2_ok3;
	when x2 < WCET2 & d2 < D2 - D1 sync require1 do {x1'=x1, x2'=x2, x3'=x3, d1'=0} goto ok1_w2_w3;
	when x2 < WCET2 & d2 >= D2 - D1 sync require1 do {x1'=x1, x2'=x2, x3'=x3, d1'=0} goto w1_ok2_w3;

loc non1_w2_ok3: while x3 <= WCET3 wait {x1'=0 & x2'=0 & x3'=1}
	when x3 = WCET3 sync done3 do {x1'=x1, x2'=x2', x3'=0} goto non1_ok2_non3;
	when x3 < WCET3 & d3 < D3 - D2 sync require1 do {x1'=x1, x2'=x2, x3'=x3, d1'=0} goto ok1_w2_w3;
	when x3 < WCET3 & d3 >= D3 - D2 sync require1 do {x1'=x1, x2'=x2, x3'=x3, d1'=0} goto w1_w2_ok3;

loc ok1_w2_w3: while x1 <= WCET1 wait {x1'=1 & x2'=0 & x3'=0}
	when x1 = WCET1 & d3 - d2 <= D3-D2 sync done1 do {x1'=0, x2'=x2, x3'=x3} goto non1_ok2_w3;
	when x1 = WCET1 & d3 - d2 > D3-D2 sync done1 do {x1'=0, x2'=x2, x3'=x3} goto non1_w2_ok3;

loc w1_ok2_w3: while x2 <= WCET2 wait {x1'=0 & x2'=1 & x3'=0}
	when x2 = WCET2 & d3 - d1 <= D3-D1 sync done2 do {x1'=x1, x2'=0, x3'=x3} goto ok1_non2_w3;
	when x2 = WCET2 & d3 - d1 > D3-D1 sync done2 do {x1'=x2, x2'=0, x3'=x3} goto w1_non2_ok3;

loc w1_w2_ok3: while x3 <= WCET3 wait {x1'=0 & x2'=0 & x3'=1}
	when x3 = WCET3 & d2 - d1 <= D2-D1 sync done3 do {x1'=x1, x2'=x2, x3'=0} goto ok1_w2_non3;
	when x3 = WCET3 & d2 - d1 > D2-D1 sync done3 do {x1'=x1, x2'=x2, x3'=0} goto w1_ok2_non3;

end

automaton T_1
var t_1:clock;
	per1, Off1:parameter;

synclabs: done1, require1;

initially init_s;

loc init_s: while t_1 <= Off1 wait {}
	when t_1 = Off1 sync require1 do {t_1'=0} goto waiting;

loc idle: while t_1 <= per1 wait {}
	when t_1 = per1 sync require1 do {t_1'=0} goto waiting;

loc waiting: while t_1 <= per1 wait {}
	when True sync done1 do {} goto idle;

end

automaton T_2
var t_2:clock;
	per2, Off2:parameter;
synclabs: done2, require2;

initially init_s;

loc init_s: while t_2 <= Off2 wait {}
	when t_2 = Off2 sync require2 do {t_2'=0} goto waiting;

loc idle: while t_2 <= per2 wait {}
	when t_2 = per2 sync require2 do {t_2'=0} goto waiting;

loc waiting: while t_2 <= per2 wait {}
	when True sync done2 do {} goto idle;

end

automaton T_3

var t_3:clock;
	per3, Off3:parameter;

synclabs: done3, require3;

initially init_s;

loc init_s: while t_3 <= Off3 wait {}
	when t_3 = Off3 sync require3 do {t_3'=0} goto waiting;

loc idle: while t_3 <= per3 wait {}
	when t_3 = per3 sync require3 do {t_3' = 0} goto waiting;

loc waiting: while t_3 <= per3 wait {}
	when True sync done3 do {} goto idle;

end

var init : region;

init := loc[stopper] = f_1_r &
	loc[scheduler_EDF] = non1_non2_non3 &
	loc[T_1] = init_s &
	loc[T_2] = init_s &
	loc[T_3]= init_s &
time = 0 &
x1 = 0 &
x2 = 0 &
x3 = 0 &
t_1 = 0 &
t_2 = 0 &
t_3 = 0 &
time = 0 &
d1 = 0 &
d2 = 0 & 
d3 = 0 --&
 
-- deadlineBasic = 134 &
---------
--Etude 1--
--WCET_1 = 20 &
--WCET_2 = 40 &
--WCET_3 = 100 &
--per1 = 100 &
--per2 = 150 &
--per3 = 350
--Off1 = 0
--Off1 = 94
--Off3 = 0
------------
-- Etude 2--
--WCET_1 = 1 &
--WCET_2 = 1 &
--WCET_3 = 2 &
--per1 = 3 &
--per2 = 5 &
--per3 = 10
------------
-- Etude 2--
--WCET_1 = 20 &
--WCET_2 = 40 &
--WCET_3 = 20 &
--per1 = 100 &
--per2 = 150 &
--per3 = 160
;