Skip to main content

Library for generating (p)ast (t)ense (l)inear (t)emporal (l)ogic monitors as aiger circuits.

Project description

py-aiger-past-ltl

Library for generating (p)ast (t)ense (l)inear (t)emporal (l)ogic monitors as aiger circuits. Builds on the py-aiger project.

Build Status codecov PyPI version License: MIT

Table of Contents

Installation

If you just need to use aiger_ptltl, you can just run:

$ pip install py-aiger-ptltl

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 for using aiger_ptltl is the PTLTLExpr class which is a simple extension of aiger.BoolExpr to support the temporal operators, historically, past (once), (variant) yesterday, and since.

import aiger_ptltl as ptltl

# Atomic Propositions
x = ptltl.atom('x')
y = ptltl.atom('y')
z = ptltl.atom('z')

# Propositional logic
expr1 = ~x
expr2 = x & (y | z)
expr3 = (x & y) | ~z
expr4 = ~(x & y & z)

# Temporal Logic
expr5 = x.historically()  #  (H x) ≡ x has held for all previous cycles (inclusive).
expr6 = x.once()  #  (P x) ≡ x once held in a past cycle (inclusive).
expr7 = x.vyest()  #  (Z x) ≡ x held in the previous cycle (true at time = 0).
expr8 = x.yest()  #  (Y x) ≡ x held in the previous cycle (false at time = 0).
expr9 = x.since(y)  #  [x S y] ≡ x has held since the cycle after y last held.

# Composition
expr9 = expr7.since(expr9.vyest().vyest())

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

py-aiger-ptltl-3.1.2.tar.gz (5.0 kB view hashes)

Uploaded Source

Built Distribution

py_aiger_ptltl-3.1.2-py3-none-any.whl (5.2 kB view hashes)

Uploaded Python 3

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