************************************************************ * 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:44  Model: ./experiments-FORTE/FMS-1/FMS-1_Spec5.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.004 second. Memory for abstract model: 906.789 KiB (i.e., 232138 words)  Starting running algorithm AGsafe...  Computing post^1 from 1 state. Computing post^2 from 2 states. Computing post^3 from 3 states. 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.  1 state merged within 21 states. Computing post^13 from 20 states.  1 state merged within 22 states. Computing post^14 from 21 states.  1 state merged within 21 states. Computing post^15 from 20 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. 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: 292 states with 800 transitions explored.  [AGsafe] Algorithm completed after 0.284 second.  Final constraint such that the system is correct:  p_B3_out_M >= 0 & p_I_B1_C1 >= 0 This good constraint is exact (sound and complete) 12.860 MiB (i.e., 1685703 words of size 8)  Result written to file './experiments-FORTE/FMS-1/FMS-1_Spec5-EF.res'.  ------------------------------------------------------------ Statistics: State space ------------------------------------------------------------ Number of states : 292 Number of transitions : 800 Number of computed states : 801 Total computation time : 0.280 second States/second in state space : 1041.9 (292/0.280 second) Computed states/second : 2858.1 (801/0.280 second) Estimated memory : 12.944 MiB (i.e., 1696650 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_Spec5-EF_cart.png'.  ------------------------------------------------------------ Statistics: Algorithm counters ------------------------------------------------------------ main algorithm : 0.282 second ------------------------------------------------------------ Statistics: Parsing counters ------------------------------------------------------------ model parsing : 0.002 second ------------------------------------------------------------ Statistics: State computation counters ------------------------------------------------------------ number of state comparisons : 1859 number of constraints comparisons : 649 ------------------------------------------------------------ Statistics: Graphics-related counters ------------------------------------------------------------ state space drawing : 0.000 second cartography drawing : 0.025 second ------------------------------------------------------------ Statistics: Global counter ------------------------------------------------------------ total : 0.309 second IMITATOR successfully terminated (after 0.311 second) Estimated memory used: 13.025 MiB (i.e., 1707218 words of size 8)