We explain how to use our tool to analyze hybrid systems using the two networked thermostats model. The tutorial consists of the following sections:

1. Running the STLmc Tool
2. Analyzing the Counterexample

---

Prerequisite

Before the tutorial, install STLmc by following the instructions and make sure that dReal is available:

stlmc-install-solvers dreal

Automatic dReal installation supports macOS and x86-64 Linux.

---

Two Networked Thermostat Systems

We consider the following hybrid automaton (Figure [1]) with three STL properties (Table [1]). To see the detailed explanation of the model and properties, please refer to this page.

Fig.1: A hybrid automaton of thermostat controllers

Label	STL formula
$\textsf{f1}$	$\lozenge_{[0,3]} ((x_0 \geq 13) \mathbf{U}_{[1,\infty)} (x_1 < 22))$
$\textsf{f2}$	$\square_{[2,4]} ((x_0 - x_1 \geq 4) \to \lozenge_{[3,10]} (x_0 - x_1 \leq -3))$
$\textsf{f3}$	$\square_{[0,10)} ((x_0 - x_1 \geq 4) \mathbf{R}_{[0,\infty)} (x_0 - x_1 \leq -3))$

Table.1: STL properties for thermostat

---

STLmc Input Model

The following code shows the STLmc input model of the above two thermostat controllers:

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;  18 <= x0;  x0 <= 22;
      on1 = 0;  18 <= x1;  x1 <= 22;
proposition:
  [p1]: x0 - x1 >= 4;    [p2]: x0 - x1 <= -3;
goal:
  # bound: 5, timebound: 30, solver: dreal
  [f1]: <>[0, 3](x0 >= 13 U[0, inf) x1 <= 22);  # threshold: 1.0, time-horizon: 7 
  [f2]: [][2, 4](p1 -> <>[3, 10] p2);		# threshold: 2.0, time-horizon: 30
  [f3]: [][0,10] (x0 > 23 R[0,inf) p1);		# threshold: 2.0, time-horizon: 7

We use the STLmc modelling language to specify the model and its properties. To see more detailed explanation of the langauge, please refer to our technical report or this page.

---

Running the STLmc Tool

We can run the STLmc tool for the $\textsf{f2}$ formula of the thermostat model with a time bound $\tau = 30$, a discrete bound $N = 5$, and a threshold $\epsilon_2 = 2.0$ as input parameters as follows:

stlmc ./therm.model -bound 5 -time-bound 30 -threshold 2 \
      -goal f2 -solver dreal -two-step -parallel -time-horizon 30 -visualize

Because the model has nonlinear dynamics, we use $\textsf{dReal}$ for an underlying solver with the algorithm $\textsf{2-step}$. For efficient model checking, we use the $\textsf{parallel}$ option. For the formulas $\textsf{f1}$ and $\textsf{f3}$, we choose thresholds $\epsilon_1 = 1.0$ and $\epsilon_3 = 2.0$, respectively.

We can run the STLmc tool using the following command:

stlmc <model file> <option1> <option2> ...

To see more command line options, use stlmc -h or refer to this page

---

Analyzing the Counterexample

The formula $\textsf{f2}$ is violated. The following command generates visualization graphs from the extra data for the visualization.

stlmc-vis ./therm_b5_f2_dreal.counterexample -output html

A counterexample can also be exported as a human-readable text report without generating a graph or providing a visualization configuration file.

stlmc-vis ./therm_b5_f2_dreal.counterexample -output text

This command creates therm_b5_f2_dreal.counterexample.txt. The report contains the analyzed goal and formula, constants, variable ranges, and the initial condition. For each bound, it shows the start and end times, selected mode, invariant and flow conditions, continuous-variable values, next mode, and available jump candidates.

Fig.2: Visualization of a counterexample (a horizontal dotted line denotes $\epsilon = 2.0$)

Figure [2] shows the visualization graphs for $\textsf{f2} = \square_{[2, 4]} (x_0 - x_1 \geq 4 \rightarrow \lozenge_{[3, 10]} (x_0 - x_1 \leq -3))$ with the subformulas:

\begin{align*} \textsf{f2}_{\textsf{1}} &= x_0 - x_1 \geq 4 \rightarrow \lozenge_{[3, 10]} (x_0 - x_1 \leq -3) \qquad \textsf{f2}_{\textsf{2}} = \neg (x_0 - x_1 \geq 4) \\\ \textsf{f2}_{\textsf{3}} &= \lozenge_{[3, 10]} (x_0 - x_1 \leq -3) \qquad \textsf{f2}_{\textsf{4}} = x_0 - x_1 \leq -3 \qquad \textsf{f2}_{\textsf{5}} = x_0 - x_1 \geq 4 \end{align*}

The robustness degree of $\textsf{f2}$ is less than $\epsilon$ at time $0$, since the robustness degree of $\textsf{f2}_{\textsf{1}}$ goes below $\epsilon$ in the interval $[2, 4]$, which is because both the degrees of $\textsf{f2}_{\textsf{2}}$ and $\textsf{f2}_{\textsf{3}}$ are less than $\epsilon$ in $[2, 4]$. The robustness degree of $\textsf{f2}_{\textsf{3}}$ is less than $\epsilon$ in $[2, 4]$, since the robustness degree of $\textsf{f2}_{\textsf{4}}$ is less than $\epsilon$ in $[5, 14] = [2, 4] + [3, 10]$.