************************************************************ * 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 10:31:09  Model: ./examples/FMS-2/FMS-2_Spec1.imi Mode: EF-synthesis. *** Warning: The second file ./examples/FMS-2/FMS-2_Spec_1_5.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_I_B4_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_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_B3_out_M} - upper-bound parameters {p_I_B1_C1}  Abstract model built after 0.012 second. Memory for abstract model: 1252.382 KiB (i.e., 320610 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.  [AGsafe] Found a new state violating the property.  5 states merged within 39 states. Computing post^4 from 34 states.  7 states merged within 72 states. Computing post^5 from 65 states.  27 states merged within 142 states. Computing post^6 from 115 states.  48 states merged within 242 states. Computing post^7 from 194 states.  81 states merged within 395 states. Computing post^8 from 314 states.  138 states merged within 621 states. Computing post^9 from 483 states.  207 states merged within 913 states. Computing post^10 from 706 states.  281 states merged within 1275 states. Computing post^11 from 995 states.  432 states merged within 1799 states. Computing post^12 from 1371 states.  564 states merged within 2417 states. Computing post^13 from 1863 states.  766 states merged within 3232 states. Computing post^14 from 2485 states.  1010 states merged within 4205 states. Computing post^15 from 3228 states.  1324 states merged within 5353 states. Computing post^16 from 4085 states.  1684 states merged within 6670 states. Computing post^17 from 5079 states.  2074 states merged within 8190 states. Computing post^18 from 6261 states.  2403 states merged within 9853 states. Computing post^19 from 7659 states.  3092 states merged within 12052 states. *** Warning: The time limit has been reached. The exploration now stops, although there were still 9249 states to explore at this iteration.  State space exploration stopped at a depth of 20: 49015 states with 179762 transitions explored.  [AGsafe] Algorithm completed after 692.840 seconds.  Final constraint such that the system is correct:  2 >= p_I_B1_C1 & p_I_B1_C1 >= 0 & p_B3_out_M >= 0 This good constraint is an over-approximation of the actual result (or the actual result itself) 176.937 GiB (i.e., 23748168349 words of size 8)  Result written to file './examples/FMS-2/FMS-2_Spec1-EF.res'.  ------------------------------------------------------------ Statistics: State space ------------------------------------------------------------ Number of states : 49015 Number of transitions : 179762 Number of computed states : 182520 Total computation time : 692.828 seconds States/second in state space : 70.7 (49015/692.828 seconds) Computed states/second : 263.4 (182520/692.828 seconds) Estimated memory : 176.937 GiB (i.e., 23748179486 words of size 8)  Drawing the cartography… Plot cartography in 2D projected on parameters p_I_B1_C1 and p_B3_out_M to file './examples/FMS-2/FMS-2_Spec1-EF_cart.png'.  ------------------------------------------------------------ Statistics: Algorithm counters ------------------------------------------------------------ main algorithm : 692.838 seconds ------------------------------------------------------------ Statistics: Parsing counters ------------------------------------------------------------ model parsing : 0.009 second ------------------------------------------------------------ Statistics: State computation counters ------------------------------------------------------------ number of state comparisons : 3120856 number of constraints comparisons : 312802 ------------------------------------------------------------ Statistics: Graphics-related counters ------------------------------------------------------------ state space drawing : 0.000 second cartography drawing : 0.126 second ------------------------------------------------------------ Statistics: Global counter ------------------------------------------------------------ total : 692.990 seconds IMITATOR successfully terminated (after 692.993 seconds) Estimated memory used: 176.937 GiB (i.e., 23748190073 words of size 8)