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

Main entry point to monitor construction DSL.

Takes a variable name and produces a monitor factory.

Parameters

var (str) –

Return type

MonitorFact

class past_mtl_monitors.MonitorFact(factory)
Parameters

factory (Factory) –

hist(start=0, end=inf)

Monitors if the child monitor was historically true over the interval [t-end, t-start] where t is the current time.

Return type

MonitorFact

once(start=0, end=inf)

Monitors if the child monitor was once true in the interval [t-end, t-start] where t is the current time.

Return type

MonitorFact

since(other)

Monitors the minimum value since the last time other’s value was greater than 0.

Note: other’s value is assumed to have been previously greater than zero when the monitor starts.

Parameters

other (MonitorFact) –

Return type

MonitorFact

implies(other)

Monitors if child monitor self implies child monitor other.

Parameters

other (MonitorFact) –

Return type

MonitorFact

__and__(other)

Combines child monitors using min. If values are {1, -1} for True and False resp., then this corresponds to logical And.

Parameters

other (MonitorFact) –

Return type

MonitorFact

__or__(other)

Combines child monitors using min. If values are {1, -1} for True and False resp., then this corresponds to logical Or.

Parameters

other (MonitorFact) –

Return type

MonitorFact

__invert__()

Negates result of child monitors.

Return type

MonitorFact

__eq__(other)

Monitors if child monitors self and other return same values.

Parameters

other (MonitorFact) –

Return type

MonitorFact

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