andre@pomelo{Python} 1001 : python IMITATOR.py simop *********************************************** * IMITATOR * * Etienne ANDRE * * 2008 - 2009 * * Laboratoire Specification et Verification * * ENS de Cachan & CNRS, France * *********************************************** Mon, 16 Feb 2009 08:22:49 Step 1 Step 2 Step 3 Step 4 Step 5 Adding inequality COMd < PLCmtt Step 6 Randomly choosing an inequality among 2 possible pi_0-incompatible inequalities Adding inequality NETd < PLCmtt Adding inequality NETd + COMd < PLCmtt Removing redundant inequality COMd < PLCmtt Removing redundant inequality NETd < PLCmtt Step 7 Randomly choosing an inequality among 2 possible pi_0-incompatible inequalities Adding inequality RIOd + NETd < PLCmtt Step 8 Randomly choosing an inequality among 2 possible pi_0-incompatible inequalities Adding inequality COMct < PLCct Step 9 Adding inequality RIOd + 2NETd < PLCmtt Step 10 Step 11 Step 12 Adding inequality PLCct < NETd + COMct + RIOd + COMd Step 13 Randomly choosing an inequality among 2 possible pi_0-incompatible inequalities Adding inequality PLCct < COMct + NETd + COMd + SIGmrt Adding inequality COMct + COMd < PLCct Removing redundant inequality COMct < PLCct Step 14 Randomly choosing an inequality among 2 possible pi_0-incompatible inequalities Adding inequality COMct + NETd + COMd < PLCct Removing redundant inequality COMct + COMd < PLCct Step 15 Randomly choosing an inequality among 5 possible pi_0-incompatible inequalities Adding inequality PLCct < NETd + COMct + SIGmrt Removing redundant inequality PLCct < COMct + NETd + COMd + SIGmrt Randomly choosing an inequality among 4 possible pi_0-incompatible inequalities Adding inequality RIOd + COMct < PLCct Randomly choosing an inequality among 2 possible pi_0-incompatible inequalities Adding inequality NETd + RIOd + COMct < PLCct Removing redundant inequality RIOd + COMct < PLCct Step 16 Step 17 Randomly choosing an inequality among 2 possible pi_0-incompatible inequalities Adding inequality 2NETd + COMct + RIOd < PLCct Step 18 Step 19 Randomly choosing an inequality among 8 possible pi_0-incompatible inequalities Adding inequality NETd + RIOd + PLCct < SIGmrt + COMct Removing redundant inequality PLCct < NETd + COMct + SIGmrt Randomly choosing an inequality among 5 possible pi_0-incompatible inequalities Adding inequality COMct < NETd + SIGmrt + COMd Randomly choosing an inequality among 4 possible pi_0-incompatible inequalities Adding inequality COMd + PLCct < 2COMct Randomly choosing an inequality among 3 possible pi_0-incompatible inequalities Adding inequality 2NETd + COMd + RIOd + PLCct < 2COMct Removing redundant inequality COMd + PLCct < 2COMct Step 20 Adding inequality COMct < SIGmrt + NETd Removing redundant inequality COMct < NETd + SIGmrt + COMd Step 21 Adding inequality COMct < SIGmrt Removing redundant inequality COMct < SIGmrt + NETd Step 22 Randomly choosing an inequality among 2 possible pi_0-incompatible inequalities Adding inequality PLCct < SIGmrt + NETd + COMd Adding inequality RIOd + COMct < SIGmrt Removing redundant inequality COMct < SIGmrt Step 23 Step 24 Adding inequality NETd + RIOd + COMct < SIGmrt Removing redundant inequality RIOd + COMct < SIGmrt Step 25 Step 26 Step 27 Randomly choosing an inequality among 4 possible pi_0-incompatible inequalities Adding inequality 2PLCct < COMct + NETd + COMd + SIGmrt Step 28 Adding inequality 2COMct < NETd + COMd + SIGmrt Step 29 Randomly choosing an inequality among 5 possible pi_0-incompatible inequalities Adding inequality 2COMct < SIGmrt + NETd Removing redundant inequality 2COMct < NETd + COMd + SIGmrt Randomly choosing an inequality among 4 possible pi_0-incompatible inequalities Adding inequality COMd + RIOd + 2PLCct + NETd < 3COMct Adding inequality COMd + RIOd + 2PLCct + 2NETd < 3COMct Step 30 Adding inequality 2COMct < SIGmrt Removing redundant inequality 2COMct < SIGmrt + NETd Step 31 Adding inequality RIOd + 2COMct < SIGmrt Removing redundant inequality 2COMct < SIGmrt Step 32 Step 33 Adding inequality NETd + RIOd + 2COMct < SIGmrt Removing redundant inequality RIOd + 2COMct < SIGmrt Step 34 Step 35 Randomly choosing an inequality among 4 possible pi_0-incompatible inequalities Adding inequality 2PLCct < SIGmrt + NETd Removing redundant inequality 2PLCct < COMct + NETd + COMd + SIGmrt Randomly choosing an inequality among 3 possible pi_0-incompatible inequalities Adding inequality RIOd + COMct + NETd + 2PLCct < SIGmrt + PLCmtt Step 36 Step 37 Randomly choosing an inequality among 5 possible pi_0-incompatible inequalities Adding inequality COMd + 3PLCct < 4COMct Randomly choosing an inequality among 4 possible pi_0-incompatible inequalities Adding inequality RIOd + COMd + 3PLCct + NETd < 4COMct Removing redundant inequality COMd + 3PLCct < 4COMct Randomly choosing an inequality among 2 possible pi_0-incompatible inequalities Adding inequality 3COMct < SIGmrt + NETd + COMd Adding inequality COMd + 3PLCct + 2NETd + RIOd < 4COMct Step 38 Adding inequality 3COMct < SIGmrt + NETd Removing redundant inequality 3COMct < SIGmrt + NETd + COMd Step 39 Randomly choosing an inequality among 3 possible pi_0-incompatible inequalities Adding inequality 4COMct < 3PLCct + COMd + PLCmtt + 2NETd + RIOd Randomly choosing an inequality among 2 possible pi_0-incompatible inequalities Adding inequality 3COMct < SIGmrt Removing redundant inequality 3COMct < SIGmrt + NETd Adding inequality 4COMct < 3PLCct + COMd + PLCmtt + NETd + RIOd Step 40 Adding inequality RIOd + 3COMct < SIGmrt Removing redundant inequality 3COMct < SIGmrt Step 41 Step 42 Step 43 Step 44 Step 45 Step 46 Adding inequality 4COMct < NETd + SIGmrt + COMd Step 47 Adding inequality 4COMct < SIGmrt + NETd Removing redundant inequality 4COMct < NETd + SIGmrt + COMd Step 48 Adding inequality 4COMct < SIGmrt Removing redundant inequality 4COMct < SIGmrt + NETd Step 49 Adding inequality RIOd + 4COMct < SIGmrt Removing redundant inequality 4COMct < SIGmrt Step 50 Step 51 Step 52 Post* was reached at step 51 with 956 states (from 71 different locations) Intersection of the inequalities of all states in post* (after preprocessing): & 3PLCct + RIOd + PLCmtt + 2NETd <= 4COMct & 3PLCct + NETd + PLCmtt + COMd <= 4COMct & 0 < NETd & NETd + COMd < PLCmtt & RIOd + 2NETd < PLCmtt & PLCct < COMct + NETd + RIOd + COMd & 4COMct < 3PLCct + COMd + RIOd + PLCmtt + NETd & RIOd + 4COMct < SIGmrt & COMct + PLCmtt <= PLCct IMITATOR ended with success :-) IMITATOR ended after 25144.6 seconds Python execution time : 152.7s HyTech execution time : 24986.01s (98 calls) ***********************************************