************************************************************ * 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:12 UTC) * * HEAD/0999a7d * ************************************************************ Model: /home/royal/Desktop/experiments/Etienne/S/flipflop/flipflop.imi Mode: parametric non-Zeno emptiness checking (CUB transformation). 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…  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 12 states. Computing post^3 from 74 states. Computing post^4 from 291 states. Computing post^5 from 808 states. Computing post^6 from 1663 states. Computing post^7 from 2619 states.  2 states merged within 3201 states. Computing post^8 from 3199 states.  5 states merged within 3048 states. Computing post^9 from 3043 states.  3 states merged within 2231 states. Computing post^10 from 2228 states.  8 states merged within 1245 states. Computing post^11 from 1237 states.  3 states merged within 539 states. Computing post^12 from 536 states.  1 state merged within 262 states. Computing post^13 from 261 states.  8 states merged within 203 states. Computing post^14 from 195 states.  22 states merged within 174 states. Computing post^15 from 152 states.  47 states merged within 213 states. Computing post^16 from 166 states.  10 states merged within 372 states. Computing post^17 from 362 states.  39 states merged within 673 states. Computing post^18 from 634 states.  274 states merged within 1213 states. Computing post^19 from 939 states.  138 states merged within 787 states. Computing post^20 from 649 states.  54 states merged within 432 states. Computing post^21 from 378 states.  112 states merged within 212 states. Computing post^22 from 100 states.  Fixpoint reached at a depth of 23: 19547 states with 79181 transitions in the final state space.  [NZCUB] Algorithm completed after 686.554 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/S/flipflop/NZCUBtrans.res'. IMITATOR successfully terminated (after 686.574 seconds)