tltk-mtl 0.0.21

A libary for effecient Metric temporal logic calculation

#Description TLTK is a tool for computing Metric Temporal logic robustness. This is done by specifing predicates in the form Ax <= b and using those in MTL formulas.

Getting Started

Building TLTk

TLTK can be built from source or run through a Docker container. Running through a Docker container is straighforward since the environment and the dependencies are automatically installed.

In the following, we provide instructions for both alternatives.

Running through Docker (Windows or Linux)

Instructions to run the tool using Docker.

• Install Docker https://docs.docker.com/get-docker/ .
• In terminal or command proment, enter the following command to pull the TLTk docker image

docker pull bardhh/tltk

• Once the docker image is pulled, a container may be intialized, in interactive mode, with the command:

docker run -it --name tltk_cont bardhh/tltk bash 

• Alternatively, to execute a script without entering the container:

docker exec -it tltk_cont bash -c 'cd demos && python phi_1.py' 

Other useful commands

• To copy a file to the container:

docker cp source_file tltk_cont:/usr/src/tltk/destination_file

If you have completed these steps, continue to the next section.

Pip install (Linux Only)

To install tltk with pip3 the command below can be ran in Bash

pip3 install --user tltk_mtl

If pip3 is not installed the command below will install it on Ubuntu

sudo apt install python3-pip

Building from Source (Linux Only)

Downloading TLTk

TLTk is currenlty hosted on bitbucket and is downloaded with the git clone command

git clone ~~~~~~~~~~~~~~~~~~~~~~~~~

Dependencies for robustness calculation

The following section describes how to install TLTk manually. There is a script that will do it automatically; skip to the bottom of the section for instructions on how to use the script

Operating System

TLTk is tested on Ubuntu linux. It can be installed on any linux distribution, but it is untested. This guide will be focused installing on the Ubuntu distribution of linux.

Installing Git

Git is needed to download TLTk source. If you do not have git, it can be downloaded with the command:

sudo apt install git 

CPU Compiler

TLTk has been tested with the gcc compiler. If gcc is not on your system, it can be installed with:

sudo apt install gcc

Installing python3

sudo apt install python3

GPU Compiler

!!! warning Not required unless you are using a GPU

To compile the gpu code you need the NVCC compiler. This compiler can be found: Here

Installing python packages

We need to install the needed python repositories. To do this we will use pip3, which we installed in the previous step. The libraries that TLTk need are numpy, scipy, and cython. To install these, you can run the following command:

pip3 install --user numpy scipy cython

Installing MATLAB for SimuLink model simulations

!!! warning Only needed if planing on using TLTk with simulink

Detailed steps can be found here

The following two commands need to be executed (depending on the MATLAB version and directory structure) for Linux using python3:

cd /usr/local/matlab/extern/engines/python/ 
python3 setup.py build --build-base=$(mktemp -d) install

Install script

There is a script that installs all the needed packages. At the start of the script it runs an apt update and upgrade. The script can be found at

tltk/robustness/install.sh

Compiling TLTk

Once all the dependencies are installed, TLTk needs to be compiled. To do this, there is a Make file in

tltk/robustness/make

This make file uses GNU make, which can be installed with

sudo apt install make

To make the gpu code, the make file can be ran like this

make gpu

Running Your First Script

Docker

Source

Adding TLTk to path

If you built TLTk by source, python needs to know where to look to find TLTk. One method is to add the directory to path at run time by using the python sys libary. For example

import sys
sys.path.insert(1,’(path from working directory)/pytaliro/robustness’)
import MTL

It can also be added to the python path at the startup of a bash instance by adding the following line to your .bashrc and restarting the bash instance.

export PYTHONPATH=(path from root)/tltk/robustness:$PYTHONPATH

Below is a simple test script to check your setup of TLTk

#import sys #uncomment if not using export statment for bash
#sys.path.insert(1, 'robustness') #uncomment if not using export for bash
#import MTL as MTL #Uncomment if .bashrc was eddited
import tltk_mtl as MTL #This is used if pip3 install was used
import numpy as np
#predicate definition
predicate = MTL.Predicate('example data',1,1)

#signal and time stamps
signal = {'example data':np.array([95,96,97,96,95],dtype=np.float32)}
time_stamps = np.array([0,.5,.7,.8,1],dtype=np.float32)

#calculate predicate and print results 
print(predicate.eval_interval(signal,time_stamps))

The MTL formula stores information for later use. If you want to use the same formula more than once the reset() method needs to be called as seen below.

#import sys #uncomment if not using export statment for bash
#sys.path.insert(1, 'robustness') #uncomment if not using export for bash
#import MTL as MTL #Uncomment if .bashrc was eddited
import tltk_mtl as MTL #This is used if pip3 install was used
import numpy as np
#predicate definition
predicate = MTL.Predicate('example data',1,1)

#signal and time stamps
signal = {'example data':np.array([95,96,97,96,95],dtype=np.float32)}
time_stamps = np.array([0,.5,.7,.8,1],dtype=np.float32)

#calculate predicate and print results 
print(predicate.eval_interval(signal,time_stamps))

predicate.reset()

signal = {'example data':np.array([92,95,92,100,95],dtype=np.float32)}
time_stamps = np.array([0,.4,.10,.80,1],dtype=np.float32)

print(predicate.eval_interval(signal,time_stamps))