andre@pomelo{Python} 1001 : python IMITATOR.py spsmall *********************************************** * IMITATOR * * Etienne ANDRE * * 2008 - 2009 * * Laboratoire Specification et Verification * * ENS de Cachan & CNRS, France * *********************************************** Wed, 11 Feb 2009 14:47:35 Step 1 Adding inequality tsetupd < tLO + tHI Step 2 Step 3 Adding inequality tsetupd < tLO + d_up_d_h Step 4 Randomly choosing an inequality among 10 possible pi_0-incompatible inequalities Adding inequality tLO < tsetupwen + d_up_en_latchd Randomly choosing an inequality among 6 possible pi_0-incompatible inequalities Adding inequality tsetupd < tsetupwen + d_up_d_h Randomly choosing an inequality among 3 possible pi_0-incompatible inequalities Adding inequality tLO < tsetupwen + d_up_net13a Adding inequality tsetupwen + d_up_en_latchwen < tLO Step 5 Adding inequality tLO < d_up_net45 + tsetupwen + d_up_net45a + d_up_en_latchwen Step 6 Randomly choosing an inequality among 15 possible pi_0-incompatible inequalities Adding inequality tLO + d_dn_wen_h < d_up_net45 + tsetupwen + d_up_net45a + d_up_en_latchwen Removing redundant inequality tLO < d_up_net45 + tsetupwen + d_up_net45a + d_up_en_latchwen Randomly choosing an inequality among 10 possible pi_0-incompatible inequalities Adding inequality d_up_net13a < d_up_en_latchd Randomly choosing an inequality among 6 possible pi_0-incompatible inequalities Adding inequality d_up_net13a < tLO Randomly choosing an inequality among 3 possible pi_0-incompatible inequalities Adding inequality tsetupd + d_up_net13a < tLO + d_up_d_h Removing redundant inequality tsetupd < tLO + d_up_d_h Adding inequality tsetupwen + d_up_net13a < tLO + d_dn_wen_h Step 7 Randomly choosing an inequality among 10 possible pi_0-incompatible inequalities Adding inequality d_up_d_h < tsetupd Randomly choosing an inequality among 6 possible pi_0-incompatible inequalities Adding inequality d_up_net13a + d_up_wela + tsetupd < tLO + d_up_d_h Removing redundant inequality tsetupd + d_up_net13a < tLO + d_up_d_h Randomly choosing an inequality among 3 possible pi_0-incompatible inequalities Adding inequality d_up_net13a + d_up_wela < d_up_en_latchd Removing redundant inequality d_up_net13a < d_up_en_latchd Adding inequality tsetupwen + d_up_net13a + d_up_wela < tLO + d_dn_wen_h Removing redundant inequality tsetupwen + d_up_net13a < tLO + d_dn_wen_h Step 8 Randomly choosing an inequality among 3 possible pi_0-incompatible inequalities Adding inequality tLO + d_dn_wen_h < tsetupwen + d_up_en_latchd Removing redundant inequality tLO < tsetupwen + d_up_en_latchd Adding inequality tsetupd + d_dn_wen_h < tsetupwen + d_up_d_h Removing redundant inequality tsetupd < tsetupwen + d_up_d_h Step 9 Randomly choosing an inequality among 3 possible pi_0-incompatible inequalities Adding inequality tsetupwen + d_up_en_latchd < d_dn_net45 + d_dn_wen_h + d_dn_net45a + tLO Adding inequality tsetupd + d_up_en_latchd < tLO + d_up_d_h Step 10 Randomly choosing an inequality among 3 possible pi_0-incompatible inequalities Adding inequality tsetupd + d_dn_net45 + d_dn_net45a + d_dn_wen_h < tsetupwen + d_up_d_h Removing redundant inequality tsetupd + d_dn_wen_h < tsetupwen + d_up_d_h Adding inequality d_dn_net45 + d_dn_net45a + tLO + d_dn_wen_h < d_dn_d_int + d_up_en_latchd + tsetupwen + d_dn_d_inta Step 11 Randomly choosing an inequality among 3 possible pi_0-incompatible inequalities Adding inequality tLO + d_up_d_h < d_dn_d_int + tsetupd + d_dn_d_inta + d_up_en_latchd Adding inequality d_dn_net45a + tsetupd + d_up_wela + d_dn_wen_h + d_dn_net45 < tsetupwen + d_up_d_h Removing redundant inequality tsetupd + d_dn_net45 + d_dn_net45a + d_dn_wen_h < tsetupwen + d_up_d_h Step 12 Step 13 Adding inequality tsetupd < d_up_d_int + d_up_d_h + d_up_d_inta Step 14 Randomly choosing an inequality among 10 possible pi_0-incompatible inequalities Adding inequality d_dn_en_latchwen < d_dn_en_latchd Randomly choosing an inequality among 6 possible pi_0-incompatible inequalities Adding inequality d_dn_en_latchwen < d_dn_net13a Randomly choosing an inequality among 3 possible pi_0-incompatible inequalities Adding inequality d_dn_en_latchwen < tHI Adding inequality tsetupd + d_dn_en_latchwen < d_up_d_int + d_up_d_inta + d_up_d_h Removing redundant inequality tsetupd < d_up_d_int + d_up_d_h + d_up_d_inta Step 15 Randomly choosing an inequality among 6 possible pi_0-incompatible inequalities Adding inequality tsetupd + d_dn_net13a < d_up_d_int + d_up_d_inta + d_up_d_h Randomly choosing an inequality among 3 possible pi_0-incompatible inequalities Adding inequality d_dn_net13a < d_dn_en_latchd Adding inequality d_dn_net13a < tHI Step 16 Randomly choosing an inequality among 6 possible pi_0-incompatible inequalities Adding inequality d_up_d_int + d_up_d_h + d_up_d_inta < tsetupd + d_dn_net13a + d_dn_wela Randomly choosing an inequality among 3 possible pi_0-incompatible inequalities Adding inequality d_up_d_int + d_up_d_h + d_up_d_inta < tsetupd + tHI Adding inequality d_up_d_int + d_up_d_h + d_up_d_inta < tsetupd + d_dn_en_latchd Step 17 Randomly choosing an inequality among 3 possible pi_0-incompatible inequalities Adding inequality d_dn_net13a + d_dn_wela < tHI Removing redundant inequality d_dn_net13a < tHI Adding inequality d_dn_en_latchd < d_dn_net13a + d_dn_wela Step 18 Step 19 Adding inequality tHI < d_up_net27 + d_dn_wela + d_up_q_0 + d_dn_net13a Step 20 Adding inequality tHI + d_up_en_latchwen < d_dn_wela + d_up_net27 + d_dn_net13a + d_up_q_0 Removing redundant inequality tHI < d_up_net27 + d_dn_wela + d_up_q_0 + d_dn_net13a Step 21 Randomly choosing an inequality among 3 possible pi_0-incompatible inequalities Adding inequality d_dn_wela + d_up_net27 + d_up_q_0 + d_dn_net13a < tHI + d_up_net13a Adding inequality d_up_net27 + d_dn_wela + d_up_q_0 + d_dn_net13a < d_dn_net45 + d_dn_net45a + d_up_en_latchwen + tHI Step 22 Adding inequality d_up_net13a < d_dn_net45 + d_dn_net45a + d_up_en_latchwen Step 23 Adding inequality d_up_net13a + d_up_wela < d_dn_net45 + d_dn_net45a + d_up_en_latchwen Removing redundant inequality d_up_net13a < d_dn_net45 + d_dn_net45a + d_up_en_latchwen Step 24 Adding inequality d_up_en_latchd < d_dn_net45 + d_dn_net45a + d_up_en_latchwen Step 25 Adding inequality d_dn_net45 + d_up_en_latchwen + d_dn_net45a < d_up_d_int + d_up_d_inta + d_up_en_latchd Step 26 Adding inequality d_up_d_int + d_up_en_latchd + d_up_d_inta < tLO Step 27 Step 28 Step 29 Step 30 Step 31 Step 32 Post* was reached at step 31 with 31 states (from 31 different locations) Intersection of the inequalities of all states in post* (after preprocessing): & 0 <= d_up_wela & 0 <= d_up_en_latchwen & d_up_en_latchd < d_dn_net45 + d_dn_net45a + d_up_en_latchwen & tLO + d_dn_wen_h < tsetupwen + d_up_en_latchd & d_dn_en_latchd < d_dn_net13a + d_dn_wela & tLO <= tsetupd & d_dn_net45 + d_dn_net45a + d_up_en_latchwen < d_up_d_int + d_up_en_latchd + d_up_d_inta & tLO < tsetupwen + d_up_net13a & d_up_d_int + d_up_d_inta + d_up_en_latchd < tLO & d_dn_net13a + d_dn_wela < tHI & d_up_net13a + d_up_wela + tsetupwen < tLO + d_dn_wen_h & tLO + d_up_d_h < d_dn_d_int + d_up_en_latchd + d_dn_d_inta + tsetupd & d_up_d_int + d_up_d_h + d_up_d_inta < tsetupd + d_dn_en_latchd & d_up_net27 + d_dn_net13a + d_up_q_0 + d_dn_wela < tHI + d_up_net13a & tsetupwen + d_up_en_latchwen < tLO & d_up_d_h < tsetupd & tsetupd < tLO + tHI & tsetupd + d_dn_net13a < d_up_d_int + d_up_d_inta + d_up_d_h & tHI + d_up_en_latchwen < d_dn_wela + d_up_net27 + d_dn_net13a + d_up_q_0 & tsetupd + d_dn_net45a + d_dn_net45 + d_dn_wen_h + d_up_wela < tsetupwen + d_up_d_h & 0 <= d_dn_en_latchwen & tLO + d_dn_wen_h < d_up_net45 + d_up_net45a + tsetupwen + d_up_en_latchwen & d_dn_en_latchwen < d_dn_net13a IMITATOR ended with success :-) IMITATOR ended after 4005.38 seconds Python execution time : 4.52s HyTech execution time : 3998.22s (78 calls)