************************************************************ * IMITATOR 2.9.2-working "Butter Incaberry" * * * * Etienne Andre, Ulrich Kuehne et al. * * 2009 - 2018 * * LSV, ENS de Cachan & CNRS, France * * LIPN, Universite Paris 13, France * * www.imitator.fr * * * * Build: 2402 (2018-06-07 12:48:34 UTC) * * HEAD/0999a7d * ************************************************************ Model: /home/royal/Desktop/experiments/Etienne/4/JLR-TACAS13/JLR-TACAS13.imi Mode: parametric non-Zeno emptiness checking (CUB transformation), distributed version. Considering fixpoint variant with monodirectional inclusion of symbolic zones (instead of equality). Time elapsing will be applied at the beginning of the computation of a new state. Merging technique of [AFS13] enabled. The result will be written to a file. ************************************************************ * IMITATOR 2.9.2-working "Butter Incaberry" * * * * Etienne Andre, Ulrich Kuehne et al. * * 2009 - 2018 * * LSV, ENS de Cachan & CNRS, France * * LIPN, Universite Paris 13, France * * www.imitator.fr * * * * Build: 2402 (2018-06-07 12:48:34 UTC) * * HEAD/0999a7d * ************************************************************ Model: /home/royal/Desktop/experiments/Etienne/4/JLR-TACAS13/JLR-TACAS13.imi Mode: parametric non-Zeno emptiness checking (CUB transformation), distributed version. Considering fixpoint variant with monodirectional inclusion of symbolic zones (instead of equality). Time elapsing will be applied at the beginning of the computation of a new state. Merging technique of [AFS13] enabled. The result will be written to a file. ************************************************************ * IMITATOR 2.9.2-working "Butter Incaberry" * * * * Etienne Andre, Ulrich Kuehne et al. * * 2009 - 2018 * * LSV, ENS de Cachan & CNRS, France * * LIPN, Universite Paris 13, France * * www.imitator.fr * * * * Build: 2402 (2018-06-07 12:48:34 UTC) * * HEAD/0999a7d * ************************************************************ Model: /home/royal/Desktop/experiments/Etienne/4/JLR-TACAS13/JLR-TACAS13.imi Mode: parametric non-Zeno emptiness checking (CUB transformation), distributed version. Considering fixpoint variant with monodirectional inclusion of symbolic zones (instead of equality). Time elapsing will be applied at the beginning of the computation of a new state. Merging technique of [AFS13] enabled. The result will be written to a file. This model is an L/U-PTA: - lower-bound parameters {a, p1} - upper-bound parameters {b, p4, p5, p3, p8, p7} This model is an L/U-PTA: - lower-bound parameters {a, p1} Generating the transformed model… - upper-bound parameters {b, p4, p5, p3, p8, p7} Generating the transformed model… ************************************************************ * IMITATOR 2.9.2-working "Butter Incaberry" * * * * Etienne Andre, Ulrich Kuehne et al. * * 2009 - 2018 * * LSV, ENS de Cachan & CNRS, France * * LIPN, Universite Paris 13, France * * www.imitator.fr * * * * Build: 2402 (2018-06-07 12:48:34 UTC) * * HEAD/0999a7d * ************************************************************ This model is an L/U-PTA: - lower-bound parameters {a, p1} - upper-bound parameters {b, p4, p5, p3, p8, p7} Generating the transformed model… Model: /home/royal/Desktop/experiments/Etienne/4/JLR-TACAS13/JLR-TACAS13.imi Mode: parametric non-Zeno emptiness checking (CUB transformation), distributed version. Considering fixpoint variant with monodirectional inclusion of symbolic zones (instead of equality). Time elapsing will be applied at the beginning of the computation of a new state. Merging technique of [AFS13] enabled. The result will be written to a file. This model is an L/U-PTA: - lower-bound parameters {a, p1} - upper-bound parameters {b, p4, p5, p3, p8, p7} Generating the transformed model…  Automaton name: aa, Number of models: 5  Transformation completed  Automaton name: aa, Number of models: 5  Transformation completed  Automaton name: aa, Number of models: 5  Transformation completed  Automaton name: aa, Number of models: 5  Transformation completed Starting running algorithm NZCUB…  Computing post^1 from 1 state. Starting running algorithm NZCUB…  Computing post^1 from 1 state. Starting running algorithm NZCUB…  Computing post^1 from 1 state. Computing post^2 from 4 states. Computing post^2 from 6 states. Computing post^2 from 12 states.  4 states merged within 10 states. Computing post^3 from 6 states.  2 states merged within 10 states. Computing post^3 from 8 states.  4 states merged within 10 states. Computing post^4 from 6 states.  [NZCUB] Found a cycle.  [NZCUB] Found a cycle.  [NZCUB] Found a cycle.  4 states merged within 20 states.  [NZCUB] Found a cycle.  [NZCUB] Found a cycle.  [NZCUB] Found a cycle.  [NZCUB] Found a cycle.  [NZCUB] Found a cycle.  Fixpoint reached at a depth of 5: 17 states with 34 transitions in the final state space.  [NZCUB] Algorithm completed after 0.831 second. Starting running algorithm NZCUB…  Computing post^1 from 1 state. Computing post^2 from 4 states.  Fixpoint reached at a depth of 3: 5 states with 4 transitions in the final state space.  [NZCUB] Algorithm completed after 0.838 second. Starting running algorithm NZCUB…  Computing post^1 from 1 state. Computing post^2 from 1 state. Computing post^3 from 16 states. Computing post^3 from 2 states. Computing post^4 from 8 states. Computing post^4 from 2 states.  [NZCUB] Found a cycle.  [NZCUB] Found a cycle.  [NZCUB] Found a cycle.  [NZCUB] Found a cycle.  Fixpoint reached at a depth of 5: 6 states with 7 transitions in the final state space.  [NZCUB] Algorithm completed after 0.851 second. IMITATOR successfully terminated (after 0.851 second)  [NZCUB] Found a cycle.  [NZCUB] Found a cycle.  [NZCUB] Found a cycle.  [NZCUB] Found a cycle.  [NZCUB] Found a cycle.  [NZCUB] Found a cycle.  [NZCUB] Found a cycle.  [NZCUB] Found a cycle.  [NZCUB] Found a cycle.  [NZCUB] Found a cycle.  [NZCUB] Found a cycle.  [NZCUB] Found a cycle.  [NZCUB] Found a cycle.  [NZCUB] Found a cycle.  Fixpoint reached at a depth of 5: 23 states with 72 transitions in the final state space.  [NZCUB] Algorithm completed after 0.884 second. IMITATOR successfully terminated (after 0.886 second) Computing post^4 from 16 states.  [NZCUB] Found a cycle.  [NZCUB] Found a cycle.  [NZCUB] Found a cycle.  [NZCUB] Found a cycle.  [NZCUB] Found a cycle.  [NZCUB] Found a cycle.  [NZCUB] Found a cycle.  [NZCUB] Found a cycle.  [NZCUB] Found a cycle.  [NZCUB] Found a cycle.  [NZCUB] Found a cycle.  [NZCUB] Found a cycle.  [NZCUB] Found a cycle.  [NZCUB] Found a cycle.  [NZCUB] Found a cycle.  [NZCUB] Found a cycle.  [NZCUB] Found a cycle.  [NZCUB] Found a cycle.  [NZCUB] Found a cycle.  [NZCUB] Found a cycle.  [NZCUB] Found a cycle.  [NZCUB] Found a cycle.  [NZCUB] Found a cycle.  [NZCUB] Found a cycle.  [NZCUB] Found a cycle.  [NZCUB] Found a cycle.  [NZCUB] Found a cycle.  [NZCUB] Found a cycle.  [NZCUB] Found a cycle.  [NZCUB] Found a cycle.  [NZCUB] Found a cycle.  [NZCUB] Found a cycle.  [NZCUB] Found a cycle.  [NZCUB] Found a cycle.  [NZCUB] Found a cycle.  [NZCUB] Found a cycle.  [NZCUB] Found a cycle.  [NZCUB] Found a cycle.  [NZCUB] Found a cycle.  [NZCUB] Found a cycle.  Fixpoint reached at a depth of 5: 45 states with 132 transitions in the final state space.  [NZCUB] Algorithm completed after 1.105 seconds. IMITATOR successfully terminated (after 1.112 seconds)  Final constraint such that the system is correct: False This good constraint is exact (sound and complete)  Result written to file '/home/royal/Desktop/experiments/Etienne/4/JLR-TACAS13/NZCUBtransdist.res'. IMITATOR successfully terminated (after 1.112 seconds)