STL API

Table of Contents

• STL API
  • Table of Contents
  • Motivation
  • Installation
    • Configure system PATH
    • Configure PYTHON PATH (for invoking STL API from other modules)
    • Configure STL PATH (for unit testing and other repository referential operations)
    • Reload .zshrc file
    • required Platform
    • required Python packages
  • Features
  • Usage (Python API)
    • Simple Math Expressions
    • Evaluate Signal with respect to STL Formula
    • STL Formula Weakening
  • Usage (REPL)
  • Structure
    • Project Structure
    • File Structure
  • FAQ
    • Common Issues
    • Special Notes
  • Future Work

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)

• Temporary Solution:

  import sys
  sys.path.append("/path/to/STL-API/directory/")
  import stl.api

• Permanent Solution:

  Adding the following line to your shell configuration file (in Unix-based OS). For Mac users, the default shell configuration file is ~/.zshrc

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

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

• Python3.9+

required Python packages

• rply (for parser and lexer)
• termcolor (for color printing tools)

Features

• Evaluate simple mathematical expressions and propositional logic
• Calculate the robustness value of a signal with respect to an STL formula
• Syntactically weaken the STL formula

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

• API-level interfaces (high-level)
  • They are designed to be simple to use with minimal overhead for training and learning.
  • API-level interfaces include stl.obj as well as programs in stl.api.
• Low-level interfaces
  • Low-level interfaces are designed to support lower-level operations like lexing and parsing of the strings passed in from the API level. It is not intended to interact with the user directly.
  • It includes all modules in stl.parsing

File Structure

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

• stllex: start the REPL for the lexical analyzer
• stlparse: start the REPL for the parser
• stlinterp: start the REPL for the interpreter
• stltest: initiate unit test
• stlsize: show the size of the codebase

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

• api.py: main entry point for importing high-level (api level) objects and functions
• tool.py: foundational tools for code repository
• unit_test.py: handle unit testing of objects and tools, can be invoked using stltest command on the command line
• obj/: imported by api.py, intended to be used by the users of the API. consists of API level objects
• parsing/: not intended to be used directly by the user. low-level (parser and lexer level objects, i.e. AST (abstract syntax tree), type signatures)
• error.py: main entry point for importing errors
• err/: all definition/implementation of errors

FAQ

Common Issues

• Vscode PyLint "Unable to Import" Error
  • See Stackoverflow
  • create ~/.pylintrc with the following content

    [MASTER]
    init-hook='import sys; sys.path.append("/path/to/STL-API")'

    Note that please replace /path/to/STL-API with the actual absolute path to the location of the respository

Special Notes

• example folder is in stl folder for unit-test purpose, a symbolic link for example folder is created in the project root directory

Future Work

• Fixed the bug when adding an integer to a floating-point number in stl interpreter

  >>> 1 + 1.5
  2
  

  possible fix, detect type mismatch, and coerce all int types to float types

• create numeric type instead of using Ints and Floats

  • reduce type check effort and automatically convert Ints to Floats

• syntax for absolute value

  • G[0, 1](|y| > 1) means that the absolute value of y must be greater than 1 between time 0 and 1 of the signal

• support for nested STL expression

  • F G[0, 10](y > 1) means that between time 0 and time 10, the y parameter of the signal will eventually always be greater than 1

• allow passing in external function/objects to evaluation

  class Coord:
    def __init__(self, x, y):
        ...
  
  def distance_between_points(p1, p2) -> float:
      ...
      return result
    
  stl_spec = STL("G[0, 1](distance_between_points(Coord(a, b), Coord(c, d)) > 3)")
  stl_spec.add_extern_func(distance_between)
  stl_spec.add_extern_obj(Coord)
  
  stl_spec.eval(...)

• improved the signal so that it can handle more continuous times

  • signal = Signal(py_dict={"0": {"content": {"timestamp": 0.1, "x": 1}}, "1": {"content": {"timestamp": 0.2, "x": 2}}})
  • when the signal has "timestamp" as a quantifiable key, the STL expressions will evaluate based upon the timestamp instead of the timeindex
  • backward compatibility