MPSat command line options
mpsat <mode> [<options>] [<in_file>] [<out_file>]
The <mode> is one of the following:
-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.
-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).