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{-two-step}$ | use the two-phase optimization | disabled |
| $\textsf{-parallel}$ | parallelize the two-phase optimization | disabled |
| $\textsf{-visualization}$ | generate extra visualization data | disabled |
| $\textsf{-solver}<\textsf{Solver}>$ | an SMT solver to be used ($\textsf{z3}$/$\textsf{yices}$/$\textsf{dreal}$) | $\textsf{z3}$ |
| $\textsf{-precision}<\delta>$ | a precision parameter for $\textsf{dreal}$ | $0.001$ |
Table.2: The command line options of STLmc
A discrete bound $N$ limits the number of mode changes and the number of variable points-at which the truth value of some STL subformula changes-in trajectories. A time horizon $T$ limits the maximum time duration of single modes in trajectories. The options $\textsf{-two-step}$ and $\textsf{-parallel}$ enable the (parallelized) two-phase optimization. When the option $\textsf{-visualize}$ is set, extra data for visualization is generated. 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. The underlying solver is chosen depending on the flow conditions of a hybrid automaton. Z3 and Yices2 can deal with linear and polynomial functions, and dReal can deal with nonlinear ODEs-which is undecidable in general for hybrid automata-approximately up to a given precision $\delta > 0$.