************************************************************ * 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 13:15:49  Model: ./examples/AIP/AIP_Spec5.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.010 second. Memory for abstract model: 1502.089 KiB (i.e., 384535 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 164 states. Computing post^12 from 129 states.  135 states merged within 233 states. Computing post^13 from 163 states.  158 states merged within 282 states. Computing post^14 from 201 states.  196 states merged within 346 states. Computing post^15 from 246 states.  214 states merged within 402 states. Computing post^16 from 298 states.  275 states merged within 484 states. Computing post^17 from 345 states.  298 states merged within 545 states. Computing post^18 from 401 states.  345 states merged within 632 states. Computing post^19 from 462 states.  395 states merged within 712 states. Computing post^20 from 519 states.  416 states merged within 751 states. Computing post^21 from 560 states.  465 states merged within 818 states. Computing post^22 from 587 states.  462 states merged within 829 states. Computing post^23 from 605 states.  470 states merged within 832 states. Computing post^24 from 614 states.  497 states merged within 876 states. Computing post^25 from 634 states.  503 states merged within 900 states. Computing post^26 from 667 states.  530 states merged within 952 states. Computing post^27 from 716 states.  602 states merged within 1068 states. Computing post^28 from 791 states.  654 states merged within 1175 states. Computing post^29 from 885 states.  767 states merged within 1335 states. Computing post^30 from 979 states.  818 states merged within 1435 states. Computing post^31 from 1065 states.  857 states merged within 1526 states. Computing post^32 from 1156 states.  904 states merged within 1656 states. Computing post^33 from 1267 states.  1031 states merged within 1841 states. Computing post^34 from 1374 states.  1087 states merged within 1981 states. Computing post^35 from 1503 states.  1161 states merged within 2168 states. Computing post^36 from 1669 states.  1332 states merged within 2454 states. Computing post^37 from 1861 states.  1478 states merged within 2709 states. Computing post^38 from 2053 states.  1580 states merged within 2904 states. Computing post^39 from 2214 states.  1672 states merged within 3046 states. Computing post^40 from 2313 states.  1673 states merged within 3053 states. Computing post^41 from 2342 states.  1657 states merged within 3020 states. Computing post^42 from 2323 states.  1731 states merged within 3071 states. Computing post^43 from 2287 states.  1581 states merged within 2891 states. Computing post^44 from 2254 states.  1680 states merged within 2985 states. *** Warning: The time limit has been reached. The exploration now stops, although there were still 2248 states to explore at this iteration.  State space exploration stopped at a depth of 45: 22571 states with 128601 transitions explored.  [AGsafe] Algorithm completed after 628.203 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) 175.265 GiB (i.e., 23523716165 words of size 8)  Result written to file './examples/AIP/AIP_Spec5-EF.res'.  ------------------------------------------------------------ Statistics: State space ------------------------------------------------------------ Number of states : 22571 Number of transitions : 128601 Number of computed states : 204839 Total computation time : 628.191 seconds States/second in state space : 35.9 (22571/628.191 seconds) Computed states/second : 326.0 (204839/628.191 seconds) Estimated memory : 175.265 GiB (i.e., 23523727106 words of size 8)  Drawing the cartography… Plot cartography in 2D projected on parameters p_is1 and p_is2 to file './examples/AIP/AIP_Spec5-EF_cart.png'.  ------------------------------------------------------------ Statistics: Algorithm counters ------------------------------------------------------------ main algorithm : 628.201 seconds ------------------------------------------------------------ Statistics: Parsing counters ------------------------------------------------------------ model parsing : 0.009 second ------------------------------------------------------------ Statistics: State computation counters ------------------------------------------------------------ number of state comparisons : 1581927 number of constraints comparisons : 295114 ------------------------------------------------------------ Statistics: Graphics-related counters ------------------------------------------------------------ state space drawing : 0.000 second cartography drawing : 0.025 second ------------------------------------------------------------ Statistics: Global counter ------------------------------------------------------------ total : 628.237 seconds IMITATOR successfully terminated (after 628.239 seconds) Estimated memory used: 175.265 GiB (i.e., 23523737487 words of size 8)