************************************************************ * 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/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/6/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/6/CUBPTA1/CUBPTA1.imi ************************************************************ * 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 * ************************************************************ 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 * ************************************************************ Merging technique of [AFS13] enabled. The result will be written to a file. Model: /home/royal/Desktop/experiments/Etienne/6/CUBPTA1/CUBPTA1.imi Model: /home/royal/Desktop/experiments/Etienne/6/CUBPTA1/CUBPTA1.imi Mode: parametric non-Zeno emptiness checking (CUB transformation), distributed version. 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. ************************************************************ * 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 {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} Model: /home/royal/Desktop/experiments/Etienne/6/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. Generating the transformed model… 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… 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…  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.349 seconds.  Automaton name: pta, Number of models: 20  Transformation completed Starting running algorithm NZCUB…  Computing post^1 from 1 state. Computing post^2 from 6 states.  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 2 states. Computing post^3 from 2 states. 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.402 seconds. Computing post^4 from 2 states. 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.407 seconds.  [NZCUB] Found a cycle.  [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.409 seconds. Starting running algorithm NZCUB…  Computing post^1 from 1 state. Computing post^2 from 6 states. Starting running algorithm NZCUB…  Computing post^1 from 1 state.  2 states merged within 6 states. Computing post^2 from 4 states. Starting running algorithm NZCUB…  Computing post^1 from 1 state. Computing post^3 from 4 states.  Automaton name: pta, Number of models: 20  Transformation completed  2 states merged within 6 states. Computing post^3 from 4 states. 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.432 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^4 from 1 state. Computing post^4 from 4 states. Computing post^4 from 6 states.  [NZCUB] Found a cycle.  [NZCUB] Non-Zeno cycle found!  Fixpoint reached at a depth of 5: 5 states with 6 transitions in the final state space.  [NZCUB] Algorithm completed after 1.445 seconds.  [NZCUB] Found a cycle.  [NZCUB] Non-Zeno cycle found!  [NZCUB] Found a cycle. Starting running algorithm NZCUB…  Computing post^1 from 1 state.  [NZCUB] Non-Zeno cycle found! Computing post^4 from 6 states.  [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: 13 states with 16 transitions in the final state space. Computing post^2 from 6 states.  [NZCUB] Algorithm completed after 1.451 seconds. Computing post^2 from 6 states.  [NZCUB] Found a cycle.  [NZCUB] Found a cycle. Starting running algorithm NZCUB…  Computing post^1 from 1 state.  [NZCUB] Non-Zeno cycle found!  [NZCUB] Non-Zeno cycle found! Computing post^2 from 4 states.  [NZCUB] Found a cycle.  [NZCUB] Non-Zeno cycle found!  [NZCUB] Found a cycle.  2 states merged within 6 states.  [NZCUB] Non-Zeno cycle found! Computing post^3 from 4 states.  Fixpoint reached at a depth of 5: 17 states with 28 transitions in the final state space.  [NZCUB] Algorithm completed after 1.461 seconds. Computing post^3 from 4 states.  [NZCUB] Found a cycle.  [NZCUB] Non-Zeno cycle found! Starting running algorithm NZCUB…  Computing post^1 from 1 state. Computing post^4 from 4 states. Computing post^2 from 2 states. Computing post^4 from 6 states.  [NZCUB] Found a cycle.  [NZCUB] Non-Zeno cycle found!  [NZCUB] Found a cycle. Computing post^3 from 2 states.  2 states merged within 6 states.  [NZCUB] Found a cycle.  [NZCUB] Non-Zeno cycle found!  [NZCUB] Non-Zeno cycle found!  [NZCUB] Found a cycle.  [NZCUB] Non-Zeno cycle found! Computing post^3 from 4 states. Computing post^4 from 2 states.  [NZCUB] Found a cycle.  Fixpoint reached at a depth of 5: 13 states with 16 transitions in the final state space.  [NZCUB] Algorithm completed after 1.482 seconds.  [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.483 seconds.  [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: 7 states with 8 transitions in the final state space.  [NZCUB] Algorithm completed after 1.486 seconds.  [NZCUB] Found a cycle.  [NZCUB] Non-Zeno cycle found! Computing post^4 from 6 states.  Fixpoint reached at a depth of 5: 17 states with 28 transitions in the final state space.  [NZCUB] Algorithm completed after 1.502 seconds. Starting running algorithm NZCUB…  Computing post^1 from 1 state.  [NZCUB] Found a cycle. Computing post^2 from 2 states. Starting running algorithm NZCUB…   [NZCUB] Non-Zeno cycle found! Computing post^1 from 1 state. Computing post^3 from 2 states.  [NZCUB] Found a cycle.  [NZCUB] Non-Zeno cycle found! Computing post^2 from 4 states. Computing post^4 from 2 states.  [NZCUB] Found a cycle. Computing post^3 from 2 states.  [NZCUB] Non-Zeno cycle found!  [NZCUB] Found a cycle.  [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.515 seconds. Starting running algorithm NZCUB…  Computing post^1 from 1 state.  [NZCUB] Found a cycle.  [NZCUB] Non-Zeno cycle found! 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.517 seconds. Computing post^4 from 4 states.  [NZCUB] Found a cycle.  [NZCUB] Non-Zeno cycle found! Starting running algorithm NZCUB…  Computing post^1 from 1 state. Computing post^3 from 2 states.  [NZCUB] Found a cycle. Computing post^2 from 1 state.  [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.526 seconds. Computing post^4 from 1 state. Computing post^3 from 2 states. Computing post^4 from 1 state.  [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: 5 states with 6 transitions in the final state space.  [NZCUB] Algorithm completed after 1.537 seconds.  Fixpoint reached at a depth of 5: 5 states with 6 transitions in the final state space.  [NZCUB] Algorithm completed after 1.537 seconds. Starting running algorithm NZCUB…  Computing post^1 from 1 state. Computing post^2 from 4 states. Computing post^3 from 2 states. Computing post^4 from 4 states.  [NZCUB] Found a cycle.  [NZCUB] Non-Zeno cycle found!  [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: 11 states with 12 transitions in the final state space.  [NZCUB] Algorithm completed after 1.563 seconds. Computing post^2 from 2 states. Computing post^3 from 1 state. Starting running algorithm NZCUB…  Computing post^1 from 1 state. Computing post^4 from 2 states. Computing post^2 from 1 state.  [NZCUB] Found a cycle. Computing post^3 from 1 state.  [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.572 seconds. Computing post^4 from 1 state.  [NZCUB] Found a cycle. IMITATOR successfully terminated (after 1.578 seconds)  [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.581 seconds. IMITATOR successfully terminated (after 1.588 seconds) IMITATOR successfully terminated (after 1.627 seconds) IMITATOR successfully terminated (after 1.627 seconds) IMITATOR successfully terminated (after 1.633 seconds)  Final constraint such that the system is correct:  p4 > 0 & p3 > 0 & p4 + p9 >= p3 & p4 + p7 >= p3 & p7 > 0 & p1 + p7 >= p3 & p5 + p7 >= p3 & p1 > 0 & p5 > 0 & p9 > 0 & p2 >= p4 & p8 >= p4 & p1 + p9 >= p3 & p5 + p9 >= p3 & p2 >= p3 & p8 >= p3 & p6 >= p4 OR p2 >= p3 & p3 > 0 & p7 > 0 & p4 > p6 & p6 > 0 & p5 > 0 & p9 > 0 & p1 > 0 & p5 + p9 >= p3 & p5 + p7 >= p3 & p1 + p7 >= p3 & p1 + p9 >= p3 & p6 + p7 >= p3 & p6 + p9 >= p3 & p8 >= p3 OR p3 > 0 & p2 >= p3 & p6 > 0 & p5 > 0 & p4 > p2 & p9 > 0 & p1 > 0 & p7 > 0 & p6 + p9 >= p3 & p1 + p9 >= p3 & p1 + p7 >= p3 & p6 + p7 >= p3 & p5 + p7 >= p3 & p5 + p9 >= p3 & p8 >= p3 This good constraint is exact (sound and complete)  Result written to file '/home/royal/Desktop/experiments/Etienne/6/CUBPTA1/NZCUBtransdist.res'. IMITATOR successfully terminated (after 1.631 seconds)