./imitator WFAS-BBLS15-det.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 12:46:24
    
    Model: WFAS-BBLS15-det.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.008 second.
    Memory for abstract model: 599.394 KiB (i.e., 153445 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 7 states.
    Computing post^6 from 10 states.
    Computing post^7 from 13 states.
    Computing post^8 from 21 states.
    Computing post^9 from 25 states.
    Computing post^10 from 37 states.
    Computing post^11 from 43 states.
    Computing post^12 from 65 states.
    Computing post^13 from 76 states.
    Computing post^14 from 104 states.
    Computing post^15 from 122 states.
    Computing post^16 from 167 states.
    Computing post^17 from 150 states.
    Computing post^18 from 195 states.
    Computing post^19 from 209 states.
    Computing post^20 from 296 states.
    Computing post^21 from 257 states.
    Computing post^22 from 337 states.
    Computing post^23 from 342 states.
    Computing post^24 from 495 states.
    Computing post^25 from 416 states.
    Computing post^26 from 541 states.
    Computing post^27 from 536 states.
    Computing post^28 from 801 states.
    Computing post^29 from 660 states.
    Computing post^30 from 885 states.
    Computing post^31 from 834 states.
    Computing post^32 from 1276 states.
    Computing post^33 from 1024 states.
    Computing post^34 from 1399 states.
    Computing post^35 from 1290 states.
 *** Warning: The time limit has been reached. The exploration now stops, although there were still 1974 states to explore at this iteration.
    
    State space exploration stopped at a depth of 36: 14614 states with 16538 transitions explored.
    
      [Parametric deadlock-freeness checking] Algorithm completed after 387.169 seconds.
    
      [Parametric deadlock-freeness checking] Starting backward under-approximation...
      [Parametric deadlock-freeness checking] Backward under-approximation completed after 456.243 seconds.
    
    Final possibly under-approximated constraint such that the system is deadlock-free:
     p1 >= 5
    & 9 >= p2
    & 2*p2 >= 17
    
    Final possibly over-approximated constraint such that the system is deadlock-free:
     p1 >= 5
    & 9 >= p2
    & 2*p2 >= 17
    OR
      p1 = 0
    & p2 = 0
    This constraint is both a possibly under-approximation and a possibly over-approximation (or the actual result itself)

    Estimated memory used: 4.065 GiB (i.e., 545680023 words of size 8)
    
    Result written to file 'WFAS-BBLS15-det.res'.
    
    --------------------
    Statistics on state space
    --------------------
    Number of states              : 14614
    Number of transitions         : 16538
    Number of computed states     : 16539
    Computation time              : 456.235 seconds
    States/second in state space  : 32.0 (14614/456.235 seconds)
    Computed states/second        : 36.2 (16539/456.235 seconds)
    
    Generating graphical output to 'WFAS-BBLS15-det-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 'WFAS-BBLS15-det-statespace.states'...
 *** ERROR: Fatal internal error: not implemented
 Please (politely) insult the developers.
 *** ERROR: IMITATOR aborted (after 1194.578 seconds)