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.