************************************************************ * 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 15:21:51  Model: ./examples/Fischer/FERA3.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. This model is an L/U-PTA: - lower-bound parameters {Delta} - upper-bound parameters {delta}  Abstract model built after 0.005 second. Memory for abstract model: 871.996 KiB (i.e., 223231 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/FERA3.imi ./examples/Fischer/FERA3-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/FERA3.cv"… Executing "/home/etienne/Boulot/SVN/andre/papiers/2017/learning/IMICV/bin/../CV/Compositional_Verifier -imi ./examples/Fischer/FERA3.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/FERA3-learning_learning_1.imi-output.cv"… Copying abstract model into "./examples/Fischer/FERA3-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 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. This model is an L/U-PTA: - lower-bound parameters {Delta} - upper-bound parameters {delta}  Abstract model built after 0.050 second. Memory for abstract model: 1310.968 KiB (i.e., 335608 words)  Original model: 5 automata. New model: 6  K1 computed by EFunsafe in 0.013 second: 15 states with 15 transitions explored.  Delta >= 0 & delta > 0 & 3 > Delta  ************************************************** ALGORITHM BC (full coverage with learning-based abstraction): iteration 2 Considering the following pi2  delta = 1 & Delta = 3 Executing: 'python /home/etienne/Boulot/SVN/andre/papiers/2017/learning/IMICV/bin/../interfaceCV.py ./examples/Fischer/FERA3.imi ./examples/Fischer/FERA3-learning_learning_2.imi delta=1,Delta=3' *-**--***---****---***--**-* Hello, this is Interfaçator! Building reference valuation… Pi0: v(delta) = 1 v(Delta) = 3 Valuating component A with pi0… Writing content to "./examples/Fischer/FERA3.cv"… Executing "/home/etienne/Boulot/SVN/andre/papiers/2017/learning/IMICV/bin/../CV/Compositional_Verifier -imi ./examples/Fischer/FERA3.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/FERA3.imi ./examples/Fischer/FERA3-learning_learning_2.imi delta=1,Delta=3' Please (politely) insult the developers. *** ERROR: IMITATOR aborted (after 4852.501 seconds)