************************************************************ * 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 15:21:34  Model: ./examples/Fischer/FERA3.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. This model is an L/U-PTA: - lower-bound parameters {Delta} - upper-bound parameters {delta}  Abstract model built after 0.006 second. Memory for abstract model: 877.292 KiB (i.e., 224587 words)  Starting running algorithm AGsafe...  Computing post^1 from 1 state. Computing post^2 from 3 states.  3 states merged within 9 states. Computing post^3 from 6 states. Computing post^4 from 12 states. Computing post^5 from 24 states. Computing post^6 from 54 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.  18 states merged within 90 states. Computing post^7 from 72 states.  8 states merged within 89 states. Computing post^8 from 81 states.  18 states merged within 108 states. Computing post^9 from 90 states.  4 states merged within 116 states. Computing post^10 from 112 states.  21 states merged within 164 states. Computing post^11 from 143 states.  24 states merged within 149 states. Computing post^12 from 125 states.  12 states merged within 93 states. Computing post^13 from 81 states. Computing post^14 from 67 states.  6 states merged within 64 states. Computing post^15 from 58 states. Computing post^16 from 46 states.  10 states merged within 40 states. Computing post^17 from 30 states. Computing post^18 from 10 states.  Fixpoint reached at a depth of 19: 1323 states with 2167 transitions explored.  [AGsafe] Algorithm completed after 2.761 seconds.  Final constraint such that the system is correct:  Delta >= 0 & delta = 0 OR 6 >= delta & delta > 0 & Delta >= 3 & Delta >= delta This good constraint is exact (sound and complete) 72.062 MiB (i.e., 9445321 words of size 8)  Result written to file './examples/Fischer/FERA3-EF.res'.  ------------------------------------------------------------ Statistics: State space ------------------------------------------------------------ Number of states : 1323 Number of transitions : 2167 Number of computed states : 2168 Total computation time : 2.755 seconds States/second in state space : 480.2 (1323/2.755 seconds) Computed states/second : 786.9 (2168/2.755 seconds) Estimated memory : 72.147 MiB (i.e., 9456550 words of size 8)  Drawing the cartography… Plot cartography in 2D projected on parameters delta and Delta to file './examples/Fischer/FERA3-EF_cart.png'.  ------------------------------------------------------------ Statistics: Algorithm counters ------------------------------------------------------------ main algorithm : 2.758 seconds ------------------------------------------------------------ Statistics: Parsing counters ------------------------------------------------------------ model parsing : 0.002 second ------------------------------------------------------------ Statistics: State computation counters ------------------------------------------------------------ number of state comparisons : 55598 number of constraints comparisons : 22734 ------------------------------------------------------------ Statistics: Graphics-related counters ------------------------------------------------------------ state space drawing : 0.000 second cartography drawing : 0.044 second ------------------------------------------------------------ Statistics: Global counter ------------------------------------------------------------ total : 2.811 seconds IMITATOR successfully terminated (after 2.814 seconds) Estimated memory used: 72.250 MiB (i.e., 9470024 words of size 8)