Usage:
mpsat mode [options] inputfilename [outputfilename]
Modes:
Reachability-like properties checking modes:
-D Deadlock checking.
-F Find a reachable marking satisfying a given REACH predicate.
-Fs Find a reachable STG state satisfying a given REACH predicate.
-Fa Check an SVA-like assertion (a global invariant).
The -Fs mode differs from -F in the following ways:
* only configurations without maximal dummy events are explored;
* REACH operators referring to STG signals become available;
* the semantics of REACH operator '@' checking the enabledness status
of an event/transition/signal changes: in addition to the usual Petri
net enabledness, an entity can be enabled via a sequence of dummies.
The -Fa mode differs from -Fs in the following ways:
* the syntax is SVA-like, i.e. a Boolean formula that can refer only to
values of STG signals;
* a global invariant rather than a reachability predicate is checked,
i.e. to check the same property using -Fs one has to invert it.
Encoding conflicts detection and resolution modes:
-C CSC conflict detection.
-N Normalcy property checking mode.
-R Resolve encoding conflicts.
-U USC conflict detection.
Synthesis modes:
-E Derive complex-gate implementation.
-G Derive gC-elements implementation.
-S Derive standard-C implementation.
-T Logic decomposition and technology mapping (experimental).
At most one the listed modes may be specified.
For the modes -C, -E, -Fs, -Fa, -G, -N, -R, -S, -T, -U the
file inputfilename must be an STG unfolding. If the
legacy *.mci format is used then transition names 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
in a more elegant way information, and also fixes other issues.
The original STG must be consistent. Moreover, it should
satisfy the CSC property for any of the synthesis modes (-E, -G, -S, -T).
The normalcy property should hold to avoid inverters on gates' inputs.
Normalcy violation can be caused by the following factors:
- An event have triggers with different signs. If this is
the case, mpsat prints a trace leading to that event.
- 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, mpsat prints two traces
leading to these instances.
- There is a CSC conflict. If this is the case, mpsat prints
results similar to the -C mode.
- Nothing above. Then mpsat makes hypothesis about the
normalcy type of each signal, based on the signs of the triggers.
Then it tries to disprove the made hypothesis, and if it is
possible, mpsat prints three traces: one to show the
event for which a hypothesis was made, and the other two to
show the violation of normalcy by definition.
Options:
-! - Disable branching on auxiliary variables.
Some of the variables in the formula might 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.
-@ - Output configurations rather than traces.
The numbering of events starts from 1.
This option is available in the following modes:
-C, -D, -F, -Fs, -Fa, -N, -U; it is silently ignored in any other 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, -D, -F, -Fs, -Fa, -N, -R, -T, -U. It is an error to specify this
option in any other mode. This option must not be specified
together with the -f option.
-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 if the input file is not a merged process.
-c[s|l|COEFF=EXPR] - Specifies the coefficients for the cost function.
This option is valid only in the encoding conflict resolution (-R) and
logic decomposition and technology mapping (-T) modes and it is silently
ignored unless also the -f option is specified.
This option specifies the coefficiens for the function computing the
cost of the transformation (signal insertion 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
usc: the number of unresolved USC cores
del: the number of delayed transitions
trig: the number of triggers of output and internal transitions
seq: the number of sequential insertions (or |U| if a concurrency
reduction U-n->t was applied)
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 the option -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*O,
where I is the numbers of inputs and O is the numbers of output or
intermal 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; the default expressions are:
csc=#s*8, usc=#s*4, del=#s*2, trig=#s*1, seq=#s*4, conc=#s*8, lock=50.
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.
-d string - Specifies additional mode-dependent data.
This option is available in the following modes:
-F[s] (extended reachability analysis) - the string must either
contain a REACH proterty the target state should satisfy or be of
the form @filename to name the file containing a REACH proterty.
-T (logic decomposition and technology mapping) - the string must
name the file containing a gate library in the GENLIB format.
It is an error to specify this option in any other mode.
-f - Looking for a solution minimising the cost function (might be slow).
Usually this means that the sum of the lengths of the traces
is minimised, though the criterion is different in the
normalcy (-N) and encoding conflict resolution (-R) modes.
This option is available in the following modes:
-C, -D, -F, -Fs, -Fa, -N, -R, -T, -U. It is an error to specify this
option in any other mode. This option must not be specified
together with the -a option.
-g[[!][N]] - Specifies gates/latches used for logic decomposition.
This option restricts the class of gates/latches which can be used in
the main loop of 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). The other
gates/latches in the library still may be used during the technology
mapping phase. For example, -g! disables the use of latches but allows
all the 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 to use only combinational gates with up to two inputs.
This option is available only in the logic decomposition (-T) mode.
-l[+|-] - Specifies 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, -E, -Fs, -Fa, -G, -N, -R, -S, -T, -U. It is an error to specify
this option in any other mode.
-mN - Using method N (1-9).
For some of the modes several solving methods are implemented,
and this option allows one to specify which one is to be used.
This option is available in the following modes:
-D (deadlock detection):
-m1 - use cut-offs
-m2 (default) - ignore cut-offs
-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.
-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 encoding conflict resolution (-R)
and logic decomposition and technology mapping (-T) modes.
It is an error to specify this option in any other mode.
The default is -p0.
-r - Allows to use concurrency reduction for encoding conflict resolution.
This option is valid only in the encoding conflict resolution (-R) mode.
One should be careful when using this option: the resulting STG is guaranteed
to be correct only if all the transitions of the STG are weakly fair. Note
that this assumption is not compositional: if concurrency reductions are
performed both in the STG and in its environment, a deadlock can be
introduced, even if the STG and the environment were initially weakly fair.
-s - Store the CNF formula for an external SAT solver.
This option is available in all modes.
-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 logic decomposition (-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 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.
This option is available in all modes.
-x - Saves the results in mpsat.xml.
This option is available in all modes.
