************************************************************ * 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/6/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/6/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/6/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/6/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} - upper-bound parameters {b, p4, p5, p3, p8, p7} 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… ************************************************************ * 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 * ************************************************************ Generating the transformed model… Model: /home/royal/Desktop/experiments/Etienne/6/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). Generating the transformed model… 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… ************************************************************ * 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/6/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… 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  Automaton name: aa, Number of models: 5  Transformation completed  Automaton name: aa, Number of models: 5  Transformation completed Starting running algorithm NZCUB…  Starting running algorithm NZCUB…  Computing post^1 from 1 state. Starting running algorithm NZCUB…  Computing post^1 from 1 state. Computing post^1 from 1 state. Starting running algorithm NZCUB…  Starting running algorithm NZCUB…  Computing post^1 from 1 state. Computing post^1 from 1 state. Computing post^2 from 1 state. Computing post^2 from 4 states. Computing post^2 from 4 states. Computing post^2 from 6 states. Computing post^2 from 12 states.  Fixpoint reached at a depth of 3: 5 states with 4 transitions in the final state space.  [NZCUB] Algorithm completed after 0.776 second.  4 states merged within 10 states. Computing post^3 from 2 states. Computing post^4 from 2 states. Computing post^3 from 6 states.  [NZCUB] Found a cycle. IMITATOR successfully terminated (after 0.832 second)  [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.836 second. IMITATOR successfully terminated (after 0.836 second)  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.  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.  [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.895 second. IMITATOR successfully terminated (after 0.897 second) Computing post^3 from 16 states. Computing post^4 from 8 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.  Fixpoint reached at a depth of 5: 23 states with 72 transitions in the final state space.  [NZCUB] Algorithm completed after 0.996 second. IMITATOR successfully terminated (after 0.999 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.122 seconds. IMITATOR successfully terminated (after 1.130 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/6/JLR-TACAS13/NZCUBtransdist.res'. IMITATOR successfully terminated (after 1.129 seconds)