Command line options of backend tools

This is a summary of command line options for some of Workcraft backend tools.

Petrify command line options

usage: ./petrify [flags] [infile]

General options:
----------------
  -v           print version only
  -d[n]        debug level (n=1,2)
  -o outfile   STG output file (default: stdout)
  -no          output file not generated
  -log logfile log filename (default: petrify.log)
  -err errfile error filename (default: stderr)
  -nolog       no log file generated
  -ip          show implicit (1-fanin 1-fanout) places
  -dead        do not check for the existence of deadlock states
  -sis         print SIS output style (~ for toggle transitions)

Options for Petri net synthesis:
--------------------------------
  -all         search for all minimal regions (even for irredundant nets)
  -sat         generate a minimal satured Petri net
  -min         generate a Petri net with minimal regions only (no place merging)
  -opt         find the best result (may override other options)
  -noec        generate a Petri net without label splitting (possibly without excitation closure)
  -hide list   hide the signals in the list
  -bisim       maintain bisimilarity after removing events
  -mints       minimize the transition system before synthesis

Options for Petri net properties:
---------------------------------
  -p           generate a pure Petri net
  -fc          generate a Free-Choice net
  -efc         generate an Extended Free-Choice net
  -uc          generate a Unique-Choice net (with no extended free choices)
  -euc         generate a Unique-Choice net (with extended free choices)
  -er          generate a different label for each excitation region
  -sm          generate an SM-decomposable net

Options for STG transformations:
--------------------------------
  -tog         all +/- transitions are converted to toggle
  -untog       all toggle and hatch transitions are converted to +/-
  -2ph         expand channel events to 2-phase protocol (default)
  -4ph         expand channel events to 4-phase protocol
  -redc        concurrency reduction for logic optimization
  -redz        concurrency reduction for RTZ events only
  -redn1       conservative concurrency reduction for noise isolation
  -redn2       concurrency reduction for noise isolation
  -noise       noise analysis

Options for synthesis of asynchronous circuits:
-----------------------------------------------
  -csc[n]      solve CSC (with blocks of at most n intersecting regions)
  -icsc[n]     same as -csc with iterative removal of internal signals
  -ncsc[n]     maximum number of inserted state signals
  -tcsc        solve CSC aiming at improving performance (default for timing optimization)
  -acsc        solve CSC aiming at improving area (default if no timing optimization)
  -io          preserve I/O interface (ignore slow input events)
  -cg          generate complex gates
  -gc          generate generalized C elements
  -gcm         generate generalized C elements with monotonic covers
  -nosi        generate complex gates even for a non-SI specification
  -mc          generate monotonic covers
  -tm[n]       technology mapping (n is the depth of search)
  -tm_ratio[x] area/delay ratio for technology mapping
  -stm         sequential technology mapping (only latches are mapped)
  -nmap[n]     maximum number of inserted signals for technology mapping
  -eqn file    generate logic description in EQN format
  -blif file   generate logic description in BLIF format
  -vl file     generate logic description in Verilog format
  -rst0        generate reset pin active at 0 (only for Verilog netlists)
  -rst1        generate reset pin active at 1 (only for Verilog netlists)
  -lib file    read gate library
  -selckt      interactive selection of gates for each non-input signal
  -latch str   define allowed latches for sequential decomposition
  -nolatch     no latches used for technology mapping
  -lit[n]      logic decomposition with gates with at most n literals
  -cgd[n]      max number of complex gates for each gate decomposition
  -algd[n]     max number of algebraic divisors for each gate decomposition
  -mcd[n]      max number of monotonic covers for each signal decomposition
  -boold[n]    max number of boolean decompositions for each gate
  -ed          exhaustive decomposition
  -topt        logic optimization using timing constraints
  -atopt       logic optimization using automatic timing constraints
  -avg         timing optimization for average case (default: worst-case)

Advanced options:
-----------------
  -s[n]        search depth for label splitting (def. -s3, infinite with -s)
  -rc[n]       max number of non-essential regions for optimal irredundancy
  -cl[n]       max size of compatibility graph for one-hot->log encoding
  -nice_csc    CSC: attempts to find nice signal insertions
  -seq         CSC: do not increase concurrency of new state signals
  -fr[n]       CSC: frontier width for exploration of insertion blocks
  -cw[x]       CSC: tune eagerness to solve conflicts
  -redfr[n]    frontier width for exploration of concurrency reduction
  -trflat[n]   BDD node limit to flatten partitioned transition relations
  -boolmin[n]  define type of boolean minimization
  -notog       No toggle changes in transition relations
  -noreord     No dynamic variable reordering
  -reord[n]    Reordering frequency

MPSat command line options

Usage:
        mpsat [-h]
or
        mpsat <mode> [<options>] [<in_file>] [<out_file>]

The <mode> is one of the following:
  Unfolding/unravelling modes:
    -U[m|p] - Build a complete merged process (-Um) or unfolding prefix (-Up).
  Reachability-based formal verification modes:
    -D - Deadlock checking.
    -F[a|e|s]=<property_file> - Check a reachability-like property.
  Temporal property formal verification mode:
    -B=<property_file> - Check a stutter-invariant temporal property.
  Encoding conflicts detection and resolution modes:
    -C[c|n|u] - Check the CSC/normalcy/USC property.
    -R - Resolve CSC conflicts.
  Synthesis modes:
    -I[e|g|s] - Derive a complex-gate/gC/standard-C implementation.
    -T[=<gate_library>] - Logic decomposition and technology mapping.

The <options> are as follows:
  -# - Allow non-local configurations as cut-off correspondents.
  -! - Disable branching on auxiliary variables.
  -$N - Switch to SAT solver N (0-1).
  -@N - Use adequate order N (0-4).
  -a[N] - Compute all solutions (might be slow).
  -b - Generate backward conflict constraints.
  -c - Do not store cut-off events.
  -d - Allow dummy cut-off events when unfolding an STG.
  -e - Print out configurations rather than traces.
  -f[s|l|<COEFF>=<EXPR>] - Minimise (and perhaps specify) the cost function.
  -g[!][N] - Filter gates/latches used for logic decomposition.
  -i[+|-] - Specify whether to generate inclusion constraints.
  -jN - The number of working threads.
  -l - Replicate places with multiple self-loops.
  -mN - Use method N (1-9).
  -nN - Switch to memory efficient unfolding algorithm after N events.
  -pN - Controls the use of parallel (concurrent) inserions.
  -q - Quit early, after checking the property syntax.
  -r - Allows to use concurrency reduction for encoding conflict resolution.
  -t - Perform logic decomposition down to the gate/latch level.
  -vN - The verbosity level (0<=N<=9, the default is 0).
  -w[N] - Wait for user before exiting (prevents the window from closing).

Detailed help

Usage:
        mpsat [-h]
or
        mpsat <mode> [<options>] [<in_file>] [<out_file>]

Here <in_file> is compulsory unless option -q is given.
If <out_file> is omitted then stdout is used in all modes except -U[m|p],
where the name of output file may be generated automatically.

If -h is specified then full help is printed. If no command-line parameters
are given then brief help is printed.

The <mode> is one of the following:
  Unfolding/unravelling modes:
    -U[m|p] - Build a complete merged process (-Um) or unfolding prefix (-Up).
    (-U is equivalent to -Up.) The format of <out_file> is specified by its
    extension. It is either a legacy format (*.mci for -Up and *.mp for -Um),
    or the new PNML-based *.pnml format, or its zipped version *.pnml.gz.
    If <out_file> is not specified then the file name for the result
    is obtained by removing from <in_file> the suffix `.ll_net',
    `.g' or `.hl_net' (if present), and appending the suffix `bp.pnml.gz',
    (for prefix) or `mp.pnml.gz' (for merged process), and the result is
    stored in the new PNML-based format.
  Reachability-based formal verification modes:
    -D - Deadlock checking.
    -F[a|e|s]=<property_file> - Check a reachability-like property.
    The difference between -Fe and -F is the semantics of REACH operator '@'
    (checking the enabledness status of an event/transition/signal): In
    addition to the usual Petri net enabledness, an entity can be enabled
    in an STG via a sequence of dummy transitions.
    The difference between -Fs and -Fe is that only configurations without
    causally maximal dummy events are explored.
    The difference between -Fa and -Fs is that the syntax is SVA-like, i.e.
    the property can refer only to values of STG signals, and the property
    is interpreted as a global invariant to be verified rather than a
    predicate whose reachability is to be checked; hence, to check the same
    property using -Fs one has to invert it.
  Temporal property formal verification mode:
    -B=<property_file> - Check a stutter-invariant temporal property.
    The property file must be in the HOA format (http://adl.github.io/hoaf/)
    and specify a stutter-invariant Buechi automaton (such automata are
    generated, e.g., for LTL-X properties). The adequate order must be -@3.
    The input file must be a Petri net or STGs, not unfolding prefix; for
    STGs, the initial values of signals mentioned in the property must be
    specified. If <out_file> is specified, an unfolding prefix of a special
    product of Buechi automaton and the input net is stored; this prefix can
    be viewed as a tableaux proving or refuting the property. If <out_file>
    is not specified, no prefix is stored. It is recommended that option -c
    is used in this mode to avoid adding cut-off events corresponding to
    unsuccessful terminals to the prefix (unless you need a complete
    tableaux stored in <out_file>).
  Encoding conflicts detection and resolution modes:
    -C[c|n|u] - Check the CSC/normalcy/USC property.
    -R - Resolve CSC conflicts.
    (-C is equivalent to -Cc.)
    Normalcy property is required to avoid inverters (bubbles) on
    gates' inputs (which often require timing assumptions). This
    property is mostly of theoretical interest. A normalcy violation
    can be caused by the following factors:
    * An event have triggers with different signs. If this is
      the case, a trace leading to that event is printed out.
    * An instance of a signal transition has triggers with the
      same sign (which means that the signal cannot be n-normal),
      while another instance of this signal has triggers with
      the opposite sign (i.e. the signal cannot be p-normal).
      If this is the case, two traces leading to these instances
      are printed out.
    * There is a CSC conflict. If this is the case, two traces are
      printed similarly to the -Cc mode.
    * None of the above. Then a hypothesis is made about the normalcy
      type of each signal, based on the signs of its triggers.
      Then this hypothesis is verified, and if it is possible to
      disprove it, three traces are printed out: one to show the
      event for which a hypothesis was made, and the other two to
      show a violation of normalcy by definition.
  Synthesis modes:
    -I[e|g|s] - Derive a complex-gate/gC/standard-C implementation.
    (-I is equivalent to -Ie.)
    -T[=<gate_library>] - Logic decomposition and technology mapping.
    The gate library must be in the GENLIB format. The in-built
    gate library is used if no file is specified.
Exactly one of the above modes must be specified.

For the modes -C[c|n|u], -I[e|g|s], -Fa, -Fe, -Fs, -R, -T,
the file <in_file> must be an STG or STG unfolding. If the
legacy *.mci format is used then each transition's name must
carry information about the corresponding signal: The
format is [prefix:]identifier[+|-][/number], where prefix is
either of O,I,i (for outputs, internal signals, and inputs,
respectively; dummies have no prefix),
e.g. O:x-/1, I:csc+/1, i:a-, dum/1, t1. This format is
produced by the PUNF tool. Alternatively, PUNF can produce new
PNML-based format *.pnml or *.pnml.gz, which stores this
information in a more elegant way, and also fixes other issues.
The original STG must be consistent. Ideally, it should also
satisfy the CSC property in the synthesis modes (-I[e|g|s] and -T),
but if not then CSC resolution will be attempted.

The <options> are as follows:
  -# - Allow non-local configurations as cut-off correspondents.
  This option is currently supported only when building an unfolding
  prefix (perhaps as an intermediate step before solving another
  problem on the built prefix), i.e. in the -C[c|n|u], -I[e|g|s], -D,
  -F[a|e|s], -Up, -R, -T modes. It is not supported in the temporal
  verification (-B) or merged process construction (-Um) modes.
  The current implementation is INEFFICIENT.

  -! - Disable branching on auxiliary variables.
  Some of the variables in the SAT instances may be functions of
  other variables, so it is possible not to branch on them
  without affecting the correctness. This, however, has mixed
  effect on performance. You can try this option if you feel lucky.
  This option is available in all modes.

  -$N - Switch to SAT solver N (0-1).
  Currently two solvers, zChaff (N=0) and MiniSat (N=1) are
  supported. The default is chosen heuristically, depending on the mode.
  This option is available in all modes.

  -@N - Use adequate order N (0-4).
  Specifies the adequate order on configurations of the unfolding.
  The default value N=3 (for prefixes) or N=4 (for merged processes).
  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 -@3 is supported in the temporal verification (-B) mode.

  -a[N] - Compute all solutions (might be slow).
  The search does not stop after the first encountered solution,
  but continues until all solutions are computed. Since the
  number of solutions can be exponential in the size of the input,
  the search may take a lot of time and memory. Optionally, the
  number of computed solutions can be restricted to N>0. Note that N
  is just an approximate value, the actual number of computed
  solutions can slightly differ from N.
  This option is available in the following modes:
  -C[c|n|u], -D, -F[a|e|s], -R, -T. It is an error to specify this
  option in any other mode. This option conflicts with -f.

  -b - Generate backward conflict constraints.
  Additional constraints are genereted, conveying that no two
  mp-events in the preset of any mp-conditon can belong to the
  same mp-configuration. These constraints are redundant, but
  can in certain cases improve the performance. This option
  is silently ignored unless a merged process is involved.

  -c - Do not store cut-off events.
  Successful terminals in the -B mode are still stored.
  This option is available in the -B and -U[m|p] modes.
  For safety reasons, it is not available in modes which
  can indirectly trigger unfolding.

  -d - Allow dummy cut-off events when unfolding an STG.
  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 specified by default if the STG contains only dummy signals.
  This option is available in the -B and -U[m|p] modes.
  For safety reasons, it is not available in modes which
  can indirectly trigger unfolding. (Currently ignored in -Um mode.)

  -e - Print out configurations rather than traces.
  The numbering of events starts from 0.
  This option is available in all modes, but in modes other than
  -C[c|n|u], -D, -F[a|e|s] it does not affect anything other than
  verbosity output.

  -f[s|l|<COEFF>=<EXPR>] - Minimise (and perhaps specify) the cost function.
  Usually the total lengths of violation traces is minimised, though the
  cost functon is different in the -N, -R and -T modes. It often slows down
  the computation considerably. This option conflicts with -a.
  Option -f (without the extra parts) is available in the -C[c|n|u], -I[e|g|s],
  -D, -F[a|e|s], -R, -T modes. It is an error to specify this
  option in any other mode. This option is assumed by default in the synthesis
  modes -I[e|g|s]. For the -I[e|g|s], -R and -T modes, the user can also specify
  the coefficients of the cost function used for evaluating transformations
  (signal insertions or concurrency reduction) on each step of the encoding
  conflict resolution or logic decomposition. This function is a weighted
  sum of the following components (with the corresponding <COEFF>):
    csc:      the number of unresolved CSC cores
    comp_csc: the number of unresolved composite CSC complementary sets
    usc:      the number of unresolved USC cores
    comp_usc: the number of unresolved composite USC complementary sets
    del:      the number of delayed transitions
    trig:     the number of triggers of output and internal transitions,
              with the triggers having the same sign as the triggered
              transition and those having the opposite sign counted separately
    seq:      the number of sequential insertions (or |U| if a concurrency
              reduction U-n->t was applied)
    fseq_inc: the total incompleteness of used sequential insertions, where
              the incompleteness of a pre-insertion S|t is |*t|-|S|, and
              the incompleteness of a post-insertion t|S is |t*|-|S|
    conc:     the number of concurrent insertions
    lock:     the number computed by adding up the following numbers for each
              pair (a,b) of non-locked signals in the modified STG:
                      1 if both a and b are inputs;
                      2 if one of a, b is an input;
                      4 if both a and b are output or internal signals;
              if -r is not used (i.e. concurrency reductions are not allowed)
              then the difference between the values for the modified and the
              original STGs is used instead, which coincides with 2*I+4*L,
              where I is the number of inputs and L is the number of local
              (i.e. output or internal) signals which are not locked with
              the newly inserted signal.
  The defining expressions EXPR for coefficients can use integer constants,
  the operations +, -, *, /, %%, and the following macros referring to the STG:
    #i - the number of input signals
    #o - the number of output signals
    #I - the number of internal signals
    #d - the number of dummies
    #s - the total number of signals (excluding dummies)
    #p - the number of places
    #t - the number of transitions
  They must evaluate to non-negative integers.
  If -cs or -cl is specified then pre-defined mode-dependent expressions are
  used, which heuristically minimise the number of signals/literals.
  If several -c options are specified, they are processed from left to right.

  -g[!][N] - Filter gates/latches used for logic decomposition.
  This option restricts the class of gates/latches which can be used
  by the decomposition algorithm as follows: `!' disables using
  latches, and N>1 is the maximal allowed number of gate/latch
  inputs (not counting the feedback for latches). For example,
  -g! disables the use of latches but allows all combinational gates
  from the library, -g2 allows to use only combinational gates and
  latches with up to two inputs (plus the feedback input for latches),
  and -g!2 combines the effect of -g! and -g2, i.e. it allows only
  combinational gates with up to two inputs. This option is
  available only in the logic decomposition (-T) mode.

  -i[+|-] - Specify whether to generate inclusion constraints.
  Inclusion constraints usually speed up the computation,
  but might lead to incorrect results for non-conflict-free
  prefixes. If this option is not specified, inclusion
  constraints are generated iff the prefix is conflict-free.
  This option is available in the following modes: -C[c|n|u],
  -I[e|g|s], -F[a|e|s], -R, -T.

  -jN - The number of working threads.
  By default, N is equal to the number of processors. Currently, only
  unfolding prefix constructon (including when called indirectly or in the
  -B mode) is parallelised, though the option is available in all modes.

  -l - Replicate places with multiple self-loops.
  Each transition reading a particular place gets its own copy of that place.
  This transformation may significantly reduce the size of unfolding prefix
  for nets with many self-loops. This option is available in all modes.

  -mN - Use method N (1-9).
  For some of the modes several solving methods are implemented,
  and this option allows one to specify which of them to use.
  This option is available in the following modes:
    -D (deadlock detection):
       -m1 - use cut-offs
       -m2 (default) - ignore cut-offs
    -C[c|n|u] (CSC/normalcy/USC checking):
       -m1 (default) - process all signals/places together
       -m2 - process each signal/place in turn
  It is an error to specify this option in any other mode, or
  to specify the method which is not defined for the current mode.

  -nN - Switch to memory efficient unfolding algorithm after N events.
  Initially a fast algorithm based on concurrency relation is used, which
  takes much memory. After N non-cut-off events are generated, the
  concurrency relation is deleted and a slower but more memory efficient
  algorithm is used. By default, N=50000.
  If N=0, the concurrency relation is not created. Ignored in the -M mode.

  -pN - Controls the use of parallel (concurrent) inserions.
  The possible values of N:
    0 - concurrent insertions are not allowed
    1 - only valid concurrent insertions of the form
        u-||n->t, where u is in ****t, are allowed
    2 - all valid concurrent insertions are allowed
  This option is valid only in the -R, -T, and -I[e|g|s] modes
  (the latter may trigger encoding conflict resolution). The default
  is -p0 for the -I[e|g|s] and -R modes, and -p2 for the -T mode.

  -q - Quit early, after checking the property syntax.
  This option is valid only in the -F[a|e|s]modes. The <in_file>
  does not have to be supplied if this option is given, but if
  it is, in addition to checking the predicate syntax, the predicate is
  also expanded using the unfolding prefix to check the correctness of
  references in the predicate. The actual verification is not performed.

  -r - Allows to use concurrency reduction for encoding conflict resolution.
  This option is valid only in the -R mode. For safety reasons, it is
  disabled in the -I[e|g|s] and -T modes which may trigger conflict
  resolution. One should be careful when using this option: concurrency
  reduction changes the contract between the circuit and its environment
  in a potentially breaking way.

  -t - Perform logic decomposition down to the gate/latch level.
  New signals are inserted until each local signal can be mapped to a single
  gate/latch in the library (perhaps, with input and/or output inversions).
  (If the option is not given, some of the local signals can be implemented
  by several gates.) This option requires more time, but produces solutions
  consistent with Petrify, so Petrify's technology mapping can be used.
  This option is valid only in the -T mode.

  -vN - The verbosity level (0<=N<=9, the default is 0).
  This option is available in all modes.

  -w[N] - Wait for user 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.
  If memory is exhausted, the program exits immediately, regardless of -w.
  This option is available in all modes.

PComp command line options

Usage:
    pcomp [options] [@]file...

 The files in the command line are interpreted as STG files, except
 when prefixed with `@', in which case the file should contain a
 list of STG files, one per line (useful for avoiding the shell
 restriction on the length of the command line when composing many
 STGs). All the STGs, both in the command line and in the `@'-prefixed
 files, are used for composition.

 * The output signals of the STGs must be disjoint (this constraint
   can be waived with the -o option), and their union comprises
   the output signals of the composition. On the other hand, the input
   signals can be shared by several STGs, and also an output signal of
   some STG can be an input signal of zero or more other STGs.
 * The internal and dummy signals, as well as places, are renamed
   whenever necessary to avoid name clashes.
 * The composed STG is simplified by removing duplicate places.
 * 2-phase, 4-phase and mixed-phase STGs can be liberally composed.

Options:
  -d  Convert the common interface signals into dummy signals
      (useful for composing handshake components).
  -f[file]
      Stores the composed STG in file rather than standard output.
      The extension (.g, .pnml, or .pnml.gz) determines the format.
      If file is not specified, pcomp.g is used.
  -h  Print this help message and exit.
  -i  Convert the common interface signals into internal signals
      (useful for composing handshake components).
  -l[file]
      If the file name is not provided then `pcomp.xml.gz' is used.
      If the file name ends with `.xml' or `xml.gz' then the
      correspondence between the places and transitions of the
      component STGs and those of the composed STG is stored.
      Otherwise place names of the composed STG are stored, so that
      the i-th line corresponds to the places of i-th component STG
      Note that the same place can occur in several lines - this
      happens when some duplicate place is removed, and some
      equivalent place is listed instead.
  -o  Allow the STGs to share outputs.
  -p  Before doing the parallel composition, remove places whose
      presets do not contain dummy transitions and whose postsets
      contain only shared input signals on which the labelling is
      injective. This transformation results in a composed STG with
      fewer places, which has bisimilar behaviour provided the
      composition is free from computational interference. This
      option is incompatible with -o.
  -r  Rename all dummy transitions, so that their names do not
      contain '+', '-', or '/'. (Needed for compatibility with tools
      that do not allow dummy transitions to have signs, e.g. Petrify.)
  -u  Keep unused signal transition phases. This option considers
      e.g. x+ and x- as independent transition labels. By default,
      if two STGs are composed, and one of them has x+ but no x-,
      while the other has x- but no x+, the composed STG will have
      no transitions labelled by either x+ or x-. However, if this
      option is specified, both labels will occur in the composed STG.

Punf command line options

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.

Table of Contents

Command line options of backend tools

Petrify command line options

MPSat command line options

PComp command line options

Punf command line options