Skip to content
Simone edited this page Jun 18, 2020 · 29 revisions

Installation

The installation script (install.m) is contained in distribution/matlab. You can 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);

Pay attention to comments. 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 allow us to load a script directly from a StringArray define with Matlab. Please refer to the Spatial-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

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
     .....    ..... 

Spatial-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.
load('dataInput.mat');


script= [
"signal { int nodeType; real battery; real temperature; }",...
"space {edges { int hop; real dist; }}",...
"domain boolean;",... 
"formula MyFirstFormula = ( nodeType==3 ) reach (hop)[0, 1] ( nodeType==2 ) ;"
];

%% 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
boolSpTempMonitor = moonlightScript.getMonitor("MyFirstFormula");

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

Similarly to the temporal example there are 5 steps:

  • STEP 1: define a Spatial-temporal signal. This signal is stored in dataInput.mat and it is composed of three parts:

    • time:
    • spatialModel:
    • values:
  • STEP 2: loading the Moonlight Script. In this case, we load the script saved in a stringArray variable named script

  • 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("MyFirstFormula") which accepts the string of the formula name we want to use.

  • STEP 5: finally we can use the generated monitor (boolSpTempMonitor) to monitor each compatible Spatial-temporal signal. We use the monitor method which accept the spatial-temporal signal (i.e., spatialModel, time and values). The result is...