./imitator NuclearPlant.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 09:42:33
    
    Model: NuclearPlant.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.007 second.
    Memory for abstract model: 489.640 KiB (i.e., 125348 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 2 states.
    Computing post^5 from 2 states.
    Computing post^6 from 1 state.
    Computing post^7 from 1 state.
    Computing post^8 from 2 states.
    Computing post^9 from 1 state.
    
    Fixpoint reached at a depth of 10: 13 states with 13 transitions explored.
    
      [Parametric deadlock-freeness checking] Algorithm completed after 0.049 second.
    
    Final constraint such that the system is deadlock-free:
     p1 > p2 + p3 + p4
    & p2 >= 0
    & p3 >= 0
    & p4 >= 0
    This constraint is exact (sound and complete)

    Estimated memory used: 1.520 MiB (i.e., 199236 words of size 8)
    
    Result written to file 'NuclearPlant.res'.
    
    --------------------
    Statistics on state space
    --------------------
    Number of states              : 13
    Number of transitions         : 13
    Number of computed states     : 14
    Computation time              : 0.042 second
    States/second in state space  : 304.8 (13/0.042 second)
    Computed states/second        : 328.3 (14/0.042 second)
    
    Generating graphical output to 'NuclearPlant-statespace.jpg'...
    Writing the states description to file 'NuclearPlant-statespace.states'...
    
    Drawing the cartography...
    Plot cartography in 2D projected on parameters p1 and p2 to file 'NuclearPlant_cart_pdfc.png'.

    IMITATOR successfully terminated (after 0.157 second)