************************************************************ * 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/Sched5/Sched5.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 * ************************************************************ ************************************************************ * 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/Sched5/Sched5.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. Model: /home/royal/Desktop/experiments/Etienne/8/Sched5/Sched5.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/Sched5/Sched5.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/Sched5/Sched5.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 * ************************************************************ ************************************************************ * 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/Sched5/Sched5.imi Mode: parametric non-Zeno emptiness checking (CUB transformation), distributed version. Considering fixpoint variant with monodirectional inclusion of symbolic zones (instead of equality). Model: /home/royal/Desktop/experiments/Etienne/8/Sched5/Sched5.imi Mode: parametric non-Zeno emptiness checking (CUB transformation), distributed version. 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 * ************************************************************ Model: /home/royal/Desktop/experiments/Etienne/8/Sched5/Sched5.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. The model contains stopwatches. Generating the transformed model… The model contains stopwatches. Generating the transformed model… The model contains stopwatches. Generating the transformed model… The model contains stopwatches. Generating the transformed model… The model contains stopwatches. Generating the transformed model… The model contains stopwatches. Generating the transformed model… The model contains stopwatches. Generating the transformed model… The model contains stopwatches. Generating the transformed model…  Automaton name: Task_t1, Number of models: 5 Automaton name: Periodic_t1_arr, Number of models: 1 Automaton name: Task_t2, Number of models: 2 Automaton name: Periodic_t2_arr, Number of models: 1 Automaton name: Task_t3, Number of models: 2 Automaton name: Periodic_t3_arr, Number of models: 1 Automaton name: Task_t4, Number of models: 2 Automaton name: Periodic_t4_arr, Number of models: 1 Automaton name: Task_t5, Number of models: 2 Automaton name: Periodic_t5_arr, Number of models: 1 Automaton name: sched_CPU1, Number of models: 1 Automaton name: OBS_dline, Number of models: 1  Transformation completed  Automaton name: Task_t1, Number of models: 5 Automaton name: Periodic_t1_arr, Number of models: 1 Automaton name: Task_t2, Number of models: 2 Automaton name: Periodic_t2_arr, Number of models: 1 Automaton name: Task_t3, Number of models: 2 Automaton name: Periodic_t3_arr, Number of models: 1 Automaton name: Task_t4, Number of models: 2 Automaton name: Periodic_t4_arr, Number of models: 1 Automaton name: Task_t5, Number of models: 2 Automaton name: Periodic_t5_arr, Number of models: 1 Automaton name: sched_CPU1, Number of models: 1 Automaton name: OBS_dline, Number of models: 1  Transformation completed  Automaton name: Task_t1, Number of models: 5 Automaton name: Periodic_t1_arr, Number of models: 1 Automaton name: Task_t2, Number of models: 2 Automaton name: Periodic_t2_arr, Number of models: 1 Automaton name: Task_t3, Number of models: 2 Automaton name: Periodic_t3_arr, Number of models: 1 Automaton name: Task_t4, Number of models: 2 Automaton name: Periodic_t4_arr, Number of models: 1 Automaton name: Task_t5, Number of models: 2 Automaton name: Periodic_t5_arr, Number of models: 1 Automaton name: sched_CPU1, Number of models: 1 Automaton name: OBS_dline, Number of models: 1  Transformation completed  Automaton name: Task_t1, Number of models: 5 Automaton name: Periodic_t1_arr, Number of models: 1 Automaton name: Task_t2, Number of models: 2 Automaton name: Periodic_t2_arr, Number of models: 1 Automaton name: Task_t3, Number of models: 2 Automaton name: Periodic_t3_arr, Number of models: 1 Automaton name: Task_t4, Number of models: 2 Automaton name: Periodic_t4_arr, Number of models: 1 Automaton name: Task_t5, Number of models: 2 Automaton name: Periodic_t5_arr, Number of models: 1 Automaton name: sched_CPU1, Number of models: 1 Automaton name: OBS_dline, Number of models: 1  Transformation completed  Automaton name: Task_t1, Number of models: 5 Automaton name: Periodic_t1_arr, Number of models: 1 Automaton name: Task_t2, Number of models: 2 Automaton name: Periodic_t2_arr, Number of models: 1 Automaton name: Task_t3, Number of models: 2 Automaton name: Periodic_t3_arr, Number of models: 1 Automaton name: Task_t4, Number of models: 2 Automaton name: Periodic_t4_arr, Number of models: 1 Automaton name: Task_t5, Number of models: 2 Automaton name: Periodic_t5_arr, Number of models: 1 Automaton name: sched_CPU1, Number of models: 1 Automaton name: OBS_dline, Number of models: 1  Transformation completed  Automaton name: Task_t1, Number of models: 5 Automaton name: Periodic_t1_arr, Number of models: 1 Automaton name: Task_t2, Number of models: 2 Automaton name: Periodic_t2_arr, Number of models: 1 Automaton name: Task_t3, Number of models: 2 Automaton name: Periodic_t3_arr, Number of models: 1 Automaton name: Task_t4, Number of models: 2 Automaton name: Periodic_t4_arr, Number of models: 1 Automaton name: Task_t5, Number of models: 2 Automaton name: Periodic_t5_arr, Number of models: 1 Automaton name: sched_CPU1, Number of models: 1 Automaton name: OBS_dline, Number of models: 1  Transformation completed Starting running algorithm NZCUB…  Starting running algorithm NZCUB…  Starting running algorithm NZCUB…  Starting running algorithm NZCUB…  Computing post^1 from 1 state. Computing post^1 from 1 state. Computing post^1 from 1 state. Computing post^1 from 1 state. Starting running algorithm NZCUB…  Computing post^1 from 1 state. Computing post^2 from 7 states. Computing post^2 from 8 states. Computing post^2 from 9 states. Computing post^2 from 8 states.  Automaton name: Task_t1, Number of models: 5 Automaton name: Periodic_t1_arr, Number of models: 1 Automaton name: Task_t2, Number of models: 2 Automaton name: Periodic_t2_arr, Number of models: 1 Automaton name: Task_t3, Number of models: 2 Automaton name: Periodic_t3_arr, Number of models: 1 Automaton name: Task_t4, Number of models: 2 Automaton name: Periodic_t4_arr, Number of models: 1 Automaton name: Task_t5, Number of models: 2 Automaton name: Periodic_t5_arr, Number of models: 1 Automaton name: sched_CPU1, Number of models: 1 Automaton name: OBS_dline, Number of models: 1  Transformation completed Starting running algorithm NZCUB…  Computing post^1 from 1 state. Computing post^2 from 8 states.  Automaton name: Task_t1, Number of models: 5 Automaton name: Periodic_t1_arr, Number of models: 1 Automaton name: Task_t2, Number of models: 2 Automaton name: Periodic_t2_arr, Number of models: 1 Automaton name: Task_t3, Number of models: 2 Automaton name: Periodic_t3_arr, Number of models: 1 Automaton name: Task_t4, Number of models: 2 Automaton name: Periodic_t4_arr, Number of models: 1 Automaton name: Task_t5, Number of models: 2 Automaton name: Periodic_t5_arr, Number of models: 1 Automaton name: sched_CPU1, Number of models: 1 Automaton name: OBS_dline, Number of models: 1  Transformation completed Starting running algorithm NZCUB…  Computing post^1 from 1 state. Computing post^2 from 7 states. Computing post^2 from 7 states. Computing post^3 from 21 states. Computing post^3 from 28 states. Computing post^3 from 28 states. Computing post^3 from 28 states. Computing post^3 from 21 states. Computing post^3 from 35 states. Computing post^3 from 21 states. Computing post^4 from 35 states. Computing post^4 from 35 states. Computing post^4 from 35 states. Computing post^4 from 57 states. Computing post^4 from 57 states. Computing post^4 from 57 states. Computing post^4 from 78 states. Computing post^5 from 35 states. Computing post^5 from 35 states. Computing post^5 from 35 states. Computing post^6 from 21 states. Computing post^6 from 21 states. Computing post^6 from 21 states. Computing post^5 from 76 states. Computing post^5 from 76 states. Computing post^5 from 76 states. Computing post^7 from 7 states. Computing post^7 from 7 states. Computing post^8 from 1 state.  Fixpoint reached at a depth of 9: 128 states with 448 transitions in the final state space.  [NZCUB] Algorithm completed after 24.981 seconds. Starting running algorithm NZCUB…  Computing post^1 from 1 state. Computing post^7 from 7 states. Computing post^2 from 8 states. Computing post^8 from 1 state.  Fixpoint reached at a depth of 9: 128 states with 448 transitions in the final state space.  [NZCUB] Algorithm completed after 25.076 seconds. Starting running algorithm NZCUB…  Computing post^1 from 1 state. Computing post^2 from 10 states. Computing post^8 from 1 state.  Fixpoint reached at a depth of 9: 128 states with 448 transitions in the final state space.  [NZCUB] Algorithm completed after 25.171 seconds. Starting running algorithm NZCUB…  Computing post^1 from 1 state. Computing post^2 from 9 states. Computing post^3 from 28 states. Computing post^5 from 111 states. Computing post^3 from 44 states. Computing post^3 from 36 states. Computing post^4 from 57 states. Computing post^6 from 75 states. Computing post^4 from 86 states. Computing post^6 from 76 states. Computing post^6 from 76 states. Computing post^4 from 114 states. Computing post^5 from 76 states. Computing post^7 from 71 states. Computing post^6 from 111 states. Computing post^7 from 77 states. Computing post^7 from 77 states. Computing post^5 from 140 states. Computing post^6 from 76 states. Computing post^8 from 79 states. Computing post^5 from 197 states. Computing post^7 from 98 states. Computing post^8 from 94 states. Computing post^8 from 94 states. Computing post^7 from 77 states. Computing post^9 from 82 states. Computing post^6 from 177 states. Computing post^8 from 94 states. Computing post^8 from 101 states. Computing post^9 from 102 states. Computing post^9 from 102 states. Computing post^10 from 61 states. Computing post^11 from 29 states. Computing post^10 from 76 states. Computing post^12 from 8 states. Computing post^9 from 103 states. Computing post^9 from 102 states. Computing post^10 from 76 states. Computing post^13 from 1 state.  Fixpoint reached at a depth of 14: 576 states with 2336 transitions in the final state space.  [NZCUB] Algorithm completed after 38.031 seconds. Starting running algorithm NZCUB…  Computing post^1 from 1 state. Computing post^2 from 8 states. Computing post^3 from 28 states. Computing post^7 from 216 states. Computing post^6 from 254 states. Computing post^4 from 57 states. Computing post^11 from 35 states. Computing post^11 from 35 states. Computing post^10 from 76 states. Computing post^10 from 76 states. Computing post^5 from 76 states. Computing post^12 from 9 states. Computing post^12 from 9 states. Computing post^13 from 1 state.  Fixpoint reached at a depth of 14: 640 states with 2720 transitions in the final state space.  [NZCUB] Algorithm completed after 41.332 seconds. Starting running algorithm NZCUB…  Computing post^1 from 1 state. Computing post^13 from 1 state.  Fixpoint reached at a depth of 14: 640 states with 2720 transitions in the final state space.  [NZCUB] Algorithm completed after 41.441 seconds. Starting running algorithm NZCUB…  Computing post^1 from 1 state. Computing post^2 from 8 states. Computing post^2 from 8 states. Computing post^3 from 28 states. Computing post^3 from 28 states. Computing post^6 from 76 states. Computing post^4 from 57 states. Computing post^4 from 57 states. Computing post^11 from 35 states. Computing post^11 from 35 states. Computing post^12 from 9 states. Computing post^5 from 76 states. Computing post^5 from 76 states. Computing post^13 from 1 state.  Fixpoint reached at a depth of 14: 640 states with 2720 transitions in the final state space.  [NZCUB] Algorithm completed after 44.499 seconds. Starting running algorithm NZCUB…  Computing post^1 from 1 state. Computing post^12 from 9 states. Computing post^2 from 10 states. Computing post^7 from 77 states. Computing post^13 from 1 state.  Fixpoint reached at a depth of 14: 768 states with 3280 transitions in the final state space.  [NZCUB] Algorithm completed after 44.908 seconds. Starting running algorithm NZCUB…  Computing post^1 from 1 state. Computing post^3 from 44 states. Computing post^2 from 9 states. Computing post^3 from 36 states. Computing post^6 from 76 states. Computing post^6 from 76 states. Computing post^7 from 299 states. Computing post^4 from 114 states. Computing post^4 from 86 states. Computing post^8 from 94 states. Computing post^8 from 290 states. Computing post^7 from 77 states. Computing post^7 from 77 states. Computing post^5 from 140 states. Computing post^5 from 197 states. Computing post^9 from 102 states. Computing post^8 from 94 states. Computing post^8 from 94 states. Computing post^6 from 177 states. Computing post^10 from 76 states. Computing post^9 from 102 states. Computing post^9 from 102 states. Computing post^8 from 388 states. Computing post^6 from 254 states. Computing post^11 from 35 states. Computing post^12 from 9 states. Computing post^10 from 76 states. Computing post^13 from 1 state.  Fixpoint reached at a depth of 14: 640 states with 2720 transitions in the final state space.  [NZCUB] Algorithm completed after 56.741 seconds. Starting running algorithm NZCUB…  Computing post^1 from 1 state. Computing post^9 from 367 states. Computing post^2 from 9 states. Computing post^10 from 76 states. Computing post^3 from 36 states. Computing post^7 from 216 states. Computing post^4 from 86 states. Computing post^11 from 35 states. Computing post^11 from 35 states. Computing post^12 from 9 states. Computing post^13 from 1 state.  Fixpoint reached at a depth of 14: 640 states with 2720 transitions in the final state space.  [NZCUB] Algorithm completed after 60.101 seconds. Starting running algorithm NZCUB…  Computing post^1 from 1 state. Computing post^2 from 9 states. Computing post^12 from 9 states. Computing post^13 from 1 state.  Fixpoint reached at a depth of 14: 640 states with 2720 transitions in the final state space.  [NZCUB] Algorithm completed after 60.559 seconds. Starting running algorithm NZCUB…  Computing post^1 from 1 state. Computing post^3 from 36 states. Computing post^5 from 140 states. Computing post^2 from 9 states. Computing post^3 from 36 states. Computing post^4 from 86 states. Computing post^4 from 86 states. Computing post^7 from 299 states. Computing post^5 from 140 states. Computing post^6 from 178 states. Computing post^5 from 140 states. Computing post^8 from 290 states. Computing post^6 from 178 states. Computing post^6 from 178 states. Computing post^10 from 373 states. Computing post^7 from 223 states. Computing post^9 from 497 states. Computing post^8 from 388 states. Computing post^7 from 223 states. Computing post^7 from 223 states. Computing post^9 from 367 states. Computing post^8 from 311 states. Computing post^11 from 321 states. Computing post^8 from 311 states. Computing post^8 from 311 states. Computing post^9 from 497 states. Computing post^10 from 373 states. Computing post^10 from 515 states. Computing post^9 from 403 states. Computing post^12 from 312 states. Computing post^9 from 403 states. Computing post^9 from 403 states. Computing post^11 from 321 states. Computing post^13 from 350 states. Computing post^10 from 413 states. Computing post^11 from 437 states. Computing post^10 from 515 states. Computing post^10 from 413 states. Computing post^10 from 413 states. Computing post^12 from 312 states. Computing post^14 from 318 states. Computing post^11 from 361 states. Computing post^12 from 405 states. Computing post^15 from 188 states. Computing post^13 from 350 states. Computing post^11 from 361 states. Computing post^11 from 437 states. Computing post^11 from 361 states. Computing post^16 from 63 states. Computing post^17 from 9 states.  Fixpoint reached at a depth of 18: 3256 states with 14924 transitions in the final state space.  [NZCUB] Algorithm completed after 129.772 seconds. Starting running algorithm NZCUB…  Computing post^1 from 1 state. Computing post^2 from 11 states. Computing post^3 from 54 states. Computing post^14 from 318 states. Computing post^12 from 370 states. Computing post^4 from 159 states. Computing post^13 from 441 states. Computing post^12 from 370 states. Computing post^12 from 370 states. Computing post^5 from 320 states. Computing post^12 from 405 states. Computing post^15 from 188 states. Computing post^16 from 63 states. Computing post^13 from 432 states. Computing post^13 from 432 states. Computing post^17 from 9 states. Computing post^14 from 393 states.  Fixpoint reached at a depth of 18: 3256 states with 14924 transitions in the final state space.  [NZCUB] Algorithm completed after 148.432 seconds. Starting running algorithm NZCUB…  Computing post^1 from 1 state. Computing post^13 from 432 states. Computing post^2 from 10 states. Computing post^3 from 45 states. Computing post^6 from 491 states. Computing post^4 from 123 states. Computing post^13 from 441 states. Computing post^5 from 234 states. Computing post^14 from 392 states. Computing post^15 from 226 states. Computing post^14 from 392 states. Computing post^14 from 392 states. Computing post^6 from 350 states. Computing post^14 from 393 states. Computing post^16 from 73 states. Computing post^17 from 10 states. Computing post^7 from 676 states.  Fixpoint reached at a depth of 18: 4304 states with 20656 transitions in the final state space.  [NZCUB] Algorithm completed after 169.075 seconds. Starting running algorithm NZCUB…  Computing post^1 from 1 state. Computing post^2 from 8 states. Computing post^3 from 28 states. Computing post^4 from 57 states. Computing post^15 from 226 states. Computing post^5 from 76 states. Computing post^6 from 76 states. Computing post^15 from 226 states. Computing post^7 from 490 states. Computing post^15 from 226 states. Computing post^7 from 77 states. Computing post^15 from 226 states. Computing post^16 from 73 states. Computing post^8 from 94 states. Computing post^16 from 73 states. Computing post^17 from 10 states. Computing post^16 from 73 states.  Fixpoint reached at a depth of 18: 3664 states with 17376 transitions in the final state space.  [NZCUB] Algorithm completed after 181.832 seconds. Starting running algorithm NZCUB…  Computing post^1 from 1 state. Computing post^2 from 8 states. Computing post^16 from 73 states. Computing post^9 from 102 states. Computing post^17 from 10 states. Computing post^3 from 28 states.  Fixpoint reached at a depth of 18: 3664 states with 17376 transitions in the final state space.  [NZCUB] Algorithm completed after 183.568 seconds. Starting running algorithm NZCUB…  Computing post^1 from 1 state. Computing post^17 from 10 states. Computing post^4 from 57 states. Computing post^2 from 8 states.  Fixpoint reached at a depth of 18: 3664 states with 17376 transitions in the final state space.  [NZCUB] Algorithm completed after 184.825 seconds. Starting running algorithm NZCUB…  Computing post^1 from 1 state. Computing post^3 from 28 states. Computing post^17 from 10 states. Computing post^2 from 10 states. Computing post^5 from 76 states. Computing post^4 from 57 states.  Fixpoint reached at a depth of 18: 4304 states with 20656 transitions in the final state space.  [NZCUB] Algorithm completed after 186.161 seconds. Computing post^10 from 76 states. Starting running algorithm NZCUB…  Computing post^1 from 1 state. Computing post^3 from 44 states. Computing post^2 from 9 states. Computing post^5 from 76 states. Computing post^4 from 114 states. Computing post^3 from 36 states. Computing post^6 from 76 states. Computing post^11 from 35 states. Computing post^4 from 86 states. Computing post^12 from 9 states. Computing post^13 from 1 state.  Fixpoint reached at a depth of 14: 640 states with 2720 transitions in the final state space.  [NZCUB] Algorithm completed after 189.636 seconds. Starting running algorithm NZCUB…  Computing post^1 from 1 state. Computing post^6 from 76 states. Computing post^2 from 9 states. Computing post^7 from 77 states. Computing post^3 from 36 states. Computing post^5 from 197 states. Computing post^4 from 86 states. Computing post^5 from 140 states. Computing post^7 from 77 states. Computing post^8 from 94 states. Computing post^5 from 140 states. Computing post^8 from 94 states. Computing post^8 from 722 states. Computing post^8 from 973 states. Computing post^6 from 177 states. Computing post^9 from 102 states. Computing post^6 from 254 states. Computing post^9 from 102 states. Computing post^6 from 178 states. Computing post^10 from 76 states. Computing post^10 from 76 states. Computing post^7 from 216 states. Computing post^11 from 35 states. Computing post^12 from 9 states. Computing post^13 from 1 state.  Fixpoint reached at a depth of 14: 640 states with 2720 transitions in the final state space.  [NZCUB] Algorithm completed after 201.884 seconds. Starting running algorithm NZCUB…  Computing post^1 from 1 state. Computing post^2 from 9 states. Computing post^11 from 35 states. Computing post^3 from 36 states. Computing post^12 from 9 states. Computing post^7 from 223 states. Computing post^13 from 1 state.  Fixpoint reached at a depth of 14: 640 states with 2720 transitions in the final state space.  [NZCUB] Algorithm completed after 203.420 seconds. Starting running algorithm NZCUB…  Computing post^1 from 1 state. Computing post^4 from 86 states. Computing post^2 from 9 states. Computing post^7 from 299 states. Computing post^3 from 36 states. Computing post^4 from 86 states. Computing post^5 from 140 states. Computing post^8 from 290 states. Computing post^5 from 140 states. Computing post^6 from 178 states. Computing post^8 from 311 states. Computing post^6 from 178 states. Computing post^7 from 223 states. Computing post^8 from 388 states. Computing post^7 from 223 states. Computing post^9 from 367 states. Computing post^8 from 311 states. Computing post^9 from 403 states. Computing post^9 from 1028 states. Computing post^8 from 311 states. Computing post^10 from 373 states. Computing post^9 from 497 states. Computing post^9 from 1397 states. Computing post^9 from 403 states. Computing post^10 from 413 states. Computing post^9 from 403 states. Computing post^11 from 321 states. Computing post^10 from 515 states. Computing post^10 from 413 states. Computing post^12 from 312 states. Computing post^10 from 413 states. Computing post^11 from 361 states. Computing post^13 from 350 states. Computing post^12 from 370 states. Computing post^11 from 361 states. Computing post^11 from 437 states. Computing post^11 from 361 states. Computing post^10 from 1255 states. Computing post^14 from 318 states. Computing post^12 from 370 states. Computing post^12 from 370 states. Computing post^13 from 432 states. Computing post^12 from 405 states. Computing post^15 from 188 states. Computing post^16 from 63 states. Computing post^13 from 441 states. Computing post^17 from 9 states.  Fixpoint reached at a depth of 18: 3256 states with 14924 transitions in the final state space.  [NZCUB] Algorithm completed after 290.998 seconds. Starting running algorithm NZCUB…  Computing post^1 from 1 state. Computing post^13 from 432 states. Computing post^2 from 11 states. Computing post^14 from 392 states. Computing post^13 from 432 states. Computing post^3 from 54 states. Computing post^4 from 159 states. Computing post^10 from 1740 states. Computing post^5 from 320 states. Computing post^15 from 226 states. Computing post^14 from 392 states. Computing post^14 from 393 states. Computing post^14 from 392 states. Computing post^16 from 73 states. Computing post^6 from 491 states. Computing post^17 from 10 states.  Fixpoint reached at a depth of 18: 3664 states with 17376 transitions in the final state space.  [NZCUB] Algorithm completed after 313.216 seconds. Starting running algorithm NZCUB…  Computing post^1 from 1 state. Computing post^2 from 10 states. Computing post^3 from 45 states. Computing post^15 from 226 states. Computing post^15 from 226 states. Computing post^4 from 123 states. Computing post^15 from 226 states. Computing post^5 from 234 states. Computing post^11 from 1356 states. Computing post^16 from 73 states. Computing post^16 from 73 states. Computing post^16 from 73 states. Computing post^17 from 10 states.  Fixpoint reached at a depth of 18: 3664 states with 17376 transitions in the final state space.  [NZCUB] Algorithm completed after 325.851 seconds. Starting running algorithm NZCUB…  Computing post^1 from 1 state. Computing post^2 from 9 states. Computing post^17 from 10 states. Computing post^6 from 350 states. Computing post^3 from 36 states.  Fixpoint reached at a depth of 18: 4304 states with 20656 transitions in the final state space.  [NZCUB] Algorithm completed after 327.520 seconds. Starting running algorithm NZCUB…  Computing post^1 from 1 state. Computing post^17 from 10 states. Computing post^7 from 676 states.  Fixpoint reached at a depth of 18: 3664 states with 17376 transitions in the final state space.  [NZCUB] Algorithm completed after 328.408 seconds. Starting running algorithm NZCUB…  Computing post^1 from 1 state. Computing post^2 from 9 states. Computing post^4 from 86 states. Computing post^3 from 36 states. Computing post^2 from 9 states. Computing post^3 from 36 states. Computing post^4 from 86 states. Computing post^4 from 86 states. Computing post^5 from 140 states. Computing post^5 from 140 states. Computing post^5 from 140 states. Computing post^6 from 178 states. Computing post^6 from 178 states. Computing post^6 from 178 states. Computing post^7 from 490 states. Computing post^7 from 223 states. Computing post^7 from 223 states. Computing post^7 from 223 states. Computing post^8 from 311 states. Computing post^8 from 311 states. Computing post^8 from 311 states. Computing post^8 from 973 states. Computing post^8 from 722 states. Computing post^9 from 403 states. Computing post^9 from 403 states. Computing post^9 from 403 states. Computing post^11 from 1873 states. Computing post^12 from 1580 states. Computing post^10 from 413 states. Computing post^10 from 413 states. Computing post^10 from 413 states. Computing post^9 from 1028 states. Computing post^11 from 361 states. Computing post^11 from 361 states. Computing post^11 from 361 states. Computing post^9 from 1397 states. Computing post^12 from 370 states. Computing post^12 from 370 states. Computing post^12 from 370 states. Computing post^13 from 432 states. Computing post^13 from 432 states. Computing post^13 from 432 states. Computing post^14 from 392 states. Computing post^14 from 392 states. Computing post^10 from 1255 states. Computing post^14 from 392 states. Computing post^13 from 2029 states. Computing post^15 from 226 states. Computing post^15 from 226 states. Computing post^15 from 226 states. Computing post^12 from 2110 states. Computing post^16 from 73 states. Computing post^16 from 73 states. Computing post^16 from 73 states. Computing post^17 from 10 states.  Fixpoint reached at a depth of 18: 3664 states with 17376 transitions in the final state space.  [NZCUB] Algorithm completed after 448.480 seconds. Computing post^17 from 10 states. Starting running algorithm NZCUB…  Computing post^1 from 1 state.  Fixpoint reached at a depth of 18: 3664 states with 17376 transitions in the final state space.  [NZCUB] Algorithm completed after 449.091 seconds. Starting running algorithm NZCUB…  Computing post^1 from 1 state. Computing post^17 from 10 states. Computing post^2 from 11 states.  Fixpoint reached at a depth of 18: 3664 states with 17376 transitions in the final state space.  [NZCUB] Algorithm completed after 449.941 seconds. Computing post^2 from 10 states. Computing post^3 from 54 states. Starting running algorithm NZCUB…  Computing post^1 from 1 state. Computing post^3 from 45 states. Computing post^2 from 10 states. Computing post^3 from 45 states. Computing post^4 from 159 states. Computing post^4 from 123 states. Computing post^4 from 123 states. Computing post^5 from 234 states. Computing post^5 from 234 states. Computing post^10 from 1740 states. Computing post^5 from 320 states. Computing post^6 from 350 states. Computing post^6 from 351 states. Computing post^6 from 491 states. Computing post^7 from 490 states. Computing post^7 from 498 states. Computing post^11 from 1356 states. Computing post^7 from 676 states. Computing post^8 from 722 states. Computing post^8 from 750 states. Computing post^8 from 973 states. Computing post^9 from 1086 states. Computing post^9 from 1028 states. Computing post^9 from 1397 states. Computing post^10 from 1255 states. Computing post^10 from 1337 states. Computing post^11 from 1356 states. Computing post^10 from 1740 states. Computing post^11 from 1460 states. Computing post^11 from 1873 states. Computing post^14 from 2309 states. Computing post^12 from 1580 states. Computing post^12 from 1749 states. Computing post^12 from 1580 states. Computing post^13 from 2675 states. Computing post^11 from 1873 states. Computing post^12 from 2110 states. Computing post^15 from 2209 states. Computing post^13 from 2029 states. Computing post^13 from 2029 states. Computing post^13 from 2305 states. Computing post^12 from 2110 states. Computing post^13 from 2675 states. Computing post^16 from 1937 states. Computing post^14 from 3076 states. Computing post^14 from 2309 states. Computing post^14 from 2309 states. Computing post^14 from 2644 states. Computing post^13 from 2675 states. Computing post^17 from 1531 states. Computing post^14 from 3076 states. Computing post^18 from 941 states. Computing post^15 from 2209 states. Computing post^15 from 2209 states. Computing post^19 from 369 states. Computing post^15 from 2938 states. Computing post^20 from 65 states.  Fixpoint reached at a depth of 21: 18584 states with 92596 transitions in the final state space.  [NZCUB] Algorithm completed after 1129.152 seconds. Starting running algorithm NZCUB…  Computing post^1 from 1 state. Computing post^15 from 2546 states. Computing post^14 from 3076 states. Computing post^2 from 10 states. Computing post^3 from 45 states. Computing post^4 from 123 states. Computing post^5 from 234 states. Computing post^6 from 351 states. Computing post^16 from 1937 states. Computing post^7 from 498 states. Computing post^16 from 1937 states. Computing post^8 from 750 states. Computing post^15 from 2938 states. Computing post^16 from 2282 states. Computing post^9 from 1086 states. Computing post^17 from 1531 states. Computing post^16 from 2508 states. Computing post^17 from 1531 states. Computing post^15 from 2938 states. Computing post^10 from 1337 states. Computing post^18 from 941 states. Computing post^18 from 941 states. Computing post^19 from 369 states. Computing post^17 from 1840 states. Computing post^20 from 65 states.  Fixpoint reached at a depth of 21: 18584 states with 92596 transitions in the final state space.  [NZCUB] Algorithm completed after 1315.529 seconds. Computing post^19 from 369 states. Starting running algorithm NZCUB…  Computing post^1 from 1 state. Computing post^16 from 2508 states. Computing post^2 from 10 states. Computing post^3 from 45 states. Computing post^20 from 65 states. Computing post^4 from 123 states. Computing post^11 from 1460 states.  Fixpoint reached at a depth of 21: 18584 states with 92596 transitions in the final state space.  [NZCUB] Algorithm completed after 1330.382 seconds. Starting running algorithm NZCUB…  Computing post^1 from 1 state. Computing post^17 from 1913 states. Computing post^5 from 234 states. Computing post^6 from 351 states. Computing post^2 from 12 states. Computing post^3 from 65 states. Computing post^4 from 214 states. Computing post^7 from 498 states. Computing post^5 from 489 states. Computing post^8 from 750 states. Computing post^16 from 2508 states. Computing post^18 from 1129 states. Computing post^6 from 860 states. Computing post^12 from 1749 states. Computing post^18 from 1139 states. Computing post^9 from 1086 states. Computing post^19 from 435 states. Computing post^17 from 1913 states. Computing post^7 from 1331 states. Computing post^20 from 75 states.  Fixpoint reached at a depth of 21: 20900 states with 107020 transitions in the final state space.  [NZCUB] Algorithm completed after 1431.450 seconds. Starting running algorithm NZCUB…  Computing post^1 from 1 state. Computing post^10 from 1337 states. Computing post^19 from 435 states. Computing post^8 from 2066 states. Computing post^2 from 11 states. Computing post^3 from 55 states. Computing post^4 from 169 states. Computing post^5 from 366 states. Computing post^11 from 1460 states. Computing post^6 from 625 states. Computing post^7 from 971 states. Computing post^18 from 1139 states. Computing post^12 from 1749 states. Computing post^8 from 1532 states. Computing post^17 from 1913 states. Computing post^13 from 2305 states. Computing post^19 from 435 states. Computing post^9 from 3205 states. Computing post^20 from 75 states.  Fixpoint reached at a depth of 21: 24564 states with 127660 transitions in the final state space.  [NZCUB] Algorithm completed after 1656.465 seconds. Starting running algorithm NZCUB…  Computing post^1 from 1 state. Computing post^13 from 2305 states. Computing post^9 from 2368 states. Computing post^14 from 2644 states. Computing post^20 from 75 states. Computing post^18 from 1139 states. Computing post^10 from 3274 states. Computing post^19 from 435 states. Computing post^20 from 75 states.  Fixpoint reached at a depth of 21: 24564 states with 127660 transitions in the final state space.  [NZCUB] Algorithm completed after 1827.211 seconds. Starting running algorithm NZCUB…  Computing post^1 from 1 state.  Fixpoint reached at a depth of 21: 24564 states with 127660 transitions in the final state space.  [NZCUB] Algorithm completed after 1863.883 seconds. =================================================================================== = BAD TERMINATION OF ONE OF YOUR APPLICATION PROCESSES = PID 5876 RUNNING AT Royal-VirtualBox = EXIT CODE: 9 = CLEANING UP REMAINING PROCESSES = YOU CAN IGNORE THE BELOW CLEANUP MESSAGES =================================================================================== YOUR APPLICATION TERMINATED WITH THE EXIT STRING: Killed (signal 9) This typically refers to a problem with your application. Please see the FAQ page for debugging suggestions