Usage:
punf [-h]
or
punf [<options>] <net_file>
The input net file must be in either FORMAT_N or FORMAT_N2
format (produced by the PEP tool). Alternatively, it must
have the suffix `.g' and be in the STG format; then an STG
unfolding prefix (which may differ from the underlying
Petri net's unfolding prefix) is produced.
As an experimental feature, high-level nets are supported.
For now, only strictly safe nets are allowed, and there are
some further restrictions, described in the manual.
Options (may be given in any order):
-h Help.
-# Using non-local configuration as cut-off correspondents.
The current implementation is VERY INEFFICIENT.
This option is not currently supported in the LTL mode.
-$N Switch to SAT solver N (0-1).
If N=0 then zChaff is used.
If N=1 then MiniSAT is used (default).
-@[N] Using adequate order N (0-4).
Specifies the adequate order on configurations of the unfolding.
If N is not specified or -@ is not used then the default
value N=3 (for prefixes) or N=4 (for merged processes) is used.
If N=0 then the set inclusion is used.
If N=1 then the McMillan's order is used.
If N=2 then the size-lexicographical order is used.
If N=3 then the total Esparza/Roemer/Vogler (ERV) order is used.
If N=4 then the total order with an efficient SAT encoding is used.
Only the ERV order is currently supported in the LTL mode.
-B=filename
Switches on the LTL-X verification mode. The file must be in
the HOA format (http://adl.github.io/hoaf/) and specify a Buechi
automaton for an LTL-X property. The adequate order must be -@3.
-c Do not store cut-off events (except the successful terminals in
the LTL mode).
-d When unfolding an STG, allow dummy cut-off events.
If this option is not specified, a dummy event e can only be
declared cut-off if its corresponding configuration C is a
subset of [e], and [e]\C contains only dummies.
This option has effect only when unfolding an STG.
It is automatically specified if the STG contains only dummy signals.
(Currently ignored if -M is specified.)
-jN Specifies the number of working threads. By default, it is equal
to the number of processors. (Currently ignored if -M is specified.)
-l Replicate places with multiple self-loops, so that each transition
reading a particular place gets its own copy of that place. This
transformation can significantly reduce the prefix size for nets
with many self-loops.
-M Generate a complete merged process.
-m[=filename]
Specifies the name of the resulting file, whose extension also
specifies the format. It can be either the legacy *.mci format
for prefixes, the legacy *.mp format for merged processes (if -M
is specified), or the new PNML-based *.pnml or *.pnml.gz format.
If this option is not specified then the filename for the result
is obtained by removing from the input filename the suffix `.ll_net',
`.g' or `.hl_net' (if present), and appending the suffix `.pnml.gz',
and the resulting prefix or merged process is stored in the new
PNML-based format. If the filename is not specified (i.e. just -m
is given) then no output file is created.
-nN Abandon the concurrency relation and switch to a slower algorithm
after the specified number of non-cut-off events is generated. The
default value of N is 50000. If N is 0, the
concurrency relation is not created. (Ignored if -M is specified.)
-vN Verbosity level (0-9). The default is 0.
-w[N] Wait for user input before exiting (prevents the window from closing).
The possible values of N:
0 - do not wait for user input, exit immediately;
1 - wait for user input only if there are errors;
2 - wait for user input only if there are errors or warnings;
3 - always wait for user input.
The default is -w0, and -w is equivalent to -w3.