************************************************************ * 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/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/4/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/4/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/4/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. 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: 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… - 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. Computing post^2 from 3 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.277 seconds.  Fixpoint reached at a depth of 3: 4 states with 3 transitions in the final state space.  [NZCUB] Algorithm completed after 1.277 seconds. 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.302 seconds. Starting running algorithm NZCUB…  Computing post^1 from 1 state. Computing post^2 from 6 states. Computing post^2 from 2 states. Computing post^3 from 2 states. Computing post^4 from 2 states.  [NZCUB] Found a cycle.  2 states merged within 6 states.  [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.319 seconds. Computing post^3 from 4 states. Starting running algorithm NZCUB…  Computing post^1 from 1 state. Computing post^2 from 6 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!  2 states merged within 6 states. Computing post^3 from 4 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: 17 states with 28 transitions in the final state space.  [NZCUB] Algorithm completed after 1.348 seconds. Computing post^4 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 4 states.  [NZCUB] Found a cycle.  [NZCUB] Non-Zeno cycle found! Computing post^3 from 4 states.  [NZCUB] Found a cycle.  [NZCUB] Non-Zeno cycle found!  [NZCUB] Found a cycle.  [NZCUB] Non-Zeno cycle found! Computing post^4 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.373 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!  Fixpoint reached at a depth of 5: 13 states with 16 transitions in the final state space.  [NZCUB] Algorithm completed after 1.379 seconds. 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.382 seconds. Starting running algorithm NZCUB…  Computing post^1 from 1 state. Starting running algorithm NZCUB…  Computing post^1 from 1 state. Computing post^2 from 1 state. Computing post^3 from 2 states. Computing post^4 from 1 state. Computing post^2 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.398 seconds.  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 4 states. Computing post^4 from 6 states.  [NZCUB] Found a cycle.  [NZCUB] Non-Zeno cycle found! Computing post^3 from 4 states.  [NZCUB] Found a cycle.  [NZCUB] Non-Zeno cycle found!  [NZCUB] Found a cycle.  [NZCUB] Non-Zeno cycle found! Computing post^4 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.438 seconds.  [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.  [NZCUB] Algorithm completed after 1.439 seconds. Starting running algorithm NZCUB…  Computing post^1 from 1 state. Computing post^2 from 2 states. Computing post^3 from 2 states. Computing post^4 from 2 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.  Fixpoint reached at a depth of 5: 7 states with 8 transitions in the final state space.  [NZCUB] Algorithm completed after 1.466 seconds. Computing post^3 from 2 states. Starting running algorithm NZCUB…  Computing post^4 from 2 states. Computing post^1 from 1 state.  [NZCUB] Found a cycle.  [NZCUB] Non-Zeno cycle found! Computing post^2 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.477 seconds. 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.497 seconds. Computing post^2 from 1 state. Computing post^3 from 2 states. Computing post^4 from 1 state.  [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.507 seconds. Starting running algorithm NZCUB…  Computing post^1 from 1 state. Computing post^2 from 1 state. Computing post^3 from 2 states. Computing post^4 from 1 state.  [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.530 seconds. Starting running algorithm NZCUB…  Computing post^1 from 1 state. Computing post^2 from 4 states. Computing post^3 from 2 states. Starting running algorithm NZCUB…  Computing post^1 from 1 state. Computing post^2 from 2 states. Computing post^3 from 1 state. Computing post^4 from 4 states.  [NZCUB] Found a cycle.  [NZCUB] Non-Zeno cycle found! Computing post^4 from 2 states.  [NZCUB] Found a cycle.  [NZCUB] Non-Zeno cycle found!  [NZCUB] Found a cycle.  Fixpoint reached at a depth of 5: 11 states with 12 transitions in the final state space.  [NZCUB] Algorithm completed after 1.555 seconds.  [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.556 seconds. Starting running algorithm NZCUB…  Computing post^1 from 1 state. Computing post^2 from 1 state. Computing post^3 from 1 state. 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.598 seconds. IMITATOR successfully terminated (after 1.599 seconds) IMITATOR successfully terminated (after 1.622 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.  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 2.330 seconds. IMITATOR successfully terminated (after 2.351 seconds)  Final constraint such that the system is correct:  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 OR p3 > 0 & p5 > 0 & p6 > 0 & p7 > 0 & p1 > p5 & p4 > p6 & p2 >= p3 & p6 + p7 >= p3 & p5 + p7 >= p3 & p8 >= p3 & p9 >= p7 OR p3 > 0 & p6 > 0 & p7 > 0 & p4 > p2 & p1 > p5 & p2 >= p3 & p5 > 0 & p5 + p7 >= p3 & p6 + p7 >= p3 & p8 >= p3 & p9 >= p7 OR p1 + p9 >= p3 & p3 > 0 & p7 > p9 & p9 > 0 & p4 > p2 & p5 > 0 & p6 > 0 & p6 + p9 >= p3 & p5 + p9 >= p3 & p1 > 0 & p2 >= p3 & p8 >= p2 OR p1 + p9 >= p3 & p3 > 0 & p4 > p6 & p6 > 0 & p7 > p9 & p9 > 0 & p5 > 0 & p6 + p9 >= p3 & p5 + p9 >= p3 & p1 > 0 & p2 >= p3 & p8 >= p2 OR p6 + p7 >= p3 & p1 + p7 >= p3 & p3 > 0 & p6 > 0 & p1 > 0 & p4 > p2 & p9 > 0 & p2 > p8 & p6 + p9 >= p3 & p1 + p9 >= p3 & p7 > 0 & p8 >= p3 & p5 >= p1 OR p6 + p7 >= p3 & p1 + p7 >= p3 & p3 > 0 & p4 > p6 & p6 > 0 & p1 > 0 & p9 > 0 & p2 > p8 & p6 + p9 >= p3 & p1 + p9 >= p3 & p7 > 0 & p8 >= p3 & p5 >= p1 OR p1 > 0 & p1 + p7 >= p3 & p2 >= p3 & p3 > 0 & p6 > 0 & p7 > 0 & p9 >= p7 & p6 + p7 >= p3 & p4 > p2 & p8 >= p2 & p5 >= p1 OR p1 > 0 & p1 + p7 >= p3 & p2 >= p3 & p3 > 0 & p4 > p6 & p6 > 0 & p7 > 0 & p9 >= p7 & p6 + p7 >= p3 & p8 >= p2 & p5 >= p1 OR p1 > p5 & p2 > p8 & p3 > 0 & p4 > p6 & p5 > 0 & p6 > 0 & p7 > p9 & p9 > 0 & p5 + p9 >= p3 & p6 + p9 >= p3 & p8 >= p3 OR p1 > p5 & p2 > p8 & p3 > 0 & p5 > 0 & p6 > 0 & p7 > p9 & p9 > 0 & p5 + p9 >= p3 & p6 + p9 >= p3 & p8 >= p3 & p4 > p2 This good constraint is exact (sound and complete)  Result written to file '/home/royal/Desktop/experiments/Etienne/4/CUBPTA1/NZCUBtransdist.res'. IMITATOR successfully terminated (after 2.363 seconds)