Matlab

Installation

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

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 value 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. We use the method loadFromFile of the Matlab class ScriptLoader. There is also another method named loadFromText that allows us to load a script directly from a StringArray define with Matlab. Please refer to the Spatio-temporal Example below for more information.
• STEP 3 (optional): we can decide to change the domain of the script on the fly 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 string of the formula name we want to use.
• STEP 5: finally we can use the generated monitor (boolFutureMonitor) to monitor each compatible temporal signal. The methods 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, the second column the values associated with each time.

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 the Matlab Script, see below:

clear;
close all;

%% STEP 1: define a spatial-temporal signal.
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 minmax;",... 
"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,300] (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 signal. This signal is stored in dataInput.mat and it is composed of three parts:

  • 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 domain of the script on the fly 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., boolSpTempMonitor) to monitor a compatible 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 a number of row equals the location size (10 in this case). Each row stores the temporal signal of the property in that location. We recall that a temporal signal is a matrix: the first column represents the time points and the second column the value of the semantics at each time point.

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.