Skip to main content
Help the Python Software Foundation raise $60,000 USD by December 31st!  Building the PSF Q4 Fundraiser

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.since(y)  #  [x S y] ≡ x has held since the cycle after y last held.

# Composition
expr9 = expr7.since(expr8.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.

Files for py-aiger-ptltl, version 3.0.1
Filename, size File type Python version Upload date Hashes
Filename, size py_aiger_ptltl-3.0.1-py3-none-any.whl (5.1 kB) File type Wheel Python version py3 Upload date Hashes View
Filename, size py-aiger-ptltl-3.0.1.tar.gz (4.8 kB) File type Source Python version None Upload date Hashes View

Supported by

Pingdom Pingdom Monitoring Google Google Object Storage and Download Analytics Sentry Sentry Error logging AWS AWS Cloud computing DataDog DataDog Monitoring Fastly Fastly CDN DigiCert DigiCert EV certificate StatusPage StatusPage Status page