************************************************************ * IMITATOR 2.9-alpha "Butter Incaberry" * * * * Etienne Andre, Ulrich Kuehne et al. * * 2009 - 2017 * * LSV, ENS de Cachan & CNRS, France * * LIPN, Universite Paris 13, Sorbonne Paris Cite, France * * www.imitator.fr * * * * Build: 2212 (2017-02-22 08:48:09 UTC) * * master/35846ec * ************************************************************ Analysis time: Wed Feb 22, 2017 17:12:29  Model: ./examples/Fischer/FERA4.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: IMITATOR will try to stop after 600 seconds. *** Warning: IMITATOR will try to stop the cartography after 600 seconds. *** Warning: The clock 'clock_Enter1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_SetX01' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_Enter2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_SetX02' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_Enter3' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_SetX03' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_Enter4' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_SetX04' 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 {Delta} - upper-bound parameters {delta}  Abstract model built after 0.006 second. Memory for abstract model: 999.925 KiB (i.e., 255981 words)   [BC (full coverage with learning-based abstraction)] Starting running cartography…   **************************************************  START THE BEHAVIORAL CARTOGRAPHY ALGORITHM **************************************************  Parametric rectangle V0:   delta = 1..10 & Delta = 1..10  Number of points inside V0: 100  ************************************************** ALGORITHM BC (full coverage with learning-based abstraction): iteration 1 Considering the following pi1  delta = 1 & Delta = 1 Executing: 'python /home/etienne/Boulot/SVN/andre/papiers/2017/learning/IMICV/bin/../interfaceCV.py ./examples/Fischer/FERA4.imi ./examples/Fischer/FERA4-learning_learning_1.imi delta=1,Delta=1' *-**--***---****---***--**-* Hello, this is Interfaçator! Building reference valuation… Pi0: v(delta) = 1 v(Delta) = 1 Valuating component A with pi0… Writing content to "./examples/Fischer/FERA4.cv"… Executing "/home/etienne/Boulot/SVN/andre/papiers/2017/learning/IMICV/bin/../CV/Compositional_Verifier -imi ./examples/Fischer/FERA4.cv"… Counter-example detected Moving learning result from "/home/etienne/Boulot/SVN/andre/papiers/2017/learning/IMICV/bin/../CV/tmp/counterexample.imi" to "./examples/Fischer/FERA4-learning_learning_1.imi-output.cv"… Copying abstract model into "./examples/Fischer/FERA4-learning_learning_1.imi"…  …The end of Interfaçator! *-**--***---****---***--**-* Model generated by learning: counter-example *** Warning: The synclab 'SetX01' 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 'Start2' 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 'SetX2' 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 'Enter2' 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 'SetX02' 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 'SetX03' 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 'Enter4' 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 'SetX04' 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_Enter1' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_SetX01' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_Enter2' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_SetX02' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_Enter3' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_SetX03' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_Enter4' is declared but never used in the model; it is therefore removed from the model. Use option -no-var-autoremove to keep it. *** Warning: The clock 'clock_SetX04' 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 {Delta} - upper-bound parameters {delta}  Abstract model built after 0.775 second. Memory for abstract model: 1566.125 KiB (i.e., 400928 words)  Original model: 6 automata. New model: 7  K1 computed by EFunsafe in 0.161 second: 102 states with 113 transitions explored.  Delta >= 0 & delta > 0 & 4 > Delta  ************************************************** ALGORITHM BC (full coverage with learning-based abstraction): iteration 2 Considering the following pi2  delta = 1 & Delta = 4 Executing: 'python /home/etienne/Boulot/SVN/andre/papiers/2017/learning/IMICV/bin/../interfaceCV.py ./examples/Fischer/FERA4.imi ./examples/Fischer/FERA4-learning_learning_2.imi delta=1,Delta=4' *-**--***---****---***--**-* Hello, this is Interfaçator! Building reference valuation… Pi0: v(delta) = 1 v(Delta) = 4 Valuating component A with pi0… Writing content to "./examples/Fischer/FERA4.cv"… Executing "/home/etienne/Boulot/SVN/andre/papiers/2017/learning/IMICV/bin/../CV/Compositional_Verifier -imi ./examples/Fischer/FERA4.cv"… Fatal error! Call to "/home/etienne/Boulot/SVN/andre/papiers/2017/learning/IMICV/bin/../CV/Compositional_Verifier" failed. Error code: -9 *** ERROR: Fatal internal error: Something went wrong in the command. Exit code: 1. Command: 'python /home/etienne/Boulot/SVN/andre/papiers/2017/learning/IMICV/bin/../interfaceCV.py ./examples/Fischer/FERA4.imi ./examples/Fischer/FERA4-learning_learning_2.imi delta=1,Delta=4' Please (politely) insult the developers. *** ERROR: IMITATOR aborted (after 3711.996 seconds)