pybanquo 0.1.0

Python bindings for Banquo offline temporal logic monitor

Banquo Python Bindings

This repository contains the python bindings for the Banquo temporal logic monitor, which is written in Rust.

Installation

We try to provide pre-built wheels for all supported python verions across a variety of common platforms. These wheels can be installed from PyPI, the central python package registry, using the command:

$ pip install pybanquo

This project can also be installed directly from GitHub using the command

$ pip install "pybanquo @ git+https://github.com/cpslab-asu/banquo-python"

Usage

Creating formulas is accomplished by combining logical expressions like Predicate with operators like And and Eventually. The result of combining these terms is a temporal logic formula, which can be used to evaluate a Trace, which is a set of system states along with the associated time for each state. This is an example of this process:

import banquo as bq
import banquo.operators as ops

# x <= 5.0
p1 = bq.Predicate({"x": 1.0}, 5.0)

# -y <= -3.0 => y > 3.0
p2 = bq.Predicate({"y": -1.0}, -3.0)

# always (p1 or p2)
f = ops.Always(ops.Or(p1, p2))

t = bq.Trace({
    0.0: {"x": 4.8, "y": 6.3},
    1.0: {"x": 4.7, "y": 9.3},
    2.0: {"x": 4.9, "y": 5.4},
    3.0: {"x": 4.6, "y": 4.1},
    4.0: {"x": 4.2, "y": 3.1},
})

rho = bq.evaluate(f, t)

More advanced usage of the operators, including the bounded Always and Eventually operators can be seen in the tests/test_conformance.py module.