./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)