andre@pioupiou{Python} 2046 : python IMITATOR.py flipflop
 ***********************************************
 *                  IMITATOR                   *
 *                              Etienne ANDRE  *
 *                                2008 - 2009  *
 *  Laboratoire Specification et Verification  *
 *               ENS de Cachan & CNRS, France  *
 ***********************************************
 Tue, 03 Feb 2009 14:55:26
 Step 1
   Adding inequality               tSetup < tLO
 Step 2
 Step 3
   Adding inequality               dG1_u < tSetup
 Step 4
 Step 5
   Adding inequality               dG3_u < tHold
 Step 6
 Step 7
   Adding inequality               dG4_u + dG3_u < tHI
 Step 8
 Step 9
   Adding inequality               0 < dG1_l

 Post* was reached at step 8 with 11 states (from 9 different locations)

 Intersection of the inequalities of all states in post* (after preprocessing):
      & dG2_l <= dG2_u
      & 0 < dG1_l
      & tSetup < tLO
      & 0 <= dG3_u
      & dG3_l <= dG3_u
      & dG1_l <= dG1_u
      & dG1_u < tSetup
      & tHold <= dG4_u + dG3_u
      & dG4_u + dG3_u < tHI
      & dG3_u < tHold
      & dG4_l + dG3_l <= tHold
      & dG4_l <= dG4_u
      & dG4_l <= tHold

 IMITATOR ended with success :-)

 IMITATOR ended after 2.06 seconds
   Python execution time : 0.14s
   HyTech execution time : 1.67s (14 calls)
 ***********************************************