./imitator flipflop.imi -mode PDFC -output-states -output-trace-set -output-cart -output-result -time-limit 300 ************************************************************ * IMITATOR 2.8-alpha "Butter Ham" * * * * Etienne Andre, Ulrich Kuehne et al. * * 2009 - 2016 * * LSV, ENS de Cachan & CNRS, France * * LIPN, Universite Paris 13, Sorbonne Paris Cite, France * * www.imitator.fr * * * * Build: 1981 (2016-05-11 07:25:18 UTC) * * master/ab08ea8 * ************************************************************ Analysis time: Wed May 11, 2016 09:42:26 Model: flipflop.imi Mode: Parametric deadlock-checking. The cartography will be drawn. The result will be written to a file. The trace set(s) will be generated in a graphical mode. Description of states will be output. *** Warning: IMITATOR will try to stop after 300 seconds. This model is a U-PTA. Abstract model built after 0.018 second. Memory for abstract model: 1116.863 KiB (i.e., 285917 words) Starting running algorithm Parametric deadlock-freeness checking... Computing post^1 from 1 state. Computing post^2 from 1 state. Computing post^3 from 1 state. Computing post^4 from 1 state. Computing post^5 from 2 states. Computing post^6 from 4 states. Computing post^7 from 5 states. Computing post^8 from 5 states. [Parametric deadlock-freeness checking] None of the parameter valuations compatible with the initial state is deadlock-free: terminate. Fixpoint reached at a depth of 9: 20 states with 19 transitions explored. [Parametric deadlock-freeness checking] Algorithm completed after 0.112 second. Final constraint such that the system is deadlock-free: False This constraint is exact (sound and complete) Estimated memory used: 3.233 MiB (i.e., 423807 words of size 8) Result written to file 'flipflop.res'. -------------------- Statistics on state space -------------------- Number of states : 20 Number of transitions : 19 Number of computed states : 20 Computation time : 0.093 second States/second in state space : 213.3 (20/0.093 second) Computed states/second : 213.3 (20/0.093 second) Generating graphical output to 'flipflop-statespace.jpg'... Writing the states description to file 'flipflop-statespace.states'... *** Warning: No cartography can be drawn since the list of constraints is empty. *** ERROR: Error while printing the cartography IMITATOR successfully terminated (after 0.211 second)