Skip to main content

A library for creating past metric temporal logic monitors.

Project description

Past MTL Monitors

A library for creating past metric temporal logic monitors.

Build Status Documentation Status codecov PyPI version License: MIT

Table of Contents

Installation

If you just need to use past-mtl-monitors, you can just run:

$ pip install past-mtl-monitors

For developers, note that this project uses the poetry python package/dependency management tool. Please familarize yourself with it and then run:

$ poetry install

Usage

The primary entry point to the past-mtl-monitors package is the atom function. This exposes a monitor factory which can be combined with other monitor factories to create complex property monitors.

Under the hood, these monitor factories are just wrappers around python coroutines that expect a (time, val) pair, where time is a float and val is a mapping from strings to robustness values (float).

Note past-mtl-monitors only implements a quantitative semantics where a value greater than 0 implies sat and a value less than 0 implies unsat.

Thus if one would like to use Boolean semantics, use 1 for True and -1 for False.

from past_mtl_monitors import atom

x, y, z = atom('x'), atom('y'), atom('z')

# Monitor that historically, x has been equal to y.
monitor = (x == y).hist().monitor()

#                    time         values
assert monitor.send((0    , {'x': 1, 'y': 1}))  ==  1   # sat
assert monitor.send((1.1  , {'x': 1, 'y': -1})) == -1   # unsat
assert monitor.send((1.5  , {'x': 1, 'y': 1}))  == -1   # unsat

monitor2 = x.once().monitor()  # Monitor's x's maximum value.
assert monitor2.send((0 , {'x': -10, 'y': 1})) == -10
assert monitor2.send((0 , {'x': 100, 'y': 2})) == 100
assert monitor2.send((0 , {'x': -100, 'y': -1})) == 100

# Monitor that x & y have been true since the last
# time that z held for 3 time units.
monitor3 = (x & y).since(z.hist(0, 3)).monitor()

Project details


Release history Release notifications

Download files

Download the file for your platform. If you're not sure which to choose, learn more about installing packages.

Files for past-mtl-monitors, version 0.1.0
Filename, size File type Python version Upload date Hashes
Filename, size past_mtl_monitors-0.1.0-py3-none-any.whl (5.2 kB) File type Wheel Python version py3 Upload date Hashes View
Filename, size past-mtl-monitors-0.1.0.tar.gz (5.0 kB) File type Source Python version None Upload date Hashes View

Supported by

Pingdom Pingdom Monitoring Google Google Object Storage and Download Analytics Sentry Sentry Error logging AWS AWS Cloud computing DataDog DataDog Monitoring Fastly Fastly CDN DigiCert DigiCert EV certificate StatusPage StatusPage Status page