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.

Source Distribution

past-mtl-monitors-0.1.0.tar.gz (5.0 kB view hashes)

Uploaded source

Built Distribution

past_mtl_monitors-0.1.0-py3-none-any.whl (5.2 kB view hashes)

Uploaded py3

Supported by

AWS AWS Cloud computing and Security Sponsor Datadog Datadog Monitoring Fastly Fastly CDN Google Google Download Analytics Microsoft Microsoft PSF Sponsor Pingdom Pingdom Monitoring Sentry Sentry Error logging StatusPage StatusPage Status page