andre@pioupiou{Python} 1001 : python IMITATOR.py RCP
 ***********************************************
 *                  IMITATOR                   *
 *                              Etienne ANDRE  *
 *                                2008 - 2009  *
 *  Laboratoire Specification et Verification  *
 *               ENS de Cachan & CNRS, France  *
 ***********************************************
 Mon, 20 Apr 2009 11:31:48
 Step 1
 Step 2
   Randomly choosing an inequality among 2 possible pi_0-incompatible inequalities
   Adding inequality               0 < rc_slow_min
   Adding inequality               0 < rc_fast_min
 Step 3
   Randomly choosing an inequality among 3 possible pi_0-incompatible inequalities
   Adding inequality               delay < rc_fast_min
     Removing redundant inequality 0 < rc_fast_min
   Randomly choosing an inequality among 2 possible pi_0-incompatible inequalities
   Adding inequality               delay < rc_slow_min
     Removing redundant inequality 0 < rc_slow_min
 Step 4
 Step 5
   Adding inequality               rc_fast_max < rc_slow_min
 Step 6
   Adding inequality               delay + rc_fast_max < rc_slow_min
     Removing redundant inequality delay < rc_slow_min
     Removing redundant inequality rc_fast_max < rc_slow_min
 Step 7
 Step 8
 Step 9
 Step 10
 Step 11
 Step 12
   Randomly choosing an inequality among 2 possible pi_0-incompatible inequalities
   Adding inequality               2delay < rc_slow_min
   Adding inequality               2delay < rc_fast_min
 Step 13
 Step 14
   Adding inequality               2delay + rc_fast_max < rc_slow_min
     Removing redundant inequality 2delay < rc_slow_min
 Step 15
 Step 16
 Step 17
 Step 18
 Step 19

 Post* was reached at step 18 with 229 states (from 52 different locations)

 Intersection of the inequalities of all states in post* (after simplification):
      & 2delay + rc_fast_max < rc_slow_min
      & rc_slow_min <= rc_slow_max
      & 2delay < rc_fast_min
      & 0 <= delay
      & rc_fast_min <= rc_fast_max

 IMITATOR ended with success :-)

 IMITATOR ended after 64.14 seconds
   Python execution time : 2.15s
   HyTech execution time : 61.49s (28 calls)
 ***********************************************