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, please download the STLmc tool, following the instructions. The tool is available for Linux (64-bit) and macOS (64-bit).

---

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.counterexample -output html

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 degrees 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]$.