-- ABR

var 	S: clock;
	E, Rnew, CR, FR, LR, AP, tfi, tla, Emx: discrete;
	t, a, b: parameter;



--****************************************************--
--****************************************************--
-- AUTOMATA
--****************************************************--
--****************************************************--


--****************************************************--
automaton env
--****************************************************--
synclabs: newRM, newD;
initially Wait;

loc Wait: while S <= t wait {}
	when True sync newRM do {Rnew'>0} goto Wait;
	when S=t sync newD goto RecD;

loc RecD: while True wait {}
	when True goto RecD;
end -- env

--****************************************************--
automaton observer
--****************************************************--
synclabs: newRM, newD;
initially Idle;

loc Idle: while True wait {}
	when True sync newRM goto updE;
	when True sync newD goto End;

loc updE: while True wait {}
	when t<S+a & asap goto Idle;
	when S+a <= t & t < S+b & asap & Rnew > E 
		do {E'= Rnew} goto Idle;
	when S+a <= t & t < S+b & asap & Rnew <= E 
		 goto Idle;
	when t >= S+b & asap 
		do {E'= Rnew} goto Idle;

loc End: while True wait {}
	when True sync newD goto End;

end -- observer


--****************************************************--
automaton approx
--****************************************************--
synclabs: newRM, newD;
initially Greater;

loc Less : while S <= tfi wait {}
	when S = tfi & tfi < tla  -- [9b]
                do {tfi'= tla, CR'= FR, FR'= LR, Emx'= LR} goto Less;
	when S < tfi sync newRM goto updAL;
	when S = tfi & tfi = tla -- [9a]
		do {CR'= FR, FR'= LR, Emx'= LR} goto Greater;
	when S < tfi sync newD goto Test;

loc updAL : while True wait {}
	when Emx <= Rnew & tfi < S+a & tfi = tla & asap
	do {LR'= Rnew, Emx'= Rnew, tla'= S+a} goto Less; -- [1a]
	when Emx <= Rnew & tfi < S+a & S+a < tla & asap
	do {LR'= Rnew, Emx'= Rnew, tla'= S+a} goto Less; --[1b]
	when Emx <= Rnew & tla <= S+a & tfi < tla & asap
	do {LR'= Rnew, Emx'= Rnew} goto Less; --[2]
	when Emx <= Rnew & tfi >= S+a & CR <= Rnew
	do {LR'= Rnew, Emx'= Rnew, FR'= Rnew, tfi'= S+a, tla'= S+a} 
	goto Less; -- [3]
	when Emx <= Rnew & tfi >= S+a & CR > Rnew & asap
	do {LR'=Rnew, Emx'= Rnew, FR'= Rnew, tla'= tfi} 
	goto Less; -- [4]
	when Emx > Rnew & Rnew < LR & asap
	do {FR'= Emx, LR'= Rnew, tla'= S+b} 
	goto Less; -- [5]
	when Emx > Rnew & Rnew >= LR & asap
	do {FR'= Emx, FR'= Rnew} 
	goto Less; -- [6]

loc Greater : while True wait {}
	when True sync newRM goto updAG;
	when True sync newD goto Test;

loc updAG : while True wait {}
	when CR<= Rnew & asap 
	do {FR'= Rnew, LR'=Rnew, Emx'= Rnew, tfi'=S+a, tla'=S+a}
	goto Less; -- [7]
	when CR> Rnew & asap 
	do {FR'= Rnew, LR'=Rnew, Emx'= Rnew, tfi'=S+b, tla'=S+b}
	goto Less; -- [8]

loc Test : while True wait {}
	when True goto Test;


end -- approx




--****************************************************--
--****************************************************--
-- ANALYSIS
--****************************************************--
--****************************************************--

var init_reg, pre_reg, post_reg, bad_reg, nZ, interEnd : region;

init_reg := loc[observer]=Idle & loc[approx]=Greater & loc[env]=Wait 
	& S=tfi & tfi=tla & tfi >=0 
	& E= Emx & CR= Emx & FR= Emx & LR= Emx
--	& 0 < a & a < b
	---START PI0---
--	& a= 3
--	& b=7
--	& t=20
	---END PI0---
;


post_reg := reach forward from init_reg endreach;

prints "---START LOG---";
print (hide non_parameters in post_reg endhide);
prints "---END LOG---";