Command Line Options
The STLmc tool provides a command-line interface with various command line options, summarized in Table [2].
| Option | Explanation | Default |
|---|---|---|
| $\textsf{-bound}<N>$ | a discrete bound $N$ | - |
| $\textsf{-time-bound}<\tau>$ | a time bound $\tau$ | - |
| $\textsf{-time-horizon}<T>$ | a mode duration bound $T$ | $\tau$ |
| $\textsf{-threshold}<\epsilon>$ | a robustness threshold $\epsilon$ | $0.01$ |
| $\textsf{-goal}<N>$ | the list of STL goals to be analyzed | all |
| $\textsf{-solver}<\textsf{Solver}>$ | an SMT solver to be used ($\textsf{auto}$/$\textsf{z3}$/$\textsf{yices}$/$\textsf{dreal}$) | $\textsf{auto}$ |
| $\textsf{-path-strategy}<\textsf{Strategy}>$ | handle transition paths symbolically or explicitly | $\textsf{symbolic}$ |
| $\textsf{-two-step}$ | use the two-phase optimization | disabled |
| $\textsf{-concrete}$ | disable unsat-core scenario generalization in two-step solving | disabled |
| $\textsf{-parallel}$ | parallelize the two-phase optimization | disabled |
| $\textsf{-parallel-core}<N>$ | the maximum number of parallel solver workers | $25$ |
| $\textsf{-solver-batch-size}<N>$ | the maximum candidates combined in one solver query | $1$ |
| $\textsf{-core-minimize-attempts}<N>$ | the number of minimized unsat cores tried per scenario | $1$ |
| $\textsf{-reach}$ | interpret a selected state goal as a reachability target | disabled |
| $\textsf{-visualize}$ | generate counterexample or witness data | disabled |
| $\textsf{-verbose}$ | print detailed progress information | disabled |
| $\textsf{-precision}<\delta>$ | a precision parameter for $\textsf{dreal}$ | $0.001$ |
| $\textsf{-save-smt2}$ | save every SMT2 query sent to the underlying solver | disabled |
| $\textsf{-smt2-dir}<\textsf{DIR}>$ | a directory for saved SMT2 queries | $\textsf{smt2-logs}$ |
Table.2: The command line options of STLmc
A discrete bound $N$ limits the number of mode changes and the number of variable points—points at which the truth value of an STL subformula changes—along a trajectory. For reachability, it limits the number of jumps. A time horizon $T$ limits the duration of each continuous segment. The option $\textsf{-two-step}$ enables abstraction-based two-step solving, while $\textsf{-parallel}$ runs its refinement checks concurrently. When the option $\textsf{-visualize}$ is set, STLmc generates counterexample or reachability-witness data that can be exported as an HTML graph, a PDF graph, or a text report. Among the STL formulas specified in the input model file, formulas to be analyzed are chosen using the $\textsf{-goal}$.
We can choose different SMT solvers using the $\textsf{-solver}$ option. The STLmc tool currently supports three SMT solvers: Z3, Yices2 and dReal. With $\textsf{auto}$, the underlying solver is chosen according to the model’s formula and dynamics. Z3 and Yices2 can deal with linear and polynomial functions. dReal can approximately handle nonlinear ODEs—which generally make reachability undecidable for hybrid automata—up to a given precision $\delta > 0$.
Reachability and Solving Strategies
A model may declare a reach goal directly. The -reach option can also
interpret a selected ordinary state goal as a reachability target:
stlmc system.model -goal target -reach
A reachable query reports reachable and, with -visualize, writes a
.witness artifact. Ordinary STL model checking reports violated when it
finds a counterexample and continues to use the .counterexample suffix.
Path exploration and continuous solving can be selected independently. The default is symbolic one-step solving. The four combinations are:
stlmc system.model -path-strategy symbolic
stlmc system.model -path-strategy symbolic -two-step
stlmc system.model -path-strategy explicit
stlmc system.model -path-strategy explicit -two-step
The -solver-batch-size option controls how many final candidates are combined
in one solver OR query. A value of 1 checks candidates individually.
Saving SMT2 Queries
By default, STLmc does not retain the SMT2 queries sent to the underlying
solver. Use -save-smt2 to save queries for dReal, Z3, and Yices:
stlmc model.model -save-smt2
The queries are written below smt2-logs/<solver>/. A different output
directory can be selected with -smt2-dir:
stlmc model.model -save-smt2 -smt2-dir solver-inputs
Saved filenames identify the model, goal, solver, and bound. For the two-step algorithm, they also identify the scenario. Existing files are not overwritten; STLmc adds a numeric suffix when necessary.