./imitator RCP.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:40
Model: RCP.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 an L/U-PTA:
- lower-bound parameters {rc_fast_min, rc_slow_min}
- upper-bound parameters {rc_fast_max, delay, rc_slow_max}
Abstract model built after 0.019 second.
Memory for abstract model: 932.457 KiB (i.e., 238709 words)
Starting running algorithm Parametric deadlock-freeness checking...
Computing post^1 from 1 state.
Computing post^2 from 4 states.
Computing post^3 from 12 states.
Computing post^4 from 32 states.
Computing post^5 from 62 states.
Computing post^6 from 94 states.
Computing post^7 from 108 states.
Computing post^8 from 150 states.
Computing post^9 from 188 states.
Computing post^10 from 164 states.
Computing post^11 from 384 states.
[Parametric deadlock-freeness checking] None of the parameter valuations compatible with the initial state is deadlock-free: terminate.
[Parametric deadlock-freeness checking] A sufficient condition to ensure termination was met although there were still 892 states to explore
State space exploration stopped at a depth of 12: 2091 states with 2752 transitions explored.
[Parametric deadlock-freeness checking] Algorithm completed after 10.649 seconds.
Final constraint such that the system is deadlock-free:
False
This constraint is exact (sound and complete)
Estimated memory used: 150.200 MiB (i.e., 19687015 words of size 8)
Result written to file 'RCP.res'.
--------------------
Statistics on state space
--------------------
Number of states : 2091
Number of transitions : 2752
Number of computed states : 2753
Computation time : 10.631 seconds
States/second in state space : 196.6 (2091/10.631 seconds)
Computed states/second : 258.9 (2753/10.631 seconds)
Generating graphical output to 'RCP-statespace.jpg'...
dot: graph is too large for cairo-renderer bitmaps. Scaling by 0.171239 to fit
Writing the states description to file 'RCP-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 75.219 seconds)