************************************************************ * 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:47:12  Model: ./examples/AIP/AIP_Spec9.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: 1493.128 KiB (i.e., 382241 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.  [AGsafe] Found a new state violating the property.  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 108 states. Computing post^10 from 75 states.  86 states merged within 145 states. Computing post^11 from 99 states.  88 states merged within 165 states. Computing post^12 from 130 states.  136 states merged within 238 states. Computing post^13 from 168 states.  165 states merged within 296 states. Computing post^14 from 213 states.  207 states merged within 372 states. Computing post^15 from 269 states.  252 states merged within 461 states. Computing post^16 from 335 states.  317 states merged within 561 states. Computing post^17 from 403 states.  369 states merged within 668 states. Computing post^18 from 487 states.  442 states merged within 802 states. Computing post^19 from 585 states.  501 states merged within 919 states. Computing post^20 from 689 states.  595 states merged within 1057 states. Computing post^21 from 781 states.  630 states merged within 1143 states. Computing post^22 from 866 states.  736 states merged within 1306 states. Computing post^23 from 954 states.  776 states merged within 1379 states. Computing post^24 from 1036 states.  854 states merged within 1523 states. Computing post^25 from 1133 states.  956 states merged within 1687 states. Computing post^26 from 1244 states.  1057 states merged within 1865 states. Computing post^27 from 1381 states.  1176 states merged within 2084 states. Computing post^28 from 1556 states.  1349 states merged within 2379 states. Computing post^29 from 1772 states.  1548 states merged within 2728 states. Computing post^30 from 2027 states.  1684 states merged within 3037 states. Computing post^31 from 2317 states.  1949 states merged within 3498 states. Computing post^32 from 2649 states.  2233 states merged within 4047 states. Computing post^33 from 3050 states.  2491 states merged within 4562 states. Computing post^34 from 3493 states.  2856 states merged within 5225 states. Computing post^35 from 3990 states.  3272 states merged within 5971 states. Computing post^36 from 4543 states.  3726 states merged within 6763 states. *** Warning: The time limit has been reached. The exploration now stops, although there were still 5131 states to explore at this iteration.  State space exploration stopped at a depth of 37: 30409 states with 132852 transitions explored.  [AGsafe] Algorithm completed after 738.807 seconds.  Final constraint such that the system is correct:  2 >= p_is1 & p_is1 >= 0 & p_is2 >= 0 This good constraint is an over-approximation of the actual result (or the actual result itself) 216.070 GiB (i.e., 29000524623 words of size 8)  Result written to file './examples/AIP/AIP_Spec9-EF.res'.  ------------------------------------------------------------ Statistics: State space ------------------------------------------------------------ Number of states : 30409 Number of transitions : 132852 Number of computed states : 208769 Total computation time : 738.795 seconds States/second in state space : 41.1 (30409/738.795 seconds) Computed states/second : 282.5 (208769/738.795 seconds) Estimated memory : 216.070 GiB (i.e., 29000535665 words of size 8)  Drawing the cartography… Plot cartography in 2D projected on parameters p_is1 and p_is2 to file './examples/AIP/AIP_Spec9-EF_cart.png'.  ------------------------------------------------------------ Statistics: Algorithm counters ------------------------------------------------------------ main algorithm : 738.804 seconds ------------------------------------------------------------ Statistics: Parsing counters ------------------------------------------------------------ model parsing : 0.008 second ------------------------------------------------------------ Statistics: State computation counters ------------------------------------------------------------ number of state comparisons : 2065604 number of constraints comparisons : 299679 ------------------------------------------------------------ Statistics: Graphics-related counters ------------------------------------------------------------ state space drawing : 0.000 second cartography drawing : 0.045 second ------------------------------------------------------------ Statistics: Global counter ------------------------------------------------------------ total : 738.863 seconds IMITATOR successfully terminated (after 738.867 seconds) Estimated memory used: 216.070 GiB (i.e., 29000546133 words of size 8)