tltk-mtl 0.0.27

Description:

tltkmtl 0.0.27

#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 g++ compiler. If g++ is not on your system, it can be installed with:
sudo apt install g++

!!! warning
tltk can be compiled with gcc however higher diminsional predicates may produce the wrong result
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))