--****************************************************--
--   Laboratoire Specification et Verification
--
--   Modeling of an "AND" and an "OR" logical gate
--   From "Verification of Concurrent Systems with Parametric Delays Using Octahedra" by Clariso and Cortadella
--
--   Modelisation: Etienne ANDRE and Laurent FRIBOURG
--
--   Version SANS compteur de B^\up
--   Version SANS variables discretes reprenant les valeurs des signaux
--
--   Created       : 2008/01
--   Last modified : 2010/12/08
--****************************************************--

var 	ckOr, ckAnd, cka, ckb
		: clock;

-- 	qa, qx
-- 		: discrete;

	dA_High_l, dA_High_u,
	dA_Low_l, dA_Low_u,
	dB_High_l, dB_High_u,
	dB_Low_l, dB_Low_u,
	dOr_l, dOr_u,
	dAnd_l, dAnd_u
			: parameter;
-- 	bpre_l, bpre_u  -- corresponds to the end of the high part of B
			-- following the rise of A



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


--****************************************************--
  automaton input
--****************************************************--
synclabs: aUp, aDown, bUp, bDown;
initially InputInit;

loc InputInit: while ckb <= dB_High_u wait {}
	when ckb >= dB_High_l sync bDown do {ckb' = 0} goto Input2; -- & nbB < nbBmax  // nbB' = nbB + 1 , 

loc Input2: while cka <= dA_High_u wait {}
	when cka >= dA_High_l sync aDown do {cka' = 0} goto Input3; --, qa'=0

loc Input3: while ckb <= dB_Low_u wait {}
	when ckb >= dB_Low_l sync bUp do {ckb' = 0} goto Input4;

loc Input4: while cka <= dA_Low_u wait {}
	when cka >= dA_Low_l sync aUp do {cka' = 0, ckb' = 0} goto InputInit; -- ,qa'=1

end -- input


--****************************************************--
  automaton andGate
--****************************************************--
-- Input 1 : t (output of OR)
-- Input 2 : b
-- Output : x

synclabs: tUp, tDown, bUp, bDown,
	xUp, xDown;
initially And111;

loc And000: while ckAnd >= 0 wait {}
	when True sync tUp do {} goto And100;
	when True sync bUp do {} goto And010;

loc And001: while ckAnd <= dAnd_u & ckAnd>=0 wait {}
	when True sync tUp do {ckAnd' = 0} goto And101;
	when True sync bUp do {ckAnd' = 0} goto And011;
	when ckAnd >= dAnd_l sync xDown do {} goto And000; -- qx'=0

loc And010: while ckAnd >= 0 wait {}
	when True sync tUp do {ckAnd' = 0} goto And110;
	when True sync bDown do {} goto And000;

loc And011: while ckAnd <= dAnd_u & ckAnd>=0 wait {}
	when True sync tUp do {} goto And111;
	when True sync bDown do {ckAnd' = 0} goto And001;
	when ckAnd >= dAnd_l sync xDown do {} goto And010; -- qx'=0

loc And100: while ckAnd >= 0 wait {}
	when True sync tDown do {} goto And000;
	when True sync bUp do {ckAnd' = 0} goto And110;

loc And101: while ckAnd <= dAnd_u & ckAnd>=0 wait {}
	when True sync tDown do {ckAnd' = 0} goto And001;
	when True sync bUp do {} goto And111;
	when ckAnd >= dAnd_l sync xDown do {} goto And100; -- qx'=0

loc And110: while ckAnd <= dAnd_u& ckAnd>=0  wait {}
	when True sync tDown do {} goto And010;
	when True sync bDown do {} goto And100;
	when ckAnd >= dAnd_l sync xUp do {} goto And111; -- qx'=1

loc And111: while ckAnd >= 0 wait {}
	when True sync tDown do {ckAnd' = 0} goto And011;
	when True sync bDown do {ckAnd' = 0} goto And101;
end -- andGate


--****************************************************--
  automaton orGate
--****************************************************--
-- Input 1 : x (output of AND)
-- Input 2 : a
-- Output : t

synclabs: xUp, xDown, aUp, aDown,
	tUp, tDown;
initially Or111;

loc Or000: while ckOr >= 0 wait {}
	when True sync xUp do {ckOr' = 0} goto Or100;
	when True sync aUp do {ckOr' = 0} goto Or010;

loc Or001: while ckOr <= dOr_u & ckOr >= 0 wait {}
	when True sync xUp do {} goto Or101;
	when True sync aUp do {} goto Or011;
	when ckOr >= dOr_l sync tDown do {} goto Or000;

loc Or010: while ckOr <= dOr_u & ckOr >= 0 wait {}
	when True sync xUp do {ckOr' = 0} goto Or110;
	when True sync aDown do {} goto Or000;
	when ckOr >= dOr_l sync tUp do {} goto Or011;

loc Or011: while ckOr >= 0 wait {}
	when True sync xUp do {} goto Or111;
	when True sync aDown do {ckOr' = 0} goto Or001;

loc Or100: while ckOr <= dOr_u & ckOr >= 0 wait {}
	when True sync xDown do {} goto Or000;
	when True sync aUp do {ckOr' = 0} goto Or110;
	when ckOr >= dOr_l sync tUp do {} goto Or101;

loc Or101: while ckOr >= 0 wait {}
	when True sync xDown do {ckOr' = 0} goto Or001;
	when True sync aUp do {} goto Or111;

loc Or110: while ckOr <= dOr_u & ckOr >= 0 wait {}
	when True sync xDown do {ckOr' = 0} goto Or010;
	when True sync aDown do {ckOr' = 0} goto Or100;
	when ckOr >= dOr_l sync tUp do {} goto Or111;

loc Or111: while ckOr >= 0 wait {}
	when True sync xDown do {} goto Or011;
	when True sync aDown do {} goto Or101;
end -- orGate



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

var init : region;

init :=
	----------------------
	-- Initial locations
	----------------------
	  loc[input] = InputInit
	& loc[andGate] = And111
	& loc[orGate] = Or111
-- 	& qa=1 & qx=1


	----------------------
	-- Clocks
	----------------------
	& ckOr  >= 0
	& ckAnd >= 0
	& cka   =  0
	& ckb   =  0
	& ckb   <= dB_High_u

	----------------------
	-- Constraints
	----------------------
	& dA_High_l <= dA_High_u
	& dA_Low_l <= dA_Low_u

	& dB_High_l <= dB_High_u
	& dB_Low_l <= dB_Low_u

	& dOr_l <= dOr_u
	& dAnd_l <= dAnd_u	

	& 0 <= dA_High_l 
	& 0 <= dA_Low_l 
	& 0 <= dB_High_l 
	& 0 <= dB_Low_l 
	& 0 <= dOr_l 
	& 0 <= dAnd_l


;