./imitator simop.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 13:09:56
Model: simop.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.
Abstract model built after 0.015 second.
Memory for abstract model: 858.035 KiB (i.e., 219657 words)
Starting running algorithm Parametric deadlock-freeness checking...
Computing post^1 from 1 state.
Computing post^2 from 1 state.
Computing post^3 from 2 states.
Computing post^4 from 4 states.
Computing post^5 from 7 states.
Computing post^6 from 11 states.
Computing post^7 from 15 states.
Computing post^8 from 21 states.
Computing post^9 from 26 states.
Computing post^10 from 34 states.
Computing post^11 from 43 states.
Computing post^12 from 65 states.
Computing post^13 from 101 states.
Computing post^14 from 164 states.
Computing post^15 from 282 states.
Computing post^16 from 485 states.
Computing post^17 from 800 states.
Computing post^18 from 1247 states.
Computing post^19 from 1826 states.
Computing post^20 from 2594 states.
Computing post^21 from 3597 states.
Computing post^22 from 4924 states.
*** Warning: The time limit has been reached. The exploration now stops, although there were still 6644 states to explore at this iteration.
State space exploration stopped at a depth of 23: 22894 states with 31043 transitions explored.
[Parametric deadlock-freeness checking] Algorithm completed after 328.872 seconds.
[Parametric deadlock-freeness checking] Starting backward under-approximation...
[Parametric deadlock-freeness checking] Backward under-approximation completed after 450.801 seconds.
Final possibly under-approximated constraint such that the system is deadlock-free:
False
Final possibly over-approximated constraint such that the system is deadlock-free:
SIGmrt > 0
& COMct >= 115
& COMct + SIGmrt >= 2465
OR
COMct + SIGmrt >= 1865
& COMct > SIGmrt
& SIGmrt > 70
& 2465 > COMct + SIGmrt
OR
COMct >= 115
& 2465 > COMct + SIGmrt
& COMct + SIGmrt >= 565
& SIGmrt >= COMct
OR
COMct + SIGmrt >= 1265
& SIGmrt >= 80
& COMct > SIGmrt
& 1865 > COMct + SIGmrt
OR
COMct + SIGmrt >= 1165
& COMct > SIGmrt
& SIGmrt + 35 >= COMct
& 1265 > COMct + SIGmrt
OR
COMct > SIGmrt
& COMct + SIGmrt >= 665
& SIGmrt + 10 >= COMct
& 1165 > COMct + SIGmrt
OR
COMct >= 115
& SIGmrt > 70 + COMct
& 565 > COMct + SIGmrt
This constraint is both a possibly under-approximation and a possibly over-approximation (or the actual result itself)
Estimated memory used: 5.648 GiB (i.e., 758124220 words of size 8)
Result written to file 'simop.res'.
--------------------
Statistics on state space
--------------------
Number of states : 22894
Number of transitions : 31043
Number of computed states : 31044
Computation time : 450.784 seconds
States/second in state space : 50.7 (22894/450.784 seconds)
Computed states/second : 68.8 (31044/450.784 seconds)
Generating graphical output to 'simop-statespace.jpg'...
dot: graph is too large for cairo-renderer bitmaps. Scaling by 0.0644532 to fit
Writing the states description to file 'simop-statespace.states'...
*** ERROR: Fatal internal error: not implemented
Please (politely) insult the developers.
*** ERROR: IMITATOR aborted (after 4995.593 seconds)