(************************************************************
 *                      IMITATOR MODEL                      
 *
 * Modeling of the circuit described in "Verification of timed circuits with symbolic delays" (Clariso -- Cortadella)
 *
 * Description     : A flip-flop circuit made of 4 gates. The environment is such that D raises, then CK raises then D falls, and then CK falls. No discrete variable.
 * Correctness     : Q should raise before CK falls
 * Source          : "Verification of timed circuits with symbolic delays" (Clariso -- Cortadella); Design Automation Conference, 2004. Proceedings of the ASP-DAC 2004. Asia and South Pacific; DOI: 10.1109/ASPDAC.2004.1337668
 * Author          : Roberto Clariso and Jordi Cortadella
 * Modeling        : Étienne André and Laurent Fribourg
 * Input by        : Étienne André
 *
 * Created         : 2007/11
 * Last modified   : 2020/09/14
 *
 * IMITATOR version: 3.0
 ************************************************************)
 
(* Not exactly the property that we would like! The real property is qUp and ckDown always occur, and qUp occurs before ckDown *)
property := #synth pattern(if ckDown then qUp has happened before);