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.
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
Release history Release notifications | RSS feed
Download files
Download the file for your platform. If you're not sure which to choose, learn more about installing packages.
Source Distribution
Built Distribution
Hashes for py_aiger_ptltl-3.1.2-py3-none-any.whl
Algorithm | Hash digest | |
---|---|---|
SHA256 | cb64d2a1699cbb1a8940d619912303079a958726c59b9862f469f896387247ae |
|
MD5 | 1fb462aac15a462f6b51a7b7a1f7b216 |
|
BLAKE2b-256 | 69804d5397997131299ac4c44a4370c7a90e91bff16f9ecaa6bd14871002a789 |