tltk-mtl 0.0.27
A libary for effecient Metric temporal logic calculation
Requires Python: >=3.6

#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
``` Bash
docker pull bardhh/tltk
```
* Once the docker image is pulled, a container may be intialized, in interactive mode, with the command:
``` Bash
docker run -it --name tltk_cont bardhh/tltk bash 
```
* Alternatively, to execute a script without entering the container:
``` Bash
docker exec -it tltk_cont bash -c 'cd demos && python phi_1.py' 
```

*Other useful commands*

* To copy a file to the container: 
``` Bash
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
```Bash
pip3 install --user tltk_mtl
```

If pip3 is not installed the command below will install it on Ubuntu
```Bash
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 

```Bash
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:
```Bash
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:

```Bash
sudo apt install g++
```

!!! warning
    tltk can be compiled with gcc however higher diminsional predicates may produce the wrong result

##### Installing python3
```Bash
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](https://developer.nvidia.com/cuda-downloads)


##### 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:
```Bash
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](https://www.scivision.dev/matlab-engine-callable-from-python-how-to-install-and-setup/)

The following two commands need to be executed (depending on the MATLAB version and directory structure) for Linux using python3:
```Bash
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
```Bash
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 
```Bash
tltk/robustness/make
```
This make file uses GNU make, which can be installed with
```Bash
sudo apt install make
```
To make the gpu code, the make file can be ran like this
```Bash
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
```Python
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.

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

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

```Python
#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.


```Python
#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))
```