************************************************************ * 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 16:42:48  Model: ./examples/Fischer/FERA4.imi Mode: EF-synthesis. *** Warning: The second file ./examples/Fischer/FERA.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_Enter1' 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_SetX01' 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_Enter2' 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_SetX02' 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_Enter3' 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_SetX03' 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_Enter4' 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_SetX04' 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 {Delta} - upper-bound parameters {delta}  Abstract model built after 1.434 seconds. Memory for abstract model: 1005.175 KiB (i.e., 257325 words)  Starting running algorithm AGsafe...  Computing post^1 from 1 state. Computing post^2 from 4 states.  6 states merged within 16 states. Computing post^3 from 10 states. Computing post^4 from 28 states.  6 states merged within 76 states. Computing post^5 from 70 states. Computing post^6 from 182 states.  [AGsafe] Found a new state violating the property.  [AGsafe] Found a new state violating the property.  [AGsafe] Found a new state violating the property.  [AGsafe] Found a new state violating the property.  60 states merged within 405 states. Computing post^7 from 345 states.  122 states merged within 638 states. Computing post^8 from 516 states.  108 states merged within 936 states. Computing post^9 from 828 states.  68 states merged within 1356 states. Computing post^10 from 1288 states.  165 states merged within 2142 states. Computing post^11 from 1977 states.  324 states merged within 3049 states. Computing post^12 from 2725 states.  630 states merged within 3947 states. Computing post^13 from 3317 states.  379 states merged within 3930 states. Computing post^14 from 3551 states.  370 states merged within 4449 states. Computing post^15 from 4079 states.  630 states merged within 5527 states. Computing post^16 from 4897 states.  952 states merged within 5575 states. *** Warning: The time limit has been reached. The exploration now stops, although there were still 4623 states to explore at this iteration.  State space exploration stopped at a depth of 17: 39750 states with 63276 transitions explored.  [AGsafe] Algorithm completed after 769.827 seconds.  Final constraint such that the system is correct:  Delta >= 0 & delta = 0 OR Delta >= delta & delta > 0 & Delta >= 4 & 7 >= delta This good constraint is an over-approximation of the actual result (or the actual result itself) 22.835 GiB (i.e., 3064951590 words of size 8)  Result written to file './examples/Fischer/FERA4-EF.res'.  ------------------------------------------------------------ Statistics: State space ------------------------------------------------------------ Number of states : 39750 Number of transitions : 63276 Number of computed states : 63277 Total computation time : 768.341 seconds States/second in state space : 51.7 (39750/768.341 seconds) Computed states/second : 82.3 (63277/768.341 seconds) Estimated memory : 22.835 GiB (i.e., 3064962968 words of size 8)  Drawing the cartography… Plot cartography in 2D projected on parameters delta and Delta to file './examples/Fischer/FERA4-EF_cart.png'.  ------------------------------------------------------------ Statistics: Algorithm counters ------------------------------------------------------------ main algorithm : 768.507 seconds ------------------------------------------------------------ Statistics: Parsing counters ------------------------------------------------------------ model parsing : 0.102 second ------------------------------------------------------------ Statistics: State computation counters ------------------------------------------------------------ number of state comparisons : 25840819 number of constraints comparisons : 9386208 ------------------------------------------------------------ Statistics: Graphics-related counters ------------------------------------------------------------ state space drawing : 0.000 second cartography drawing : 0.420 second ------------------------------------------------------------ Statistics: Global counter ------------------------------------------------------------ total : 769.009 seconds IMITATOR successfully terminated (after 770.330 seconds) Estimated memory used: 22.835 GiB (i.e., 3064976499 words of size 8)