andre@pioupiou{Python} 2046 : python IMITATOR.py latchValmem *********************************************** * IMITATOR * * Etienne ANDRE * * 2008 - 2009 * * Laboratoire Specification et Verification * * ENS de Cachan & CNRS, France * *********************************************** Tue, 03 Feb 2009 13:51:34 Step 1 Adding inequality dSetup < dClockLow Step 2 Step 3 Step 4 Randomly choosing an inequality among 5 possible pi_0-incompatible inequalities Adding inequality dAndUp2_l < dHold Randomly choosing an inequality among 2 possible pi_0-incompatible inequalities Adding inequality dAndUp2_l < dNot1Down_l Adding inequality dAndUp2_l < dXorUp2Up_l Step 5 Randomly choosing an inequality among 5 possible pi_0-incompatible inequalities Adding inequality dXorUp2Up_l < dLatchUp_l + dAndUp2_l Randomly choosing an inequality among 2 possible pi_0-incompatible inequalities Adding inequality dNot1Down_l < dHold Step 6 Randomly choosing an inequality among 3 possible pi_0-incompatible inequalities Adding inequality dXorUp2Up_l < dHold Adding inequality dNot1Down_l < dLatchUp_l + dAndUp2_l Step 7 Randomly choosing an inequality among 3 possible pi_0-incompatible inequalities Adding inequality dLatchUp_l + dAndUp2_l < dHold Removing redundant inequality dAndUp2_l < dHold Adding inequality dNot2Up_l + dNot1Down_l < dLatchUp_l + dAndUp2_l Removing redundant inequality dNot1Down_l < dLatchUp_l + dAndUp2_l Step 8 Adding inequality dLatchUp_l + dAndUp2_l < dNot2Up_l + dNot1Down_l + dXorDown1Up_l Step 9 Adding inequality dHold < dNot2Up_l + dXorDown1Up_l + dNot1Down_l Step 10 Step 11 Step 12 Post* was reached at step 11 with 18 states (from 12 different locations) Intersection of the inequalities of all states in post* (after preprocessing): & dHold < dXorDown1Up_l + dNot2Up_l + dXorUp2Up_l & 0 <= dNot2Up_l & dXorUp2Up_l = dNot1Down_l & 0 <= dAndUp2_l & dLatchUp_l + dAndUp2_l < dHold & dAndUp2_l < dXorUp2Up_l & dXorUp2Up_l + dXorDown1Up_l + dAndDown1_l + dNot2Up_l <= dClockHigh & 0 <= dSetup & dSetup < dClockLow & 0 < dAndDown1_l & dXorUp2Up_l + dNot2Up_l < dLatchUp_l + dAndUp2_l IMITATOR ended with success :-) IMITATOR ended after 20.15 seconds Python execution time : 0.37s HyTech execution time : 16.85s (24 calls) ***********************************************