************************************************************ * 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 * ************************************************************ ************************************************************ * 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/8/CUBPTA1/CUBPTA1.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. ************************************************************ * 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/8/CUBPTA1/CUBPTA1.imi Mode: parametric non-Zeno emptiness checking (CUB transformation), distributed version. Model: /home/royal/Desktop/experiments/Etienne/8/CUBPTA1/CUBPTA1.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. 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. 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/8/CUBPTA1/CUBPTA1.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/8/CUBPTA1/CUBPTA1.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/8/CUBPTA1/CUBPTA1.imi Mode: parametric non-Zeno emptiness checking (CUB transformation), distributed version. ************************************************************ * 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 * ************************************************************ Considering fixpoint variant with monodirectional inclusion of symbolic zones (instead of equality). Model: /home/royal/Desktop/experiments/Etienne/8/CUBPTA1/CUBPTA1.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. 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 {p3} - upper-bound parameters {p2, p1, p5, p6, p4, p8, p9, p7} This model is an L/U-PTA: - lower-bound parameters {p3} - upper-bound parameters {p2, p1, p5, p6, p4, p8, p9, p7} Generating the transformed model… Generating the transformed model… This model is an L/U-PTA: - lower-bound parameters {p3} - upper-bound parameters {p2, p1, p5, p6, p4, p8, p9, p7} Generating the transformed model… This model is an L/U-PTA: - lower-bound parameters {p3} - upper-bound parameters {p2, p1, p5, p6, p4, p8, p9, 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/8/CUBPTA1/CUBPTA1.imi This model is an L/U-PTA: - lower-bound parameters {p3} - upper-bound parameters {p2, p1, p5, p6, p4, p8, p9, p7} Generating the transformed model… 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 {p3} - upper-bound parameters {p2, p1, p5, p6, p4, p8, p9, p7} Generating the transformed model… This model is an L/U-PTA: - lower-bound parameters {p3} - upper-bound parameters {p2, p1, p5, p6, p4, p8, p9, p7} Generating the transformed model… This model is an L/U-PTA: - lower-bound parameters {p3} - upper-bound parameters {p2, p1, p5, p6, p4, p8, p9, p7} Generating the transformed model…  Automaton name: pta, Number of models: 20  Transformation completed  Automaton name: pta, Number of models: 20  Transformation completed  Automaton name: pta, Number of models: 20  Transformation completed Starting running algorithm NZCUB…  Starting running algorithm NZCUB…  Computing post^1 from 1 state. Computing post^1 from 1 state.  Automaton name: pta, Number of models: 20  Transformation completed Starting running algorithm NZCUB…  Computing post^1 from 1 state.  Automaton name: pta, Number of models: 20  Transformation completed Starting running algorithm NZCUB…  Computing post^1 from 1 state. Computing post^2 from 3 states.  Fixpoint reached at a depth of 3: 4 states with 3 transitions in the final state space.  [NZCUB] Algorithm completed after 1.266 seconds. Computing post^2 from 6 states. Computing post^2 from 2 states.  Automaton name: pta, Number of models: 20  Starting running algorithm NZCUB…  Computing post^1 from 1 state. Transformation completed Starting running algorithm NZCUB…  Computing post^1 from 1 state. Computing post^2 from 3 states. Computing post^2 from 4 states.  Fixpoint reached at a depth of 3: 4 states with 3 transitions in the final state space.  [NZCUB] Algorithm completed after 1.287 seconds.  Automaton name: pta, Number of models: 20  Transformation completed Starting running algorithm NZCUB…  Computing post^1 from 1 state. Starting running algorithm NZCUB…  Computing post^1 from 1 state. Computing post^2 from 3 states.  Fixpoint reached at a depth of 3: 4 states with 3 transitions in the final state space.  [NZCUB] Algorithm completed after 1.291 seconds. Starting running algorithm NZCUB…  Computing post^1 from 1 state. Computing post^3 from 4 states. Computing post^2 from 1 state. Computing post^3 from 2 states. Computing post^3 from 2 states.  2 states merged within 6 states. Computing post^4 from 2 states. Computing post^4 from 1 state. Computing post^4 from 4 states. Computing post^3 from 4 states.  [NZCUB] Found a cycle.  [NZCUB] Found a cycle.  [NZCUB] Non-Zeno cycle found!  [NZCUB] Found a cycle.  [NZCUB] Non-Zeno cycle found!  [NZCUB] Non-Zeno cycle found!  Fixpoint reached at a depth of 5: 7 states with 8 transitions in the final state space.  [NZCUB] Algorithm completed after 1.301 seconds.  Fixpoint reached at a depth of 5: 5 states with 6 transitions in the final state space.  [NZCUB] Algorithm completed after 1.302 seconds. Starting running algorithm NZCUB…  Computing post^1 from 1 state.  [NZCUB] Found a cycle.  [NZCUB] Non-Zeno cycle found! Starting running algorithm NZCUB…  Computing post^1 from 1 state.  Fixpoint reached at a depth of 5: 13 states with 16 transitions in the final state space.  [NZCUB] Algorithm completed after 1.307 seconds. Computing post^2 from 4 states. Computing post^4 from 6 states. Computing post^2 from 6 states. Starting running algorithm NZCUB…  Computing post^1 from 1 state.  [NZCUB] Found a cycle.  [NZCUB] Non-Zeno cycle found! Computing post^2 from 2 states.  [NZCUB] Found a cycle. Computing post^3 from 2 states. Computing post^3 from 4 states.  [NZCUB] Non-Zeno cycle found! Computing post^2 from 3 states.  Fixpoint reached at a depth of 3: 4 states with 3 transitions in the final state space.  [NZCUB] Algorithm completed after 1.319 seconds. Computing post^4 from 2 states.  [NZCUB] Found a cycle.  [NZCUB] Non-Zeno cycle found! Computing post^2 from 6 states. Starting running algorithm NZCUB…  Computing post^1 from 1 state.  2 states merged within 6 states.  [NZCUB] Found a cycle. Computing post^3 from 4 states.  [NZCUB] Non-Zeno cycle found! Computing post^4 from 4 states.  Fixpoint reached at a depth of 5: 7 states with 8 transitions in the final state space.  [NZCUB] Algorithm completed after 1.324 seconds. Computing post^2 from 2 states.  [NZCUB] Found a cycle.  [NZCUB] Non-Zeno cycle found!  [NZCUB] Found a cycle. Starting running algorithm NZCUB…   [NZCUB] Non-Zeno cycle found! Computing post^1 from 1 state. Computing post^3 from 2 states.  Fixpoint reached at a depth of 5: 17 states with 28 transitions in the final state space.  [NZCUB] Algorithm completed after 1.327 seconds. Computing post^4 from 2 states.  [NZCUB] Found a cycle. Computing post^2 from 4 states.  [NZCUB] Non-Zeno cycle found! Computing post^4 from 6 states.  Fixpoint reached at a depth of 5: 13 states with 16 transitions in the final state space.  [NZCUB] Algorithm completed after 1.331 seconds.  2 states merged within 6 states.  [NZCUB] Found a cycle. Starting running algorithm NZCUB…  Computing post^1 from 1 state. Computing post^3 from 2 states.  [NZCUB] Non-Zeno cycle found!  [NZCUB] Found a cycle.  [NZCUB] Non-Zeno cycle found! Computing post^3 from 4 states.  Fixpoint reached at a depth of 5: 7 states with 8 transitions in the final state space.  [NZCUB] Algorithm completed after 1.334 seconds. Computing post^2 from 1 state.  [NZCUB] Found a cycle. Computing post^3 from 2 states.  [NZCUB] Non-Zeno cycle found! Computing post^4 from 1 state. Starting running algorithm NZCUB…  Computing post^1 from 1 state. Computing post^2 from 1 state. Computing post^4 from 4 states.  [NZCUB] Found a cycle.  [NZCUB] Found a cycle.  [NZCUB] Non-Zeno cycle found!  [NZCUB] Found a cycle.  [NZCUB] Non-Zeno cycle found!  [NZCUB] Non-Zeno cycle found! Starting running algorithm NZCUB…   Fixpoint reached at a depth of 5: 5 states with 6 transitions in the final state space.  [NZCUB] Algorithm completed after 1.343 seconds. Computing post^3 from 2 states. Computing post^1 from 1 state. Computing post^4 from 6 states.  [NZCUB] Found a cycle.  [NZCUB] Non-Zeno cycle found! Computing post^4 from 1 state.  [NZCUB] Found a cycle.  [NZCUB] Non-Zeno cycle found!  Fixpoint reached at a depth of 5: 11 states with 12 transitions in the final state space.  [NZCUB] Algorithm completed after 1.347 seconds. Computing post^2 from 4 states.  [NZCUB] Found a cycle.  [NZCUB] Found a cycle.  [NZCUB] Non-Zeno cycle found!  [NZCUB] Non-Zeno cycle found!  Fixpoint reached at a depth of 5: 17 states with 28 transitions in the final state space.  [NZCUB] Algorithm completed after 1.348 seconds.  Fixpoint reached at a depth of 5: 5 states with 6 transitions in the final state space.  [NZCUB] Algorithm completed after 1.349 seconds.  [NZCUB] Found a cycle. Computing post^3 from 2 states.  [NZCUB] Non-Zeno cycle found! Starting running algorithm NZCUB…  Computing post^1 from 1 state. Computing post^2 from 2 states.  [NZCUB] Found a cycle.  [NZCUB] Non-Zeno cycle found! Computing post^3 from 1 state.  [NZCUB] Found a cycle.  [NZCUB] Non-Zeno cycle found! Computing post^4 from 2 states. Computing post^4 from 4 states. Starting running algorithm NZCUB…  Computing post^1 from 1 state.  [NZCUB] Found a cycle.  [NZCUB] Found a cycle. Computing post^2 from 1 state.  Fixpoint reached at a depth of 5: 17 states with 28 transitions in the final state space.  [NZCUB] Algorithm completed after 1.364 seconds.  [NZCUB] Non-Zeno cycle found!  [NZCUB] Non-Zeno cycle found!  Fixpoint reached at a depth of 5: 6 states with 6 transitions in the final state space.  [NZCUB] Algorithm completed after 1.365 seconds. Computing post^3 from 1 state.  [NZCUB] Found a cycle.  [NZCUB] Non-Zeno cycle found!  Fixpoint reached at a depth of 5: 11 states with 12 transitions in the final state space.  [NZCUB] Algorithm completed after 1.368 seconds. Computing post^4 from 1 state.  [NZCUB] Found a cycle.  [NZCUB] Non-Zeno cycle found!  Fixpoint reached at a depth of 5: 4 states with 4 transitions in the final state space.  [NZCUB] Algorithm completed after 1.372 seconds. IMITATOR successfully terminated (after 1.383 seconds) IMITATOR successfully terminated (after 1.409 seconds) IMITATOR successfully terminated (after 1.420 seconds) IMITATOR successfully terminated (after 1.427 seconds)  Automaton name: pta, Number of models: 20  Transformation completed Starting running algorithm NZCUB…  Computing post^1 from 1 state. IMITATOR successfully terminated (after 1.458 seconds) Computing post^2 from 6 states. IMITATOR successfully terminated (after 1.473 seconds)  2 states merged within 6 states. Computing post^3 from 4 states. Computing post^4 from 6 states.  [NZCUB] Found a cycle.  [NZCUB] Non-Zeno cycle found!  [NZCUB] Found a cycle.  [NZCUB] Non-Zeno cycle found!  [NZCUB] Found a cycle.  [NZCUB] Non-Zeno cycle found!  [NZCUB] Found a cycle.  [NZCUB] Non-Zeno cycle found!  Fixpoint reached at a depth of 5: 17 states with 28 transitions in the final state space.  [NZCUB] Algorithm completed after 1.528 seconds. IMITATOR successfully terminated (after 1.543 seconds)  Final constraint such that the system is correct:  p1 + p9 >= p3 & p3 > 0 & p1 > 0 & p1 + p7 >= p3 & p6 > 0 & p7 > 0 & p9 > 0 & p5 > 0 & p4 > p2 & p5 + p7 >= p3 & p5 + p9 >= p3 & p6 + p7 >= p3 & p6 + p9 >= p3 & p2 >= p3 & p8 >= p3 OR p1 + p7 >= p3 & p3 > 0 & p1 > 0 & p1 + p9 >= p3 & p7 > 0 & p6 > 0 & p4 > p6 & p9 > 0 & p5 > 0 & p5 + p9 >= p3 & p5 + p7 >= p3 & p6 + p7 >= p3 & p6 + p9 >= p3 & p2 >= p3 & p8 >= p3 OR p3 > 0 & p4 + p7 >= p3 & p2 >= p3 & p2 >= p4 & p4 + p9 >= p3 & p4 > 0 & p7 > 0 & p1 > 0 & p5 > 0 & p9 > 0 & p8 >= p4 & p1 + p9 >= p3 & p5 + p9 >= p3 & p1 + p7 >= p3 & p5 + p7 >= p3 & p8 >= p3 & p6 >= p4 This good constraint is exact (sound and complete)  Result written to file '/home/royal/Desktop/experiments/Etienne/8/CUBPTA1/NZCUBtransdist.res'. IMITATOR successfully terminated (after 1.544 seconds)