Examples
MTL Formulas
The TLTk uses python objects to represent MTL operations. The currently supported MTL operarations are:
Predicate Definition:
MTL.Predicate(dataName, AMatrix, bMatrix)
For example, we can define
speedPred = Predicate('speed', AMatrix, bMatrix)
rpmPred = Predicate('rpm', AMatrix, bMatrix)
MTL Operators
Not:
phi = MTL.Not(speedPred)
And:
phi = MTL.And(speedPred,rpmPred)
Or:
phi = MTL.Or(speedPred,rpmPred)
Next:
phi = MTL.Next(speedPred)
Eventually:
phi = MTL.Finally(lowerTimeBound,upperTimeBound,Subformula)
Always:
phi = MTL.Globaly(lowerTimeBound,upperTimeBound,Subformula)
Until:
phi = MTL.Until(lowerTimeBound,upperTimeBound,Subformula1,Subformula2)
Simple MTL Formula Example
We define a simple predicate as follows:
r1 = MTL.Predicate('data1', [1, 1], [150])
Where x_1 and x_2 are the signals the trajectory is defined over.
We define the MTL formula \varphi=F_{[0,3.14]} (r1) as:
phi = MTL.Finally(0,3.14,r1)
Getting Started Script
The script can be found in tltk/gettingStarted/hello-tltk-rob.py
First, we import the python libraries
import sys
import os
import tltk_mtl as MTL
import numpy as np
import time
## Options
mode = 'cpu_threaded'
Next, we define the predicates and MTL formula for \varphi=\neg(F_{[0,\infty]}(speed>160 \wedge rpm>4500))
## Predicates and Formulas
Ar1 = -1
br1 = -160
r1 = MTL.Predicate('data1',Ar1,br1)
root = MTL.Not(MTL.Finally(0,float('inf'),r1))
Ar2 = -1
br2 = -4500
r2 = MTL.Predicate('data2',Ar2,br2)
# root = F(r1 /\ r2)
root = MTL.Not(MTL.Finally(0,float('inf'),MTL.And(r1,r2)))
After, we set the system output trace and time stamps.
## Trace and Time Stamps
#trace defined as a dictionary
traces = {'data1': np.ones(10,dtype=np.float32)*5, 'data2': np.ones(10,dtype=np.float32)*10}
time_stamps = np.arange(1, 10 + 1,dtype=np.float32)
Finally, we compute and print the robustness of the trace with respect to the MTL specification.
## Evaluate Robustness
t0 = time.time()
root.eval_interval(traces, time_stamps)
t1 = time.time()
print("TLTk" ,"\t | Mode:" ,mode,'\t| Time: ', '%.4f'%(t1 - t0), ' \t| Robustness:', root.robustness)
Falsification Example
We will run the falsification script found in tltk/experiments/falsification/AT1.py
First, we import the python libraries
import matlab.engine
import sys
sys.path.insert(1, '../../')
import numpy as np
import tltk
import tltk_mtl as MTL
Note that this script requires a matlab installation on the system. In addtion, the matlab python package should be configured.
We define the model and simulation parameters:
model = 'models/sldemo_autotrans_mod01'
model_outputs = ['speed','rpm','gear']
step = 0.05
inp_range = [0, 100]
simulation_time = 30
opt = ['simulink', step, inp_range, simulation_time, model_outputs]
interpolation = 'pconst'
mode = 'cpu_threaded'
The specification:
r1 = MTL.Predicate('speed',1,120)
predicates = [r1]
The control points for the input signal:
cp_bounds = [(0,100) for i in range(7)]
Finally, we run the falsification algorithm:
root = MTL.Global(0,20,r1)
results = tltk.falsify(model, interpolation, cp_bounds, predicates, root, opt)