A library for creating past metric temporal logic monitors.
Project description
Past MTL Monitors
A library for creating past metric temporal logic monitors.
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 | RSS feed
Download files
Download the file for your platform. If you're not sure which to choose, learn more about installing packages.
Source Distribution
Built Distribution
Hashes for past_mtl_monitors-0.1.0-py3-none-any.whl
Algorithm | Hash digest | |
---|---|---|
SHA256 | 11b5061cb21b2862a18ea82f616b52ce32bf293555dd10ab86d27a47ba3f6c25 |
|
MD5 | db599a82dc1e1dda88a2ebe9567edf22 |
|
BLAKE2b-256 | c46218ea3acb5eba0009e482c0eb53114a3b25a351f97d78fc21b1f68cadf6f9 |