andre@pioupiou{Python} 2046 : python IMITATOR.py toyPTA *********************************************** * IMITATOR * * Etienne ANDRE * * 2008 - 2009 * * Laboratoire Specification et Verification * * ENS de Cachan & CNRS, France * *********************************************** Tue, 03 Feb 2009 10:52:44 Step 1 Randomly choosing an inequality among 2 possible pi_0-incompatible inequalities Adding inequality 0 < p2 Adding inequality 0 < p3 Step 2 Adding inequality p1 < p3 Removing redundant inequality 0 < p3 Step 3 Post* was reached at step 2 with 2 states (from 2 different locations) Intersection of the inequalities of all states in post* (after preprocessing): & 0 < p2 & p1 < p3 & p2 <= p1 Script ended with success :-) Script ended after 0.37 seconds Python execution time : 0.01s HyTech execution time : 0.19s (6 executions) ***********************************************