************************************************************ * 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:55:39  Model: ./examples/FMS-2/FMS-2_Spec2.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.011 second. Memory for abstract model: 1252.390 KiB (i.e., 320612 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 646.486 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.229 GiB (i.e., 22982101452 words of size 8)  Result written to file './examples/FMS-2/FMS-2_Spec2-EF.res'.  ------------------------------------------------------------ Statistics: State space ------------------------------------------------------------ Number of states : 43346 Number of transitions : 174116 Number of computed states : 176886 Total computation time : 646.475 seconds States/second in state space : 67.0 (43346/646.475 seconds) Computed states/second : 273.6 (176886/646.475 seconds) Estimated memory : 171.230 GiB (i.e., 22982112492 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_Spec2-EF_cart.png'.  ------------------------------------------------------------ Statistics: Algorithm counters ------------------------------------------------------------ main algorithm : 646.483 seconds ------------------------------------------------------------ Statistics: Parsing counters ------------------------------------------------------------ model parsing : 0.007 second ------------------------------------------------------------ Statistics: State computation counters ------------------------------------------------------------ number of state comparisons : 2680357 number of constraints comparisons : 304404 ------------------------------------------------------------ Statistics: Graphics-related counters ------------------------------------------------------------ state space drawing : 0.000 second cartography drawing : 0.049 second ------------------------------------------------------------ Statistics: Global counter ------------------------------------------------------------ total : 646.548 seconds IMITATOR successfully terminated (after 646.552 seconds) Estimated memory used: 171.230 GiB (i.e., 22982123004 words of size 8)