Matlab

Installation

The installation script (install.m) is contained in distribution/matlab. You need to execute it once.

⚠️ WARNING: The Matlab integration only works with the Java 8 version of Moonlight. Refer to the java8 branch to install it.

Alternatively, we recommend to interact with it via python!

Getting Started

Temporal Example

Let start from a simple example (multipleMonitorSimple.m) that you can find in example/TemporalExamples/SimpleExamples/

The script which defines formulas, domain, and type, is contained in multipleMonitor.mls.

% file multipleMonitor.mls

signal { real x; real y}
domain boolean; 
formula future = globally [0, 0.2]  (x > y);
formula past = historically [0, 0.2]  (x > y);

As you can see, it is a temporal script, there are two formulas: future and past and the domain is Boolean.
The signal should be composed of two real values, represented by the variable x and y.
For more details about Moonlight scripts, please visit the dedicated section

This script has been loaded and used in multipleMonitor.m which is reported below

% file multipleMonitorSimple.m

clear
close all;

%% STEP 1: generating signal
trajFunction = @(t)[sin(t);cos(t)]';
time = 0:0.1:3.1;
values = trajFunction(time);

%% STEP 2: loading the MoonLight Script
moonlightScript = ScriptLoader.loadFromFile("multipleMonitors");

%% STEP 3 (optional): change the domain on the fly
moonlightScript.setMinMaxDomain();

%% STEP 4: getting the monitor associated with a target formula
boolFutureMonitor = moonlightScript.getMonitor("future");

%% STEP 5: monitor the signal 
boolFutureMonitorResult = boolFutureMonitor.monitor(time,values);

As you can see there are 5 steps:

• STEP 1: define a temporal signal
• STEP 2: loading the MoonLight Script from a file named multipleMonitors.mls and contained in the same folder as our MATLAB script (i.e., multipleMonitorSimple.m). We use the method loadFromFile of the MATLAB class ScriptLoader. In the same class, there is also the method named loadFromText to load a script directly from a StringArray define within MATLAB. We use this method in the spatio-temporal example reported below.
• STEP 3 (optional): we can decide to change the domain of the script by using one of the two methods setMinMaxDomain() or setBooleanDomain() to set the minmax or Boolean Domain, respectively.
• STEP 4: getting the monitor associated with a target formula. We use the method getMonitor("future") which accepts the name of the formula we are going to use.
• STEP 5: finally we can use the generated monitor (boolFutureMonitor) to monitor a proper temporal signal. The method is monitor(time,values). If there are parameters in the script, you have to define their values by passing an array (e.g., parametersVector) to this method: monitor(time,values,parametersVector). For an example, see example/TemporalExamples/SimpleExamples/parametricMonitor.m

boolFutureMonitorResult is a matrix containing the output signal (i.e., generated by the monitor). The first column represents the time step, the second column the values associated with each time step.

boolFutureMonitorResult = 
    0.0000   -1.0000
    0.1000   -0.8952
    0.2000   -0.7814
    0.3000   -0.6598
     .....    ..... 

Spatio-temporal Example

Let start from a simple example (sensorNetworkTestScript.m) stored in SpatioTemporalExamples/SensorNetworkExamples/

In this case, we define the MoonLight Script directly in MATLAB, as reported below:

% file sensorNetworkTestScript.m

clear;
close all;

%% STEP 1: define a spatial-temporal model.
numSteps        = 7;   % number of frames
num_nodes       = 10;    % number of nodes
framePlot = false; % to enable or disable the plot of the graph
% see the sensorModel function for the description of the output
[~,spatialModel, time, values]= sensorModel(num_nodes,numSteps, framePlot);

script= [
"signal { int nodeType; real battery; real temperature; }",...
"space {edges { int hop; real dist; }}",...
"domain boolean;",... 
"formula P1 = ( nodeType==3 ) reach (hop)[0, 1] ( nodeType==1 | nodeType==2 ) ;",...
"formula P2 = escape(hop)[5,inf] (battery > 0.5) ;",...
"formula P3 = somewhere(dist)[0,250] (battery > 0.5))"
];

%% STEP 2: loading the MoonLight Script for a stringArray variable (i.e., script)
moonlightScript = ScriptLoader.loadFromText(script);

%% STEP 3 (optional): change the domain on the fly
moonlightScript.setMinMaxDomain();

%% STEP 4: getting the monitor associated with a target formula
spTempMonitor = moonlightScript.getMonitor("P3");

%% STEP 5: monitor the signal 
result = spTempMonitor.monitor(spatialModel,time,values);

Similarly to the temporal example, there are 5 steps:

• STEP 1: define a spatio-temporal model. We use sensorModel.m to produce a spatio-temporal with a number of locations equals to num_nodes and 7 time steps (i.e., numSteps)

  • time: an array of time points at which observations are provided;
  • spatialModel: an array of MATLAB specifying the spatial structure (a graph structures) at each point in time;
  • values: a map (a cell array), with a cell for each node. In each cell, there is a matrix (n×m) where each row represents the values of the signals at the time points specified by time (with n equal to the number of time points and m the number of the considered signals)

• STEP 2: loading the MoonLight Script. In this case, we load the script saved in a string array variable named script. We use the method loadFromText of the class ScriptLoader

• STEP 3 (optional): we can change the default domain of the script by using one of the two methods setMinMaxDomain() or setBooleanDomain() to set the MinMax or Boolean domain, respectively.

• STEP 4: getting the monitor associated with a target formula. We use the method getMonitor("P3") which accepts as an argument the name of the formula that we want to use.

• STEP 5: finally, we use the generated monitor (i.e., spTempMonitor) to monitor a proper spatio-temporal signal. We use the monitor method which accepts the spatio-temporal signal (i.e., spatialModel, time, and values). The result is a matrix with a number of rows equals to the location size (10 in this case). Each nth-row stores the monitor result of the formula in the nth location. The monitor result is a temporal signal that we save as a matrix: the first column represents the time points and the second column the value of the semantics of the formula at each time point. See below.

result(3,:,1) =  [ 1     2     3     4     5     6     7 ]
result(3,:,2) = [-0.0309    0.0274    0.3574    0.3999    0.4448    0.3263    0.3564]

• result(3,:,1) is the vector of time points
• result(3,:,2) is the value of the minmax semantics of P3 at each time points of result(3,:,1) at location 3.