--****************************************************--
--****************************************************--
--   Laboratoire Specification et Verification
--
--   Modeling of the circuit described in "Verification of timed circuits with symbolic delays" (Clariso -- Cortadella)
--   Non deterministic trace with pi_0 verifying Clariso -- Cortadella's constraints
--
--   Etienne ANDRE and Laurent FRIBOURG
--
--   Created      : 2010/03/24
--   Last modified: 2010/12/10
--****************************************************--
--****************************************************--



----- BAD ONE -----
-- 	& tHI = 20
-- 	& tLO = 15
-- 	& tSetup = 10
-- 	& tHold = 15
-- 	& dG1_l = 1
-- 	& dG1_u = 1
-- 	& dG2_l = 8
--  	& dG2_u = 10
-- 	& dG3_l = 5
--  	& dG3_u = 6
-- 	& dG4_l = 3
-- 	& dG4_u = 5




-- ----- PI0 IJFCS -----
-- 	& tHI=24
-- 	& tLO=15
-- 	& tSetup= 10
-- 	& tHold= 17
-- 	& dG1_l = 7
-- 	& dG1_u = 7
-- 	& dG2_l=5
-- 	& dG2_u= 6
-- 	& dG3_l=8
-- 	& dG3_u= 10
-- 	& dG4_l=3
-- 	& dG4_u=7

----- V0 : dG3_u et dG4_u-----
	& tHI    = 24
	& tLO    = 15
	& tSetup = 10
	& tHold  = 17
	& dG1_l  = 7
	& dG1_u  = 7
	& dG2_l  = 5
	& dG2_u  = 6
	& dG3_l  = 8
	& dG3_u  = 8 .. 30 -- 10
	& dG4_l  = 3
	& dG4_u  = 3 .. 30 -- 7

----- V0 : TOUT-----
-- 	& tHI    = 0 .. 30 -- 24
-- 	& tLO    = 0 .. 30 -- 15
-- 	& tSetup = 0 .. 30 -- 10
-- 	& tHold  = 0 .. 30 -- 17
-- 	& dG1_l  = 0 .. 30 -- 7
-- 	& dG1_u  = 0 .. 30 -- 7
-- 	& dG2_l  = 0 .. 30 -- 5
-- 	& dG2_u  = 0 .. 30 -- 6
-- 	& dG3_l  = 0 .. 30 -- 8
-- 	& dG3_u  = 0 .. 30 -- 8 .. 30
-- 	& dG4_l  = 0 .. 30 -- 3
-- 	& dG4_u  = 0 .. 30 -- 3 .. 30