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


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


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

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

AWS AWS Cloud computing Datadog Datadog Monitoring DigiCert DigiCert EV certificate Facebook / Instagram Facebook / Instagram PSF Sponsor Fastly Fastly CDN Google Google Object Storage and Download Analytics Microsoft Microsoft PSF Sponsor Pingdom Pingdom Monitoring Salesforce Salesforce PSF Sponsor Sentry Sentry Error logging StatusPage StatusPage Status page