--****************************************************--
--****************************************************--
--   Toy Example
--
--   Modeling by Etienne ANDRE (LSV)
--
--   Created :       29/11/2008
--   Last modified : 29/11/2008
--****************************************************--
--****************************************************--

var 	x1, x2
		: clock;

	p1, p2, p3
			: parameter;

--****************************************************--
--****************************************************--
-- AUTOMATON
--****************************************************--
--****************************************************--

--****************************************************--
automaton toy
--****************************************************--
synclabs: a, b;
initially Q0;

loc Q0: while x1 <= p1 wait {}
	when x2 >= p2 sync a do {x1' = 0} goto Q1;
	when x1 >= p3 sync b do {}        goto Q2;

loc Q1: while x1 >= 0 wait {}
	when True do {} goto Q1;

loc Q2: while x1 >= 0 wait {}
	when True do {} goto Q2;
end -- toy

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

var init_reg, post_reg
	: region;

init_reg :=
	----------------------
	-- Initial locations
	----------------------
	  loc[toy] = Q0

	----------------------
	-- Clocks
	----------------------
	& x1 = 0
	& x2 = 0

	----------------------
	---START PI0---
	----------------------
--	& p1 = 4
--	& p2 = 2
--	& p3 = 6
	----------------------
	---END PI0---
	----------------------
;

post_reg := reach forward from init_reg endreach;


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