************************************************************ * 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:43  Model: ./experiments-FORTE/FMS-1/FMS-1_Spec3.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_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.003 second. Memory for abstract model: 910.062 KiB (i.e., 232976 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 0.368 second: 399 states with 967 transitions explored.  p_B3_out_M >= 0 & p_I_B1_C1 >= 0  [BC (full coverage)] Successfully terminated after 0.373 second.  Final constraints such that the system is correct/incorrect: False p_B3_out_M >= 0 & p_I_B1_C1 >= 0 The good constraint is exact (sound and complete). The bad constraint is exact (sound and complete). 20.577 MiB (i.e., 2697188 words of size 8)  Result written to file './experiments-FORTE/FMS-1/FMS-1_Spec3-PRPC.res'.  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_Spec3-PRPC_cart.png'.  ------------------------------------------------------------ Statistics: Algorithm counters ------------------------------------------------------------ main algorithm : 0.372 second find next point : 0.000 second (0 call) ------------------------------------------------------------ Statistics: Parsing counters ------------------------------------------------------------ model parsing : 0.002 second ------------------------------------------------------------ Statistics: State computation counters ------------------------------------------------------------ number of state comparisons : 2518 number of constraints comparisons : 585 ------------------------------------------------------------ Statistics: Graphics-related counters ------------------------------------------------------------ state space drawing : 0.000 second cartography drawing : 0.024 second ------------------------------------------------------------ Statistics: Global counter ------------------------------------------------------------ total : 0.397 second IMITATOR successfully terminated (after 0.399 second) Estimated memory used: 20.713 MiB (i.e., 2714996 words of size 8)