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.
