************************************************************ * 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:37  Model: ./examples/Fischer/FERA3.imi Mode: parametric reachability preservation cartography. Considering fixpoint variant with inclusion of symbolic zones (instead of equality). Merging technique of [AFS13] enabled. *** 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.003 second. Memory for abstract model: 871.644 KiB (i.e., 223141 words)   [BC (full coverage)] Starting running cartography…   **************************************************  START THE BEHAVIORAL CARTOGRAPHY ALGORITHM **************************************************  Parametric rectangle V0:   delta = 1..10 & Delta = 1..10  Number of points inside V0: 100  ************************************************** ALGORITHM BC (full coverage): iteration 1 Considering the following pi1  delta = 1 & Delta = 1  K1 computed by PRP in 3.921 seconds: 1379 states with 2325 transitions explored.  3 > Delta & delta > 0 & Delta >= 0  ************************************************** ALGORITHM BC (full coverage): iteration 2 Considering the following pi2  delta = 1 & Delta = 3  K2 computed by PRP in 2.656 seconds: 1006 states with 1620 transitions explored.  Delta >= delta & 6 >= delta & delta >= 0 & Delta >= 3  ************************************************** ALGORITHM BC (full coverage): iteration 3 Considering the following pi3  delta = 4 & Delta = 3  K3 computed by PRP in 3.587 seconds: 1330 states with 2228 transitions explored.  delta > Delta & Delta >= 0  ************************************************** ALGORITHM BC (full coverage): iteration 4 Considering the following pi4  delta = 7 & Delta = 7  K4 computed by PRP in 3.862 seconds: 1384 states with 2258 transitions explored.  delta > 6 & Delta >= 0  [BC (full coverage)] Successfully terminated after 14.033 seconds.  Final constraints such that the system is correct/incorrect:  Delta >= delta & 6 >= delta & delta >= 0 & Delta >= 3 3 > Delta & delta > 0 & Delta >= 0 OR delta > Delta & Delta >= 0 OR delta > 6 & Delta >= 0 The good constraint is exact (sound and complete). The bad constraint is exact (sound and complete). 369.950 MiB (i.e., 48490149 words of size 8)  Result written to file './examples/Fischer/FERA3-PRPC.res'.  Drawing the cartography… Plot cartography in 2D projected on parameters delta and Delta to file './examples/Fischer/FERA3-PRPC_cart.png'.  ------------------------------------------------------------ Statistics: Algorithm counters ------------------------------------------------------------ main algorithm : 14.032 seconds find next point : 0.000 second (0 call) ------------------------------------------------------------ Statistics: Parsing counters ------------------------------------------------------------ model parsing : 0.002 second ------------------------------------------------------------ Statistics: State computation counters ------------------------------------------------------------ number of state comparisons : 226269 number of constraints comparisons : 103135 ------------------------------------------------------------ Statistics: Graphics-related counters ------------------------------------------------------------ state space drawing : 0.000 second cartography drawing : 0.045 second ------------------------------------------------------------ Statistics: Global counter ------------------------------------------------------------ total : 14.079 seconds IMITATOR successfully terminated (after 14.081 seconds) Estimated memory used: 370.160 MiB (i.e., 48517731 words of size 8)