andre@pioupiou{Python} 2046 : python IMITATOR.py AndOr
 ***********************************************
 *                  IMITATOR                   *
 *                              Etienne ANDRE  *
 *                                2008 - 2009  *
 *  Laboratoire Specification et Verification  *
 *               ENS de Cachan & CNRS, France  *
 ***********************************************
 Tue, 03 Feb 2009 15:35:11
 Step 1
 Step 2
 Step 3
   Adding inequality               bpre_u + dAnd_u < dAUp_l
 Step 4
 Step 5
   Adding inequality               dOr_u + dAUp_u < bpre_l + dBDown_l
 Step 6
 Step 7
 Step 8
   Adding inequality               dOr_u < bpre_l
 Step 9
   Adding inequality               dAnd_u + dOr_u < bpre_l
     Removing redundant inequality dOr_u < bpre_l
 Step 10

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

 Intersection of the inequalities of all states in post* (after preprocessing):
      & bpre_l + dBDown_l <= dADown_u + dAUp_u
      & dAUp_l <= dAUp_u
      & 0 < dAnd_l
      & 0 < dOr_l
      & bpre_l <= bpre_u
      & dAnd_u + dOr_u < bpre_l
      & bpre_u + dAnd_u < dAUp_l
      & dOr_u + dAUp_u < bpre_l + dBDown_l
      & 0 < dADown_l
      & dBDown_l <= dBDown_u
      & dOr_l <= dOr_u
      & dAnd_l <= dAnd_u
      & dADown_l <= dADown_u

 IMITATOR ended with success :-)

 IMITATOR ended after 2.5 seconds
   Python execution time : 0.17s
   HyTech execution time : 2.07s (14 calls)
 ***********************************************