************************************************************ * 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 12:51:21  Model: ./examples/AIP/AIP_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_task2A' 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_task2B' 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_task1B' 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_task1A' 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_CL_TU3_1' 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_CL_TU3_2' 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_L3_out_TU3_2' 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_L3_out_TU3_1' 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_CL_TU2_1' 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_L2_TU2_1' 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_L2_AS2_1' 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_L2_AS2_1' 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_L2_TU2_1' 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_CL_TU2_1' 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_CL_TU3_2' 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_CL_TU2_2' 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_L2_TU2_2' 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_L2_AS2_2' 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_L2_AS2_2' 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_L2_TU2_2' 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_CL_TU3_1' 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_CL_TU1_1' 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_L1_TU1_1' 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_L1_AS1_1' 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_L1_AS1_1' 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_L1_TU1_1' 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_CL_TU1_1' 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_CL_TU2_2' 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_CL_TU1_2' 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_L1_TU1_2' 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_L1_AS1_2' 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_L1_AS1_2' 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_L1_TU1_2' 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_CL_TU1_2' 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_L3_TU3_1' 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_L3_I1' 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_product1' 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_L3_TU3_2' 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_L3_I2' 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_product2' 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_L3_TU3_2' 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_L3_TU3_1' 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 a U-PTA.  Abstract model built after 0.007 second. Memory for abstract model: 1498.359 KiB (i.e., 383580 words)   [BC (full coverage)] Starting running cartography…   **************************************************  START THE BEHAVIORAL CARTOGRAPHY ALGORITHM **************************************************  Parametric rectangle V0:   p_is1 = 1..10 & p_is2 = 1..10  Number of points inside V0: 100  ************************************************** ALGORITHM BC (full coverage): iteration 1 Considering the following pi1  p_is1 = 1 & p_is2 = 1  K1 computed by PRP in 796.418 seconds: 29279 states with 134763 transitions explored.  p_is2 >= 0 & p_is1 >= 0 *** 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 796.426 seconds.  Final constraints such that the system is correct/incorrect: False p_is2 >= 0 & p_is1 >= 0 The good constraint is exact (sound and complete). The bad constraint is exact (sound and complete). 233.912 GiB (i.e., 31395185505 words of size 8)  Result written to file './examples/AIP/AIP_Spec3-PRPC.res'.  Drawing the cartography… Plot cartography in 2D projected on parameters p_is1 and p_is2 to file './examples/AIP/AIP_Spec3-PRPC_cart.png'.  ------------------------------------------------------------ Statistics: Algorithm counters ------------------------------------------------------------ main algorithm : 796.424 seconds find next point : 0.000 second (0 call) ------------------------------------------------------------ Statistics: Parsing counters ------------------------------------------------------------ model parsing : 0.005 second ------------------------------------------------------------ Statistics: State computation counters ------------------------------------------------------------ number of state comparisons : 3002418 number of constraints comparisons : 298377 ------------------------------------------------------------ Statistics: Graphics-related counters ------------------------------------------------------------ state space drawing : 0.000 second cartography drawing : 0.043 second ------------------------------------------------------------ Statistics: Global counter ------------------------------------------------------------ total : 796.472 seconds IMITATOR successfully terminated (after 796.474 seconds) Estimated memory used: 233.912 GiB (i.e., 31395202889 words of size 8)