--****************************************************--
--****************************************************--
--   Laboratoire Specification et Verification
--
--   Example of PTA for comparing the variants of IM
--
--   Etienne ANDRE
--
--   Created       : 2011/03/08
--   Last modified : 2011/03/08
--****************************************************--
--****************************************************--

var 	x1, x2
		: clock;
	p1, p2
		: parameter;


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


--****************************************************--
  automaton aa
--****************************************************--
synclabs: a, b, c;
initially Q0;

loc Q0: while 2 x1 <= p1 & x1 <= 2 wait {}
	when True sync a do {x1' = 0, x2' = 0} goto Q1;
	when x1 >= p2 sync c do {} goto Q4;

loc Q1: while True wait {}
	when x1 >= p1 sync a do {} goto Q2;
	when x1 >= 3 sync b do {} goto Q3;
-- 	when True sync c do {} goto Q3;


loc Q3: while x1 <= p2 wait {}
	when True sync b do {} goto Q3;

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

loc Q4: while True wait {}
	when True sync c goto Q4;

end -- aa



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

var init
	: region;

init :=
	----------------------
	-- Initial locations
	----------------------
	  loc[aa] = Q0

	----------------------
	-- Clocks
	----------------------
	& x1 = 0
	& x2 = 0
	
	----------------------
	-- initial constraint
	----------------------
	& p1 >= 0
	& p2 >= 0
;

-- init := reach forward from init endreach;