(************************************************************
 *                      IMITATOR MODEL                      
 *
 * Modeling of an "AND" and an "OR" logical gate
 *
 * Description     : Modeling of an "AND" and an "OR" logical gate
 * Correctness     : Alternating sequence: b- x- a- b+ a+ x+
 * Source          : From "Verification of Concurrent Systems with Parametric Delays Using Octahedra" (2005) by Clariso and Cortadella; Fig 3a
 * Author          : Roberto Clariso and Jordi Cortadella
 * Modeling        : Etienne Andre and Laurent Fribourg
 * Input by        : Etienne Andre
 *
 * Created         : 2008/01
 * Last modified   : 2020/04/30
 *
 * IMITATOR version: 3
 ************************************************************)

property := #synth IM(
(*	--- STANDARD ---*)
	& dA_High_l = 13
	& dA_High_u = 14
	& dA_Low_l = 16
	& dA_Low_u = 18
(*-- 	& dB_High_l = 10
-- 	& dB_High_u = 12*)
	& dB_High_l = 7
	& dB_High_u = 8
	& dB_Low_l = 19
	& dB_Low_u = 20
	& dAnd_l = 3
	& dAnd_u = 4
	& dOr_l = 1
	& dOr_u = 2

(*
	--- LOOPING PI0 ! ---
-- 	& dA_High_l = 13
-- 	& dA_High_u = 14
-- 	& dA_Low_l = 16
-- 	& dA_Low_u = 18
-- 	& dB_High_l = 2 -- this value is responsible for the loop
-- 	& dB_High_u = 3
-- 	& dB_Low_l = 19
-- 	& dB_Low_u = 20
-- 	& dAnd_l = 3
-- 	& dAnd_u = 4
-- 	& dOr_l = 1
-- 	& dOr_u = 2
-- 
*)
);