************************************************************ * 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/flipflop/flipflop.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/flipflop/flipflop.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/flipflop/flipflop.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/flipflop/flipflop.imi Model: /home/royal/Desktop/experiments/Etienne/8/flipflop/flipflop.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 * ************************************************************ 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/flipflop/flipflop.imi Considering fixpoint variant with monodirectional inclusion of symbolic zones (instead of equality). 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. ************************************************************ * 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/flipflop/flipflop.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/flipflop/flipflop.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. Generating the transformed model… Generating the transformed model… Generating the transformed model… Generating the transformed model… Generating the transformed model… Generating the transformed model… Generating the transformed model… Generating the transformed model…  Automaton name: input, Number of models: 4 Automaton name: g1, Number of models: 2 Automaton name: g2, Number of models: 1 Automaton name: g3, Number of models: 1 Automaton name: g4, Number of models: 3 Automaton name: automatically_generated_observer, Number of models: 1  Transformation completed  Automaton name: input, Number of models: 4 Automaton name: g1, Number of models: 2 Automaton name: g2, Number of models: 1 Automaton name: g3, Number of models: 1 Automaton name: g4, Number of models: 3 Automaton name: automatically_generated_observer, Number of models: 1  Transformation completed Starting running algorithm NZCUB…  Computing post^1 from 1 state.  Automaton name: input, Number of models: 4 Automaton name: g1, Number of models: 2 Automaton name: g2, Number of models: 1 Automaton name: g3, Number of models: 1 Automaton name: g4, Number of models: 3 Automaton name: automatically_generated_observer, Number of models: 1  Transformation completed Starting running algorithm NZCUB…  Computing post^1 from 1 state.  Automaton name: input, Number of models: 4 Automaton name: g1, Number of models: 2 Automaton name: g2, Number of models: 1 Automaton name: g3, Number of models: 1 Automaton name: g4, Number of models: 3 Automaton name: automatically_generated_observer, Number of models: 1  Transformation completed Computing post^2 from 7 states. Starting running algorithm NZCUB…   Automaton name: input, Number of models: 4 Automaton name: g1, Number of models: 2 Automaton name: g2, Number of models: 1 Automaton name: g3, Number of models: 1 Automaton name: g4, Number of models: 3 Automaton name: automatically_generated_observer, Number of models: 1  Transformation completed Computing post^1 from 1 state. Starting running algorithm NZCUB…  Computing post^1 from 1 state. Computing post^2 from 10 states.  Automaton name: input, Number of models: 4 Automaton name: g1, Number of models: 2 Automaton name: g2, Number of models: 1 Automaton name: g3, Number of models: 1 Automaton name: g4, Number of models: 3 Automaton name: automatically_generated_observer, Number of models: 1  Transformation completed Computing post^2 from 6 states. Starting running algorithm NZCUB…  Computing post^1 from 1 state. Computing post^2 from 10 states.  Automaton name: input, Number of models: 4 Automaton name: g1, Number of models: 2 Automaton name: g2, Number of models: 1 Automaton name: g3, Number of models: 1 Automaton name: g4, Number of models: 3 Automaton name: automatically_generated_observer, Number of models: 1  Transformation completed Starting running algorithm NZCUB…  Computing post^1 from 1 state. Computing post^2 from 10 states. Computing post^2 from 6 states. Computing post^3 from 20 states. Computing post^3 from 14 states.  Automaton name: input, Number of models: 4 Automaton name: g1, Number of models: 2 Automaton name: g2, Number of models: 1 Automaton name: g3, Number of models: 1 Automaton name: g4, Number of models: 3 Automaton name: automatically_generated_observer, Number of models: 1  Transformation completed Starting running algorithm NZCUB…  Computing post^1 from 1 state. Computing post^3 from 14 states. Computing post^2 from 10 states. Computing post^3 from 38 states. Computing post^3 from 38 states. Computing post^3 from 38 states. Computing post^4 from 16 states. Computing post^4 from 16 states. Computing post^4 from 32 states. Computing post^3 from 38 states. Computing post^5 from 9 states. Computing post^5 from 9 states. Computing post^6 from 2 states.  Fixpoint reached at a depth of 7: 48 states with 128 transitions in the final state space.  [NZCUB] Algorithm completed after 2.736 seconds. Starting running algorithm NZCUB…  Computing post^1 from 1 state. Computing post^2 from 7 states. Computing post^6 from 2 states.  Fixpoint reached at a depth of 7: 48 states with 128 transitions in the final state space.  [NZCUB] Algorithm completed after 2.775 seconds. Starting running algorithm NZCUB…  Computing post^1 from 1 state. Computing post^2 from 5 states. Computing post^3 from 20 states. Computing post^3 from 10 states. Computing post^5 from 35 states. Computing post^4 from 72 states. Computing post^4 from 10 states. Computing post^4 from 72 states. Computing post^5 from 5 states. Computing post^4 from 72 states. Computing post^4 from 31 states. Computing post^6 from 1 state.  Fixpoint reached at a depth of 7: 32 states with 80 transitions in the final state space.  [NZCUB] Algorithm completed after 3.007 seconds. Starting running algorithm NZCUB…  Computing post^1 from 1 state. Computing post^4 from 72 states. Computing post^2 from 9 states. Computing post^3 from 30 states. Computing post^6 from 29 states. Computing post^5 from 30 states. Computing post^7 from 24 states. Computing post^4 from 50 states. Computing post^6 from 20 states. Computing post^5 from 73 states.  4 states merged within 40 states. Computing post^7 from 13 states. Computing post^8 from 36 states. Computing post^5 from 73 states.  2 states merged within 20 states. Computing post^5 from 73 states. Computing post^8 from 18 states. Computing post^5 from 73 states.  4 states merged within 26 states. Computing post^9 from 22 states. Computing post^5 from 45 states. Computing post^9 from 42 states.  4 states merged within 30 states. Computing post^6 from 38 states. Computing post^10 from 26 states. Computing post^6 from 21 states. Computing post^6 from 38 states. Computing post^6 from 38 states. Computing post^6 from 38 states. Computing post^7 from 4 states.  Fixpoint reached at a depth of 8: 160 states with 528 transitions in the final state space.  [NZCUB] Algorithm completed after 4.375 seconds. Computing post^7 from 8 states. Starting running algorithm NZCUB…  Computing post^1 from 1 state.  Fixpoint reached at a depth of 8: 240 states with 832 transitions in the final state space.  [NZCUB] Algorithm completed after 4.391 seconds. Starting running algorithm NZCUB…  Computing post^1 from 1 state. Computing post^2 from 9 states. Computing post^2 from 6 states. Computing post^3 from 15 states. Computing post^7 from 8 states.  Fixpoint reached at a depth of 8: 240 states with 832 transitions in the final state space.  [NZCUB] Algorithm completed after 4.569 seconds. Starting running algorithm NZCUB…  Computing post^1 from 1 state. Computing post^7 from 8 states. Computing post^3 from 30 states.  Fixpoint reached at a depth of 8: 240 states with 832 transitions in the final state space.  [NZCUB] Algorithm completed after 4.583 seconds. Starting running algorithm NZCUB…  Computing post^1 from 1 state. Computing post^7 from 8 states.  Fixpoint reached at a depth of 8: 240 states with 832 transitions in the final state space.  [NZCUB] Algorithm completed after 4.608 seconds.  14 states merged within 56 states. Starting running algorithm NZCUB…  Computing post^1 from 1 state. Computing post^2 from 5 states. Computing post^2 from 9 states. Computing post^2 from 9 states. Computing post^4 from 22 states. Computing post^10 from 42 states. Computing post^3 from 10 states. Computing post^3 from 30 states. Computing post^4 from 10 states. Computing post^3 from 30 states.  2 states merged within 25 states. Computing post^5 from 5 states. Computing post^6 from 1 state. Computing post^5 from 23 states.  Fixpoint reached at a depth of 7: 32 states with 80 transitions in the final state space.  [NZCUB] Algorithm completed after 4.857 seconds. Starting running algorithm NZCUB…  Computing post^1 from 1 state. Computing post^4 from 50 states. Computing post^2 from 6 states. Computing post^3 from 15 states.  1 state merged within 19 states. Computing post^6 from 18 states. Computing post^11 from 56 states. Computing post^4 from 50 states. Computing post^4 from 21 states. Computing post^4 from 50 states.  1 state merged within 18 states. Computing post^7 from 17 states.  1 state merged within 20 states. Computing post^5 from 19 states. Computing post^5 from 45 states. Computing post^8 from 28 states. Computing post^6 from 12 states.  1 state merged within 10 states. Computing post^7 from 9 states. Computing post^5 from 45 states. Computing post^5 from 45 states. Computing post^8 from 14 states. Computing post^6 from 21 states.  9 states merged within 42 states. Computing post^9 from 33 states. Computing post^7 from 4 states.  Fixpoint reached at a depth of 8: 160 states with 528 transitions in the final state space.  [NZCUB] Algorithm completed after 5.861 seconds. Starting running algorithm NZCUB…  Computing post^1 from 1 state.  5 states merged within 22 states. Computing post^2 from 5 states. Computing post^9 from 17 states. Computing post^3 from 10 states. Computing post^6 from 21 states. Computing post^4 from 10 states. Computing post^6 from 21 states. Computing post^7 from 4 states.  Fixpoint reached at a depth of 8: 160 states with 528 transitions in the final state space.  [NZCUB] Algorithm completed after 6.101 seconds. Starting running algorithm NZCUB…  Computing post^1 from 1 state. Computing post^5 from 5 states. Computing post^7 from 4 states.  Fixpoint reached at a depth of 8: 160 states with 528 transitions in the final state space.  [NZCUB] Algorithm completed after 6.128 seconds. Computing post^2 from 9 states. Starting running algorithm NZCUB…  Computing post^1 from 1 state. Computing post^6 from 1 state.  Fixpoint reached at a depth of 7: 32 states with 80 transitions in the final state space.  [NZCUB] Algorithm completed after 6.149 seconds. Starting running algorithm NZCUB…  Computing post^1 from 1 state. Computing post^11 from 74 states. Computing post^2 from 6 states. Computing post^2 from 9 states.  11 states merged within 32 states. Computing post^3 from 15 states. Computing post^10 from 21 states. Computing post^3 from 30 states. Computing post^3 from 30 states. Computing post^4 from 22 states. Computing post^10 from 37 states. Computing post^4 from 50 states. Computing post^5 from 23 states. Computing post^4 from 50 states. Computing post^6 from 18 states. Computing post^7 from 17 states. Computing post^5 from 45 states. Computing post^5 from 45 states.  2 states merged within 28 states. Computing post^8 from 26 states. Computing post^9 from 25 states.  6 states merged within 63 states. Computing post^6 from 21 states. Computing post^6 from 21 states. Computing post^11 from 57 states. Computing post^7 from 4 states.  Fixpoint reached at a depth of 8: 160 states with 528 transitions in the final state space.  [NZCUB] Algorithm completed after 7.392 seconds. Starting running algorithm NZCUB…  Computing post^7 from 4 states. Computing post^1 from 1 state.  Fixpoint reached at a depth of 8: 160 states with 528 transitions in the final state space.  [NZCUB] Algorithm completed after 7.405 seconds. Starting running algorithm NZCUB…  Computing post^1 from 1 state. Computing post^2 from 5 states. Computing post^2 from 9 states. Computing post^3 from 10 states.  4 states merged within 29 states. Computing post^10 from 25 states. Computing post^4 from 10 states. Computing post^3 from 30 states. Computing post^5 from 5 states. Computing post^6 from 1 state.  Fixpoint reached at a depth of 7: 32 states with 80 transitions in the final state space.  [NZCUB] Algorithm completed after 7.789 seconds. Starting running algorithm NZCUB…  Computing post^1 from 1 state. Computing post^2 from 9 states. Computing post^3 from 30 states.  4 states merged within 89 states. Computing post^4 from 50 states. Computing post^11 from 85 states. Computing post^4 from 50 states. Computing post^11 from 52 states. Computing post^5 from 45 states. Computing post^12 from 102 states. Computing post^5 from 45 states. Computing post^6 from 21 states. Computing post^7 from 4 states.  Fixpoint reached at a depth of 8: 160 states with 528 transitions in the final state space.  [NZCUB] Algorithm completed after 9.040 seconds. Starting running algorithm NZCUB…  Computing post^1 from 1 state. Computing post^2 from 6 states. Computing post^3 from 15 states. Computing post^6 from 21 states. Computing post^4 from 21 states. Computing post^7 from 4 states.  Fixpoint reached at a depth of 8: 160 states with 528 transitions in the final state space.  [NZCUB] Algorithm completed after 9.340 seconds. IMITATOR successfully terminated (after 9.345 seconds) Computing post^5 from 19 states. Computing post^6 from 12 states. Computing post^7 from 9 states.  1 state merged within 14 states. Computing post^8 from 13 states. Computing post^9 from 13 states.  2 states merged within 17 states. Computing post^10 from 15 states. Computing post^12 from 114 states. Computing post^11 from 38 states. Computing post^12 from 85 states. Computing post^12 from 76 states.  18 states merged within 138 states. Computing post^12 from 120 states.  13 states merged within 150 states. Computing post^12 from 137 states.  46 states merged within 176 states. Computing post^13 from 130 states.  59 states merged within 226 states. Computing post^13 from 167 states.  43 states merged within 162 states. Computing post^13 from 119 states.  34 states merged within 128 states. Computing post^13 from 94 states.  17 states merged within 86 states. Computing post^14 from 69 states.  18 states merged within 102 states. Computing post^14 from 84 states.  51 states merged within 294 states. Computing post^13 from 243 states.  12 states merged within 75 states. Computing post^14 from 63 states.  7 states merged within 51 states. Computing post^15 from 44 states.  41 states merged within 227 states. Computing post^13 from 186 states.  13 states merged within 91 states. Computing post^14 from 78 states.  10 states merged within 74 states. Computing post^15 from 64 states.  10 states merged within 22 states. Computing post^16 from 12 states.  Fixpoint reached at a depth of 17: 570 states with 1102 transitions in the final state space.  [NZCUB] Algorithm completed after 58.303 seconds. IMITATOR successfully terminated (after 58.311 seconds)  7 states merged within 51 states. Computing post^15 from 44 states.  32 states merged within 56 states. Computing post^16 from 24 states.  Fixpoint reached at a depth of 17: 795 states with 1684 transitions in the final state space.  [NZCUB] Algorithm completed after 80.601 seconds. IMITATOR successfully terminated (after 80.645 seconds)  43 states merged within 234 states. Computing post^14 from 191 states.  10 states merged within 74 states. Computing post^15 from 64 states.  8 states merged within 20 states. Computing post^16 from 12 states.  Fixpoint reached at a depth of 17: 451 states with 816 transitions in the final state space.  [NZCUB] Algorithm completed after 116.326 seconds. IMITATOR successfully terminated (after 116.333 seconds)  28 states merged within 194 states. Computing post^14 from 166 states.  11 states merged within 94 states. Computing post^15 from 83 states.  12 states merged within 26 states. Computing post^16 from 14 states.  Fixpoint reached at a depth of 17: 953 states with 1800 transitions in the final state space.  [NZCUB] Algorithm completed after 171.395 seconds. IMITATOR successfully terminated (after 171.457 seconds)  32 states merged within 56 states. Computing post^16 from 24 states.  Fixpoint reached at a depth of 17: 631 states with 1257 transitions in the final state space.  [NZCUB] Algorithm completed after 178.825 seconds. IMITATOR successfully terminated (after 178.836 seconds)  9 states merged within 88 states. Computing post^15 from 79 states.  20 states merged within 34 states. Computing post^16 from 14 states.  Fixpoint reached at a depth of 17: 757 states with 1374 transitions in the final state space.  [NZCUB] Algorithm completed after 465.663 seconds. IMITATOR successfully terminated (after 465.789 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/8/flipflop/NZCUBtransdist.res'. IMITATOR successfully terminated (after 465.791 seconds)