Tutorial

Checking Three Thermostat Properties

Check three nested STL properties of two networked thermostats over ten time units, then inspect a counterexample through temperature and robustness plots. The model starts at fixed temperatures $x_0=20$ and $x_1=18$ with both heaters off.

Model

Two rooms exchange heat through an open door. Each room has a heater, but the controller allows at most one heater to be on at a time.

Variables	Meaning	Initial state
`x0`, `x1`	Room temperatures, with declared range `[10,35]`	`x0 = 20`, `x1 = 18`
`on0`, `on1`	Heater switches: `0` means off, `1` means on	Both are off

The three modes are both heaters off, only the second on, and only the first on. Temperatures are continuous across mode switches and follow each mode’s ODEs between switches. on1 > 0.5 tests whether the second heater is on. The controller permits this heater to switch off once x1 >= 26; it does not require it to heat the room to 30.

Install the Prerequisites

Follow the installation instructions for the current STLmc version, in a virtual environment with CPython 3.11–3.14. Then install the default internal reasoning backend, dReal, and the HTML/PDF renderers:

stlmc-installer install --solver z3 dreal --visualize html pdf

stlmc-installer check --solver z3 dreal --visualize html pdf

The official dReal 3 download supports Linux x86-64 and Intel macOS; Apple Silicon requires Rosetta. See the detailed installation guide for platform restrictions and the official solver’s known limitations. Installation checks are not a general guarantee of ODE correctness.

Run in the GUI

Complete the prerequisites above first. In the same activated STLmc environment, install and check the GUI dependencies:

stlmc-installer install --ui

stlmc-installer check --ui

For a locally hosted GUI, run:

stlmc-gui

This opens http://127.0.0.1:8766/; keep the terminal open and connect using its Session token. The API on port 8765 is not a web page.

Alternatively, to use this website’s GUI, run the following command instead, then open the link. Analysis still runs on your computer, not on the website:

stlmc-gui --allow-origin https://stlmc.github.io --no-browser

For a local website preview, replace the allowed origin with the preview’s exact scheme, hostname, and port. Paste the terminal’s Session token and choose Connect. The default Bridge URL, under Advanced connection settings, is http://127.0.0.1:8765. Allow local-network access if your browser asks.

Safari: Connecting from this HTTPS website to the local HTTP bridge is currently unsupported: Safari blocks the request as mixed content, even with the correct --allow-origin setting and session token. Use the locally hosted GUI at http://127.0.0.1:8766/ in Safari instead. This restriction concerns the connection from this website, not running STLmc or using the local GUI.

The following steps apply to either GUI. See the GUI user guide for file management, run history, and remote connections.

Download therm-tutorial.model and therm-tutorial.cfg.
Use Open model file and Open configuration to select these files.
Select All goals from Goal. Set Final solver to dreal, Bound to 4, Global time bound to 10, and Robustness threshold to 0. Leave Reachability target unchecked. Under Advanced options, enable Two-step solving, leave Explicit paths unchecked, and set Wall-clock timeout (seconds) to 240. Goal labels and settings are read by STLmc’s parser from the loaded model and configuration; only form fields you edit override the configuration.
Choose Run analysis. The reference results are f1 and f2 satisfied up to bound 4, and f3 violated at bound 2.
Open Visualization to inspect the interactive temperature and robustness plots. The submitted model is named input.model. The generated data and HTML files are:
```
input_b2_f3_dreal.counterexample
input_b2_f3_dreal.counterexample.html
```

The GUI and CLI walkthroughs were checked on Linux with the official dReal 3.16.06.02 binary installed by default. Execution times and the particular trace can vary. Interactive plots load Bokeh from its CDN and may require internet access.

Command-line Walkthrough

The following steps run the same example without the web workspace.

Download the Model

Download therm-tutorial.model into an empty working directory. For example:

mkdir -p stlmc-tutorial

cd stlmc-tutorial

curl -fL https://stlmc.github.io/assets/files/benchmarks/therm-tutorial.model -o therm-tutorial.model

The model declares three properties:

\[\begin{aligned} \textsf{f1} &= \square_{[0,8]}\lozenge_{[0,2]}(x_0\geq9),\\ \textsf{f2} &= \lozenge_{[0,2]}\square_{[0,8]}(x_1\geq9),\\ \textsf{f3} &= \square_{[0,5]}\bigl((\mathit{on1}>0.5)\Rightarrow\lozenge_{[0,1]}(x_1\geq30)\bigr). \end{aligned}\]

The inner interval is relative to the time selected by the outer operator:

Goal	Outer time	Inner requirement
`f1`: always eventually	Every time $t$ in $[0,8]$	At least once during $[t,t+2]$, $x_0\geq9$
`f2`: eventually always	Some start time $t$ in $[0,2]$	Throughout $[t,t+8]$, $x_1\geq9$
`f3`: always respond	Every time $t$ in $[0,5]$ when heater 1 is on	At least once during $[t,t+1]$, $x_1\geq30$

For example, f1 at time 3 examines $[3,5]$, not the fixed interval $[0,2]$. For f2, choosing start time 1 requires the condition throughout $[1,9]$. The first two properties follow from the declared temperature range $[10,35]$. The third asks whether every on-state of the second heater is followed within one time unit by a temperature of at least 30. This obligation applies at every time the heater is on, not just at its switch-on instant. For example, an on-state at time 3.5 requires a response during $[3.5,4.5]$. Because switching off is allowed from temperature 26, the controller need not meet this stronger response requirement.

The commands below use the downloaded file; you do not need to retype it.

Read or copy the complete model

int on0;                int on1;
[10, 35] x0;            [10, 35] x1;
const k0 = 0.015;       const k1 = 0.045;
const h0 = 100;         const h1 = 200;
const c0 = 0.98;        const c1 = 0.97;
const d0 = 0.01;        const d1 = 0.03;

{ mode: on0 = 0;        on1 = 0;
  inv:  x0 > 10;        x1 > 10;
  flow:
    d/dt[x0] = - k0 * (c0 * x0 - d0 * x1);
    d/dt[x1] = - k1 * (c1 * x1 - d1 * x0);
  jump:
    x0 <= 17 => (and (on0' = 1) (on1' = on1)
                     (x0' = x0) (x1' = x1));
    x1 <= 16 => (and (on1' = 1) (on0' = on0)
                     (x0' = x0) (x1' = x1));
}
{ mode: on0 = 0;        on1 = 1;
  inv:  10 < x0;        x1 < 30;
  flow:
    d/dt[x0] = - k0 * (c0 * x0 - d0 * x1);
    d/dt[x1] = k1 * (h1 - (c1 * x1 - d1 * x0));
  jump:
    x0 <= 17 => (and (on0' = 1) (on1' = 0)
                         (x0' = x0) (x1' = x1));
    x1 >= 26 => (and (on1' = 0) (on0' = on0)
                     (x0' = x0) (x1' = x1));
}
{ mode: on0 = 1;        on1 = 0;
  inv:  x0 < 30;        x1 > 10;
  flow:
    d/dt[x0] = k0 * (h0 - (c0 * x0 - d0 * x1));
    d/dt[x1] = - k1 * (c1 * x1 - d1 * x0);
  jump:
    x1 <= 16 => (and (on0' = 0) (on1' = 1)
                         (x0' = x0) (x1' = x1));
    x0 >= 25 => (and (on0' = 0) (on1' = on1)
                     (x0' = x0) (x1' = x1));
}
init: on0 = 0; x0 = 20;
      on1 = 0; x1 = 18;
proposition:
  [p1]: x0 - x1 >= 4;    [p2]: x0 - x1 <= -3;
goal:
  [f1]: [][0, 8] <>[0, 2] (x0 >= 9);
  [f2]: <>[0, 2] [][0, 8] (x1 >= 9);
  [f3]: [][0, 5] ((on1 > 0.5) -> <>[0, 1] (x1 >= 30));

See the input language guide for the individual sections.

Run the Checks

The checks use these settings:

Option	Meaning in this walkthrough
`-goal`	Select one of the three labeled properties
`-bound 4`	Limit the discrete STL partition, counting mode changes and STL variable points
`-time-bound 10`	Model an execution lasting ten time units
`-time-horizon 10`	Allow each continuous segment to last at most ten time units
`-threshold 0`	Check the property without requiring a positive robustness margin
`-precision 0.000001`	Set dReal’s separate numerical delta tolerance
`-visualize`	Save data for later plotting or text inspection

One-step and two-step are alternative ways of solving the same bounded question. The choices below are for execution performance; they do not change the properties’ meanings. -parallel-core 4 limits the two-step workers to four.

Check all three goals using two-step parallel solving:

stlmc therm-tutorial.model -goal f1 -bound 4 -time-bound 10 -time-horizon 10 -threshold 0 -precision 0.000001 -solver dreal -two-step -parallel -parallel-core 4 -visualize

stlmc therm-tutorial.model -goal f2 -bound 4 -time-bound 10 -time-horizon 10 -threshold 0 -precision 0.000001 -solver dreal -two-step -parallel -parallel-core 4 -visualize

Then check the heater-response goal and save its counterexample:

stlmc therm-tutorial.model -goal f3 -bound 4 -time-bound 10 -time-horizon 10 -threshold 0 -precision 0.000001 -solver dreal -two-step -parallel -parallel-core 4 -visualize

The global time bound is ten time units; time-horizon limits each continuous segment to at most ten time units. Neither is a wall-clock timeout. The discrete bound limits mode transitions and extra STL partition points, not elapsed physical time. Model comments do not set these analysis options.

With STLmc and the official dReal 3.16.06.02 binary, the first two commands report satisfied up to bound 4. The third produces the following counterexample result. The particular trace can vary between runs.

Goal	Result	Interpretation
`f1`	Satisfied up to bound 4	No counterexample to the first temperature check in this search
`f2`	Satisfied up to bound 4	No counterexample to the second temperature check in this search
`f3`	Violated at bound 2	The second heater is on, but its room does not reach 30 within the required response window

Result
  status      : violated at bound 2
  artifacts   : therm-tutorial_b2_f3_dreal.counterexample
                therm-tutorial_b2_f3_dreal.cfg

These queries use robustness threshold zero. dReal’s -precision 0.000001 sets its separate delta-decision tolerance; it is not the robustness threshold or an exact trajectory certificate. A result satisfied up to bound 4 means no counterexample was found within that bounded search, not an unbounded safety proof.

Inspect the Counterexample

When verification finds a counterexample, -visualize writes its data and configuration paths under artifacts in the terminal output. Use those actual paths: the filename contains the discovery bound, which can be smaller than the maximum bound supplied on the command line.

For the example output above, run:

stlmc-vis therm-tutorial_b2_f3_dreal.counterexample -cfg therm-tutorial_b2_f3_dreal.cfg -output html

stlmc-vis therm-tutorial_b2_f3_dreal.counterexample -cfg therm-tutorial_b2_f3_dreal.cfg -output pdf

stlmc-vis therm-tutorial_b2_f3_dreal.counterexample -output text

Open the generated HTML file in a browser for an interactive trajectory and sampled-robustness plot. In this example it is named therm-tutorial_b2_f3_dreal.counterexample.html. The PDF command produces state_x0_x1.pdf and rob_f3_0_f3_1_f3_2_f3_3_f3_4_f3_5.pdf for this example. The text command produces therm-tutorial_b2_f3_dreal.counterexample.txt, listing the model, formula, initial condition, and per-segment state and endpoint data without needing either plotting renderer.

You can also download the counterexample data and its visualization configuration, the text report, or the PDF plots of temperatures and robustness.

The interactive plot below is the HTML output for this example. This saved trace comes from the downloaded model with f3 selected. It shows one obtained trace; another run may choose different switching times. The graphs use reconstructed trajectories and sampled robustness, not an independent exact certificate.

Read the plots in this order:

In the upper plot, follow the x1 temperature using its legend label: its slope changes from cooling to heating near time 3.23, then back to cooling near time 4.50. It reaches about 26 when the heater turns off, then cools again.
In the lower plot, use the legend to inspect f3_5 (the on-state test) and f3_4 (the temperature-at-least-30 condition). An on-state at time 3.5 requires the temperature condition somewhere in $[3.5,4.5]$, but this trace stays below 30.
Compare the full goal f3’s robustness at time zero with the red threshold line at zero. A negative value is the counterexample to the selected goal.

In this trace, the modes change from both heaters off to the second heater on at approximately $3.23$, then back to both off at approximately $4.50$. The heater-on interval lasts about 1.27 time units. Its temperature never reaches 30, so the required response fails even though the controller follows its permitted switch-off rule. Reconstructing the saved trace gives robustness $-0.5$ at time zero. Older pickle-based artifacts cannot be read by the current release; rerun verification to regenerate them.