Skip to main content
Join the official 2019 Python Developers SurveyStart the survey!

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 1.0.0
Filename, size File type Python version Upload date Hashes
Filename, size py_aiger_ptltl-1.0.0-py3-none-any.whl (5.0 kB) File type Wheel Python version py3 Upload date Hashes View hashes
Filename, size py-aiger-ptltl-1.0.0.tar.gz (4.7 kB) File type Source Python version None Upload date Hashes View hashes

Supported by

Elastic Elastic Search Pingdom Pingdom Monitoring Google Google BigQuery Sentry Sentry Error logging AWS AWS Cloud computing DataDog DataDog Monitoring Fastly Fastly CDN SignalFx SignalFx Supporter DigiCert DigiCert EV certificate StatusPage StatusPage Status page