Library for generating (p)ast (t)ense (l)inear (t)emporal (l)ogic monitors as aiger circuits.
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
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
The primary entry point for using
aiger_ptltl is the
class which is a simple extension of
aiger.BoolExpr to support the
temporal operators, historically, past (once), (variant) yesterday,
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())
Release history Release notifications | RSS feed
Download the file for your platform. If you're not sure which to choose, learn more about installing packages.
|Filename, size||File type||Python version||Upload date||Hashes|
|Filename, size py_aiger_ptltl-3.1.0-py3-none-any.whl (5.1 kB)||File type Wheel||Python version py3||Upload date||Hashes View|
|Filename, size py-aiger-ptltl-3.1.0.tar.gz (4.9 kB)||File type Source||Python version None||Upload date||Hashes View|
Hashes for py_aiger_ptltl-3.1.0-py3-none-any.whl