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.