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