Install the STLmc Tool
STLmc requires CPython 3.11 through 3.14. Create and activate a virtual environment on Linux or macOS:
python3.11 -m venv .venv
. .venv/bin/activate
python -m pip install --upgrade pip
Install the latest available prerelease:
python -m pip install --pre stlmc
For detailed setup and troubleshooting, see the installation guide.
Install Solvers and Visualization
The default package includes no solver backends or HTML/PDF renderers. For a first installation, install Z3 and both renderers:
stlmc-installer install --solver z3 --visualize html pdf
stlmc-installer check --solver z3 --visualize html pdf
Additional solvers can be installed as needed. Z3 is also required by the default internal reasoning backend when another final solver is selected:
stlmc-installer install --solver cvc5 yices dreal
Native solver availability depends on the platform. The managed dReal download is the official 3.16.06.02 release; Apple Silicon requires Rosetta. This release has known correctness limitations for some ODE invariants. Parallel final Yices checks require a thread-safe native library. See dReal on Apple Silicon and Yices on macOS for platform-specific setup.
Run STLmc
After installing STLmc and the solver/renderers above, install and check the GUI dependencies in the same activated virtual environment:
stlmc-installer install --ui
stlmc-installer check --ui
Start the locally hosted GUI:
stlmc-gui
The browser opens at http://127.0.0.1:8766/. Keep the terminal open, then
paste its session token into the GUI and choose Connect. Models and analyses
remain on your computer. See the GUI user guide
for editing files, analysis settings, results, and SSH connections.
Follow the tutorial for a complete model, executable commands, and counterexample plots. To see the available options:
stlmc -h
stlmc-vis -h
HTML output uses Bokeh and PDF output uses Matplotlib; Gnuplot is not required.
Text reports need no additional renderer. The -visualize option saves data
for later rendering, rather than opening a graph. Use the filename printed
by STLmc with stlmc-vis as shown in the tutorial.
Older pickle-based result files are unsupported; rerun model checking to
generate current .counterexample or .witness files.