************************************************************ * IMITATOR 2.9-alpha "Butter Incaberry" * * * * Etienne Andre, Ulrich Kuehne et al. * * 2009 - 2017 * * LSV, ENS de Cachan & CNRS, France * * LIPN, Universite Paris 13, Sorbonne Paris Cite, France * * www.imitator.fr * * * * Build: 2212 (2017-02-22 08:48:09 UTC) * * master/35846ec * ************************************************************ Analysis time: Wed Feb 22, 2017 14:26:11  Model: ./examples/AIP/AIP_Spec8.imi Mode: EF-synthesis. *** Warning: The second file ./examples/AIP/AIP.v0 will be ignored since this is a synthesis with respect to a property. *** Warning: A maximum computation for the cartography has been set, but IMITATOR does not run in cartography mode. Ignored. Considering fixpoint variant with inclusion of symbolic zones (instead of equality). Merging technique of [AFS13] enabled. The cartography will be drawn. The result will be written to a file. *** Warning: IMITATOR will try to stop after 600 seconds. *** Warning: IMITATOR will try to stop the cartography after 600 seconds. *** Warning: The clock 'clock_task2A' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_task2B' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_task1B' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_task1A' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_CL_TU3_1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_CL_TU3_2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_L3_out_TU3_2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_L3_out_TU3_1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_CL_TU2_1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_I_L2_TU2_1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_L2_AS2_1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_I_L2_AS2_1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_L2_TU2_1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_I_CL_TU2_1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_I_CL_TU3_2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_CL_TU2_2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_I_L2_TU2_2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_L2_AS2_2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_I_L2_AS2_2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_L2_TU2_2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_I_CL_TU3_1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_CL_TU1_1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_I_L1_TU1_1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_L1_AS1_1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_I_L1_AS1_1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_L1_TU1_1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_I_CL_TU1_1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_I_CL_TU2_2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_CL_TU1_2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_I_L1_TU1_2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_L1_AS1_2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_I_L1_AS1_2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_L1_TU1_2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_I_CL_TU1_2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_I_L3_TU3_1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_L3_I1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_product1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_I_L3_TU3_2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_L3_I2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_product2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_L3_TU3_2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_L3_TU3_1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. This model is a U-PTA.  Abstract model built after 0.012 second. Memory for abstract model: 1485.855 KiB (i.e., 380379 words)  Starting running algorithm AGsafe...  Computing post^1 from 1 state.  1 state merged within 3 states. Computing post^2 from 3 states.  4 states merged within 7 states. Computing post^3 from 5 states.  6 states merged within 11 states. Computing post^4 from 8 states.  11 states merged within 17 states. Computing post^5 from 12 states.  15 states merged within 27 states. Computing post^6 from 19 states.  28 states merged within 44 states. Computing post^7 from 28 states.  27 states merged within 51 states. Computing post^8 from 40 states.  43 states merged within 76 states. Computing post^9 from 55 states.  62 states merged within 107 states. Computing post^10 from 74 states.  85 states merged within 141 states. Computing post^11 from 95 states.  101 states merged within 174 states. Computing post^12 from 122 states.  110 states merged within 204 states. Computing post^13 from 155 states.  153 states merged within 273 states. Computing post^14 from 195 states.  164 states merged within 316 states. Computing post^15 from 244 states.  238 states merged within 420 states. Computing post^16 from 297 states.  261 states merged within 476 states. Computing post^17 from 353 states.  310 states merged within 570 states. Computing post^18 from 421 states.  380 states merged within 689 states. Computing post^19 from 502 states.  441 states merged within 801 states. Computing post^20 from 589 states.  512 states merged within 901 states. Computing post^21 from 661 states.  561 states merged within 989 states. Computing post^22 from 727 states.  615 states merged within 1090 states. Computing post^23 from 800 states.  638 states merged within 1146 states. Computing post^24 from 873 states.  782 states merged within 1341 states. Computing post^25 from 956 states.  768 states merged within 1392 states. Computing post^26 from 1060 states.  926 states merged within 1627 states. Computing post^27 from 1191 states.  1039 states merged within 1826 states. Computing post^28 from 1350 states.  1223 states merged within 2119 states. Computing post^29 from 1540 states.  1318 states merged within 2348 states. Computing post^30 from 1765 states.  1497 states merged within 2677 states. Computing post^31 from 2020 states.  1732 states merged within 3089 states. Computing post^32 from 2307 states.  1887 states merged within 3459 states. Computing post^33 from 2641 states.  2177 states merged within 3964 states. Computing post^34 from 3007 states.  2470 states merged within 4504 states. Computing post^35 from 3412 states.  2773 states merged within 5072 states. Computing post^36 from 3860 states.  3134 states merged within 5697 states. Computing post^37 from 4327 states.  3455 states merged within 6244 states. *** Warning: The time limit has been reached. The exploration now stops, although there were still 4765 states to explore at this iteration.  State space exploration stopped at a depth of 38: 23946 states with 123074 transitions explored.  [AGsafe] Algorithm completed after 622.209 seconds.  Final constraint such that the system is correct:  p_is2 >= 0 & p_is1 >= 0 This good constraint is an over-approximation of the actual result (or the actual result itself) 189.935 GiB (i.e., 25492764175 words of size 8)  Result written to file './examples/AIP/AIP_Spec8-EF.res'.  ------------------------------------------------------------ Statistics: State space ------------------------------------------------------------ Number of states : 23946 Number of transitions : 123074 Number of computed states : 196506 Total computation time : 622.197 seconds States/second in state space : 38.4 (23946/622.197 seconds) Computed states/second : 315.8 (196506/622.197 seconds) Estimated memory : 189.935 GiB (i.e., 25492775116 words of size 8)  Drawing the cartography… Plot cartography in 2D projected on parameters p_is1 and p_is2 to file './examples/AIP/AIP_Spec8-EF_cart.png'.  ------------------------------------------------------------ Statistics: Algorithm counters ------------------------------------------------------------ main algorithm : 622.206 seconds ------------------------------------------------------------ Statistics: Parsing counters ------------------------------------------------------------ model parsing : 0.008 second ------------------------------------------------------------ Statistics: State computation counters ------------------------------------------------------------ number of state comparisons : 1932208 number of constraints comparisons : 279337 ------------------------------------------------------------ Statistics: Graphics-related counters ------------------------------------------------------------ state space drawing : 0.000 second cartography drawing : 0.041 second ------------------------------------------------------------ Statistics: Global counter ------------------------------------------------------------ total : 622.259 seconds IMITATOR successfully terminated (after 622.262 seconds) Estimated memory used: 189.936 GiB (i.e., 25492785497 words of size 8)