************************************************************ * 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/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/4/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/4/flipflop/flipflop.imi Model: /home/royal/Desktop/experiments/Etienne/4/flipflop/flipflop.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). 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. 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. 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  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. Starting running algorithm NZCUB…  Computing post^1 from 1 state. Computing post^2 from 6 states. Computing post^2 from 10 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 Computing post^3 from 38 states. Starting running algorithm NZCUB…  Computing post^1 from 1 state. Computing post^2 from 10 states. Computing post^4 from 16 states. Computing post^5 from 9 states. Computing post^3 from 38 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.468 seconds. Starting running algorithm NZCUB…  Computing post^1 from 1 state. Computing post^2 from 7 states. Computing post^3 from 20 states. Computing post^4 from 72 states. Computing post^4 from 32 states. Computing post^4 from 72 states. Computing post^5 from 35 states. Computing post^6 from 29 states. Computing post^5 from 73 states. Computing post^7 from 24 states. Computing post^5 from 73 states.  4 states merged within 40 states. Computing post^8 from 36 states. Computing post^6 from 38 states. Computing post^9 from 42 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.151 seconds. Starting running algorithm NZCUB…  Computing post^1 from 1 state. Computing post^2 from 6 states. Computing post^6 from 38 states. Computing post^3 from 14 states. Computing post^4 from 16 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.516 seconds. Starting running algorithm NZCUB…  Computing post^1 from 1 state. Computing post^2 from 10 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 4.624 seconds. Starting running algorithm NZCUB…  Computing post^1 from 1 state. Computing post^2 from 10 states.  14 states merged within 56 states. Computing post^10 from 42 states. Computing post^3 from 38 states. Computing post^3 from 38 states. Computing post^4 from 72 states. Computing post^4 from 72 states. Computing post^5 from 73 states. Computing post^5 from 73 states. Computing post^11 from 74 states. Computing post^6 from 38 states. Computing post^6 from 38 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 6.927 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 6.984 seconds. Starting running algorithm NZCUB…  Computing post^2 from 7 states. 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^4 from 10 states. Computing post^4 from 31 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.492 seconds. Starting running algorithm NZCUB…  Computing post^1 from 1 state. Computing post^2 from 9 states. Computing post^3 from 30 states. Computing post^5 from 30 states. Computing post^6 from 20 states. Computing post^4 from 50 states. Computing post^7 from 13 states.  2 states merged within 20 states. Computing post^8 from 18 states.  4 states merged within 26 states. Computing post^9 from 22 states. Computing post^5 from 45 states.  4 states merged within 30 states. Computing post^10 from 26 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 9 states. Computing post^3 from 30 states. Computing post^11 from 56 states. Computing post^4 from 50 states. Computing post^12 from 114 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 10.585 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^4 from 22 states.  2 states merged within 25 states. Computing post^5 from 23 states.  1 state merged within 19 states. Computing post^6 from 18 states.  1 state merged within 18 states. Computing post^7 from 17 states. Computing post^8 from 28 states.  9 states merged within 42 states. Computing post^9 from 33 states. Computing post^10 from 37 states. Computing post^12 from 102 states.  4 states merged within 89 states. Computing post^11 from 85 states.  13 states merged within 150 states. Computing post^12 from 137 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.  18 states merged within 102 states. Computing post^14 from 84 states.  51 states merged within 294 states. Computing post^13 from 243 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.  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 82.750 seconds. Starting running algorithm NZCUB…  Computing post^1 from 1 state. Computing post^2 from 5 states. Computing post^3 from 10 states. Computing post^4 from 10 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 83.542 seconds. Starting running algorithm NZCUB…  Computing post^1 from 1 state. Computing post^2 from 9 states. Computing post^3 from 30 states. Computing post^4 from 50 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 85.047 seconds. Starting running algorithm NZCUB…  Computing post^1 from 1 state. Computing post^2 from 9 states. Computing post^3 from 30 states. Computing post^4 from 50 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 86.400 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^4 from 21 states.  1 state merged within 20 states. Computing post^5 from 19 states. Computing post^6 from 12 states.  1 state merged within 10 states. Computing post^7 from 9 states. Computing post^8 from 14 states.  5 states merged within 22 states. Computing post^9 from 17 states.  11 states merged within 32 states. Computing post^10 from 21 states.  6 states merged within 63 states. Computing post^11 from 57 states.  18 states merged within 138 states. Computing post^12 from 120 states.  10 states merged within 74 states. Computing post^15 from 64 states.  43 states merged within 234 states. Computing post^14 from 191 states.  41 states merged within 227 states. Computing post^13 from 186 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.  32 states merged within 56 states. Computing post^16 from 24 states.  Fixpoint reached at a depth of 17: 953 states with 1800 transitions in the final state space.  [NZCUB] Algorithm completed after 179.771 seconds. Starting running algorithm NZCUB…  Computing post^1 from 1 state. Computing post^2 from 5 states. Computing post^3 from 10 states. Computing post^4 from 10 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 181.220 seconds. Starting running algorithm NZCUB…  Computing post^1 from 1 state. Computing post^2 from 9 states. Computing post^3 from 30 states. Computing post^4 from 50 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 182.629 seconds. Starting running algorithm NZCUB…  Computing post^1 from 1 state. Computing post^2 from 9 states. Computing post^3 from 30 states. Computing post^4 from 50 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 183.965 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^4 from 22 states. Computing post^5 from 23 states. Computing post^6 from 18 states. Computing post^7 from 17 states.  Fixpoint reached at a depth of 17: 631 states with 1257 transitions in the final state space.  [NZCUB] Algorithm completed after 184.807 seconds. Starting running algorithm NZCUB…  Computing post^1 from 1 state.  2 states merged within 28 states. Computing post^8 from 26 states. Computing post^9 from 25 states.  4 states merged within 29 states. Computing post^10 from 25 states. Computing post^2 from 5 states. Computing post^3 from 10 states. Computing post^4 from 10 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 185.843 seconds. Starting running algorithm NZCUB…  Computing post^1 from 1 state. Computing post^2 from 9 states. Computing post^3 from 30 states. Computing post^11 from 52 states. Computing post^4 from 50 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 187.259 seconds. Starting running algorithm NZCUB…  Computing post^1 from 1 state. Computing post^2 from 9 states. Computing post^3 from 30 states. Computing post^4 from 50 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 188.551 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^12 from 85 states. Computing post^4 from 21 states. 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^11 from 38 states. Computing post^12 from 76 states.  46 states merged within 176 states. Computing post^13 from 130 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.  28 states merged within 194 states. Computing post^14 from 166 states.  7 states merged within 51 states. Computing post^15 from 44 states.  12 states merged within 75 states. Computing post^14 from 63 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 234.500 seconds. IMITATOR successfully terminated (after 234.511 seconds)  7 states merged within 51 states. Computing post^15 from 44 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 293.994 seconds. IMITATOR successfully terminated (after 294.006 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 552.195 seconds. IMITATOR successfully terminated (after 552.306 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/4/flipflop/NZCUBtransdist.res'. IMITATOR successfully terminated (after 552.308 seconds)