************************************************************ * 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 11:41:08  Model: ./examples/FMS-2/FMS-2_Spec5.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.009 second. Memory for abstract model: 1239.644 KiB (i.e., 317349 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.  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.  1005 states merged within 4200 states. Computing post^15 from 3228 states.  1327 states merged within 5356 states. Computing post^16 from 4085 states.  1678 states merged within 6664 states. Computing post^17 from 5079 states.  2015 states merged within 8133 states. Computing post^18 from 6263 states.  2454 states merged within 9906 states. Computing post^19 from 7664 states.  3037 states merged within 11991 states. *** Warning: The time limit has been reached. The exploration now stops, although there were still 9257 states to explore at this iteration.  State space exploration stopped at a depth of 20: 43346 states with 174116 transitions explored.  [AGsafe] Algorithm completed after 633.191 seconds.  Final constraint such that the system is correct:  p_B3_out_M >= 0 & p_I_B1_C1 >= 0 This good constraint is an over-approximation of the actual result (or the actual result itself) 171.251 GiB (i.e., 22984997998 words of size 8)  Result written to file './examples/FMS-2/FMS-2_Spec5-EF.res'.  ------------------------------------------------------------ Statistics: State space ------------------------------------------------------------ Number of states : 43346 Number of transitions : 174116 Number of computed states : 176886 Total computation time : 633.181 seconds States/second in state space : 68.4 (43346/633.181 seconds) Computed states/second : 279.3 (176886/633.181 seconds) Estimated memory : 171.251 GiB (i.e., 22985009034 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_Spec5-EF_cart.png'.  ------------------------------------------------------------ Statistics: Algorithm counters ------------------------------------------------------------ main algorithm : 633.188 seconds ------------------------------------------------------------ Statistics: Parsing counters ------------------------------------------------------------ model parsing : 0.006 second ------------------------------------------------------------ Statistics: State computation counters ------------------------------------------------------------ number of state comparisons : 3446477 number of constraints comparisons : 304405 ------------------------------------------------------------ Statistics: Graphics-related counters ------------------------------------------------------------ state space drawing : 0.000 second cartography drawing : 0.055 second ------------------------------------------------------------ Statistics: Global counter ------------------------------------------------------------ total : 633.262 seconds IMITATOR successfully terminated (after 633.266 seconds) Estimated memory used: 171.251 GiB (i.e., 22985019542 words of size 8)