andre@pioupiou{Python} 1001 : python IMITATOR.py brp
 ***********************************************
 *                  IMITATOR                   *
 *                              Etienne ANDRE  *
 *                                2008 - 2009  *
 *  Laboratoire Specification et Verification  *
 *               ENS de Cachan & CNRS, France  *
 ***********************************************
 Thu, 05 Feb 2009 14:37:03
 Step 1
 Step 2
 Step 3
   Adding inequality               1 < N
 Step 4
   Adding inequality               TD < T1
 Step 5
 Step 6
 Step 7
   Adding inequality               1 < MAX
 Step 8
   Randomly choosing an inequality among 2 possible pi_0-incompatible inequalities
   Adding inequality               2TD < T1
   Adding inequality               TD < TR
 Step 9
   Randomly choosing an inequality among 2 possible pi_0-incompatible inequalities
   Adding inequality               MAX <= 2
   Adding inequality               T1 <= TR
 Step 10
   Randomly choosing an inequality among 2 possible pi_0-incompatible inequalities
   Adding inequality               TD + T1 <= TR
   Adding inequality               N <= 2
 Step 11
   Adding inequality               2T1 <= TR
 Step 12
   Adding inequality               TD + 2T1 <= TR
 Step 13
   Adding inequality               3T1 <= TR
 Step 14
 Step 15
 Step 16
   Adding inequality               TD + 3T1 < TR
     Removing redundant inequality TD < TR
     Removing redundant inequality 3T1 <= TR
 Step 17
 Step 18
   Adding inequality               2TD + 3T1 <= TR
 Step 19
   Adding inequality               3TD + 3T1 <= TR
 Step 20
   Adding inequality               2TD + 4T1 <= TR
 Step 21
   Adding inequality               3TD + 4T1 <= TR
 Step 22
 Step 23
 Step 24
 Step 25
 Step 26
 Step 27
 Step 28
 Step 29
 Step 30

 Post* was reached at step 29 with 427 states (from 25 different locations)

 Intersection of the inequalities of all states in post* (after preprocessing):
      & 5T1 < TD + TR
      & N = 2
      & MAX = 2
      & 0 < TD
      & TR <= TD + SYNC
      & 2TD < T1
      & 3TD + 4T1 <= TR
      & TR < 2TD + 5T1

 IMITATOR ended with success :-)

 IMITATOR ended after 923.23 seconds
   Python execution time : 13.53s
   HyTech execution time : 908.76s (47 calls)
 ***********************************************