Skip to content

Latest commit

 

History

History
118 lines (76 loc) · 3.18 KB

index.rst

File metadata and controls

118 lines (76 loc) · 3.18 KB
Raw

past-mtl-monitors

A library for creating past metric temporal logic monitors.

Basic Usage:

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()

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](https://poetry.eustace.io/) python package/dependency management tool. Please familarize yourself with it and then run:

$ poetry install

API

The past-mtl-monitor API centers around the MonitorFactory type with atom as the primary entrypoint into the API.

past_mtl_monitors.atom

past_mtl_monitors.MonitorFact

past_mtl_monitors.MonitorFact.hist

past_mtl_monitors.MonitorFact.once

past_mtl_monitors.MonitorFact.since

past_mtl_monitors.MonitorFact.implies

past_mtl_monitors.MonitorFact.__and__

past_mtl_monitors.MonitorFact.__or__

past_mtl_monitors.MonitorFact.__invert__

past_mtl_monitors.MonitorFact.__eq__

Extending

The MonitorFact type is a simple wrapper around python co-routines. This makes is easy to write your own monitors that integrate well with the past-mtl-monitor library. For example: consider the following monitor which aggregates the child's monitor's results:

from past_mtl_monitors import MonitorFact


def aggregate_monitor(child_factory):
    """Sums the child values using piecewise constant interpolation."""

    def avg_factory():
        child_monitor = child_factory.monitor()
        payload = (time, _) = yield    # Get initial payload.
                                       # payload = (time, child input).

        total = prev_val = 0
        while True:
            child_val = child_monitor.send(payload)

            prev_time = time
            payload = (time, _) = yield total

            total += prev_val * (time - prev_time)
            prev_val = child_val

    return MonitorFact(avg)

Indices and tables

  • genindex
  • modindex
  • search