View on GitHub

STL-API

STL API

Table of Contents

Motivation

STL API is used to evaluate Signal Temporal Logic specification with respect to an arbitrary signal.

Installation

Configure system PATH

export PATH="/path/to/STL-API/bin/directory:$PATH"

Configure PYTHON PATH (for invoking STL API from other modules)

Configure STL PATH (for unit testing and other repository referential operations)

export STLPATH="/path/to/STL-API/"

Reload .zshrc file

finally, execute the following command on the command line to reload .zshrc zsh configuration file

  source ~/.zshrc

required Platform

required Python packages

Features

Usage (Python API)

Below we will be showing a simple example demonstrating the usage of the STL API by evaluating a simple STL expression G[0, 1](x > y) with respect to a signal

To begin, we have to import the essential libraries from the STL API

from stl import Signal, STL

Simple Math Expressions

spec = STL("1 + 1")
# 2

spec = STL("true => false")
# False

signal = Signal(py_dict={"0": {"content": {"x": 1, "y": 2}},
                         "1": {"content": {"x": 2, "y": 1}}})  
spec = STL("x > 0")
# True

Evaluate Signal with respect to STL Formula

Then, we define a (global) start time in int type, as well as defining an arbitrary signal

time_begin = 0
signal = Signal(py_dict={"0": {"content": {"x": 1, "y": 2}},
                         "1": {"content": {"x": 2, "y": 1}}})

Next, we define the STL expression we would like to evaluate

stl_spec = STL("G[0, 1](x > y)")

There are often two parameters that we can obtain from the evaluation of STL expressions, namely, the satisfaction value, in bool type (True/False), and the robustness value and the robustness value, in float type. There are two ways of accessing these values:

The first approach is a fairly straightforward one:

satisfy    : bool  = stl_spec.satisfy(time_begin, signal)     # obtain the satisfaction value
robustness : float = stl_spec.robustness(time_begin, signal)  # obtain the robustness value

The second approach is a bit less straightforward, but it allows the evaluation results to be cached for future access within an object called Eval_Result

stl_eval: Eval_Result = stl_spec.eval(time_begin, signal)

satisfy    : bool  = stl_eval.satisfy
robustness : float = stl_eval.robustness

STL Formula Weakening

We can also use the Python API to weaken the constraint of an STL formula. For example, suppose we have an STL expression with the following form

stl_spec = STL("G[0, 1](0 < x < 1)")

One way of weakening the formula is by relaxing the bound of the atomic proposition in the STL formula

weakened_stl_spec_1 = stl_spec.weaken("ap-range", 2, 3)
print(weakened_stl_spec_1)
# G[0, 1]((0 - 2) < x < (1 + 3))

weakened_stl_spec_2 = stl_spec.weaken("time-range", 2, 3)
# G[0 - 2, 1 + 3](0 < x < 1)

Usage (REPL)

We can simply the usage procedure above into a simply REPL interface. Users can start the REPL by typing stlinterp on the command line

$ stlinterp
Time Start: 0
Signal:
{
    "0": {
        "content": {
            "x": 1,
            "y": 2
        }
    },
    "1": {
        "content": {
            "x": 2,
            "y": 1
        }
    }
}
Please enter STL expressions to be interpreted.
>>>

Once the REPL is started, it will prompt you to enter the STL expression. Users can simply type the expression G[0, 1](x > y) after the >>> , click Enter to evaluate the expression.

>>> G[0, 1](x > y)
satisfy     : False
robustness  : -1.0

Structure

Project Structure

File Structure

bin/: consists of bash scripts. must be added to system PATH variable to be executed on the command line.

code-style/: consists of code-writing guidelines excerpted from Google for code consistency purposes (for developers of the repository)

example/ -> stl/example/: demonstrate example usage of the internal helper functions, low-level structures (lexer and parser level) as well as high-level objects (api level)

stl/: main code repository

FAQ

Common Issues

Special Notes

Future Work