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

Uploaded Source

Built Distribution

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

Uploaded Python 3

File details

Details for the file py-aiger-ptltl-3.1.2.tar.gz.

File metadata

  • Download URL: py-aiger-ptltl-3.1.2.tar.gz
  • Upload date:
  • Size: 5.0 kB
  • Tags: Source
  • Uploaded using Trusted Publishing? No
  • Uploaded via: poetry/1.1.14 CPython/3.9.13 Linux/6.0.0

File hashes

Hashes for py-aiger-ptltl-3.1.2.tar.gz
Algorithm Hash digest
SHA256 84f383c740603414ca1194497b43302ac18e524ae3d2ba63e829b1221be46728
MD5 b671083490d3a9dd49316e8b269595b8
BLAKE2b-256 874a8b74056e7d2731ba4f15d0ae71e26226f74616418dbce6e47f5428add199

See more details on using hashes here.

File details

Details for the file py_aiger_ptltl-3.1.2-py3-none-any.whl.

File metadata

  • Download URL: py_aiger_ptltl-3.1.2-py3-none-any.whl
  • Upload date:
  • Size: 5.2 kB
  • Tags: Python 3
  • Uploaded using Trusted Publishing? No
  • Uploaded via: poetry/1.1.14 CPython/3.9.13 Linux/6.0.0

File hashes

Hashes for py_aiger_ptltl-3.1.2-py3-none-any.whl
Algorithm Hash digest
SHA256 cb64d2a1699cbb1a8940d619912303079a958726c59b9862f469f896387247ae
MD5 1fb462aac15a462f6b51a7b7a1f7b216
BLAKE2b-256 69804d5397997131299ac4c44a4370c7a90e91bff16f9ecaa6bd14871002a789

See more details on using hashes here.

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