Python

The Python interface can be accessed in distribution/python.

Installation method 1: Pip package

If you are planning to only use Moonlight in python, there is an experimental PyPi package available via pip (pip install moonlight).

The only extra requirement is that you install Java 21+.

In this case you can directly download the examples as a zip file to play with them.

Installation method 2

Preliminaries

To work with the python interface, you need to have the jnius library (which can be installed via pip as "pyjnius"), and a Java 8+ JDK available on the PATH environment variable.

⚠️ WARNING: There are issues currently in running Moonlight from Anaconda/Conda/Miniconda. Please prefer standard python installations (or pyenv on MacOS)!

Note: If you want to work with Moonlight on python, you either have to put your code in the distribution directory, or you have to copy the moonlight.py file and the jar directory in your working directory.

All the examples at the moment can be found in the same directory as the moonlight.py file. They are mainly made to be accessed as Jupyter notebooks. You can open them via modern IDEs, or by launching them in command-line interface via: jupyter notebook.

Getting Started

Let's start with a few simple examples. You can paste the code blocks in your IDE or run the jupyter notebook directly (getting_started.ipynb)

Temporal Example

We present now a basic usage for a temporal script. In this scenario, there are two formulas: future and past, while the domain is Boolean.
The signal should be composed of two real values, represented by the variables x and y.

For more details about Moonlight scripts, please visit the dedicated section.
5 key steps can be identified:

STEP 1: generate the signal

time = list(np.arange(0,10,0.05)) # we build a list of 10 time points, starting from 0 and incrementing by 0.5
f1,f2 = np.sin(time),np.cos(time) # we define a sinusoidal signal on the provided 

STEP 2: describe and load the property

We use the method loadFromText to load a script directly from a StringArray. We use the method loadFromFile of the MATLAB class ScriptLoader. In the same class, There is also the method named loadFromFile to load a moolight script. We use this method in the next example reported below.

# we simply want a 2-d real-valued signal and we want to evaluate the formulae by boolean semantics.
# We consider two basic formulae: 
#      'future', that checks that x is greater than y for the next 0.2 times, and 
#.     'past' that does the same for the previous 0.2 times
script = """
signal { real x; real y;}
domain boolean; 
formula future = globally [0, 0.2]  (x > y);
formula past = historically [0, 0.2]  (x > y);
"""
moonlightScript = ScriptLoader.loadFromText(script). # we load from the 'script' variable the MoonLightScript to evaluate

STEP 3 (optional): change the domain on the fly

We can decide to change the domain of the script by using one of the two methods setMinMaxDomain() or setBooleanDomain() to set the Reals or Boolean Domain, respectively.

moonlightScript.setMinMaxDomain(); # MinMaxDomain represents a robustness domain defined on double numbers

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.

boolFutureMonitor = moonlightScript.getMonitor("future"); # returns a monitor for the formula called 'future'

STEP 5: monitor the signal

At last, we can use the generated monitor (futureMonitor) to monitor a proper temporal signal. The method is monitor(time,signals).

signals = list(zip(f1,f2)) # we prepare a list of pairs (x, y) that will be provided as input to the monitor
boolFutureMonitorResult = np.array(futureMonitor.monitor(time,signals)) # we execute and collect the results from the monitor, 
                                                       # feeding it with the time points and the data

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.0, -1.0],
 [0.8, 1.0],
 [3.75, -1.0],
 [7.1000000000000005, 1.0],
 [9.750000000000002, 1.0]]

Spatio-Temporal Example

In this example we are considering a spatial formula that is loaded from the file script.mls.

STEP 1: we load the script and initialize the monitor

scriptPath = "script.mls"
moonlightScript = ScriptLoader.loadFromFile(scriptPath)
monitor = moonlightScript.getMonitor("MyFirstFormula")

STEP 2: we define the spatial model

We now define the spatial model of interest.
It will be defined as a list of triples; to express that 0 <-> 3 has distance 1, we write [0, 3, 1].

graph = [[[0.0, 1.0, 1.0], [0.0, 3.0, 1.0], [0.0, 4.0, 1.0], 
          [1.0, 0.0, 1.0], [1.0, 4.0, 1.0], [1.0, 2.0, 1.0], 
          [2.0, 1.0, 1.0], [2.0, 4.0, 1.0], [2.0, 3.0, 1.0], 
          [3.0, 0.0, 1.0], [3.0, 2.0, 1.0], [3.0, 4.0, 1.0],
          [4.0, 0.0, 1.0], [4.0, 1.0, 1.0], [4.0, 2.0, 1.0], 
          [4.0, 3.0, 1.0]]]
locationTimeArray = [0.0] # the time points at which the spatial model changes. In this case it is constant

STEP 3: we define the signal

signal = [[[1.0]], [[3.0]], [[3.0]], [[3.0]], [[3.0]]] # We have a simple 1-d signal

STEP 4: we execute the monitoring and collect the results

When doing spatio-temporal monitoring, we also have to pass to the monitor the spatial model (i.e. the graph) and its evolution over time (i.e. the locationTimeArray)

result = monitor.monitor(locationTimeArray,graph,locationTimeArray,signal)

Further examples

Other examples are available on some more concrete use cases:

• bike.ipynb: shows the evaluation of properties for a bike-sharing settings over real data
• pancreas.ipynb: shows monitoring applied to the simulation of a pancreas model
• stoc_sim.ipynb: shows monitoring applied to the simulation of a stochastic model