************************************************************ * 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: Fri Feb 24, 2017 09:20:42  Model: ./experiments-FORTE/FMS-1/FMS-1_Spec1.imi Mode: EF-synthesis. *** Warning: The second file ./experiments-FORTE/FMS-1/FMS-1_Spec_1_3.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_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_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_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_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_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_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_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_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_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.008 second. Memory for abstract model: 931.953 KiB (i.e., 238580 words)  Starting running algorithm AGsafe...  Computing post^1 from 1 state. Computing post^2 from 2 states. Computing post^3 from 3 states.  [AGsafe] Found a new state violating the property. Computing post^4 from 4 states. Computing post^5 from 5 states. Computing post^6 from 8 states. Computing post^7 from 11 states.  1 state merged within 14 states. Computing post^8 from 13 states.  1 state merged within 14 states. Computing post^9 from 13 states. Computing post^10 from 13 states. Computing post^11 from 16 states.  1 state merged within 20 states. Computing post^12 from 19 states.  2 states merged within 22 states. Computing post^13 from 20 states. Computing post^14 from 21 states. Computing post^15 from 20 states.  3 states merged within 21 states. Computing post^16 from 18 states. Computing post^17 from 16 states. Computing post^18 from 15 states. Computing post^19 from 16 states.  1 state merged within 16 states. Computing post^20 from 15 states.  3 states merged within 14 states. Computing post^21 from 11 states. Computing post^22 from 7 states. Computing post^23 from 6 states. Computing post^24 from 6 states. Computing post^25 from 5 states. Computing post^26 from 4 states. Computing post^27 from 3 states. Computing post^28 from 1 state.  Fixpoint reached at a depth of 29: 332 states with 840 transitions explored.  [AGsafe] Algorithm completed after 0.302 second.  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 exact (sound and complete) 13.947 MiB (i.e., 1828063 words of size 8)  Result written to file './experiments-FORTE/FMS-1/FMS-1_Spec1-EF.res'.  ------------------------------------------------------------ Statistics: State space ------------------------------------------------------------ Number of states : 332 Number of transitions : 840 Number of computed states : 841 Total computation time : 0.294 second States/second in state space : 1126.5 (332/0.294 second) Computed states/second : 2853.7 (841/0.294 second) Estimated memory : 14.031 MiB (i.e., 1839113 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 './experiments-FORTE/FMS-1/FMS-1_Spec1-EF_cart.png'.  ------------------------------------------------------------ Statistics: Algorithm counters ------------------------------------------------------------ main algorithm : 0.299 second ------------------------------------------------------------ Statistics: Parsing counters ------------------------------------------------------------ model parsing : 0.004 second ------------------------------------------------------------ Statistics: State computation counters ------------------------------------------------------------ number of state comparisons : 2158 number of constraints comparisons : 671 ------------------------------------------------------------ Statistics: Graphics-related counters ------------------------------------------------------------ state space drawing : 0.000 second cartography drawing : 0.045 second ------------------------------------------------------------ Statistics: Global counter ------------------------------------------------------------ total : 0.346 second IMITATOR successfully terminated (after 0.349 second) Estimated memory used: 14.112 MiB (i.e., 1849769 words of size 8)