./imitator coffee.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 11:45:46
Model: coffee.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.005 second.
Memory for abstract model: 451.312 KiB (i.e., 115536 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 3 states.
Computing post^5 from 5 states.
Computing post^6 from 6 states.
Computing post^7 from 7 states.
Computing post^8 from 8 states.
Computing post^9 from 9 states.
Computing post^10 from 10 states.
Computing post^11 from 11 states.
Computing post^12 from 12 states.
Computing post^13 from 13 states.
Computing post^14 from 14 states.
Computing post^15 from 15 states.
Computing post^16 from 16 states.
Computing post^17 from 17 states.
Computing post^18 from 18 states.
Computing post^19 from 19 states.
Computing post^20 from 20 states.
Computing post^21 from 21 states.
Computing post^22 from 22 states.
Computing post^23 from 23 states.
Computing post^24 from 24 states.
Computing post^25 from 25 states.
Computing post^26 from 26 states.
Computing post^27 from 27 states.
Computing post^28 from 28 states.
Computing post^29 from 29 states.
Computing post^30 from 30 states.
Computing post^31 from 31 states.
Computing post^32 from 32 states.
Computing post^33 from 33 states.
Computing post^34 from 34 states.
Computing post^35 from 35 states.
Computing post^36 from 36 states.
Computing post^37 from 37 states.
Computing post^38 from 38 states.
Computing post^39 from 39 states.
Computing post^40 from 40 states.
Computing post^41 from 41 states.
Computing post^42 from 42 states.
Computing post^43 from 43 states.
Computing post^44 from 44 states.
Computing post^45 from 45 states.
Computing post^46 from 46 states.
Computing post^47 from 47 states.
Computing post^48 from 48 states.
Computing post^49 from 49 states.
Computing post^50 from 50 states.
Computing post^51 from 51 states.
Computing post^52 from 52 states.
Computing post^53 from 53 states.
Computing post^54 from 54 states.
Computing post^55 from 55 states.
Computing post^56 from 56 states.
Computing post^57 from 57 states.
Computing post^58 from 58 states.
Computing post^59 from 59 states.
Computing post^60 from 60 states.
Computing post^61 from 61 states.
Computing post^62 from 62 states.
Computing post^63 from 63 states.
Computing post^64 from 64 states.
Computing post^65 from 65 states.
Computing post^66 from 66 states.
Computing post^67 from 67 states.
Computing post^68 from 68 states.
Computing post^69 from 69 states.
Computing post^70 from 70 states.
Computing post^71 from 71 states.
Computing post^72 from 72 states.
Computing post^73 from 73 states.
Computing post^74 from 74 states.
Computing post^75 from 75 states.
Computing post^76 from 76 states.
Computing post^77 from 77 states.
Computing post^78 from 78 states.
Computing post^79 from 79 states.
Computing post^80 from 80 states.
Computing post^81 from 81 states.
Computing post^82 from 82 states.
Computing post^83 from 83 states.
Computing post^84 from 84 states.
Computing post^85 from 85 states.
Computing post^86 from 86 states.
Computing post^87 from 87 states.
Computing post^88 from 88 states.
Computing post^89 from 89 states.
Computing post^90 from 90 states.
Computing post^91 from 91 states.
Computing post^92 from 92 states.
Computing post^93 from 93 states.
Computing post^94 from 94 states.
Computing post^95 from 95 states.
Computing post^96 from 96 states.
Computing post^97 from 97 states.
Computing post^98 from 98 states.
Computing post^99 from 99 states.
Computing post^100 from 100 states.
Computing post^101 from 101 states.
Computing post^102 from 102 states.
Computing post^103 from 103 states.
Computing post^104 from 104 states.
Computing post^105 from 105 states.
Computing post^106 from 106 states.
Computing post^107 from 107 states.
Computing post^108 from 108 states.
Computing post^109 from 109 states.
Computing post^110 from 110 states.
Computing post^111 from 111 states.
Computing post^112 from 112 states.
Computing post^113 from 113 states.
Computing post^114 from 114 states.
Computing post^115 from 115 states.
Computing post^116 from 116 states.
Computing post^117 from 117 states.
Computing post^118 from 118 states.
Computing post^119 from 119 states.
Computing post^120 from 120 states.
Computing post^121 from 121 states.
Computing post^122 from 122 states.
Computing post^123 from 123 states.
Computing post^124 from 124 states.
Computing post^125 from 125 states.
Computing post^126 from 126 states.
Computing post^127 from 127 states.
Computing post^128 from 128 states.
Computing post^129 from 129 states.
Computing post^130 from 130 states.
Computing post^131 from 131 states.
Computing post^132 from 132 states.
Computing post^133 from 133 states.
*** Warning: The time limit has been reached. The exploration now stops, although there were still 134 states to explore at this iteration.
State space exploration stopped at a depth of 134: 9042 states with 13459 transitions explored.
[Parametric deadlock-freeness checking] Algorithm completed after 308.939 seconds.
[Parametric deadlock-freeness checking] Starting backward under-approximation...
[Parametric deadlock-freeness checking] Backward under-approximation completed after 317.363 seconds.
Final possibly under-approximated constraint such that the system is deadlock-free:
65*p1 > p2
& p2 >= 0
& p3 >= p2
Final possibly over-approximated constraint such that the system is deadlock-free:
p1 >= 0
& p2 >= 0
& p3 >= p2
OR
p3 >= 0
& p2 > p3
& p1 = 0
This constraint is both a possibly under-approximation and a possibly over-approximation (or the actual result itself)
Estimated memory used: 6.244 GiB (i.e., 838075078 words of size 8)
Result written to file 'coffee.res'.
--------------------
Statistics on state space
--------------------
Number of states : 9042
Number of transitions : 13459
Number of computed states : 13460
Computation time : 317.358 seconds
States/second in state space : 28.4 (9042/317.358 seconds)
Computed states/second : 42.4 (13460/317.358 seconds)
Generating graphical output to 'coffee-statespace.jpg'...
^C *** ERROR: Something went wrong when calling 'dot'. Exit code: 255. Maybe you forgot to install the 'dot' utility (from the 'graphviz' package in Debian).
Writing the states description to file 'coffee-statespace.states'...
*** ERROR: Fatal internal error: not implemented
Please (politely) insult the developers.
*** ERROR: IMITATOR aborted (after 3619.556 seconds)