Script Syntax

A monitor in MoonLight is specified via a MoonLight script.
Consider the following

(1) signal { int nodeType;  real battery;  real temperature; } 
(2) space { edges { int hop; real dist; }  } 
(3) domain boolean;
(4) formula atom = (nodeType==3);
(5) formula P1 = atom reach(hop)[0, 1] {(nodeType==1) |  (nodeType==2)};
(6) formula Ppar(int k) = atom reach(hop)[0, k] (nodeType== 2);

Script Description

The script (line 1) starts with the definition of the domains of input signal. We recall that STREL is interpreted over spatio-temporal signals. In our scenario, these values are: the type of node, the temperature level, and the battery level.

As domains, the node type is represented by an integer (int) and the battery and temperature by real values (real). Spatial structures in STREL can change over time. This enables to model the behaviour of the mobile nodes in our example by updating edges and edge labels. The edges can have more than one label with different domain. These are defined in line 2 of our example. In this case we have two labels: hop having type int domain, and dust with type real. Note that, if one is only interested in temporal properties, this part is omitted in the script.

MoonLight, like STREL, supports different semantics for monitoring. A user can specify the desired one by indicating the specific monitoring domain (line 3). Currently, MoonLight supports qualitative (boolean) and quantitative (minmax) semantics of STREL.

After this initial declarations, a script contains the list of formulas that can be monitored (lines 4-6). Formulas can have parameters that are instantiated when monitoring is performed. A formula can be used within another formula.

Syntax of formulas

Formulas are built by using standard Boolean operators:

• negation: !
• conjunction: &
• disjunction: |
• implication: =>

Atomic Expression

An atomic expression consists of Boolean expressions on signal variables like, for instance

(battery > 0.5) | (nodeType == 2)

As expected, the interpretation of atomic formulas depends on the domain of the monitoring.

Temporal Properties

Temporal properties are specified via the standard until and since operators from which we can derive the future eventually and always operators and the corresponding past variants, once and historically.

All these operators may take an interval of the form [exp1,exp2] to define where the property should be evaluated. Such an interval can be omitted in case of unbounded temporal operators.

Examples:\

formula phi1 = eventually[1,2](battery > 0.5)
formula phi2 = globally(X > 2)
formula phi3 = once[1,2](battery > 0.5)
formula phi4 = historically[3,4](X > 2)

Spatio-temporal Properties

Spatial modalities, instead, are reach and escape operators, and the derivable operators somewhere and everywhere. All these operators may be decorated with a distance expression and a distance interval. The distance expression consists of an expression that is used to compute the length of an edge. If omitted, the real value 1.0 is used. Let us consider the following property

P1 = (nodeType==3)reach(hop)[0, 1]{(nodeType==1)|(nodeType==2)}

P1 holds if from a node of type3 (an end device), we can reach a node of type1 or 2(a coordinatoror a router), following a path in the spatial graph such that the hop distance along this path (i.e. its number of edges) is not bigger than 1.

The other operator of STREL, escape, can be used to express the ability to move away from a given point. Let us consider the following property

P2 = escape(hop)[5,inf] (battery > 0.5)

P2 states that from a given location, we can find a path of (hop) length at least 5 such that all nodes along the path have a battery level greater than 0.5 To specify properties around a given location, operators somewhere and everywhere can be used.

P3 = somewhere(dist)[0,300] (battery > 0.5))

P3 is satisfied (at a given location) whenever there is a node at a distance between 0 and 300 having a battery greater than 0.5.

The everywhere operator works in a similar way, however, it requires that its subformula all nodes satisfying the distance constraints.

P4 = everywhere(dist)[0, 10]{eventually[0,5](battery > 0.5)}

More details and examples about STREL can be found here