./imitator AndOr.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:17:16 Model: AndOr.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 {dOr_l, dAnd_l} - upper-bound parameters {dOr_u, dAnd_u} Abstract model built after 0.036 second. Memory for abstract model: 764.617 KiB (i.e., 195742 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 9 states. Computing post^7 from 12 states. Computing post^8 from 17 states. Computing post^9 from 33 states. Computing post^10 from 45 states. Computing post^11 from 69 states. Computing post^12 from 107 states. Computing post^13 from 163 states. Computing post^14 from 201 states. Computing post^15 from 336 states. Computing post^16 from 434 states. Computing post^17 from 625 states. Computing post^18 from 778 states. Computing post^19 from 1135 states. *** Warning: The time limit has been reached. The exploration now stops, although there were still 1289 states to explore at this iteration. State space exploration stopped at a depth of 20: 5265 states with 6146 transitions explored. [Parametric deadlock-freeness checking] Algorithm completed after 373.662 seconds. [Parametric deadlock-freeness checking] Starting backward under-approximation... [Parametric deadlock-freeness checking] Backward under-approximation completed after 541.524 seconds. Final possibly under-approximated constraint such that the system is deadlock-free: dOr_l + dAnd_l > 8 & dOr_u + dAnd_u + 2 >= 2*dAnd_l & dAnd_u >= dAnd_l & dAnd_u >= 5 & 19 > dAnd_u & dOr_l >= 0 & 21 > dOr_u + dAnd_u & dOr_l + 2*dAnd_l > 14 & 7 > dOr_u & dOr_u >= dOr_l OR dOr_l + 2*dAnd_l > 14 & dOr_l + dAnd_l > 8 & 19 > dAnd_u & dAnd_l + 11 > dOr_u + dAnd_u & dOr_l >= 0 & dAnd_u >= dAnd_l & 7 > dOr_u & 2*dAnd_l > 2 + dOr_u + dAnd_u & dOr_u >= dOr_l OR dOr_l + dAnd_l > 8 & dAnd_u >= dAnd_l & dAnd_u >= 5 & 14 >= dOr_l + 2*dAnd_l & 21 > dOr_u + dAnd_u & 7 > dOr_u & dOr_u >= dOr_l OR dOr_l > 15 + dAnd_u & dAnd_l >= 0 & 21 > dOr_u + dAnd_u & dAnd_u >= dAnd_l & dOr_u >= dOr_l OR 5 > dAnd_u & dOr_l > 18 & dOr_u >= dOr_l & dOr_u + dAnd_u >= 21 & dAnd_u >= dAnd_l & dAnd_l >= 0 OR dOr_l >= 0 & 5 > dAnd_u & 7 > dOr_u + dAnd_u & dAnd_l >= 0 & dAnd_u >= dAnd_l & dOr_u >= dOr_l OR dAnd_u >= dAnd_l & 5 > dAnd_u & dOr_l + dAnd_l > 8 & 7 > dOr_u & dOr_u >= dOr_l OR dOr_l > 15 + dAnd_u & dAnd_u >= dAnd_l & dAnd_l >= 0 & 18 >= dOr_l & dOr_u + dAnd_u >= 21 OR dOr_l >= 0 & dAnd_l + 11 > dOr_u + dAnd_u & 19 > dAnd_u & dOr_u + 11 > dAnd_l & 7 > dOr_u & dOr_u + dAnd_u >= 21 & dOr_u + dAnd_u + 2 >= 2*dAnd_l & dOr_u >= dOr_l OR dOr_l >= 0 & dOr_u + dAnd_u >= 11 + dAnd_l & dAnd_l > 14 & 19 > dAnd_u & 7 > dOr_u & dOr_u >= dOr_l Final possibly over-approximated constraint such that the system is deadlock-free: dOr_l >= 0 & dAnd_u >= dAnd_l & dOr_u >= dOr_l & dAnd_l >= 0 This constraint is both a possibly under-approximation and a possibly over-approximation (or the actual result itself) Estimated memory used: 861.429 MiB (i.e., 112909242 words of size 8) Result written to file 'AndOr.res'. -------------------- Statistics on state space -------------------- Number of states : 5265 Number of transitions : 6146 Number of computed states : 6147 Computation time : 541.801 seconds States/second in state space : 9.7 (5265/541.801 seconds) Computed states/second : 11.3 (6147/541.801 seconds) Generating graphical output to 'AndOr-statespace.jpg'... dot: graph is too large for cairo-renderer bitmaps. Scaling by 0.555967 to fit Writing the states description to file 'AndOr-statespace.states'... *** ERROR: Fatal internal error: not implemented Please (politely) insult the developers. *** ERROR: IMITATOR aborted (after 1620.262 seconds)