************************************************************ * 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 10:42:42  Model: ./examples/FMS-2/FMS-2_Spec1.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_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_O_B2_R3' 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_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_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_B4_R3' 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_B4_in_L' 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_B4_out_L' 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_B4_L' 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_B4_R4' 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_B4_L' 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_B6_in_P' 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_B6_out_P' 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_B6_P' 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_B6_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_O_B6_P' 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_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_B2_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_B4_in_R3' 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_B4_out_R4' 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_B6_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.010 second. Memory for abstract model: 1246.703 KiB (i.e., 319156 words)   [BC (full coverage)] Starting running cartography…   **************************************************  START THE BEHAVIORAL CARTOGRAPHY ALGORITHM **************************************************  Parametric rectangle V0:   p_I_B1_C1 = 1..10 & p_B3_out_M = 1..10  Number of points inside V0: 100  ************************************************** ALGORITHM BC (full coverage): iteration 1 Considering the following pi1  p_I_B1_C1 = 1 & p_B3_out_M = 1  K1 computed by PRP in 687.998 seconds: 43348 states with 174095 transitions explored.  2 >= p_I_B1_C1 & p_I_B1_C1 >= 0 & p_B3_out_M >= 0  K1 is not valid: discarded! *** Warning: The time limit for the cartography has been reached. The exploration now stops although there may be some more points to cover.  [BC (full coverage)] Successfully terminated after 688.010 seconds.  Final constraints such that the system is correct/incorrect: False False The good constraint is exact (sound and complete). The bad constraint is exact (sound and complete). 171.344 GiB (i.e., 22997536067 words of size 8)  Result written to file './examples/FMS-2/FMS-2_Spec1-PRPC.res'.  Drawing the cartography… Plot cartography in 2D projected on parameters p_I_B1_C1 and p_B3_out_M to file './examples/FMS-2/FMS-2_Spec1-PRPC_cart.png'.  ------------------------------------------------------------ Statistics: Algorithm counters ------------------------------------------------------------ main algorithm : 688.006 seconds find next point : 0.000 second (0 call) ------------------------------------------------------------ Statistics: Parsing counters ------------------------------------------------------------ model parsing : 0.006 second ------------------------------------------------------------ Statistics: State computation counters ------------------------------------------------------------ number of state comparisons : 2980046 number of constraints comparisons : 304587 ------------------------------------------------------------ Statistics: Graphics-related counters ------------------------------------------------------------ state space drawing : 0.000 second cartography drawing : 0.033 second ------------------------------------------------------------ Statistics: Global counter ------------------------------------------------------------ total : 688.066 seconds IMITATOR successfully terminated (after 688.069 seconds) Estimated memory used: 171.345 GiB (i.e., 22997550798 words of size 8)