etienne@MakBook:~/Boulot/SVN/andre/papiers/2017/learning$ sh runexpsgrouping.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 08:46:16 Model: experiments-FORTE/grouping/FMS-1_Spec1-grouping1.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_B1_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_in_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_out_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B3_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_I_B3_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B3_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B1_out' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B1_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_in_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_out_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B5_in_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_I_B5_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B5_A' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B5_out_A' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_product' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. This model is an L/U-PTA: - lower-bound parameters {p_B3_out_M} - upper-bound parameters {p_I_B1_C1} Abstract model built after 0.006 second. Memory for abstract model: 916.011 KiB (i.e., 234499 words) [BC (full coverage with learning-based abstraction)] Starting running cartography… ************************************************** START THE BEHAVIORAL CARTOGRAPHY ALGORITHM ************************************************** Parametric rectangle V0: p_I_B1_C1 = 1..10 & p_B3_out_M = 1..10 Number of points inside V0: 100 ************************************************** ALGORITHM BC (full coverage 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/grouping/FMS-1_Spec1-grouping1.imi experiments-FORTE/grouping/FMS-1_Spec1-grouping1_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/grouping/FMS-1_Spec1-grouping1.cv"… Executing "/home/etienne/Boulot/SVN/andre/papiers/2017/learning/IMICV/bin/../CV/Compositional_Verifier -imi experiments-FORTE/grouping/FMS-1_Spec1-grouping1.cv"… Abstraction detected Moving learning result from "/home/etienne/Boulot/SVN/andre/papiers/2017/learning/IMICV/bin/../CV/tmp/assumption.imi" to "experiments-FORTE/grouping/FMS-1_Spec1-grouping1_learning_1.imi-output.cv"… Copying abstract model into "experiments-FORTE/grouping/FMS-1_Spec1-grouping1_learning_1.imi"… …The end of Interfaçator! *-**--***---****---***--**-* Model generated by learning: abstraction *** Warning: The clock 'clock_B1_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_in_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_out_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B3_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_I_B3_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B3_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B1_out' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B1_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_in_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_out_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B5_in_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_I_B5_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B5_A' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B5_out_A' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_product' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. This model is an L/U-PTA: - lower-bound parameters {p_B3_out_M} - upper-bound parameters {p_I_B1_C1} Abstract model built after 0.931 second. Memory for abstract model: 1690.324 KiB (i.e., 432723 words) Original model: 6 automata. New model: 4 K1 computed by PRP in 0.047 second: 39 states with 95 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/grouping/FMS-1_Spec1-grouping1.imi experiments-FORTE/grouping/FMS-1_Spec1-grouping1_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/grouping/FMS-1_Spec1-grouping1.cv"… Executing "/home/etienne/Boulot/SVN/andre/papiers/2017/learning/IMICV/bin/../CV/Compositional_Verifier -imi experiments-FORTE/grouping/FMS-1_Spec1-grouping1.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/grouping/FMS-1_Spec1-grouping1_learning_2.imi-output.cv"… Copying abstract model into "experiments-FORTE/grouping/FMS-1_Spec1-grouping1_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 '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 clock 'clock_B1_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_in_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_out_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B3_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_I_B3_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B3_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B1_out' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B1_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_in_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_out_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B5_in_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_I_B5_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B5_A' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B5_out_A' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_product' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. This model is an L/U-PTA: - lower-bound parameters {p_B3_out_M} - upper-bound parameters {p_I_B1_C1} Abstract model built after 1.137 seconds. Memory for abstract model: 3331.894 KiB (i.e., 852965 words) Original model: 6 automata. New model: 7 K2 computed by EFunsafe in 0.002 second: 4 states with 3 transitions explored. p_I_B1_C1 > 2 & p_B3_out_M >= 0 [BC (full coverage with learning-based abstraction)] Successfully terminated after 1.140 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). 6.918 MiB (i.e., 906847 words of size 8) Result written to file 'experiments-FORTE/grouping/FMS-1_Spec1-grouping1.res'. ------------------------------------------------------------ Statistics: Algorithm counters ------------------------------------------------------------ main algorithm : 1.137 seconds find next point : 0.000 second (0 call) learning : 1.071 seconds (2 calls | 0.535667419434 second/call) learning: re-parsing : 0.008 second (2 calls | 0.00449395179749 second/call) abstractions learnt : 1 counter-examples learnt : 1 ------------------------------------------------------------ Statistics: Parsing counters ------------------------------------------------------------ model parsing : 0.003 second ------------------------------------------------------------ Statistics: State computation counters ------------------------------------------------------------ number of state comparisons : 149 number of constraints comparisons : 93 ------------------------------------------------------------ Statistics: Graphics-related counters ------------------------------------------------------------ state space drawing : 0.000 second ------------------------------------------------------------ Statistics: Global counter ------------------------------------------------------------ total : 1.137 seconds IMITATOR successfully terminated (after 1.141 seconds) Estimated memory used: 7.043 MiB (i.e., 923251 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 08:46:17 Model: experiments-FORTE/grouping/FMS-1_Spec1-grouping2.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_B1_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_in_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_out_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B3_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_I_B3_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B3_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B1_out' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B1_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_in_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_out_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B5_in_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_I_B5_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B5_A' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B5_out_A' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_product' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. This model is an L/U-PTA: - lower-bound parameters {p_B3_out_M} - upper-bound parameters {p_I_B1_C1} Abstract model built after 0.007 second. Memory for abstract model: 916.011 KiB (i.e., 234499 words) [BC (full coverage with learning-based abstraction)] Starting running cartography… ************************************************** START THE BEHAVIORAL CARTOGRAPHY ALGORITHM ************************************************** Parametric rectangle V0: p_I_B1_C1 = 1..10 & p_B3_out_M = 1..10 Number of points inside V0: 100 ************************************************** ALGORITHM BC (full coverage 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/grouping/FMS-1_Spec1-grouping2.imi experiments-FORTE/grouping/FMS-1_Spec1-grouping2_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/grouping/FMS-1_Spec1-grouping2.cv"… Executing "/home/etienne/Boulot/SVN/andre/papiers/2017/learning/IMICV/bin/../CV/Compositional_Verifier -imi experiments-FORTE/grouping/FMS-1_Spec1-grouping2.cv"… Abstraction detected Moving learning result from "/home/etienne/Boulot/SVN/andre/papiers/2017/learning/IMICV/bin/../CV/tmp/assumption.imi" to "experiments-FORTE/grouping/FMS-1_Spec1-grouping2_learning_1.imi-output.cv"… Copying abstract model into "experiments-FORTE/grouping/FMS-1_Spec1-grouping2_learning_1.imi"… …The end of Interfaçator! *-**--***---****---***--**-* Model generated by learning: abstraction *** Warning: The clock 'clock_B1_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_in_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_out_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B3_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_I_B3_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B3_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B1_out' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B1_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_in_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_out_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B5_in_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_I_B5_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B5_A' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B5_out_A' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_product' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. This model is an L/U-PTA: - lower-bound parameters {p_B3_out_M} - upper-bound parameters {p_I_B1_C1} Abstract model built after 0.057 second. Memory for abstract model: 1318.453 KiB (i.e., 337524 words) Original model: 6 automata. New model: 5 K1 computed by PRP in 0.048 second: 43 states with 90 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/grouping/FMS-1_Spec1-grouping2.imi experiments-FORTE/grouping/FMS-1_Spec1-grouping2_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/grouping/FMS-1_Spec1-grouping2.cv"… Executing "/home/etienne/Boulot/SVN/andre/papiers/2017/learning/IMICV/bin/../CV/Compositional_Verifier -imi experiments-FORTE/grouping/FMS-1_Spec1-grouping2.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/grouping/FMS-1_Spec1-grouping2_learning_2.imi-output.cv"… Copying abstract model into "experiments-FORTE/grouping/FMS-1_Spec1-grouping2_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 '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 clock 'clock_B1_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_in_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_out_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B3_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_I_B3_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B3_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B1_out' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B1_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_in_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_out_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B5_in_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_I_B5_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B5_A' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B5_out_A' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_product' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. This model is an L/U-PTA: - lower-bound parameters {p_B3_out_M} - upper-bound parameters {p_I_B1_C1} Abstract model built after 0.145 second. Memory for abstract model: 2602.042 KiB (i.e., 666123 words) Original model: 6 automata. New model: 7 K2 computed by EFunsafe in 0.005 second: 4 states with 3 transitions explored. p_I_B1_C1 > 2 & p_B3_out_M >= 0 [BC (full coverage with learning-based abstraction)] Successfully terminated after 0.151 second. 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). 5.493 MiB (i.e., 720005 words of size 8) Result written to file 'experiments-FORTE/grouping/FMS-1_Spec1-grouping2.res'. ------------------------------------------------------------ Statistics: Algorithm counters ------------------------------------------------------------ main algorithm : 0.148 second find next point : 0.000 second (0 call) learning : 0.077 second (2 calls | 0.0386829376221 second/call) learning: re-parsing : 0.009 second (2 calls | 0.00478959083558 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 : 98 number of constraints comparisons : 63 ------------------------------------------------------------ Statistics: Graphics-related counters ------------------------------------------------------------ state space drawing : 0.000 second ------------------------------------------------------------ Statistics: Global counter ------------------------------------------------------------ total : 0.149 second IMITATOR successfully terminated (after 0.152 second) Estimated memory used: 5.618 MiB (i.e., 736391 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 08:46:17 Model: experiments-FORTE/grouping/FMS-1_Spec1-grouping3.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_B1_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_in_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_out_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B3_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_I_B3_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B3_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B1_out' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B1_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_in_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_out_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B5_in_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_I_B5_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B5_A' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B5_out_A' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_product' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. This model is an L/U-PTA: - lower-bound parameters {p_B3_out_M} - upper-bound parameters {p_I_B1_C1} Abstract model built after 0.008 second. Memory for abstract model: 916.058 KiB (i.e., 234511 words) [BC (full coverage with learning-based abstraction)] Starting running cartography… ************************************************** START THE BEHAVIORAL CARTOGRAPHY ALGORITHM ************************************************** Parametric rectangle V0: p_I_B1_C1 = 1..10 & p_B3_out_M = 1..10 Number of points inside V0: 100 ************************************************** ALGORITHM BC (full coverage 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/grouping/FMS-1_Spec1-grouping3.imi experiments-FORTE/grouping/FMS-1_Spec1-grouping3_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/grouping/FMS-1_Spec1-grouping3.cv"… Executing "/home/etienne/Boulot/SVN/andre/papiers/2017/learning/IMICV/bin/../CV/Compositional_Verifier -imi experiments-FORTE/grouping/FMS-1_Spec1-grouping3.cv"… Abstraction detected Moving learning result from "/home/etienne/Boulot/SVN/andre/papiers/2017/learning/IMICV/bin/../CV/tmp/assumption.imi" to "experiments-FORTE/grouping/FMS-1_Spec1-grouping3_learning_1.imi-output.cv"… Copying abstract model into "experiments-FORTE/grouping/FMS-1_Spec1-grouping3_learning_1.imi"… …The end of Interfaçator! *-**--***---****---***--**-* Model generated by learning: abstraction *** Warning: The clock 'clock_B1_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_in_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_out_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B3_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_I_B3_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B3_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B1_out' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B1_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_in_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_out_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B5_in_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_I_B5_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B5_A' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B5_out_A' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_product' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. This model is an L/U-PTA: - lower-bound parameters {p_B3_out_M} - upper-bound parameters {p_I_B1_C1} Abstract model built after 4.611 seconds. Memory for abstract model: 1821.199 KiB (i.e., 466227 words) Original model: 6 automata. New model: 5 K1 computed by PRP in 0.224 second: 138 states with 403 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/grouping/FMS-1_Spec1-grouping3.imi experiments-FORTE/grouping/FMS-1_Spec1-grouping3_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/grouping/FMS-1_Spec1-grouping3.cv"… Executing "/home/etienne/Boulot/SVN/andre/papiers/2017/learning/IMICV/bin/../CV/Compositional_Verifier -imi experiments-FORTE/grouping/FMS-1_Spec1-grouping3.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/grouping/FMS-1_Spec1-grouping3_learning_2.imi-output.cv"… Copying abstract model into "experiments-FORTE/grouping/FMS-1_Spec1-grouping3_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 '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 'O_B3_R2' 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_out_R2' 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_B1_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_in_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_out_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B3_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_I_B3_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B3_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B1_out' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B1_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_in_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_out_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B5_in_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_I_B5_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B5_A' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B5_out_A' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_product' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. This model is an L/U-PTA: - lower-bound parameters {p_B3_out_M} - upper-bound parameters {p_I_B1_C1} Abstract model built after 5.403 seconds. Memory for abstract model: 8182.761 KiB (i.e., 2094787 words) Original model: 6 automata. New model: 7 K2 computed by EFunsafe in 0.005 second: 4 states with 3 transitions explored. p_I_B1_C1 > 2 & p_B3_out_M >= 0 [BC (full coverage with learning-based abstraction)] Successfully terminated after 5.409 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). 16.392 MiB (i.e., 2148587 words of size 8) Result written to file 'experiments-FORTE/grouping/FMS-1_Spec1-grouping3.res'. ------------------------------------------------------------ Statistics: Algorithm counters ------------------------------------------------------------ main algorithm : 5.406 seconds find next point : 0.000 second (0 call) learning : 5.152 seconds (2 calls | 2.57645845414 second/call) learning: re-parsing : 0.013 second (2 calls | 0.00688338279725 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 : 1003 number of constraints comparisons : 408 ------------------------------------------------------------ Statistics: Graphics-related counters ------------------------------------------------------------ state space drawing : 0.000 second ------------------------------------------------------------ Statistics: Global counter ------------------------------------------------------------ total : 5.406 seconds IMITATOR successfully terminated (after 5.410 seconds) Estimated memory used: 16.517 MiB (i.e., 2164980 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 08:46:23 Model: experiments-FORTE/grouping/FMS-1_Spec1-grouping4.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_B1_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_in_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_out_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B3_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_I_B3_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B3_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B1_out' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B1_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_in_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_out_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B5_in_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_I_B5_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B5_A' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B5_out_A' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_product' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. This model is an L/U-PTA: - lower-bound parameters {p_B3_out_M} - upper-bound parameters {p_I_B1_C1} Abstract model built after 0.007 second. Memory for abstract model: 916.097 KiB (i.e., 234521 words) [BC (full coverage with learning-based abstraction)] Starting running cartography… ************************************************** START THE BEHAVIORAL CARTOGRAPHY ALGORITHM ************************************************** Parametric rectangle V0: p_I_B1_C1 = 1..10 & p_B3_out_M = 1..10 Number of points inside V0: 100 ************************************************** ALGORITHM BC (full coverage 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/grouping/FMS-1_Spec1-grouping4.imi experiments-FORTE/grouping/FMS-1_Spec1-grouping4_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/grouping/FMS-1_Spec1-grouping4.cv"… Executing "/home/etienne/Boulot/SVN/andre/papiers/2017/learning/IMICV/bin/../CV/Compositional_Verifier -imi experiments-FORTE/grouping/FMS-1_Spec1-grouping4.cv"… Abstraction detected Moving learning result from "/home/etienne/Boulot/SVN/andre/papiers/2017/learning/IMICV/bin/../CV/tmp/assumption.imi" to "experiments-FORTE/grouping/FMS-1_Spec1-grouping4_learning_1.imi-output.cv"… Copying abstract model into "experiments-FORTE/grouping/FMS-1_Spec1-grouping4_learning_1.imi"… …The end of Interfaçator! *-**--***---****---***--**-* Model generated by learning: abstraction *** Warning: The clock 'clock_B1_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_in_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_out_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B3_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_I_B3_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B3_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B1_out' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B1_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_in_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_out_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B5_in_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_I_B5_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B5_A' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B5_out_A' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_product' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. This model is an L/U-PTA: - lower-bound parameters {p_B3_out_M} - upper-bound parameters {p_I_B1_C1} Abstract model built after 4.989 seconds. Memory for abstract model: 2351.441 KiB (i.e., 601969 words) Original model: 6 automata. New model: 5 K1 computed by PRP in 0.286 second: 156 states with 536 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/grouping/FMS-1_Spec1-grouping4.imi experiments-FORTE/grouping/FMS-1_Spec1-grouping4_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/grouping/FMS-1_Spec1-grouping4.cv"… Executing "/home/etienne/Boulot/SVN/andre/papiers/2017/learning/IMICV/bin/../CV/Compositional_Verifier -imi experiments-FORTE/grouping/FMS-1_Spec1-grouping4.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/grouping/FMS-1_Spec1-grouping4_learning_2.imi-output.cv"… Copying abstract model into "experiments-FORTE/grouping/FMS-1_Spec1-grouping4_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 '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 'I_B5_R2' 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_B1_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_in_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_out_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B3_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_I_B3_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B3_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B1_out' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B1_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_in_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_out_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B5_in_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_I_B5_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B5_A' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B5_out_A' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_product' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. This model is an L/U-PTA: - lower-bound parameters {p_B3_out_M} - upper-bound parameters {p_I_B1_C1} Abstract model built after 5.975 seconds. Memory for abstract model: 10152.714 KiB (i.e., 2599095 words) Original model: 6 automata. New model: 7 K2 computed by EFunsafe in 0.007 second: 4 states with 3 transitions explored. p_I_B1_C1 > 2 & p_B3_out_M >= 0 [BC (full coverage with learning-based abstraction)] Successfully terminated after 5.983 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). 20.239 MiB (i.e., 2652828 words of size 8) Result written to file 'experiments-FORTE/grouping/FMS-1_Spec1-grouping4.res'. ------------------------------------------------------------ Statistics: Algorithm counters ------------------------------------------------------------ main algorithm : 5.980 seconds find next point : 0.000 second (0 call) learning : 5.663 seconds (2 calls | 2.83166396618 second/call) learning: re-parsing : 0.013 second (2 calls | 0.00660300254822 second/call) abstractions learnt : 1 counter-examples learnt : 1 ------------------------------------------------------------ Statistics: Parsing counters ------------------------------------------------------------ model parsing : 0.003 second ------------------------------------------------------------ Statistics: State computation counters ------------------------------------------------------------ number of state comparisons : 1297 number of constraints comparisons : 571 ------------------------------------------------------------ Statistics: Graphics-related counters ------------------------------------------------------------ state space drawing : 0.000 second ------------------------------------------------------------ Statistics: Global counter ------------------------------------------------------------ total : 5.980 seconds IMITATOR successfully terminated (after 5.984 seconds) Estimated memory used: 20.364 MiB (i.e., 2669221 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 08:46:29 Model: experiments-FORTE/grouping/FMS-1_Spec1-grouping5.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_B1_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_in_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_out_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B3_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_I_B3_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B3_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B1_out' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B1_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_in_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_out_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B5_in_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_I_B5_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B5_A' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B5_out_A' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_product' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. This model is an L/U-PTA: - lower-bound parameters {p_B3_out_M} - upper-bound parameters {p_I_B1_C1} Abstract model built after 0.006 second. Memory for abstract model: 916.031 KiB (i.e., 234504 words) [BC (full coverage with learning-based abstraction)] Starting running cartography… ************************************************** START THE BEHAVIORAL CARTOGRAPHY ALGORITHM ************************************************** Parametric rectangle V0: p_I_B1_C1 = 1..10 & p_B3_out_M = 1..10 Number of points inside V0: 100 ************************************************** ALGORITHM BC (full coverage 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/grouping/FMS-1_Spec1-grouping5.imi experiments-FORTE/grouping/FMS-1_Spec1-grouping5_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/grouping/FMS-1_Spec1-grouping5.cv"… Executing "/home/etienne/Boulot/SVN/andre/papiers/2017/learning/IMICV/bin/../CV/Compositional_Verifier -imi experiments-FORTE/grouping/FMS-1_Spec1-grouping5.cv"… Abstraction detected Moving learning result from "/home/etienne/Boulot/SVN/andre/papiers/2017/learning/IMICV/bin/../CV/tmp/assumption.imi" to "experiments-FORTE/grouping/FMS-1_Spec1-grouping5_learning_1.imi-output.cv"… Copying abstract model into "experiments-FORTE/grouping/FMS-1_Spec1-grouping5_learning_1.imi"… …The end of Interfaçator! *-**--***---****---***--**-* Model generated by learning: abstraction *** Warning: The clock 'clock_B1_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_in_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_out_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B3_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_I_B3_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B3_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B1_out' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B1_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_in_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_out_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B5_in_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_I_B5_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B5_A' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B5_out_A' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_product' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. This model is an L/U-PTA: - lower-bound parameters {p_B3_out_M} - upper-bound parameters {p_I_B1_C1} Abstract model built after 0.096 second. Memory for abstract model: 1360.910 KiB (i.e., 348393 words) Original model: 6 automata. New model: 6 K1 computed by PRP in 0.141 second: 146 states with 357 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/grouping/FMS-1_Spec1-grouping5.imi experiments-FORTE/grouping/FMS-1_Spec1-grouping5_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/grouping/FMS-1_Spec1-grouping5.cv"… Executing "/home/etienne/Boulot/SVN/andre/papiers/2017/learning/IMICV/bin/../CV/Compositional_Verifier -imi experiments-FORTE/grouping/FMS-1_Spec1-grouping5.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/grouping/FMS-1_Spec1-grouping5_learning_2.imi-output.cv"… Copying abstract model into "experiments-FORTE/grouping/FMS-1_Spec1-grouping5_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 '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 'O_B3_R2' 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_out_R2' 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_B1_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_in_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_out_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B3_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_I_B3_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B3_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B1_out' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B1_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_in_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_out_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B5_in_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_I_B5_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B5_A' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B5_out_A' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_product' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. This model is an L/U-PTA: - lower-bound parameters {p_B3_out_M} - upper-bound parameters {p_I_B1_C1} Abstract model built after 0.286 second. Memory for abstract model: 4856.554 KiB (i.e., 1243278 words) Original model: 6 automata. New model: 7 K2 computed by EFunsafe in 0.006 second: 4 states with 3 transitions explored. p_I_B1_C1 > 2 & p_B3_out_M >= 0 [BC (full coverage with learning-based abstraction)] Successfully terminated after 0.293 second. 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). 9.895 MiB (i.e., 1297034 words of size 8) Result written to file 'experiments-FORTE/grouping/FMS-1_Spec1-grouping5.res'. ------------------------------------------------------------ Statistics: Algorithm counters ------------------------------------------------------------ main algorithm : 0.290 second find next point : 0.000 second (0 call) learning : 0.123 second (2 calls | 0.061993598938 second/call) learning: re-parsing : 0.010 second (2 calls | 0.00504744052887 second/call) abstractions learnt : 1 counter-examples learnt : 1 ------------------------------------------------------------ Statistics: Parsing counters ------------------------------------------------------------ model parsing : 0.003 second ------------------------------------------------------------ Statistics: State computation counters ------------------------------------------------------------ number of state comparisons : 718 number of constraints comparisons : 262 ------------------------------------------------------------ Statistics: Graphics-related counters ------------------------------------------------------------ state space drawing : 0.000 second ------------------------------------------------------------ Statistics: Global counter ------------------------------------------------------------ total : 0.290 second IMITATOR successfully terminated (after 0.294 second) Estimated memory used: 10.020 MiB (i.e., 1313397 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 08:46:29 Model: experiments-FORTE/grouping/FMS-1_Spec1-grouping6.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_B1_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_in_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_out_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B3_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_I_B3_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B3_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B1_out' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B1_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_in_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_out_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B5_in_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_I_B5_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B5_A' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B5_out_A' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_product' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. This model is an L/U-PTA: - lower-bound parameters {p_B3_out_M} - upper-bound parameters {p_I_B1_C1} Abstract model built after 0.006 second. Memory for abstract model: 916.050 KiB (i.e., 234509 words) [BC (full coverage with learning-based abstraction)] Starting running cartography… ************************************************** START THE BEHAVIORAL CARTOGRAPHY ALGORITHM ************************************************** Parametric rectangle V0: p_I_B1_C1 = 1..10 & p_B3_out_M = 1..10 Number of points inside V0: 100 ************************************************** ALGORITHM BC (full coverage 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/grouping/FMS-1_Spec1-grouping6.imi experiments-FORTE/grouping/FMS-1_Spec1-grouping6_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/grouping/FMS-1_Spec1-grouping6.cv"… Executing "/home/etienne/Boulot/SVN/andre/papiers/2017/learning/IMICV/bin/../CV/Compositional_Verifier -imi experiments-FORTE/grouping/FMS-1_Spec1-grouping6.cv"… Abstraction detected Moving learning result from "/home/etienne/Boulot/SVN/andre/papiers/2017/learning/IMICV/bin/../CV/tmp/assumption.imi" to "experiments-FORTE/grouping/FMS-1_Spec1-grouping6_learning_1.imi-output.cv"… Copying abstract model into "experiments-FORTE/grouping/FMS-1_Spec1-grouping6_learning_1.imi"… …The end of Interfaçator! *-**--***---****---***--**-* Model generated by learning: abstraction *** Warning: The clock 'clock_B1_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_in_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_out_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B3_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_I_B3_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B3_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B1_out' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B1_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_in_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_out_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B5_in_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_I_B5_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B5_A' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B5_out_A' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_product' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. This model is an L/U-PTA: - lower-bound parameters {p_B3_out_M} - upper-bound parameters {p_I_B1_C1} Abstract model built after 0.087 second. Memory for abstract model: 1356.792 KiB (i.e., 347339 words) Original model: 6 automata. New model: 6 K1 computed by PRP in 0.213 second: 172 states with 532 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/grouping/FMS-1_Spec1-grouping6.imi experiments-FORTE/grouping/FMS-1_Spec1-grouping6_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/grouping/FMS-1_Spec1-grouping6.cv"… Executing "/home/etienne/Boulot/SVN/andre/papiers/2017/learning/IMICV/bin/../CV/Compositional_Verifier -imi experiments-FORTE/grouping/FMS-1_Spec1-grouping6.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/grouping/FMS-1_Spec1-grouping6_learning_2.imi-output.cv"… Copying abstract model into "experiments-FORTE/grouping/FMS-1_Spec1-grouping6_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 '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 'I_B5_R2' 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_B1_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_in_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_out_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B3_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_I_B3_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B3_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B1_out' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B1_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_in_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_out_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B5_in_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_I_B5_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B5_A' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B5_out_A' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_product' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. This model is an L/U-PTA: - lower-bound parameters {p_B3_out_M} - upper-bound parameters {p_I_B1_C1} Abstract model built after 0.357 second. Memory for abstract model: 6136.691 KiB (i.e., 1570993 words) Original model: 6 automata. New model: 7 K2 computed by EFunsafe in 0.005 second: 4 states with 3 transitions explored. p_I_B1_C1 > 2 & p_B3_out_M >= 0 [BC (full coverage with learning-based abstraction)] Successfully terminated after 0.364 second. 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). 12.395 MiB (i.e., 1624673 words of size 8) Result written to file 'experiments-FORTE/grouping/FMS-1_Spec1-grouping6.res'. ------------------------------------------------------------ Statistics: Algorithm counters ------------------------------------------------------------ main algorithm : 0.360 second find next point : 0.000 second (0 call) learning : 0.119 second (2 calls | 0.0598545074463 second/call) learning: re-parsing : 0.010 second (2 calls | 0.00501084327698 second/call) abstractions learnt : 1 counter-examples learnt : 1 ------------------------------------------------------------ Statistics: Parsing counters ------------------------------------------------------------ model parsing : 0.003 second ------------------------------------------------------------ Statistics: State computation counters ------------------------------------------------------------ number of state comparisons : 1074 number of constraints comparisons : 421 ------------------------------------------------------------ Statistics: Graphics-related counters ------------------------------------------------------------ state space drawing : 0.000 second ------------------------------------------------------------ Statistics: Global counter ------------------------------------------------------------ total : 0.361 second IMITATOR successfully terminated (after 0.365 second) Estimated memory used: 12.520 MiB (i.e., 1641056 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 08:46:29 Model: experiments-FORTE/grouping/FMS-1_Spec1-grouping7.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_B1_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_in_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_out_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B3_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_I_B3_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B3_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B1_out' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B1_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_in_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_out_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B5_in_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_I_B5_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B5_A' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B5_out_A' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_product' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. This model is an L/U-PTA: - lower-bound parameters {p_B3_out_M} - upper-bound parameters {p_I_B1_C1} Abstract model built after 0.008 second. Memory for abstract model: 916.117 KiB (i.e., 234526 words) [BC (full coverage with learning-based abstraction)] Starting running cartography… ************************************************** START THE BEHAVIORAL CARTOGRAPHY ALGORITHM ************************************************** Parametric rectangle V0: p_I_B1_C1 = 1..10 & p_B3_out_M = 1..10 Number of points inside V0: 100 ************************************************** ALGORITHM BC (full coverage 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/grouping/FMS-1_Spec1-grouping7.imi experiments-FORTE/grouping/FMS-1_Spec1-grouping7_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/grouping/FMS-1_Spec1-grouping7.cv"… Executing "/home/etienne/Boulot/SVN/andre/papiers/2017/learning/IMICV/bin/../CV/Compositional_Verifier -imi experiments-FORTE/grouping/FMS-1_Spec1-grouping7.cv"… Abstraction detected Moving learning result from "/home/etienne/Boulot/SVN/andre/papiers/2017/learning/IMICV/bin/../CV/tmp/assumption.imi" to "experiments-FORTE/grouping/FMS-1_Spec1-grouping7_learning_1.imi-output.cv"… Copying abstract model into "experiments-FORTE/grouping/FMS-1_Spec1-grouping7_learning_1.imi"… …The end of Interfaçator! *-**--***---****---***--**-* Model generated by learning: abstraction *** Warning: The clock 'clock_B1_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_in_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_out_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B3_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_I_B3_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B3_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B1_out' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B1_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_in_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_out_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B5_in_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_I_B5_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B5_A' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B5_out_A' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_product' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. This model is an L/U-PTA: - lower-bound parameters {p_B3_out_M} - upper-bound parameters {p_I_B1_C1} Abstract model built after 4.996 seconds. Memory for abstract model: 1519.703 KiB (i.e., 389044 words) Original model: 6 automata. New model: 6 K1 computed by PRP in 0.501 second: 276 states with 884 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/grouping/FMS-1_Spec1-grouping7.imi experiments-FORTE/grouping/FMS-1_Spec1-grouping7_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/grouping/FMS-1_Spec1-grouping7.cv"… Executing "/home/etienne/Boulot/SVN/andre/papiers/2017/learning/IMICV/bin/../CV/Compositional_Verifier -imi experiments-FORTE/grouping/FMS-1_Spec1-grouping7.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/grouping/FMS-1_Spec1-grouping7_learning_2.imi-output.cv"… Copying abstract model into "experiments-FORTE/grouping/FMS-1_Spec1-grouping7_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 '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 'O_B3_R2' 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_out_R2' 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_B5_R2' 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_B1_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_in_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_out_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B3_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_I_B3_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B3_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B1_out' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B1_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_in_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_out_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B5_in_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_I_B5_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B5_A' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B5_out_A' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_product' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. This model is an L/U-PTA: - lower-bound parameters {p_B3_out_M} - upper-bound parameters {p_I_B1_C1} Abstract model built after 6.678 seconds. Memory for abstract model: 16910.312 KiB (i.e., 4329040 words) Original model: 6 automata. New model: 7 K2 computed by EFunsafe in 0.013 second: 4 states with 3 transitions explored. p_I_B1_C1 > 2 & p_B3_out_M >= 0 [BC (full coverage with learning-based abstraction)] Successfully terminated after 6.693 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). 33.436 MiB (i.e., 4382586 words of size 8) Result written to file 'experiments-FORTE/grouping/FMS-1_Spec1-grouping7.res'. ------------------------------------------------------------ Statistics: Algorithm counters ------------------------------------------------------------ main algorithm : 6.690 seconds find next point : 0.000 second (0 call) learning : 6.150 seconds (2 calls | 3.07506990433 second/call) learning: re-parsing : 0.013 second (2 calls | 0.00694596767426 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 : 2448 number of constraints comparisons : 913 ------------------------------------------------------------ Statistics: Graphics-related counters ------------------------------------------------------------ state space drawing : 0.000 second ------------------------------------------------------------ Statistics: Global counter ------------------------------------------------------------ total : 6.690 seconds IMITATOR successfully terminated (after 6.694 seconds) Estimated memory used: 33.561 MiB (i.e., 4398979 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 08:46:36 Model: experiments-FORTE/grouping/FMS-1_Spec3-grouping1.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_B1_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_in_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_out_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B3_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_I_B3_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B3_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B1_out' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B1_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_in_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_out_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B5_in_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_I_B5_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B5_A' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B5_out_A' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_product' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. This model is an L/U-PTA: - lower-bound parameters {p_B3_out_M} - upper-bound parameters {p_I_B1_C1} Abstract model built after 0.007 second. Memory for abstract model: 900.015 KiB (i.e., 230404 words) [BC (full coverage with learning-based abstraction)] Starting running cartography… ************************************************** START THE BEHAVIORAL CARTOGRAPHY ALGORITHM ************************************************** Parametric rectangle V0: p_I_B1_C1 = 1..10 & p_B3_out_M = 1..10 Number of points inside V0: 100 ************************************************** ALGORITHM BC (full coverage 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/grouping/FMS-1_Spec3-grouping1.imi experiments-FORTE/grouping/FMS-1_Spec3-grouping1_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/grouping/FMS-1_Spec3-grouping1.cv"… Executing "/home/etienne/Boulot/SVN/andre/papiers/2017/learning/IMICV/bin/../CV/Compositional_Verifier -imi experiments-FORTE/grouping/FMS-1_Spec3-grouping1.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/grouping/FMS-1_Spec3-grouping1_learning_1.imi-output.cv"… Copying abstract model into "experiments-FORTE/grouping/FMS-1_Spec3-grouping1_learning_1.imi"… …The end of Interfaçator! *-**--***---****---***--**-* Model generated by learning: counter-example *** Warning: The synclab 'B1_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_B1_C1' 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 'O_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 clock 'clock_B1_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_in_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_out_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B3_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_I_B3_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B3_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B1_out' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B1_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_in_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_out_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B5_in_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_I_B5_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B5_A' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B5_out_A' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_product' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. This model is an L-PTA. Abstract model built after 0.148 second. Memory for abstract model: 1361.976 KiB (i.e., 348666 words) Original model: 6 automata. New model: 7 K1 computed by EFunsafe in 0.003 second: 3 states with 2 transitions explored. p_B3_out_M >= 0 & p_I_B1_C1 >= 0 [BC (full coverage with learning-based abstraction)] Successfully terminated after 0.152 second. Final constraints such that the system is correct/incorrect: False p_B3_out_M >= 0 & p_I_B1_C1 >= 0 The good constraint is exact (sound and complete). The bad constraint is exact (sound and complete). 2.971 MiB (i.e., 389489 words of size 8) Result written to file 'experiments-FORTE/grouping/FMS-1_Spec3-grouping1.res'. ------------------------------------------------------------ Statistics: Algorithm counters ------------------------------------------------------------ main algorithm : 0.149 second find next point : 0.000 second (0 call) learning : 0.133 second (1 call | 0.133157968522 second/call) learning: re-parsing : 0.006 second (1 call | 0.0063819885254 second/call) abstractions learnt : 0 counter-examples learnt : 1 ------------------------------------------------------------ Statistics: Parsing counters ------------------------------------------------------------ model parsing : 0.004 second ------------------------------------------------------------ Statistics: State computation counters ------------------------------------------------------------ number of state comparisons : 0 number of constraints comparisons : 0 ------------------------------------------------------------ Statistics: Graphics-related counters ------------------------------------------------------------ state space drawing : 0.000 second ------------------------------------------------------------ Statistics: Global counter ------------------------------------------------------------ total : 0.149 second IMITATOR successfully terminated (after 0.152 second) Estimated memory used: 3.093 MiB (i.e., 405482 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 08:46:36 Model: experiments-FORTE/grouping/FMS-1_Spec3-grouping2.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_B1_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_in_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_out_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B3_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_I_B3_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B3_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B1_out' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B1_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_in_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_out_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B5_in_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_I_B5_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B5_A' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B5_out_A' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_product' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. This model is an L/U-PTA: - lower-bound parameters {p_B3_out_M} - upper-bound parameters {p_I_B1_C1} Abstract model built after 0.006 second. Memory for abstract model: 900.066 KiB (i.e., 230417 words) [BC (full coverage with learning-based abstraction)] Starting running cartography… ************************************************** START THE BEHAVIORAL CARTOGRAPHY ALGORITHM ************************************************** Parametric rectangle V0: p_I_B1_C1 = 1..10 & p_B3_out_M = 1..10 Number of points inside V0: 100 ************************************************** ALGORITHM BC (full coverage 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/grouping/FMS-1_Spec3-grouping2.imi experiments-FORTE/grouping/FMS-1_Spec3-grouping2_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/grouping/FMS-1_Spec3-grouping2.cv"… Executing "/home/etienne/Boulot/SVN/andre/papiers/2017/learning/IMICV/bin/../CV/Compositional_Verifier -imi experiments-FORTE/grouping/FMS-1_Spec3-grouping2.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/grouping/FMS-1_Spec3-grouping2_learning_1.imi-output.cv"… Copying abstract model into "experiments-FORTE/grouping/FMS-1_Spec3-grouping2_learning_1.imi"… …The end of Interfaçator! *-**--***---****---***--**-* Model generated by learning: counter-example *** 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 clock 'clock_B1_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_in_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_out_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B3_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_I_B3_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B3_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B1_out' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B1_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_in_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_out_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B5_in_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_I_B5_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B5_A' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B5_out_A' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_product' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. This model is an L/U-PTA: - lower-bound parameters {p_B3_out_M} - upper-bound parameters {p_I_B1_C1} Abstract model built after 0.049 second. Memory for abstract model: 1485.308 KiB (i.e., 380239 words) Original model: 6 automata. New model: 7 K1 computed by EFunsafe in 0.014 second: 17 states with 16 transitions explored. 1 >= p_B3_out_M & p_B3_out_M >= 0 & p_I_B1_C1 >= 1 ************************************************** ALGORITHM BC (full coverage with learning-based abstraction): iteration 2 Considering the following pi2 p_I_B1_C1 = 1 & p_B3_out_M = 2 Executing: 'python /home/etienne/Boulot/SVN/andre/papiers/2017/learning/IMICV/bin/../interfaceCV.py experiments-FORTE/grouping/FMS-1_Spec3-grouping2.imi experiments-FORTE/grouping/FMS-1_Spec3-grouping2_learning_2.imi p_I_B1_C1=1,p_B3_out_M=2' *-**--***---****---***--**-* Hello, this is Interfaçator! Building reference valuation… Pi0: v(p_I_B1_C1) = 1 v(p_B3_out_M) = 2 Valuating component A with pi0… Writing content to "experiments-FORTE/grouping/FMS-1_Spec3-grouping2.cv"… Executing "/home/etienne/Boulot/SVN/andre/papiers/2017/learning/IMICV/bin/../CV/Compositional_Verifier -imi experiments-FORTE/grouping/FMS-1_Spec3-grouping2.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/grouping/FMS-1_Spec3-grouping2_learning_2.imi-output.cv"… Copying abstract model into "experiments-FORTE/grouping/FMS-1_Spec3-grouping2_learning_2.imi"… …The end of Interfaçator! *-**--***---****---***--**-* Model generated by learning: counter-example *** 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 clock 'clock_B1_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_in_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_out_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B3_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_I_B3_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B3_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B1_out' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B1_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_in_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_out_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B5_in_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_I_B5_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B5_A' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B5_out_A' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_product' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. This model is an L/U-PTA: - lower-bound parameters {p_B3_out_M} - upper-bound parameters {p_I_B1_C1} Abstract model built after 0.112 second. Memory for abstract model: 2239.273 KiB (i.e., 573254 words) Original model: 6 automata. New model: 7 K2 computed by EFunsafe in 0.013 second: 17 states with 16 transitions explored. p_B3_out_M >= 0 & p_I_B1_C1 >= 0 [BC (full coverage with learning-based abstraction)] Successfully terminated after 0.126 second. Final constraints such that the system is correct/incorrect: False p_B3_out_M >= 0 & p_I_B1_C1 >= 0 The good constraint is exact (sound and complete). The bad constraint is exact (sound and complete). 4.923 MiB (i.e., 645368 words of size 8) Result written to file 'experiments-FORTE/grouping/FMS-1_Spec3-grouping2.res'. ------------------------------------------------------------ Statistics: Algorithm counters ------------------------------------------------------------ main algorithm : 0.123 second find next point : 0.000 second (0 call) learning : 0.077 second (2 calls | 0.0385154485703 second/call) learning: re-parsing : 0.012 second (2 calls | 0.00613844394684 second/call) abstractions learnt : 0 counter-examples learnt : 2 ------------------------------------------------------------ Statistics: Parsing counters ------------------------------------------------------------ model parsing : 0.003 second ------------------------------------------------------------ Statistics: State computation counters ------------------------------------------------------------ number of state comparisons : 2 number of constraints comparisons : 0 ------------------------------------------------------------ Statistics: Graphics-related counters ------------------------------------------------------------ state space drawing : 0.000 second ------------------------------------------------------------ Statistics: Global counter ------------------------------------------------------------ total : 0.123 second IMITATOR successfully terminated (after 0.126 second) Estimated memory used: 5.046 MiB (i.e., 661426 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 08:46:36 Model: experiments-FORTE/grouping/FMS-1_Spec3-grouping3.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_B1_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_in_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_out_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B3_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_I_B3_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B3_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B1_out' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B1_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_in_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_out_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B5_in_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_I_B5_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B5_A' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B5_out_A' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_product' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. This model is an L/U-PTA: - lower-bound parameters {p_B3_out_M} - upper-bound parameters {p_I_B1_C1} Abstract model built after 0.006 second. Memory for abstract model: 900.062 KiB (i.e., 230416 words) [BC (full coverage with learning-based abstraction)] Starting running cartography… ************************************************** START THE BEHAVIORAL CARTOGRAPHY ALGORITHM ************************************************** Parametric rectangle V0: p_I_B1_C1 = 1..10 & p_B3_out_M = 1..10 Number of points inside V0: 100 ************************************************** ALGORITHM BC (full coverage 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/grouping/FMS-1_Spec3-grouping3.imi experiments-FORTE/grouping/FMS-1_Spec3-grouping3_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/grouping/FMS-1_Spec3-grouping3.cv"… Executing "/home/etienne/Boulot/SVN/andre/papiers/2017/learning/IMICV/bin/../CV/Compositional_Verifier -imi experiments-FORTE/grouping/FMS-1_Spec3-grouping3.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/grouping/FMS-1_Spec3-grouping3_learning_1.imi-output.cv"… Copying abstract model into "experiments-FORTE/grouping/FMS-1_Spec3-grouping3_learning_1.imi"… …The end of Interfaçator! *-**--***---****---***--**-* Model generated by learning: counter-example *** Warning: The synclab 'B1_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_B1_C1' 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 'O_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 clock 'clock_B1_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_in_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_out_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B3_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_I_B3_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B3_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B1_out' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B1_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_in_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_out_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B5_in_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_I_B5_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B5_A' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B5_out_A' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_product' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. This model is an L-PTA. Abstract model built after 0.056 second. Memory for abstract model: 1362.089 KiB (i.e., 348695 words) Original model: 6 automata. New model: 7 K1 computed by EFunsafe in 0.002 second: 3 states with 2 transitions explored. p_B3_out_M >= 0 & p_I_B1_C1 >= 0 [BC (full coverage with learning-based abstraction)] Successfully terminated after 0.059 second. Final constraints such that the system is correct/incorrect: False p_B3_out_M >= 0 & p_I_B1_C1 >= 0 The good constraint is exact (sound and complete). The bad constraint is exact (sound and complete). 2.971 MiB (i.e., 389533 words of size 8) Result written to file 'experiments-FORTE/grouping/FMS-1_Spec3-grouping3.res'. ------------------------------------------------------------ Statistics: Algorithm counters ------------------------------------------------------------ main algorithm : 0.056 second find next point : 0.000 second (0 call) learning : 0.040 second (1 call | 0.0400061607361 second/call) learning: re-parsing : 0.007 second (1 call | 0.00740098953248 second/call) abstractions learnt : 0 counter-examples learnt : 1 ------------------------------------------------------------ Statistics: Parsing counters ------------------------------------------------------------ model parsing : 0.004 second ------------------------------------------------------------ Statistics: State computation counters ------------------------------------------------------------ number of state comparisons : 0 number of constraints comparisons : 0 ------------------------------------------------------------ Statistics: Graphics-related counters ------------------------------------------------------------ state space drawing : 0.000 second ------------------------------------------------------------ Statistics: Global counter ------------------------------------------------------------ total : 0.057 second IMITATOR successfully terminated (after 0.060 second) Estimated memory used: 3.094 MiB (i.e., 405571 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 08:46:37 Model: experiments-FORTE/grouping/FMS-1_Spec3-grouping4.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_B1_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_in_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_out_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B3_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_I_B3_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B3_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B1_out' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B1_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_in_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_out_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B5_in_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_I_B5_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B5_A' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B5_out_A' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_product' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. This model is an L/U-PTA: - lower-bound parameters {p_B3_out_M} - upper-bound parameters {p_I_B1_C1} Abstract model built after 0.007 second. Memory for abstract model: 900.101 KiB (i.e., 230426 words) [BC (full coverage with learning-based abstraction)] Starting running cartography… ************************************************** START THE BEHAVIORAL CARTOGRAPHY ALGORITHM ************************************************** Parametric rectangle V0: p_I_B1_C1 = 1..10 & p_B3_out_M = 1..10 Number of points inside V0: 100 ************************************************** ALGORITHM BC (full coverage 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/grouping/FMS-1_Spec3-grouping4.imi experiments-FORTE/grouping/FMS-1_Spec3-grouping4_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/grouping/FMS-1_Spec3-grouping4.cv"… Executing "/home/etienne/Boulot/SVN/andre/papiers/2017/learning/IMICV/bin/../CV/Compositional_Verifier -imi experiments-FORTE/grouping/FMS-1_Spec3-grouping4.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/grouping/FMS-1_Spec3-grouping4_learning_1.imi-output.cv"… Copying abstract model into "experiments-FORTE/grouping/FMS-1_Spec3-grouping4_learning_1.imi"… …The end of Interfaçator! *-**--***---****---***--**-* Model generated by learning: counter-example *** Warning: The synclab 'B1_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_B1_C1' 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 'O_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 'I_B5_R2' 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_B1_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_in_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_out_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B3_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_I_B3_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B3_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B1_out' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B1_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_in_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_out_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B5_in_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_I_B5_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B5_A' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B5_out_A' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_product' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. This model is an L-PTA. Abstract model built after 0.839 second. Memory for abstract model: 1362.789 KiB (i.e., 348874 words) Original model: 6 automata. New model: 7 K1 computed by EFunsafe in 0.003 second: 3 states with 2 transitions explored. p_B3_out_M >= 0 & p_I_B1_C1 >= 0 [BC (full coverage with learning-based abstraction)] Successfully terminated after 0.844 second. Final constraints such that the system is correct/incorrect: False p_B3_out_M >= 0 & p_I_B1_C1 >= 0 The good constraint is exact (sound and complete). The bad constraint is exact (sound and complete). 2.972 MiB (i.e., 389605 words of size 8) Result written to file 'experiments-FORTE/grouping/FMS-1_Spec3-grouping4.res'. ------------------------------------------------------------ Statistics: Algorithm counters ------------------------------------------------------------ main algorithm : 0.842 second find next point : 0.001 second (0 call) learning : 0.824 second (1 call | 0.82482290268 second/call) learning: re-parsing : 0.006 second (1 call | 0.00613403320313 second/call) abstractions learnt : 0 counter-examples learnt : 1 ------------------------------------------------------------ Statistics: Parsing counters ------------------------------------------------------------ model parsing : 0.004 second ------------------------------------------------------------ Statistics: State computation counters ------------------------------------------------------------ number of state comparisons : 0 number of constraints comparisons : 0 ------------------------------------------------------------ Statistics: Graphics-related counters ------------------------------------------------------------ state space drawing : 0.000 second ------------------------------------------------------------ Statistics: Global counter ------------------------------------------------------------ total : 0.842 second IMITATOR successfully terminated (after 0.845 second) Estimated memory used: 3.094 MiB (i.e., 405606 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 08:46:37 Model: experiments-FORTE/grouping/FMS-1_Spec3-grouping5.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_B1_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_in_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_out_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B3_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_I_B3_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B3_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B1_out' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B1_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_in_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_out_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B5_in_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_I_B5_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B5_A' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B5_out_A' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_product' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. This model is an L/U-PTA: - lower-bound parameters {p_B3_out_M} - upper-bound parameters {p_I_B1_C1} Abstract model built after 0.006 second. Memory for abstract model: 900.035 KiB (i.e., 230409 words) [BC (full coverage with learning-based abstraction)] Starting running cartography… ************************************************** START THE BEHAVIORAL CARTOGRAPHY ALGORITHM ************************************************** Parametric rectangle V0: p_I_B1_C1 = 1..10 & p_B3_out_M = 1..10 Number of points inside V0: 100 ************************************************** ALGORITHM BC (full coverage 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/grouping/FMS-1_Spec3-grouping5.imi experiments-FORTE/grouping/FMS-1_Spec3-grouping5_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/grouping/FMS-1_Spec3-grouping5.cv"… Executing "/home/etienne/Boulot/SVN/andre/papiers/2017/learning/IMICV/bin/../CV/Compositional_Verifier -imi experiments-FORTE/grouping/FMS-1_Spec3-grouping5.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/grouping/FMS-1_Spec3-grouping5_learning_1.imi-output.cv"… Copying abstract model into "experiments-FORTE/grouping/FMS-1_Spec3-grouping5_learning_1.imi"… …The end of Interfaçator! *-**--***---****---***--**-* Model generated by learning: counter-example *** Warning: The synclab 'B1_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_B1_C1' 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_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 '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 'O_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 'B1_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_B1_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_in_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_out_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B3_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_I_B3_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B3_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B1_out' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B1_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_in_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_out_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B5_in_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_I_B5_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B5_A' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B5_out_A' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_product' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. This model is an L-PTA. Abstract model built after 0.044 second. Memory for abstract model: 1362.882 KiB (i.e., 348898 words) Original model: 6 automata. New model: 7 K1 computed by EFunsafe in 0.001 second: 3 states with 2 transitions explored. p_B3_out_M >= 0 & p_I_B1_C1 >= 0 [BC (full coverage with learning-based abstraction)] Successfully terminated after 0.047 second. Final constraints such that the system is correct/incorrect: False p_B3_out_M >= 0 & p_I_B1_C1 >= 0 The good constraint is exact (sound and complete). The bad constraint is exact (sound and complete). 2.972 MiB (i.e., 389658 words of size 8) Result written to file 'experiments-FORTE/grouping/FMS-1_Spec3-grouping5.res'. ------------------------------------------------------------ Statistics: Algorithm counters ------------------------------------------------------------ main algorithm : 0.044 second find next point : 0.000 second (0 call) learning : 0.034 second (1 call | 0.0342741012574 second/call) learning: re-parsing : 0.003 second (1 call | 0.0033609867096 second/call) abstractions learnt : 0 counter-examples learnt : 1 ------------------------------------------------------------ Statistics: Parsing counters ------------------------------------------------------------ model parsing : 0.002 second ------------------------------------------------------------ Statistics: State computation counters ------------------------------------------------------------ number of state comparisons : 0 number of constraints comparisons : 0 ------------------------------------------------------------ Statistics: Graphics-related counters ------------------------------------------------------------ state space drawing : 0.000 second ------------------------------------------------------------ Statistics: Global counter ------------------------------------------------------------ total : 0.044 second IMITATOR successfully terminated (after 0.047 second) Estimated memory used: 3.095 MiB (i.e., 405683 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 08:46:37 Model: experiments-FORTE/grouping/FMS-1_Spec3-grouping6.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_B1_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_in_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_out_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B3_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_I_B3_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B3_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B1_out' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B1_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_in_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_out_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B5_in_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_I_B5_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B5_A' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B5_out_A' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_product' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. This model is an L/U-PTA: - lower-bound parameters {p_B3_out_M} - upper-bound parameters {p_I_B1_C1} Abstract model built after 0.008 second. Memory for abstract model: 900.054 KiB (i.e., 230414 words) [BC (full coverage with learning-based abstraction)] Starting running cartography… ************************************************** START THE BEHAVIORAL CARTOGRAPHY ALGORITHM ************************************************** Parametric rectangle V0: p_I_B1_C1 = 1..10 & p_B3_out_M = 1..10 Number of points inside V0: 100 ************************************************** ALGORITHM BC (full coverage 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/grouping/FMS-1_Spec3-grouping6.imi experiments-FORTE/grouping/FMS-1_Spec3-grouping6_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/grouping/FMS-1_Spec3-grouping6.cv"… Executing "/home/etienne/Boulot/SVN/andre/papiers/2017/learning/IMICV/bin/../CV/Compositional_Verifier -imi experiments-FORTE/grouping/FMS-1_Spec3-grouping6.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/grouping/FMS-1_Spec3-grouping6_learning_1.imi-output.cv"… Copying abstract model into "experiments-FORTE/grouping/FMS-1_Spec3-grouping6_learning_1.imi"… …The end of Interfaçator! *-**--***---****---***--**-* Model generated by learning: counter-example *** 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 'I_B5_R2' 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_B1_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_in_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_out_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B3_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_I_B3_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B3_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B1_out' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B1_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_in_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_out_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B5_in_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_I_B5_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B5_A' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B5_out_A' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_product' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. This model is an L/U-PTA: - lower-bound parameters {p_B3_out_M} - upper-bound parameters {p_I_B1_C1} Abstract model built after 0.064 second. Memory for abstract model: 1486.472 KiB (i.e., 380537 words) Original model: 6 automata. New model: 7 K1 computed by EFunsafe in 0.013 second: 17 states with 16 transitions explored. 1 >= p_B3_out_M & p_B3_out_M >= 0 & p_I_B1_C1 >= 1 ************************************************** ALGORITHM BC (full coverage with learning-based abstraction): iteration 2 Considering the following pi2 p_I_B1_C1 = 1 & p_B3_out_M = 2 Executing: 'python /home/etienne/Boulot/SVN/andre/papiers/2017/learning/IMICV/bin/../interfaceCV.py experiments-FORTE/grouping/FMS-1_Spec3-grouping6.imi experiments-FORTE/grouping/FMS-1_Spec3-grouping6_learning_2.imi p_I_B1_C1=1,p_B3_out_M=2' *-**--***---****---***--**-* Hello, this is Interfaçator! Building reference valuation… Pi0: v(p_I_B1_C1) = 1 v(p_B3_out_M) = 2 Valuating component A with pi0… Writing content to "experiments-FORTE/grouping/FMS-1_Spec3-grouping6.cv"… Executing "/home/etienne/Boulot/SVN/andre/papiers/2017/learning/IMICV/bin/../CV/Compositional_Verifier -imi experiments-FORTE/grouping/FMS-1_Spec3-grouping6.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/grouping/FMS-1_Spec3-grouping6_learning_2.imi-output.cv"… Copying abstract model into "experiments-FORTE/grouping/FMS-1_Spec3-grouping6_learning_2.imi"… …The end of Interfaçator! *-**--***---****---***--**-* Model generated by learning: counter-example *** 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 'I_B5_R2' 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_B1_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_in_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_out_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B3_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_I_B3_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B3_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B1_out' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B1_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_in_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_out_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B5_in_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_I_B5_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B5_A' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B5_out_A' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_product' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. This model is an L/U-PTA: - lower-bound parameters {p_B3_out_M} - upper-bound parameters {p_I_B1_C1} Abstract model built after 0.130 second. Memory for abstract model: 2238.355 KiB (i.e., 573019 words) Original model: 6 automata. New model: 7 K2 computed by EFunsafe in 0.017 second: 17 states with 16 transitions explored. p_B3_out_M >= 0 & p_I_B1_C1 >= 0 [BC (full coverage with learning-based abstraction)] Successfully terminated after 0.148 second. Final constraints such that the system is correct/incorrect: False p_B3_out_M >= 0 & p_I_B1_C1 >= 0 The good constraint is exact (sound and complete). The bad constraint is exact (sound and complete). 4.915 MiB (i.e., 644298 words of size 8) Result written to file 'experiments-FORTE/grouping/FMS-1_Spec3-grouping6.res'. ------------------------------------------------------------ Statistics: Algorithm counters ------------------------------------------------------------ main algorithm : 0.144 second find next point : 0.000 second (0 call) learning : 0.096 second (2 calls | 0.0484304428101 second/call) learning: re-parsing : 0.009 second (2 calls | 0.0048190355301 second/call) abstractions learnt : 0 counter-examples learnt : 2 ------------------------------------------------------------ Statistics: Parsing counters ------------------------------------------------------------ model parsing : 0.004 second ------------------------------------------------------------ Statistics: State computation counters ------------------------------------------------------------ number of state comparisons : 2 number of constraints comparisons : 0 ------------------------------------------------------------ Statistics: Graphics-related counters ------------------------------------------------------------ state space drawing : 0.000 second ------------------------------------------------------------ Statistics: Global counter ------------------------------------------------------------ total : 0.145 second IMITATOR successfully terminated (after 0.149 second) Estimated memory used: 5.038 MiB (i.e., 660349 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 08:46:38 Model: experiments-FORTE/grouping/FMS-1_Spec3-grouping7.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_B1_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_in_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_out_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B3_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_I_B3_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B3_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B1_out' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B1_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_in_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_out_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B5_in_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_I_B5_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B5_A' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B5_out_A' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_product' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. This model is an L/U-PTA: - lower-bound parameters {p_B3_out_M} - upper-bound parameters {p_I_B1_C1} Abstract model built after 0.006 second. Memory for abstract model: 900.121 KiB (i.e., 230431 words) [BC (full coverage with learning-based abstraction)] Starting running cartography… ************************************************** START THE BEHAVIORAL CARTOGRAPHY ALGORITHM ************************************************** Parametric rectangle V0: p_I_B1_C1 = 1..10 & p_B3_out_M = 1..10 Number of points inside V0: 100 ************************************************** ALGORITHM BC (full coverage 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/grouping/FMS-1_Spec3-grouping7.imi experiments-FORTE/grouping/FMS-1_Spec3-grouping7_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/grouping/FMS-1_Spec3-grouping7.cv"… Executing "/home/etienne/Boulot/SVN/andre/papiers/2017/learning/IMICV/bin/../CV/Compositional_Verifier -imi experiments-FORTE/grouping/FMS-1_Spec3-grouping7.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/grouping/FMS-1_Spec3-grouping7_learning_1.imi-output.cv"… Copying abstract model into "experiments-FORTE/grouping/FMS-1_Spec3-grouping7_learning_1.imi"… …The end of Interfaçator! *-**--***---****---***--**-* Model generated by learning: counter-example *** Warning: The synclab 'B1_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_B1_C1' 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 'O_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 'I_B5_R2' 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_B1_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_in_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_out_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B3_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_I_B3_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B3_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B1_out' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B1_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_in_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_out_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B5_in_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_I_B5_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B5_A' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B5_out_A' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_product' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. This model is an L-PTA. Abstract model built after 0.052 second. Memory for abstract model: 1363.011 KiB (i.e., 348931 words) Original model: 6 automata. New model: 7 K1 computed by EFunsafe in 0.001 second: 3 states with 2 transitions explored. p_B3_out_M >= 0 & p_I_B1_C1 >= 0 [BC (full coverage with learning-based abstraction)] Successfully terminated after 0.054 second. Final constraints such that the system is correct/incorrect: False p_B3_out_M >= 0 & p_I_B1_C1 >= 0 The good constraint is exact (sound and complete). The bad constraint is exact (sound and complete). 2.972 MiB (i.e., 389621 words of size 8) Result written to file 'experiments-FORTE/grouping/FMS-1_Spec3-grouping7.res'. ------------------------------------------------------------ Statistics: Algorithm counters ------------------------------------------------------------ main algorithm : 0.051 second find next point : 0.000 second (0 call) learning : 0.042 second (1 call | 0.042270898819 second/call) learning: re-parsing : 0.002 second (1 call | 0.00293588638306 second/call) abstractions learnt : 0 counter-examples learnt : 1 ------------------------------------------------------------ Statistics: Parsing counters ------------------------------------------------------------ model parsing : 0.002 second ------------------------------------------------------------ Statistics: State computation counters ------------------------------------------------------------ number of state comparisons : 0 number of constraints comparisons : 0 ------------------------------------------------------------ Statistics: Graphics-related counters ------------------------------------------------------------ state space drawing : 0.000 second ------------------------------------------------------------ Statistics: Global counter ------------------------------------------------------------ total : 0.051 second IMITATOR successfully terminated (after 0.055 second) Estimated memory used: 3.094 MiB (i.e., 405654 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 08:46:38 Model: experiments-FORTE/grouping/FMS-1_Spec5-grouping1.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_B1_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_in_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_out_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B3_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_I_B3_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B3_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B1_out' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B1_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_in_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_out_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B5_in_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_I_B5_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B5_A' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B5_out_A' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_product' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. This model is an L/U-PTA: - lower-bound parameters {p_B3_out_M} - upper-bound parameters {p_I_B1_C1} Abstract model built after 0.008 second. Memory for abstract model: 892.285 KiB (i.e., 228425 words) [BC (full coverage with learning-based abstraction)] Starting running cartography… ************************************************** START THE BEHAVIORAL CARTOGRAPHY ALGORITHM ************************************************** Parametric rectangle V0: p_I_B1_C1 = 1..10 & p_B3_out_M = 1..10 Number of points inside V0: 100 ************************************************** ALGORITHM BC (full coverage 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/grouping/FMS-1_Spec5-grouping1.imi experiments-FORTE/grouping/FMS-1_Spec5-grouping1_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/grouping/FMS-1_Spec5-grouping1.cv"… Executing "/home/etienne/Boulot/SVN/andre/papiers/2017/learning/IMICV/bin/../CV/Compositional_Verifier -imi experiments-FORTE/grouping/FMS-1_Spec5-grouping1.cv"… Abstraction detected Moving learning result from "/home/etienne/Boulot/SVN/andre/papiers/2017/learning/IMICV/bin/../CV/tmp/assumption.imi" to "experiments-FORTE/grouping/FMS-1_Spec5-grouping1_learning_1.imi-output.cv"… Copying abstract model into "experiments-FORTE/grouping/FMS-1_Spec5-grouping1_learning_1.imi"… …The end of Interfaçator! *-**--***---****---***--**-* Model generated by learning: abstraction *** Warning: The clock 'clock_I_B1_C1' is declared but 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_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_in_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_out_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B3_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_I_B3_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B3_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B1_out' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B1_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_in_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_out_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B5_in_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_I_B5_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B5_A' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B5_out_A' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_product' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. This model is an L/U-PTA: - lower-bound parameters {p_B3_out_M} - upper-bound parameters {p_I_B1_C1} Abstract model built after 0.229 second. Memory for abstract model: 1632.957 KiB (i.e., 418037 words) Original model: 6 automata. New model: 4 K1 computed by PRP in 0.044 second: 42 states with 136 transitions explored. p_B3_out_M >= 0 & p_I_B1_C1 >= 0 [BC (full coverage with learning-based abstraction)] Successfully terminated after 0.273 second. Final constraints such that the system is correct/incorrect: p_B3_out_M >= 0 & p_I_B1_C1 >= 0 False The good constraint is exact (sound and complete). The bad constraint is exact (sound and complete). 5.932 MiB (i.e., 777579 words of size 8) Result written to file 'experiments-FORTE/grouping/FMS-1_Spec5-grouping1.res'. ------------------------------------------------------------ Statistics: Algorithm counters ------------------------------------------------------------ main algorithm : 0.270 second find next point : 0.000 second (0 call) learning : 0.211 second (1 call | 0.211130142212 second/call) learning: re-parsing : 0.008 second (1 call | 0.00820708274842 second/call) abstractions learnt : 1 counter-examples learnt : 0 ------------------------------------------------------------ Statistics: Parsing counters ------------------------------------------------------------ model parsing : 0.004 second ------------------------------------------------------------ Statistics: State computation counters ------------------------------------------------------------ number of state comparisons : 322 number of constraints comparisons : 127 ------------------------------------------------------------ Statistics: Graphics-related counters ------------------------------------------------------------ state space drawing : 0.000 second ------------------------------------------------------------ Statistics: Global counter ------------------------------------------------------------ total : 0.287 second IMITATOR successfully terminated (after 0.290 second) Estimated memory used: 6.054 MiB (i.e., 793571 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 08:46:38 Model: experiments-FORTE/grouping/FMS-1_Spec5-grouping2.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_B1_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_in_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_out_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B3_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_I_B3_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B3_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B1_out' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B1_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_in_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_out_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B5_in_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_I_B5_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B5_A' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B5_out_A' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_product' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. This model is an L/U-PTA: - lower-bound parameters {p_B3_out_M} - upper-bound parameters {p_I_B1_C1} Abstract model built after 0.008 second. Memory for abstract model: 892.285 KiB (i.e., 228425 words) [BC (full coverage with learning-based abstraction)] Starting running cartography… ************************************************** START THE BEHAVIORAL CARTOGRAPHY ALGORITHM ************************************************** Parametric rectangle V0: p_I_B1_C1 = 1..10 & p_B3_out_M = 1..10 Number of points inside V0: 100 ************************************************** ALGORITHM BC (full coverage 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/grouping/FMS-1_Spec5-grouping2.imi experiments-FORTE/grouping/FMS-1_Spec5-grouping2_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/grouping/FMS-1_Spec5-grouping2.cv"… Executing "/home/etienne/Boulot/SVN/andre/papiers/2017/learning/IMICV/bin/../CV/Compositional_Verifier -imi experiments-FORTE/grouping/FMS-1_Spec5-grouping2.cv"… Abstraction detected Moving learning result from "/home/etienne/Boulot/SVN/andre/papiers/2017/learning/IMICV/bin/../CV/tmp/assumption.imi" to "experiments-FORTE/grouping/FMS-1_Spec5-grouping2_learning_1.imi-output.cv"… Copying abstract model into "experiments-FORTE/grouping/FMS-1_Spec5-grouping2_learning_1.imi"… …The end of Interfaçator! *-**--***---****---***--**-* Model generated by learning: abstraction *** Warning: The clock 'clock_B1_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_in_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_out_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B3_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_I_B3_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B3_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B1_out' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B1_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_in_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_out_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B5_in_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_I_B5_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B5_A' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B5_out_A' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_product' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. This model is an L/U-PTA: - lower-bound parameters {p_B3_out_M} - upper-bound parameters {p_I_B1_C1} Abstract model built after 0.099 second. Memory for abstract model: 1318.167 KiB (i.e., 337451 words) Original model: 6 automata. New model: 5 K1 computed by PRP in 0.089 second: 86 states with 266 transitions explored. p_B3_out_M >= 0 & p_I_B1_C1 >= 0 [BC (full coverage with learning-based abstraction)] Successfully terminated after 0.189 second. Final constraints such that the system is correct/incorrect: p_B3_out_M >= 0 & p_I_B1_C1 >= 0 False The good constraint is exact (sound and complete). The bad constraint is exact (sound and complete). 6.654 MiB (i.e., 872204 words of size 8) Result written to file 'experiments-FORTE/grouping/FMS-1_Spec5-grouping2.res'. ------------------------------------------------------------ Statistics: Algorithm counters ------------------------------------------------------------ main algorithm : 0.186 second find next point : 0.000 second (0 call) learning : 0.082 second (1 call | 0.0826539993287 second/call) learning: re-parsing : 0.007 second (1 call | 0.00721597671509 second/call) abstractions learnt : 1 counter-examples learnt : 0 ------------------------------------------------------------ Statistics: Parsing counters ------------------------------------------------------------ model parsing : 0.004 second ------------------------------------------------------------ Statistics: State computation counters ------------------------------------------------------------ number of state comparisons : 638 number of constraints comparisons : 211 ------------------------------------------------------------ Statistics: Graphics-related counters ------------------------------------------------------------ state space drawing : 0.000 second ------------------------------------------------------------ Statistics: Global counter ------------------------------------------------------------ total : 0.187 second IMITATOR successfully terminated (after 0.191 second) Estimated memory used: 6.776 MiB (i.e., 888210 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 08:46:38 Model: experiments-FORTE/grouping/FMS-1_Spec5-grouping3.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_B1_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_in_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_out_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B3_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_I_B3_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B3_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B1_out' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B1_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_in_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_out_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B5_in_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_I_B5_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B5_A' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B5_out_A' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_product' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. This model is an L/U-PTA: - lower-bound parameters {p_B3_out_M} - upper-bound parameters {p_I_B1_C1} Abstract model built after 0.007 second. Memory for abstract model: 892.332 KiB (i.e., 228437 words) [BC (full coverage with learning-based abstraction)] Starting running cartography… ************************************************** START THE BEHAVIORAL CARTOGRAPHY ALGORITHM ************************************************** Parametric rectangle V0: p_I_B1_C1 = 1..10 & p_B3_out_M = 1..10 Number of points inside V0: 100 ************************************************** ALGORITHM BC (full coverage 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/grouping/FMS-1_Spec5-grouping3.imi experiments-FORTE/grouping/FMS-1_Spec5-grouping3_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/grouping/FMS-1_Spec5-grouping3.cv"… Executing "/home/etienne/Boulot/SVN/andre/papiers/2017/learning/IMICV/bin/../CV/Compositional_Verifier -imi experiments-FORTE/grouping/FMS-1_Spec5-grouping3.cv"… Abstraction detected Moving learning result from "/home/etienne/Boulot/SVN/andre/papiers/2017/learning/IMICV/bin/../CV/tmp/assumption.imi" to "experiments-FORTE/grouping/FMS-1_Spec5-grouping3_learning_1.imi-output.cv"… Copying abstract model into "experiments-FORTE/grouping/FMS-1_Spec5-grouping3_learning_1.imi"… …The end of Interfaçator! *-**--***---****---***--**-* Model generated by learning: abstraction *** Warning: The clock 'clock_I_B1_C1' is declared but 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_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_in_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_out_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B3_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_I_B3_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B3_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B1_out' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B1_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_in_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_out_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B5_in_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_I_B5_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B5_A' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B5_out_A' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_product' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. This model is an L/U-PTA: - lower-bound parameters {p_B3_out_M} - upper-bound parameters {p_I_B1_C1} Abstract model built after 1.112 seconds. Memory for abstract model: 1745.304 KiB (i.e., 446798 words) Original model: 6 automata. New model: 5 K1 computed by PRP in 0.098 second: 102 states with 282 transitions explored. p_B3_out_M >= 0 & p_I_B1_C1 >= 0 [BC (full coverage with learning-based abstraction)] Successfully terminated after 1.211 seconds. Final constraints such that the system is correct/incorrect: p_B3_out_M >= 0 & p_I_B1_C1 >= 0 False The good constraint is exact (sound and complete). The bad constraint is exact (sound and complete). 10.161 MiB (i.e., 1331859 words of size 8) Result written to file 'experiments-FORTE/grouping/FMS-1_Spec5-grouping3.res'. ------------------------------------------------------------ Statistics: Algorithm counters ------------------------------------------------------------ main algorithm : 1.208 seconds find next point : 0.000 second (0 call) learning : 1.094 seconds (1 call | 1.09421896935 second/call) learning: re-parsing : 0.009 second (1 call | 0.0092031955719 second/call) abstractions learnt : 1 counter-examples learnt : 0 ------------------------------------------------------------ Statistics: Parsing counters ------------------------------------------------------------ model parsing : 0.004 second ------------------------------------------------------------ Statistics: State computation counters ------------------------------------------------------------ number of state comparisons : 586 number of constraints comparisons : 256 ------------------------------------------------------------ Statistics: Graphics-related counters ------------------------------------------------------------ state space drawing : 0.000 second ------------------------------------------------------------ Statistics: Global counter ------------------------------------------------------------ total : 1.210 seconds IMITATOR successfully terminated (after 1.213 seconds) Estimated memory used: 10.283 MiB (i.e., 1347870 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 08:46:39 Model: experiments-FORTE/grouping/FMS-1_Spec5-grouping4.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_B1_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_in_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_out_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B3_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_I_B3_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B3_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B1_out' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B1_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_in_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_out_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B5_in_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_I_B5_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B5_A' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B5_out_A' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_product' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. This model is an L/U-PTA: - lower-bound parameters {p_B3_out_M} - upper-bound parameters {p_I_B1_C1} Abstract model built after 0.007 second. Memory for abstract model: 892.371 KiB (i.e., 228447 words) [BC (full coverage with learning-based abstraction)] Starting running cartography… ************************************************** START THE BEHAVIORAL CARTOGRAPHY ALGORITHM ************************************************** Parametric rectangle V0: p_I_B1_C1 = 1..10 & p_B3_out_M = 1..10 Number of points inside V0: 100 ************************************************** ALGORITHM BC (full coverage 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/grouping/FMS-1_Spec5-grouping4.imi experiments-FORTE/grouping/FMS-1_Spec5-grouping4_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/grouping/FMS-1_Spec5-grouping4.cv"… Executing "/home/etienne/Boulot/SVN/andre/papiers/2017/learning/IMICV/bin/../CV/Compositional_Verifier -imi experiments-FORTE/grouping/FMS-1_Spec5-grouping4.cv"… Abstraction detected Moving learning result from "/home/etienne/Boulot/SVN/andre/papiers/2017/learning/IMICV/bin/../CV/tmp/assumption.imi" to "experiments-FORTE/grouping/FMS-1_Spec5-grouping4_learning_1.imi-output.cv"… Copying abstract model into "experiments-FORTE/grouping/FMS-1_Spec5-grouping4_learning_1.imi"… …The end of Interfaçator! *-**--***---****---***--**-* Model generated by learning: abstraction *** Warning: The clock 'clock_I_B1_C1' is declared but 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_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_in_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_out_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B3_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_I_B3_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B3_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B1_out' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B1_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_in_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_out_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B5_in_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_I_B5_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B5_A' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B5_out_A' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_product' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. This model is an L/U-PTA: - lower-bound parameters {p_B3_out_M} - upper-bound parameters {p_I_B1_C1} Abstract model built after 0.747 second. Memory for abstract model: 1946.574 KiB (i.e., 498323 words) Original model: 6 automata. New model: 5 K1 computed by PRP in 0.136 second: 126 states with 429 transitions explored. p_B3_out_M >= 0 & p_I_B1_C1 >= 0 [BC (full coverage with learning-based abstraction)] Successfully terminated after 0.884 second. Final constraints such that the system is correct/incorrect: p_B3_out_M >= 0 & p_I_B1_C1 >= 0 False The good constraint is exact (sound and complete). The bad constraint is exact (sound and complete). 12.818 MiB (i.e., 1680122 words of size 8) Result written to file 'experiments-FORTE/grouping/FMS-1_Spec5-grouping4.res'. ------------------------------------------------------------ Statistics: Algorithm counters ------------------------------------------------------------ main algorithm : 0.881 second find next point : 0.000 second (0 call) learning : 0.729 second (1 call | 0.729363918305 second/call) learning: re-parsing : 0.009 second (1 call | 0.00987005233765 second/call) abstractions learnt : 1 counter-examples learnt : 0 ------------------------------------------------------------ Statistics: Parsing counters ------------------------------------------------------------ model parsing : 0.003 second ------------------------------------------------------------ Statistics: State computation counters ------------------------------------------------------------ number of state comparisons : 1035 number of constraints comparisons : 418 ------------------------------------------------------------ Statistics: Graphics-related counters ------------------------------------------------------------ state space drawing : 0.000 second ------------------------------------------------------------ Statistics: Global counter ------------------------------------------------------------ total : 0.884 second IMITATOR successfully terminated (after 0.887 second) Estimated memory used: 12.940 MiB (i.e., 1696122 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 08:46:40 Model: experiments-FORTE/grouping/FMS-1_Spec5-grouping5.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_B1_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_in_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_out_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B3_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_I_B3_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B3_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B1_out' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B1_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_in_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_out_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B5_in_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_I_B5_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B5_A' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B5_out_A' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_product' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. This model is an L/U-PTA: - lower-bound parameters {p_B3_out_M} - upper-bound parameters {p_I_B1_C1} Abstract model built after 0.007 second. Memory for abstract model: 892.304 KiB (i.e., 228430 words) [BC (full coverage with learning-based abstraction)] Starting running cartography… ************************************************** START THE BEHAVIORAL CARTOGRAPHY ALGORITHM ************************************************** Parametric rectangle V0: p_I_B1_C1 = 1..10 & p_B3_out_M = 1..10 Number of points inside V0: 100 ************************************************** ALGORITHM BC (full coverage 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/grouping/FMS-1_Spec5-grouping5.imi experiments-FORTE/grouping/FMS-1_Spec5-grouping5_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/grouping/FMS-1_Spec5-grouping5.cv"… Executing "/home/etienne/Boulot/SVN/andre/papiers/2017/learning/IMICV/bin/../CV/Compositional_Verifier -imi experiments-FORTE/grouping/FMS-1_Spec5-grouping5.cv"… Abstraction detected Moving learning result from "/home/etienne/Boulot/SVN/andre/papiers/2017/learning/IMICV/bin/../CV/tmp/assumption.imi" to "experiments-FORTE/grouping/FMS-1_Spec5-grouping5_learning_1.imi-output.cv"… Copying abstract model into "experiments-FORTE/grouping/FMS-1_Spec5-grouping5_learning_1.imi"… …The end of Interfaçator! *-**--***---****---***--**-* Model generated by learning: abstraction *** Warning: The clock 'clock_B1_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_in_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_out_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B3_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_I_B3_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B3_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B1_out' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B1_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_in_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_out_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B5_in_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_I_B5_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B5_A' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B5_out_A' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_product' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. This model is an L/U-PTA: - lower-bound parameters {p_B3_out_M} - upper-bound parameters {p_I_B1_C1} Abstract model built after 0.133 second. Memory for abstract model: 1323.730 KiB (i.e., 338875 words) Original model: 6 automata. New model: 6 K1 computed by PRP in 0.149 second: 176 states with 437 transitions explored. p_B3_out_M >= 0 & p_I_B1_C1 >= 0 [BC (full coverage with learning-based abstraction)] Successfully terminated after 0.283 second. Final constraints such that the system is correct/incorrect: p_B3_out_M >= 0 & p_I_B1_C1 >= 0 False The good constraint is exact (sound and complete). The bad constraint is exact (sound and complete). 9.712 MiB (i.e., 1272997 words of size 8) Result written to file 'experiments-FORTE/grouping/FMS-1_Spec5-grouping5.res'. ------------------------------------------------------------ Statistics: Algorithm counters ------------------------------------------------------------ main algorithm : 0.279 second find next point : 0.000 second (0 call) learning : 0.119 second (1 call | 0.119642019272 second/call) learning: re-parsing : 0.004 second (1 call | 0.00438308715821 second/call) abstractions learnt : 1 counter-examples learnt : 0 ------------------------------------------------------------ Statistics: Parsing counters ------------------------------------------------------------ model parsing : 0.004 second ------------------------------------------------------------ Statistics: State computation counters ------------------------------------------------------------ number of state comparisons : 1128 number of constraints comparisons : 329 ------------------------------------------------------------ Statistics: Graphics-related counters ------------------------------------------------------------ state space drawing : 0.000 second ------------------------------------------------------------ Statistics: Global counter ------------------------------------------------------------ total : 0.281 second IMITATOR successfully terminated (after 0.285 second) Estimated memory used: 9.834 MiB (i.e., 1288997 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 08:46:41 Model: experiments-FORTE/grouping/FMS-1_Spec5-grouping6.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_B1_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_in_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_out_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B3_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_I_B3_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B3_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B1_out' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B1_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_in_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_out_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B5_in_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_I_B5_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B5_A' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B5_out_A' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_product' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. This model is an L/U-PTA: - lower-bound parameters {p_B3_out_M} - upper-bound parameters {p_I_B1_C1} Abstract model built after 0.009 second. Memory for abstract model: 892.324 KiB (i.e., 228435 words) [BC (full coverage with learning-based abstraction)] Starting running cartography… ************************************************** START THE BEHAVIORAL CARTOGRAPHY ALGORITHM ************************************************** Parametric rectangle V0: p_I_B1_C1 = 1..10 & p_B3_out_M = 1..10 Number of points inside V0: 100 ************************************************** ALGORITHM BC (full coverage 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/grouping/FMS-1_Spec5-grouping6.imi experiments-FORTE/grouping/FMS-1_Spec5-grouping6_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/grouping/FMS-1_Spec5-grouping6.cv"… Executing "/home/etienne/Boulot/SVN/andre/papiers/2017/learning/IMICV/bin/../CV/Compositional_Verifier -imi experiments-FORTE/grouping/FMS-1_Spec5-grouping6.cv"… Abstraction detected Moving learning result from "/home/etienne/Boulot/SVN/andre/papiers/2017/learning/IMICV/bin/../CV/tmp/assumption.imi" to "experiments-FORTE/grouping/FMS-1_Spec5-grouping6_learning_1.imi-output.cv"… Copying abstract model into "experiments-FORTE/grouping/FMS-1_Spec5-grouping6_learning_1.imi"… …The end of Interfaçator! *-**--***---****---***--**-* Model generated by learning: abstraction *** Warning: The clock 'clock_B1_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_in_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_out_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B3_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_I_B3_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B3_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B1_out' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B1_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_in_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_out_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B5_in_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_I_B5_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B5_A' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B5_out_A' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_product' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. This model is an L/U-PTA: - lower-bound parameters {p_B3_out_M} - upper-bound parameters {p_I_B1_C1} Abstract model built after 0.330 second. Memory for abstract model: 1401.726 KiB (i.e., 358842 words) Original model: 6 automata. New model: 6 K1 computed by PRP in 0.306 second: 258 states with 841 transitions explored. p_B3_out_M >= 0 & p_I_B1_C1 >= 0 [BC (full coverage with learning-based abstraction)] Successfully terminated after 0.637 second. Final constraints such that the system is correct/incorrect: p_B3_out_M >= 0 & p_I_B1_C1 >= 0 False The good constraint is exact (sound and complete). The bad constraint is exact (sound and complete). 15.334 MiB (i.e., 2009935 words of size 8) Result written to file 'experiments-FORTE/grouping/FMS-1_Spec5-grouping6.res'. ------------------------------------------------------------ Statistics: Algorithm counters ------------------------------------------------------------ main algorithm : 0.634 second find next point : 0.000 second (0 call) learning : 0.314 second (1 call | 0.314592838288 second/call) learning: re-parsing : 0.005 second (1 call | 0.00538110733033 second/call) abstractions learnt : 1 counter-examples learnt : 0 ------------------------------------------------------------ Statistics: Parsing counters ------------------------------------------------------------ model parsing : 0.005 second ------------------------------------------------------------ Statistics: State computation counters ------------------------------------------------------------ number of state comparisons : 2163 number of constraints comparisons : 675 ------------------------------------------------------------ Statistics: Graphics-related counters ------------------------------------------------------------ state space drawing : 0.000 second ------------------------------------------------------------ Statistics: Global counter ------------------------------------------------------------ total : 0.637 second IMITATOR successfully terminated (after 0.641 second) Estimated memory used: 15.456 MiB (i.e., 2025935 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 08:46:41 Model: experiments-FORTE/grouping/FMS-1_Spec5-grouping7.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_B1_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_in_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_out_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B3_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_I_B3_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B3_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B1_out' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B1_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_in_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_out_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B5_in_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_I_B5_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B5_A' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B5_out_A' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_product' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. This model is an L/U-PTA: - lower-bound parameters {p_B3_out_M} - upper-bound parameters {p_I_B1_C1} Abstract model built after 0.008 second. Memory for abstract model: 892.390 KiB (i.e., 228452 words) [BC (full coverage with learning-based abstraction)] Starting running cartography… ************************************************** START THE BEHAVIORAL CARTOGRAPHY ALGORITHM ************************************************** Parametric rectangle V0: p_I_B1_C1 = 1..10 & p_B3_out_M = 1..10 Number of points inside V0: 100 ************************************************** ALGORITHM BC (full coverage 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/grouping/FMS-1_Spec5-grouping7.imi experiments-FORTE/grouping/FMS-1_Spec5-grouping7_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/grouping/FMS-1_Spec5-grouping7.cv"… Executing "/home/etienne/Boulot/SVN/andre/papiers/2017/learning/IMICV/bin/../CV/Compositional_Verifier -imi experiments-FORTE/grouping/FMS-1_Spec5-grouping7.cv"… Abstraction detected Moving learning result from "/home/etienne/Boulot/SVN/andre/papiers/2017/learning/IMICV/bin/../CV/tmp/assumption.imi" to "experiments-FORTE/grouping/FMS-1_Spec5-grouping7_learning_1.imi-output.cv"… Copying abstract model into "experiments-FORTE/grouping/FMS-1_Spec5-grouping7_learning_1.imi"… …The end of Interfaçator! *-**--***---****---***--**-* Model generated by learning: abstraction *** Warning: The clock 'clock_I_B1_C1' is declared but 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_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_in_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_out_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B3_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_I_B3_M' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B3_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B1_out' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B1_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_in_R1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B3_out_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B5_in_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_I_B5_R2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_O_B5_A' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_B5_out_A' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_product' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. This model is an L/U-PTA: - lower-bound parameters {p_B3_out_M} - upper-bound parameters {p_I_B1_C1} Abstract model built after 0.119 second. Memory for abstract model: 1305.402 KiB (i.e., 334183 words) Original model: 6 automata. New model: 6 K1 computed by PRP in 0.140 second: 148 states with 444 transitions explored. p_B3_out_M >= 0 & p_I_B1_C1 >= 0 [BC (full coverage with learning-based abstraction)] Successfully terminated after 0.260 second. Final constraints such that the system is correct/incorrect: p_B3_out_M >= 0 & p_I_B1_C1 >= 0 False The good constraint is exact (sound and complete). The bad constraint is exact (sound and complete). 11.935 MiB (i.e., 1564421 words of size 8) Result written to file 'experiments-FORTE/grouping/FMS-1_Spec5-grouping7.res'. ------------------------------------------------------------ Statistics: Algorithm counters ------------------------------------------------------------ main algorithm : 0.257 second find next point : 0.000 second (0 call) learning : 0.104 second (1 call | 0.104744195939 second/call) learning: re-parsing : 0.005 second (1 call | 0.00530004501343 second/call) abstractions learnt : 1 counter-examples learnt : 0 ------------------------------------------------------------ Statistics: Parsing counters ------------------------------------------------------------ model parsing : 0.005 second ------------------------------------------------------------ Statistics: State computation counters ------------------------------------------------------------ number of state comparisons : 1168 number of constraints comparisons : 408 ------------------------------------------------------------ Statistics: Graphics-related counters ------------------------------------------------------------ state space drawing : 0.000 second ------------------------------------------------------------ Statistics: Global counter ------------------------------------------------------------ total : 0.258 second IMITATOR successfully terminated (after 0.262 second) Estimated memory used: 12.057 MiB (i.e., 1580421 words of size 8) Done etienne@MakBook:~/Boulot/SVN/andre/papiers/2017/learning$