***********************************************
 *                  IMITATOR                   *
 *                              Etienne ANDRE  *
 *                                2008 - 2009  *
 *  Laboratoire Specification et Verification  *
 *               ENS de Cachan & CNRS, France  *
 ***********************************************
 Mon, 20 Apr 2009 12:43:56
 Step 1
 Step 2
 Step 3
 Step 4
 Step 5
 Step 6
   Adding inequality               0 < lambda
 Step 7
   Randomly choosing an inequality among 6 possible pi_0-incompatible inequalities
   Adding inequality               sigma < timeslot
   Randomly choosing an inequality among 3 possible pi_0-incompatible inequalities
   Adding inequality               3timeslot < lambda
     Removing redundant inequality 0 < lambda
 Step 8
 Step 9
   Randomly choosing an inequality among 3 possible pi_0-incompatible inequalities
   Adding inequality               6timeslot < lambda
 Step 10
 Step 11
   Randomly choosing an inequality among 3 possible pi_0-incompatible inequalities
   Adding inequality               8timeslot < lambda
   Adding inequality               9timeslot < lambda
 Step 12
 Step 13
   Randomly choosing an inequality among 3 possible pi_0-incompatible inequalities
   Adding inequality               12timeslot < lambda
 Step 14
 Step 15
   Randomly choosing an inequality among 3 possible pi_0-incompatible inequalities
   Adding inequality               14timeslot < lambda
   Adding inequality               15timeslot < lambda
 Step 16
 Step 17
   Randomly choosing an inequality among 3 possible pi_0-incompatible inequalities
   Adding inequality               lambda < 18timeslot
   Randomly choosing an inequality among 2 possible pi_0-incompatible inequalities
   Adding inequality               lambda < 16timeslot
 Step 18

 Post* was reached at step 17 with 218 states (from 50 different locations)

 Intersection of the inequalities of all states in post* (after simplification):
      & 0 <= sigma
      & 15timeslot < lambda
      & sigma < timeslot
      & lambda < 16timeslot

 IMITATOR ended with success :-)

 IMITATOR ended after 43.94 seconds
   Python execution time : 1.26s
   HyTech execution time : 42.2s (29 calls)
 ***********************************************