************************************************************ * 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:00:29  Model: ./examples/AIP/AIP_Spec7.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.013 second. Memory for abstract model: 1483.582 KiB (i.e., 379797 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 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 295 states. Computing post^14 from 212 states.  204 states merged within 366 states. Computing post^15 from 265 states.  244 states merged within 449 states. Computing post^16 from 328 states.  304 states merged within 541 states. Computing post^17 from 392 states.  335 states merged within 620 states. Computing post^18 from 467 states.  427 states merged within 767 states. Computing post^19 from 554 states.  495 states merged within 886 states. Computing post^20 from 645 states.  574 states merged within 997 states. Computing post^21 from 719 states.  589 states merged within 1052 states. Computing post^22 from 786 states.  648 states merged within 1157 states. Computing post^23 from 856 states.  740 states merged within 1276 states. Computing post^24 from 923 states.  736 states merged within 1329 states. Computing post^25 from 1008 states.  867 states merged within 1519 states. Computing post^26 from 1114 states.  907 states merged within 1640 states. Computing post^27 from 1253 states.  1116 states merged within 1951 states. Computing post^28 from 1430 states.  1273 states merged within 2229 states. Computing post^29 from 1645 states.  1464 states merged within 2575 states. Computing post^30 from 1900 states.  1623 states merged within 2907 states. Computing post^31 from 2186 states.  1922 states merged within 3389 states. Computing post^32 from 2502 states.  2056 states merged within 3765 states. Computing post^33 from 2871 states.  2374 states merged within 4321 states. Computing post^34 from 3273 states.  2633 states merged within 4850 states. Computing post^35 from 3724 states.  3083 states merged within 5582 states. Computing post^36 from 4209 states.  3312 states merged within 6096 states. Computing post^37 from 4708 states.  3755 states merged within 6773 states. *** Warning: The time limit has been reached. The exploration now stops, although there were still 5162 states to explore at this iteration.  State space exploration stopped at a depth of 38: 25872 states with 134985 transitions explored.  [AGsafe] Algorithm completed after 768.085 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) 224.852 GiB (i.e., 30179245856 words of size 8)  Result written to file './examples/AIP/AIP_Spec7-EF.res'.  ------------------------------------------------------------ Statistics: State space ------------------------------------------------------------ Number of states : 25872 Number of transitions : 134985 Number of computed states : 215072 Total computation time : 768.071 seconds States/second in state space : 33.6 (25872/768.071 seconds) Computed states/second : 280.0 (215072/768.071 seconds) Estimated memory : 224.852 GiB (i.e., 30179256817 words of size 8)  Drawing the cartography… Plot cartography in 2D projected on parameters p_is1 and p_is2 to file './examples/AIP/AIP_Spec7-EF_cart.png'.  ------------------------------------------------------------ Statistics: Algorithm counters ------------------------------------------------------------ main algorithm : 768.081 seconds ------------------------------------------------------------ Statistics: Parsing counters ------------------------------------------------------------ model parsing : 0.009 second ------------------------------------------------------------ Statistics: State computation counters ------------------------------------------------------------ number of state comparisons : 2299037 number of constraints comparisons : 310255 ------------------------------------------------------------ Statistics: Graphics-related counters ------------------------------------------------------------ state space drawing : 0.000 second cartography drawing : 0.510 second ------------------------------------------------------------ Statistics: Global counter ------------------------------------------------------------ total : 768.603 seconds IMITATOR successfully terminated (after 768.607 seconds) Estimated memory used: 224.853 GiB (i.e., 30179267210 words of size 8)