etienne@MakBook:~/Boulot/SVN/andre/papiers/2017/learning$ sh runexpscala.sh ************************************************************ * 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:45:48 Model: experiments-FORTE/scalability/FMS-2_Spec1.imi Mode: behavioral cartography algorithm with full coverage and step 1 and using learning-based abstractions. Considering variant of IM with inclusion in the fixpoint [AS11]. Merging technique of [AFS13] enabled. *** 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.012 second. Memory for abstract model: 1243.367 KiB (i.e., 318302 words) [BC (full coverage with learning-based abstraction)] Starting running cartography… ************************************************** START THE BEHAVIORAL CARTOGRAPHY ALGORITHM ************************************************** Parametric rectangle V0: p_I_B1_C1 = 1..50 & p_B3_out_M = 1..50 Number of points inside V0: 2500 ************************************************** ALGORITHM BC (full coverage with learning-based abstraction): iteration 1 Considering the following pi1 p_I_B1_C1 = 1 & p_B3_out_M = 1 Executing: 'python /home/etienne/Boulot/SVN/andre/papiers/2017/learning/IMICV/bin/../interfaceCV.py experiments-FORTE/scalability/FMS-2_Spec1.imi experiments-FORTE/scalability/FMS-2_Spec1_learning_1.imi p_I_B1_C1=1,p_B3_out_M=1' *-**--***---****---***--**-* Hello, this is Interfaçator! Building reference valuation… Pi0: v(p_I_B1_C1) = 1 v(p_B3_out_M) = 1 Valuating component A with pi0… Writing content to "experiments-FORTE/scalability/FMS-2_Spec1.cv"… Executing "/home/etienne/Boulot/SVN/andre/papiers/2017/learning/IMICV/bin/../CV/Compositional_Verifier -imi experiments-FORTE/scalability/FMS-2_Spec1.cv"… Abstraction detected Moving learning result from "/home/etienne/Boulot/SVN/andre/papiers/2017/learning/IMICV/bin/../CV/tmp/assumption.imi" to "experiments-FORTE/scalability/FMS-2_Spec1_learning_1.imi-output.cv"… Copying abstract model into "experiments-FORTE/scalability/FMS-2_Spec1_learning_1.imi"… …The end of Interfaçator! *-**--***---****---***--**-* Model generated by learning: abstraction *** 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_I_B6_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_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_B6_in_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 80.930 seconds. Memory for abstract model: 1815.062 KiB (i.e., 464656 words) Original model: 11 automata. New model: 7 K1 computed by PRP in 4.527 seconds: 916 states with 3165 transitions explored. 2 >= p_I_B1_C1 & p_I_B1_C1 >= 0 & p_B3_out_M >= 0 ************************************************** ALGORITHM BC (full coverage with learning-based abstraction): iteration 2 Considering the following pi2 p_I_B1_C1 = 3 & p_B3_out_M = 1 Executing: 'python /home/etienne/Boulot/SVN/andre/papiers/2017/learning/IMICV/bin/../interfaceCV.py experiments-FORTE/scalability/FMS-2_Spec1.imi experiments-FORTE/scalability/FMS-2_Spec1_learning_2.imi p_I_B1_C1=3,p_B3_out_M=1' *-**--***---****---***--**-* Hello, this is Interfaçator! Building reference valuation… Pi0: v(p_I_B1_C1) = 3 v(p_B3_out_M) = 1 Valuating component A with pi0… Writing content to "experiments-FORTE/scalability/FMS-2_Spec1.cv"… Executing "/home/etienne/Boulot/SVN/andre/papiers/2017/learning/IMICV/bin/../CV/Compositional_Verifier -imi experiments-FORTE/scalability/FMS-2_Spec1.cv"… Counter-example detected Moving learning result from "/home/etienne/Boulot/SVN/andre/papiers/2017/learning/IMICV/bin/../CV/tmp/counterexample.imi" to "experiments-FORTE/scalability/FMS-2_Spec1_learning_2.imi-output.cv"… Copying abstract model into "experiments-FORTE/scalability/FMS-2_Spec1_learning_2.imi"… …The end of Interfaçator! *-**--***---****---***--**-* Model generated by learning: counter-example *** Warning: The synclab 'O_B1_R1' is not used in (at least) the automaton 'AbstractERA' where it is declared: it will thus be removed from the whole model. *** Warning: The synclab 'B2_in' is not used in (at least) the automaton 'AbstractERA' where it is declared: it will thus be removed from the whole model. *** Warning: The synclab 'I_B2_C2' is not used in (at least) the automaton 'AbstractERA' where it is declared: it will thus be removed from the whole model. *** Warning: The synclab 'O_B2_R3' is not used in (at least) the automaton 'AbstractERA' where it is declared: it will thus be removed from the whole model. *** Warning: The synclab 'I_B3_R1' is not used in (at least) the automaton 'AbstractERA' where it is declared: it will thus be removed from the whole model. *** Warning: The synclab 'B3_in_M' is not used in (at least) the automaton 'AbstractERA' where it is declared: it will thus be removed from the whole model. *** Warning: The synclab 'I_B3_M' is not used in (at least) the automaton 'AbstractERA' where it is declared: it will thus be removed from the whole model. *** Warning: The synclab 'B2_out' is not used in (at least) the automaton 'AbstractERA' where it is declared: it will thus be removed from the whole model. *** 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 85.529 seconds. Memory for abstract model: 145776.085 KiB (i.e., 37318678 words) Original model: 11 automata. New model: 12 K2 computed by EFunsafe in 0.198 second: 96 states with 192 transitions explored. p_I_B1_C1 > 2 & p_B3_out_M >= 0 [BC (full coverage with learning-based abstraction)] Successfully terminated after 85.745 seconds. Final constraints such that the system is correct/incorrect: 2 >= p_I_B1_C1 & p_I_B1_C1 >= 0 & p_B3_out_M >= 0 p_I_B1_C1 > 2 & p_B3_out_M >= 0 The good constraint is exact (sound and complete). The bad constraint is exact (sound and complete). 295.528 MiB (i.e., 38735520 words of size 8) Result written to file 'experiments-FORTE/scalability/FMS-2_Spec1.res'. ------------------------------------------------------------ Statistics: Algorithm counters ------------------------------------------------------------ main algorithm : 85.742 seconds find next point : 0.017 second (0 call) learning : 80.967 seconds (2 calls | 40.4839224816 second/call) learning: re-parsing : 0.014 second (2 calls | 0.00725948810578 second/call) abstractions learnt : 1 counter-examples learnt : 1 ------------------------------------------------------------ Statistics: Parsing counters ------------------------------------------------------------ model parsing : 0.008 second ------------------------------------------------------------ Statistics: State computation counters ------------------------------------------------------------ number of state comparisons : 33549 number of constraints comparisons : 7653 ------------------------------------------------------------ Statistics: Graphics-related counters ------------------------------------------------------------ state space drawing : 0.000 second ------------------------------------------------------------ Statistics: Global counter ------------------------------------------------------------ total : 85.743 seconds IMITATOR successfully terminated (after 85.747 seconds) Estimated memory used: 295.653 MiB (i.e., 38751931 words of size 8) ************************************************************ * 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:47:13 Model: experiments-FORTE/scalability/FMS-2_Spec1.imi Mode: behavioral cartography algorithm with full coverage and step 1 and using learning-based abstractions. Considering variant of IM with inclusion in the fixpoint [AS11]. Merging technique of [AFS13] enabled. *** 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: 1243.367 KiB (i.e., 318302 words) [BC (full coverage with learning-based abstraction)] Starting running cartography… ************************************************** START THE BEHAVIORAL CARTOGRAPHY ALGORITHM ************************************************** Parametric rectangle V0: p_I_B1_C1 = 1..100 & p_B3_out_M = 1..100 Number of points inside V0: 10000 ************************************************** ALGORITHM BC (full coverage with learning-based abstraction): iteration 1 Considering the following pi1 p_I_B1_C1 = 1 & p_B3_out_M = 1 Executing: 'python /home/etienne/Boulot/SVN/andre/papiers/2017/learning/IMICV/bin/../interfaceCV.py experiments-FORTE/scalability/FMS-2_Spec1.imi experiments-FORTE/scalability/FMS-2_Spec1_learning_1.imi p_I_B1_C1=1,p_B3_out_M=1' *-**--***---****---***--**-* Hello, this is Interfaçator! Building reference valuation… Pi0: v(p_I_B1_C1) = 1 v(p_B3_out_M) = 1 Valuating component A with pi0… Writing content to "experiments-FORTE/scalability/FMS-2_Spec1.cv"… Executing "/home/etienne/Boulot/SVN/andre/papiers/2017/learning/IMICV/bin/../CV/Compositional_Verifier -imi experiments-FORTE/scalability/FMS-2_Spec1.cv"… Abstraction detected Moving learning result from "/home/etienne/Boulot/SVN/andre/papiers/2017/learning/IMICV/bin/../CV/tmp/assumption.imi" to "experiments-FORTE/scalability/FMS-2_Spec1_learning_1.imi-output.cv"… Copying abstract model into "experiments-FORTE/scalability/FMS-2_Spec1_learning_1.imi"… …The end of Interfaçator! *-**--***---****---***--**-* Model generated by learning: abstraction *** 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_I_B6_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_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_B6_in_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 82.423 seconds. Memory for abstract model: 1815.066 KiB (i.e., 464657 words) Original model: 11 automata. New model: 7 K1 computed by PRP in 4.503 seconds: 916 states with 3165 transitions explored. 2 >= p_I_B1_C1 & p_I_B1_C1 >= 0 & p_B3_out_M >= 0 ************************************************** ALGORITHM BC (full coverage with learning-based abstraction): iteration 2 Considering the following pi2 p_I_B1_C1 = 3 & p_B3_out_M = 1 Executing: 'python /home/etienne/Boulot/SVN/andre/papiers/2017/learning/IMICV/bin/../interfaceCV.py experiments-FORTE/scalability/FMS-2_Spec1.imi experiments-FORTE/scalability/FMS-2_Spec1_learning_2.imi p_I_B1_C1=3,p_B3_out_M=1' *-**--***---****---***--**-* Hello, this is Interfaçator! Building reference valuation… Pi0: v(p_I_B1_C1) = 3 v(p_B3_out_M) = 1 Valuating component A with pi0… Writing content to "experiments-FORTE/scalability/FMS-2_Spec1.cv"… Executing "/home/etienne/Boulot/SVN/andre/papiers/2017/learning/IMICV/bin/../CV/Compositional_Verifier -imi experiments-FORTE/scalability/FMS-2_Spec1.cv"… Counter-example detected Moving learning result from "/home/etienne/Boulot/SVN/andre/papiers/2017/learning/IMICV/bin/../CV/tmp/counterexample.imi" to "experiments-FORTE/scalability/FMS-2_Spec1_learning_2.imi-output.cv"… Copying abstract model into "experiments-FORTE/scalability/FMS-2_Spec1_learning_2.imi"… …The end of Interfaçator! *-**--***---****---***--**-* Model generated by learning: counter-example *** Warning: The synclab 'O_B1_R1' is not used in (at least) the automaton 'AbstractERA' where it is declared: it will thus be removed from the whole model. *** Warning: The synclab 'B2_in' is not used in (at least) the automaton 'AbstractERA' where it is declared: it will thus be removed from the whole model. *** Warning: The synclab 'I_B2_C2' is not used in (at least) the automaton 'AbstractERA' where it is declared: it will thus be removed from the whole model. *** Warning: The synclab 'O_B2_R3' is not used in (at least) the automaton 'AbstractERA' where it is declared: it will thus be removed from the whole model. *** Warning: The synclab 'I_B3_R1' is not used in (at least) the automaton 'AbstractERA' where it is declared: it will thus be removed from the whole model. *** Warning: The synclab 'B3_in_M' is not used in (at least) the automaton 'AbstractERA' where it is declared: it will thus be removed from the whole model. *** Warning: The synclab 'I_B3_M' is not used in (at least) the automaton 'AbstractERA' where it is declared: it will thus be removed from the whole model. *** Warning: The synclab 'B2_out' is not used in (at least) the automaton 'AbstractERA' where it is declared: it will thus be removed from the whole model. *** 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 86.997 seconds. Memory for abstract model: 145776.089 KiB (i.e., 37318679 words) Original model: 11 automata. New model: 12 K2 computed by EFunsafe in 0.196 second: 96 states with 192 transitions explored. p_I_B1_C1 > 2 & p_B3_out_M >= 0 [BC (full coverage with learning-based abstraction)] Successfully terminated after 87.278 seconds. Final constraints such that the system is correct/incorrect: 2 >= p_I_B1_C1 & p_I_B1_C1 >= 0 & p_B3_out_M >= 0 p_I_B1_C1 > 2 & p_B3_out_M >= 0 The good constraint is exact (sound and complete). The bad constraint is exact (sound and complete). 313.879 MiB (i.e., 41140827 words of size 8) Result written to file 'experiments-FORTE/scalability/FMS-2_Spec1.res'. ------------------------------------------------------------ Statistics: Algorithm counters ------------------------------------------------------------ main algorithm : 87.276 seconds find next point : 0.084 second (0 call) learning : 82.465 seconds (2 calls | 41.2329795361 second/call) learning: re-parsing : 0.014 second (2 calls | 0.0072250366211 second/call) abstractions learnt : 1 counter-examples learnt : 1 ------------------------------------------------------------ Statistics: Parsing counters ------------------------------------------------------------ model parsing : 0.007 second ------------------------------------------------------------ Statistics: State computation counters ------------------------------------------------------------ number of state comparisons : 33549 number of constraints comparisons : 7653 ------------------------------------------------------------ Statistics: Graphics-related counters ------------------------------------------------------------ state space drawing : 0.000 second ------------------------------------------------------------ Statistics: Global counter ------------------------------------------------------------ total : 87.277 seconds IMITATOR successfully terminated (after 87.279 seconds) Estimated memory used: 314.004 MiB (i.e., 41157229 words of size 8) ************************************************************ * 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:48:41 Model: experiments-FORTE/scalability/FMS-2_Spec1.imi Mode: behavioral cartography algorithm with full coverage and step 1 and using learning-based abstractions. Considering variant of IM with inclusion in the fixpoint [AS11]. Merging technique of [AFS13] enabled. *** 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.011 second. Memory for abstract model: 1243.367 KiB (i.e., 318302 words) [BC (full coverage with learning-based abstraction)] Starting running cartography… ************************************************** START THE BEHAVIORAL CARTOGRAPHY ALGORITHM ************************************************** Parametric rectangle V0: p_I_B1_C1 = 1..500 & p_B3_out_M = 1..500 Number of points inside V0: 250000 ************************************************** ALGORITHM BC (full coverage with learning-based abstraction): iteration 1 Considering the following pi1 p_I_B1_C1 = 1 & p_B3_out_M = 1 Executing: 'python /home/etienne/Boulot/SVN/andre/papiers/2017/learning/IMICV/bin/../interfaceCV.py experiments-FORTE/scalability/FMS-2_Spec1.imi experiments-FORTE/scalability/FMS-2_Spec1_learning_1.imi p_I_B1_C1=1,p_B3_out_M=1' *-**--***---****---***--**-* Hello, this is Interfaçator! Building reference valuation… Pi0: v(p_I_B1_C1) = 1 v(p_B3_out_M) = 1 Valuating component A with pi0… Writing content to "experiments-FORTE/scalability/FMS-2_Spec1.cv"… Executing "/home/etienne/Boulot/SVN/andre/papiers/2017/learning/IMICV/bin/../CV/Compositional_Verifier -imi experiments-FORTE/scalability/FMS-2_Spec1.cv"… Abstraction detected Moving learning result from "/home/etienne/Boulot/SVN/andre/papiers/2017/learning/IMICV/bin/../CV/tmp/assumption.imi" to "experiments-FORTE/scalability/FMS-2_Spec1_learning_1.imi-output.cv"… Copying abstract model into "experiments-FORTE/scalability/FMS-2_Spec1_learning_1.imi"… …The end of Interfaçator! *-**--***---****---***--**-* Model generated by learning: abstraction *** 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_I_B6_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_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_B6_in_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 82.000 seconds. Memory for abstract model: 1815.097 KiB (i.e., 464665 words) Original model: 11 automata. New model: 7 K1 computed by PRP in 4.508 seconds: 916 states with 3165 transitions explored. 2 >= p_I_B1_C1 & p_I_B1_C1 >= 0 & p_B3_out_M >= 0 ************************************************** ALGORITHM BC (full coverage with learning-based abstraction): iteration 2 Considering the following pi2 p_I_B1_C1 = 3 & p_B3_out_M = 1 Executing: 'python /home/etienne/Boulot/SVN/andre/papiers/2017/learning/IMICV/bin/../interfaceCV.py experiments-FORTE/scalability/FMS-2_Spec1.imi experiments-FORTE/scalability/FMS-2_Spec1_learning_2.imi p_I_B1_C1=3,p_B3_out_M=1' *-**--***---****---***--**-* Hello, this is Interfaçator! Building reference valuation… Pi0: v(p_I_B1_C1) = 3 v(p_B3_out_M) = 1 Valuating component A with pi0… Writing content to "experiments-FORTE/scalability/FMS-2_Spec1.cv"… Executing "/home/etienne/Boulot/SVN/andre/papiers/2017/learning/IMICV/bin/../CV/Compositional_Verifier -imi experiments-FORTE/scalability/FMS-2_Spec1.cv"… Counter-example detected Moving learning result from "/home/etienne/Boulot/SVN/andre/papiers/2017/learning/IMICV/bin/../CV/tmp/counterexample.imi" to "experiments-FORTE/scalability/FMS-2_Spec1_learning_2.imi-output.cv"… Copying abstract model into "experiments-FORTE/scalability/FMS-2_Spec1_learning_2.imi"… …The end of Interfaçator! *-**--***---****---***--**-* Model generated by learning: counter-example *** Warning: The synclab 'O_B1_R1' is not used in (at least) the automaton 'AbstractERA' where it is declared: it will thus be removed from the whole model. *** Warning: The synclab 'B2_in' is not used in (at least) the automaton 'AbstractERA' where it is declared: it will thus be removed from the whole model. *** Warning: The synclab 'I_B2_C2' is not used in (at least) the automaton 'AbstractERA' where it is declared: it will thus be removed from the whole model. *** Warning: The synclab 'O_B2_R3' is not used in (at least) the automaton 'AbstractERA' where it is declared: it will thus be removed from the whole model. *** Warning: The synclab 'I_B3_R1' is not used in (at least) the automaton 'AbstractERA' where it is declared: it will thus be removed from the whole model. *** Warning: The synclab 'B3_in_M' is not used in (at least) the automaton 'AbstractERA' where it is declared: it will thus be removed from the whole model. *** Warning: The synclab 'I_B3_M' is not used in (at least) the automaton 'AbstractERA' where it is declared: it will thus be removed from the whole model. *** Warning: The synclab 'B2_out' is not used in (at least) the automaton 'AbstractERA' where it is declared: it will thus be removed from the whole model. *** 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 86.581 seconds. Memory for abstract model: 145776.121 KiB (i.e., 37318687 words) Original model: 11 automata. New model: 12 K2 computed by EFunsafe in 0.193 second: 96 states with 192 transitions explored. p_I_B1_C1 > 2 & p_B3_out_M >= 0 [BC (full coverage with learning-based abstraction)] Successfully terminated after 89.000 seconds. Final constraints such that the system is correct/incorrect: 2 >= p_I_B1_C1 & p_I_B1_C1 >= 0 & p_B3_out_M >= 0 p_I_B1_C1 > 2 & p_B3_out_M >= 0 The good constraint is exact (sound and complete). The bad constraint is exact (sound and complete). 902.887 MiB (i.e., 118343317 words of size 8) Result written to file 'experiments-FORTE/scalability/FMS-2_Spec1.res'. ------------------------------------------------------------ Statistics: Algorithm counters ------------------------------------------------------------ main algorithm : 88.998 seconds find next point : 2.224 seconds (0 call) learning : 82.041 seconds (2 calls | 41.0209565163 second/call) learning: re-parsing : 0.012 second (2 calls | 0.0063021183014 second/call) abstractions learnt : 1 counter-examples learnt : 1 ------------------------------------------------------------ Statistics: Parsing counters ------------------------------------------------------------ model parsing : 0.010 second ------------------------------------------------------------ Statistics: State computation counters ------------------------------------------------------------ number of state comparisons : 33549 number of constraints comparisons : 7653 ------------------------------------------------------------ Statistics: Graphics-related counters ------------------------------------------------------------ state space drawing : 0.000 second ------------------------------------------------------------ Statistics: Global counter ------------------------------------------------------------ total : 88.999 seconds IMITATOR successfully terminated (after 89.001 seconds) Estimated memory used: 903.013 MiB (i.e., 118359730 words of size 8) ************************************************************ * 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:50:10 Model: experiments-FORTE/scalability/FMS-2_Spec1.imi Mode: behavioral cartography algorithm with full coverage and step 1 and using learning-based abstractions. Considering variant of IM with inclusion in the fixpoint [AS11]. Merging technique of [AFS13] enabled. *** 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.012 second. Memory for abstract model: 1243.367 KiB (i.e., 318302 words) [BC (full coverage with learning-based abstraction)] Starting running cartography… ************************************************** START THE BEHAVIORAL CARTOGRAPHY ALGORITHM ************************************************** Parametric rectangle V0: p_I_B1_C1 = 1..1000 & p_B3_out_M = 1..1000 Number of points inside V0: 1000000 ************************************************** ALGORITHM BC (full coverage with learning-based abstraction): iteration 1 Considering the following pi1 p_I_B1_C1 = 1 & p_B3_out_M = 1 Executing: 'python /home/etienne/Boulot/SVN/andre/papiers/2017/learning/IMICV/bin/../interfaceCV.py experiments-FORTE/scalability/FMS-2_Spec1.imi experiments-FORTE/scalability/FMS-2_Spec1_learning_1.imi p_I_B1_C1=1,p_B3_out_M=1' *-**--***---****---***--**-* Hello, this is Interfaçator! Building reference valuation… Pi0: v(p_I_B1_C1) = 1 v(p_B3_out_M) = 1 Valuating component A with pi0… Writing content to "experiments-FORTE/scalability/FMS-2_Spec1.cv"… Executing "/home/etienne/Boulot/SVN/andre/papiers/2017/learning/IMICV/bin/../CV/Compositional_Verifier -imi experiments-FORTE/scalability/FMS-2_Spec1.cv"… Abstraction detected Moving learning result from "/home/etienne/Boulot/SVN/andre/papiers/2017/learning/IMICV/bin/../CV/tmp/assumption.imi" to "experiments-FORTE/scalability/FMS-2_Spec1_learning_1.imi-output.cv"… Copying abstract model into "experiments-FORTE/scalability/FMS-2_Spec1_learning_1.imi"… …The end of Interfaçator! *-**--***---****---***--**-* Model generated by learning: abstraction *** 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_I_B6_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_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_B6_in_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 83.030 seconds. Memory for abstract model: 1815.105 KiB (i.e., 464667 words) Original model: 11 automata. New model: 7 K1 computed by PRP in 4.488 seconds: 916 states with 3165 transitions explored. 2 >= p_I_B1_C1 & p_I_B1_C1 >= 0 & p_B3_out_M >= 0 ************************************************** ALGORITHM BC (full coverage with learning-based abstraction): iteration 2 Considering the following pi2 p_I_B1_C1 = 3 & p_B3_out_M = 1 Executing: 'python /home/etienne/Boulot/SVN/andre/papiers/2017/learning/IMICV/bin/../interfaceCV.py experiments-FORTE/scalability/FMS-2_Spec1.imi experiments-FORTE/scalability/FMS-2_Spec1_learning_2.imi p_I_B1_C1=3,p_B3_out_M=1' *-**--***---****---***--**-* Hello, this is Interfaçator! Building reference valuation… Pi0: v(p_I_B1_C1) = 3 v(p_B3_out_M) = 1 Valuating component A with pi0… Writing content to "experiments-FORTE/scalability/FMS-2_Spec1.cv"… Executing "/home/etienne/Boulot/SVN/andre/papiers/2017/learning/IMICV/bin/../CV/Compositional_Verifier -imi experiments-FORTE/scalability/FMS-2_Spec1.cv"… Counter-example detected Moving learning result from "/home/etienne/Boulot/SVN/andre/papiers/2017/learning/IMICV/bin/../CV/tmp/counterexample.imi" to "experiments-FORTE/scalability/FMS-2_Spec1_learning_2.imi-output.cv"… Copying abstract model into "experiments-FORTE/scalability/FMS-2_Spec1_learning_2.imi"… …The end of Interfaçator! *-**--***---****---***--**-* Model generated by learning: counter-example *** Warning: The synclab 'O_B1_R1' is not used in (at least) the automaton 'AbstractERA' where it is declared: it will thus be removed from the whole model. *** Warning: The synclab 'B2_in' is not used in (at least) the automaton 'AbstractERA' where it is declared: it will thus be removed from the whole model. *** Warning: The synclab 'I_B2_C2' is not used in (at least) the automaton 'AbstractERA' where it is declared: it will thus be removed from the whole model. *** Warning: The synclab 'O_B2_R3' is not used in (at least) the automaton 'AbstractERA' where it is declared: it will thus be removed from the whole model. *** Warning: The synclab 'I_B3_R1' is not used in (at least) the automaton 'AbstractERA' where it is declared: it will thus be removed from the whole model. *** Warning: The synclab 'B3_in_M' is not used in (at least) the automaton 'AbstractERA' where it is declared: it will thus be removed from the whole model. *** Warning: The synclab 'I_B3_M' is not used in (at least) the automaton 'AbstractERA' where it is declared: it will thus be removed from the whole model. *** Warning: The synclab 'B2_out' is not used in (at least) the automaton 'AbstractERA' where it is declared: it will thus be removed from the whole model. *** 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 87.587 seconds. Memory for abstract model: 145776.113 KiB (i.e., 37318685 words) Original model: 11 automata. New model: 12 K2 computed by EFunsafe in 0.201 second: 96 states with 192 transitions explored. p_I_B1_C1 > 2 & p_B3_out_M >= 0 [BC (full coverage with learning-based abstraction)] Successfully terminated after 96.665 seconds. Final constraints such that the system is correct/incorrect: 2 >= p_I_B1_C1 & p_I_B1_C1 >= 0 & p_B3_out_M >= 0 p_I_B1_C1 > 2 & p_B3_out_M >= 0 The good constraint is exact (sound and complete). The bad constraint is exact (sound and complete). 2.680 GiB (i.e., 359746871 words of size 8) Result written to file 'experiments-FORTE/scalability/FMS-2_Spec1.res'. ------------------------------------------------------------ Statistics: Algorithm counters ------------------------------------------------------------ main algorithm : 96.661 seconds find next point : 8.876 seconds (0 call) learning : 83.067 seconds (2 calls | 41.5337331296 second/call) learning: re-parsing : 0.011 second (2 calls | 0.00590252876282 second/call) abstractions learnt : 1 counter-examples learnt : 1 ------------------------------------------------------------ Statistics: Parsing counters ------------------------------------------------------------ model parsing : 0.008 second ------------------------------------------------------------ Statistics: State computation counters ------------------------------------------------------------ number of state comparisons : 33549 number of constraints comparisons : 7653 ------------------------------------------------------------ Statistics: Graphics-related counters ------------------------------------------------------------ state space drawing : 0.000 second ------------------------------------------------------------ Statistics: Global counter ------------------------------------------------------------ total : 96.732 seconds IMITATOR successfully terminated (after 96.735 seconds) Estimated memory used: 2.680 GiB (i.e., 359763291 words of size 8) ************************************************************ * 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:51:46 Model: experiments-FORTE/scalability/FMS-2_Spec1.imi Mode: behavioral cartography algorithm with full coverage and step 1 and using learning-based abstractions. Considering variant of IM with inclusion in the fixpoint [AS11]. Merging technique of [AFS13] enabled. *** 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: 1243.367 KiB (i.e., 318302 words) [BC (full coverage with learning-based abstraction)] Starting running cartography… ************************************************** START THE BEHAVIORAL CARTOGRAPHY ALGORITHM ************************************************** Parametric rectangle V0: p_I_B1_C1 = 1..5000 & p_B3_out_M = 1..5000 Number of points inside V0: 25000000 ************************************************** ALGORITHM BC (full coverage with learning-based abstraction): iteration 1 Considering the following pi1 p_I_B1_C1 = 1 & p_B3_out_M = 1 Executing: 'python /home/etienne/Boulot/SVN/andre/papiers/2017/learning/IMICV/bin/../interfaceCV.py experiments-FORTE/scalability/FMS-2_Spec1.imi experiments-FORTE/scalability/FMS-2_Spec1_learning_1.imi p_I_B1_C1=1,p_B3_out_M=1' *-**--***---****---***--**-* Hello, this is Interfaçator! Building reference valuation… Pi0: v(p_I_B1_C1) = 1 v(p_B3_out_M) = 1 Valuating component A with pi0… Writing content to "experiments-FORTE/scalability/FMS-2_Spec1.cv"… Executing "/home/etienne/Boulot/SVN/andre/papiers/2017/learning/IMICV/bin/../CV/Compositional_Verifier -imi experiments-FORTE/scalability/FMS-2_Spec1.cv"… Abstraction detected Moving learning result from "/home/etienne/Boulot/SVN/andre/papiers/2017/learning/IMICV/bin/../CV/tmp/assumption.imi" to "experiments-FORTE/scalability/FMS-2_Spec1_learning_1.imi-output.cv"… Copying abstract model into "experiments-FORTE/scalability/FMS-2_Spec1_learning_1.imi"… …The end of Interfaçator! *-**--***---****---***--**-* Model generated by learning: abstraction *** 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_I_B6_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_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_B6_in_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 83.063 seconds. Memory for abstract model: 1815.109 KiB (i.e., 464668 words) Original model: 11 automata. New model: 7 K1 computed by PRP in 4.505 seconds: 916 states with 3165 transitions explored. 2 >= p_I_B1_C1 & p_I_B1_C1 >= 0 & p_B3_out_M >= 0 ************************************************** ALGORITHM BC (full coverage with learning-based abstraction): iteration 2 Considering the following pi2 p_I_B1_C1 = 3 & p_B3_out_M = 1 Executing: 'python /home/etienne/Boulot/SVN/andre/papiers/2017/learning/IMICV/bin/../interfaceCV.py experiments-FORTE/scalability/FMS-2_Spec1.imi experiments-FORTE/scalability/FMS-2_Spec1_learning_2.imi p_I_B1_C1=3,p_B3_out_M=1' *-**--***---****---***--**-* Hello, this is Interfaçator! Building reference valuation… Pi0: v(p_I_B1_C1) = 3 v(p_B3_out_M) = 1 Valuating component A with pi0… Writing content to "experiments-FORTE/scalability/FMS-2_Spec1.cv"… Executing "/home/etienne/Boulot/SVN/andre/papiers/2017/learning/IMICV/bin/../CV/Compositional_Verifier -imi experiments-FORTE/scalability/FMS-2_Spec1.cv"… Counter-example detected Moving learning result from "/home/etienne/Boulot/SVN/andre/papiers/2017/learning/IMICV/bin/../CV/tmp/counterexample.imi" to "experiments-FORTE/scalability/FMS-2_Spec1_learning_2.imi-output.cv"… Copying abstract model into "experiments-FORTE/scalability/FMS-2_Spec1_learning_2.imi"… …The end of Interfaçator! *-**--***---****---***--**-* Model generated by learning: counter-example *** Warning: The synclab 'O_B1_R1' is not used in (at least) the automaton 'AbstractERA' where it is declared: it will thus be removed from the whole model. *** Warning: The synclab 'B2_in' is not used in (at least) the automaton 'AbstractERA' where it is declared: it will thus be removed from the whole model. *** Warning: The synclab 'I_B2_C2' is not used in (at least) the automaton 'AbstractERA' where it is declared: it will thus be removed from the whole model. *** Warning: The synclab 'O_B2_R3' is not used in (at least) the automaton 'AbstractERA' where it is declared: it will thus be removed from the whole model. *** Warning: The synclab 'I_B3_R1' is not used in (at least) the automaton 'AbstractERA' where it is declared: it will thus be removed from the whole model. *** Warning: The synclab 'B3_in_M' is not used in (at least) the automaton 'AbstractERA' where it is declared: it will thus be removed from the whole model. *** Warning: The synclab 'I_B3_M' is not used in (at least) the automaton 'AbstractERA' where it is declared: it will thus be removed from the whole model. *** Warning: The synclab 'B2_out' is not used in (at least) the automaton 'AbstractERA' where it is declared: it will thus be removed from the whole model. *** 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 87.634 seconds. Memory for abstract model: 145776.117 KiB (i.e., 37318686 words) Original model: 11 automata. New model: 12 K2 computed by EFunsafe in 0.194 second: 96 states with 192 transitions explored. p_I_B1_C1 > 2 & p_B3_out_M >= 0 [BC (full coverage with learning-based abstraction)] Successfully terminated after 309.041 seconds. Final constraints such that the system is correct/incorrect: 2 >= p_I_B1_C1 & p_I_B1_C1 >= 0 & p_B3_out_M >= 0 p_I_B1_C1 > 2 & p_B3_out_M >= 0 The good constraint is exact (sound and complete). The bad constraint is exact (sound and complete). 60.252 GiB (i.e., 8086985506 words of size 8) Result written to file 'experiments-FORTE/scalability/FMS-2_Spec1.res'. ------------------------------------------------------------ Statistics: Algorithm counters ------------------------------------------------------------ main algorithm : 309.037 seconds find next point : 221.211 seconds (0 call) learning : 83.101 seconds (2 calls | 41.5508404971 second/call) learning: re-parsing : 0.012 second (2 calls | 0.00634646415711 second/call) abstractions learnt : 1 counter-examples learnt : 1 ------------------------------------------------------------ Statistics: Parsing counters ------------------------------------------------------------ model parsing : 0.007 second ------------------------------------------------------------ Statistics: State computation counters ------------------------------------------------------------ number of state comparisons : 33549 number of constraints comparisons : 7653 ------------------------------------------------------------ Statistics: Graphics-related counters ------------------------------------------------------------ state space drawing : 0.000 second ------------------------------------------------------------ Statistics: Global counter ------------------------------------------------------------ total : 309.038 seconds IMITATOR successfully terminated (after 309.042 seconds) Estimated memory used: 60.252 GiB (i.e., 8087001957 words of size 8) ************************************************************ * 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:56:55 Model: experiments-FORTE/scalability/FMS-2_Spec1.imi Mode: behavioral cartography algorithm with full coverage and step 1 and using learning-based abstractions. Considering variant of IM with inclusion in the fixpoint [AS11]. Merging technique of [AFS13] enabled. *** 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.005 second. Memory for abstract model: 1243.378 KiB (i.e., 318305 words) [BC (full coverage with learning-based abstraction)] Starting running cartography… ************************************************** START THE BEHAVIORAL CARTOGRAPHY ALGORITHM ************************************************** Parametric rectangle V0: p_I_B1_C1 = 1..10000 & p_B3_out_M = 1..10000 Number of points inside V0: 100000000 ************************************************** ALGORITHM BC (full coverage with learning-based abstraction): iteration 1 Considering the following pi1 p_I_B1_C1 = 1 & p_B3_out_M = 1 Executing: 'python /home/etienne/Boulot/SVN/andre/papiers/2017/learning/IMICV/bin/../interfaceCV.py experiments-FORTE/scalability/FMS-2_Spec1.imi experiments-FORTE/scalability/FMS-2_Spec1_learning_1.imi p_I_B1_C1=1,p_B3_out_M=1' *-**--***---****---***--**-* Hello, this is Interfaçator! Building reference valuation… Pi0: v(p_I_B1_C1) = 1 v(p_B3_out_M) = 1 Valuating component A with pi0… Writing content to "experiments-FORTE/scalability/FMS-2_Spec1.cv"… Executing "/home/etienne/Boulot/SVN/andre/papiers/2017/learning/IMICV/bin/../CV/Compositional_Verifier -imi experiments-FORTE/scalability/FMS-2_Spec1.cv"… Abstraction detected Moving learning result from "/home/etienne/Boulot/SVN/andre/papiers/2017/learning/IMICV/bin/../CV/tmp/assumption.imi" to "experiments-FORTE/scalability/FMS-2_Spec1_learning_1.imi-output.cv"… Copying abstract model into "experiments-FORTE/scalability/FMS-2_Spec1_learning_1.imi"… …The end of Interfaçator! *-**--***---****---***--**-* Model generated by learning: abstraction *** 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_I_B6_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_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_B6_in_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 83.476 seconds. Memory for abstract model: 1815.125 KiB (i.e., 464672 words) Original model: 11 automata. New model: 7 K1 computed by PRP in 4.473 seconds: 916 states with 3165 transitions explored. 2 >= p_I_B1_C1 & p_I_B1_C1 >= 0 & p_B3_out_M >= 0 ************************************************** ALGORITHM BC (full coverage with learning-based abstraction): iteration 2 Considering the following pi2 p_I_B1_C1 = 3 & p_B3_out_M = 1 Executing: 'python /home/etienne/Boulot/SVN/andre/papiers/2017/learning/IMICV/bin/../interfaceCV.py experiments-FORTE/scalability/FMS-2_Spec1.imi experiments-FORTE/scalability/FMS-2_Spec1_learning_2.imi p_I_B1_C1=3,p_B3_out_M=1' *-**--***---****---***--**-* Hello, this is Interfaçator! Building reference valuation… Pi0: v(p_I_B1_C1) = 3 v(p_B3_out_M) = 1 Valuating component A with pi0… Writing content to "experiments-FORTE/scalability/FMS-2_Spec1.cv"… Executing "/home/etienne/Boulot/SVN/andre/papiers/2017/learning/IMICV/bin/../CV/Compositional_Verifier -imi experiments-FORTE/scalability/FMS-2_Spec1.cv"… Counter-example detected Moving learning result from "/home/etienne/Boulot/SVN/andre/papiers/2017/learning/IMICV/bin/../CV/tmp/counterexample.imi" to "experiments-FORTE/scalability/FMS-2_Spec1_learning_2.imi-output.cv"… Copying abstract model into "experiments-FORTE/scalability/FMS-2_Spec1_learning_2.imi"… …The end of Interfaçator! *-**--***---****---***--**-* Model generated by learning: counter-example *** Warning: The synclab 'O_B1_R1' is not used in (at least) the automaton 'AbstractERA' where it is declared: it will thus be removed from the whole model. *** Warning: The synclab 'B2_in' is not used in (at least) the automaton 'AbstractERA' where it is declared: it will thus be removed from the whole model. *** Warning: The synclab 'I_B2_C2' is not used in (at least) the automaton 'AbstractERA' where it is declared: it will thus be removed from the whole model. *** Warning: The synclab 'O_B2_R3' is not used in (at least) the automaton 'AbstractERA' where it is declared: it will thus be removed from the whole model. *** Warning: The synclab 'I_B3_R1' is not used in (at least) the automaton 'AbstractERA' where it is declared: it will thus be removed from the whole model. *** Warning: The synclab 'B3_in_M' is not used in (at least) the automaton 'AbstractERA' where it is declared: it will thus be removed from the whole model. *** Warning: The synclab 'I_B3_M' is not used in (at least) the automaton 'AbstractERA' where it is declared: it will thus be removed from the whole model. *** Warning: The synclab 'B2_out' is not used in (at least) the automaton 'AbstractERA' where it is declared: it will thus be removed from the whole model. *** 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 88.020 seconds. Memory for abstract model: 145776.164 KiB (i.e., 37318698 words) Original model: 11 automata. New model: 12 K2 computed by EFunsafe in 0.210 second: 96 states with 192 transitions explored. p_I_B1_C1 > 2 & p_B3_out_M >= 0 [BC (full coverage with learning-based abstraction)] Successfully terminated after 976.352 seconds. Final constraints such that the system is correct/incorrect: 2 >= p_I_B1_C1 & p_I_B1_C1 >= 0 & p_B3_out_M >= 0 p_I_B1_C1 > 2 & p_B3_out_M >= 0 The good constraint is exact (sound and complete). The bad constraint is exact (sound and complete). 240.177 GiB (i.e., 32236090223 words of size 8) Result written to file 'experiments-FORTE/scalability/FMS-2_Spec1.res'. ------------------------------------------------------------ Statistics: Algorithm counters ------------------------------------------------------------ main algorithm : 976.350 seconds find next point : 888.120 seconds (0 call) learning : 83.525 seconds (2 calls | 41.7626029254 second/call) learning: re-parsing : 0.010 second (2 calls | 0.00503098964692 second/call) abstractions learnt : 1 counter-examples learnt : 1 ------------------------------------------------------------ Statistics: Parsing counters ------------------------------------------------------------ model parsing : 0.004 second ------------------------------------------------------------ Statistics: State computation counters ------------------------------------------------------------ number of state comparisons : 33549 number of constraints comparisons : 7653 ------------------------------------------------------------ Statistics: Graphics-related counters ------------------------------------------------------------ state space drawing : 0.000 second ------------------------------------------------------------ Statistics: Global counter ------------------------------------------------------------ total : 976.351 seconds IMITATOR successfully terminated (after 976.353 seconds) Estimated memory used: 240.177 GiB (i.e., 32236106650 words of size 8) Done etienne@MakBook:~/Boulot/SVN/andre/papiers/2017/learning$