************************************************************ * 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 12:02:59  Model: ./examples/FMS-2/FMS-2_Spec6.imi Mode: EF-synthesis. *** Warning: The second file ./examples/FMS-2/FMS-2_Spec6.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_O_B1_R1' 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_B2_R3' 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_B3_in_M' 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_B3_out_M' 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_B3_M' 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_B3_R2' 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_B3_M' 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_B4_in_L' 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_B4_out_L' 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_B4_L' 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_B4_R4' 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_B4_L' 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_B6_in_P' 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_B6_out_P' 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_B6_P' 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_B6_A' 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_B6_P' 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_B1_out' 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_B3_in_R1' 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_B3_out_R2' 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_B5_in_R2' 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_B5_R2' 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_B5_A' 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_B2_out' 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_B4_in_R3' 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_B4_out_R4' 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_B5_out_A' 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_B6_out_A' 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_product' 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 an L/U-PTA: - lower-bound parameters {p_I_B4_R3} - upper-bound parameters {p_I_B2_C2}  Abstract model built after 0.010 second. Memory for abstract model: 1258.566 KiB (i.e., 322193 words)  Starting running algorithm AGsafe...  Computing post^1 from 1 state. Computing post^2 from 5 states.  1 state merged within 16 states. Computing post^3 from 15 states.  4 states merged within 38 states. Computing post^4 from 34 states.  12 states merged within 77 states. Computing post^5 from 65 states.  18 states merged within 133 states. Computing post^6 from 115 states.  51 states merged within 245 states. Computing post^7 from 194 states.  80 states merged within 394 states. Computing post^8 from 314 states.  145 states merged within 630 states. Computing post^9 from 485 states.  189 states merged within 904 states. Computing post^10 from 715 states.  315 states merged within 1333 states. Computing post^11 from 1018 states.  378 states merged within 1794 states. Computing post^12 from 1416 states.  596 states merged within 2541 states. Computing post^13 from 1945 states.  723 states merged within 3354 states. Computing post^14 from 2631 states.  1159 states merged within 4638 states. Computing post^15 from 3479 states.  1351 states merged within 5836 states. Computing post^16 from 4485 states.  1670 states merged within 7345 states. Computing post^17 from 5675 states.  2269 states merged within 9394 states. Computing post^18 from 7125 states.  2684 states merged within 11577 states. Computing post^19 from 8893 states.  3430 states merged within 14420 states. *** Warning: The time limit has been reached. The exploration now stops, although there were still 10990 states to explore at this iteration.  State space exploration stopped at a depth of 20: 49600 states with 194003 transitions explored.  [AGsafe] Algorithm completed after 784.081 seconds.  Final constraint such that the system is correct:  p_I_B4_R3 >= 0 & p_I_B2_C2 >= 0 This good constraint is an over-approximation of the actual result (or the actual result itself) 205.264 GiB (i.e., 27550135356 words of size 8)  Result written to file './examples/FMS-2/FMS-2_Spec6-EF.res'.  ------------------------------------------------------------ Statistics: State space ------------------------------------------------------------ Number of states : 49600 Number of transitions : 194003 Number of computed states : 194004 Total computation time : 784.070 seconds States/second in state space : 63.2 (49600/784.070 seconds) Computed states/second : 247.4 (194004/784.070 seconds) Estimated memory : 205.264 GiB (i.e., 27550146409 words of size 8)  Drawing the cartography… Plot cartography in 2D projected on parameters p_I_B2_C2 and p_I_B4_R3 to file './examples/FMS-2/FMS-2_Spec6-EF_cart.png'.  ------------------------------------------------------------ Statistics: Algorithm counters ------------------------------------------------------------ main algorithm : 784.079 seconds ------------------------------------------------------------ Statistics: Parsing counters ------------------------------------------------------------ model parsing : 0.008 second ------------------------------------------------------------ Statistics: State computation counters ------------------------------------------------------------ number of state comparisons : 2892370 number of constraints comparisons : 400486 ------------------------------------------------------------ Statistics: Graphics-related counters ------------------------------------------------------------ state space drawing : 0.000 second cartography drawing : 0.060 second ------------------------------------------------------------ Statistics: Global counter ------------------------------------------------------------ total : 784.152 seconds IMITATOR successfully terminated (after 784.154 seconds) Estimated memory used: 205.264 GiB (i.e., 27550156924 words of size 8)