Symbolic algorithms for solving games of infinite duration.
A package of symbolic algorithms using binary decision diagrams (BDDs) for synthesizing implementations from temporal logic specifications. This is useful for designing systems, especially vehicles that carry humans.
- generalized Streett(1) specifications (known as GR(1))
- generalized Rabin(1) specifications (counter-strategies to GR(1))
- detection of trivial realizability in GR(1) specifications.
omega.games.gr1and the example
Enumeration of state machines (as
networkxgraphs) from the synthesized symbolic implementations. See
Facilities to simulate the resulting implementations with little and readable user code. See
omega.stepsand the example
Code generation for the synthesized symbolic implementations. This code is correct-by-construction. See
Minimal covering with a symbolic algorithm to find a minimal cover, and to enumerate all minimal covers. Used to convert BDDs to minimal formulas. See
omega.symbolic.cover_enum, and the example
Bitblaster of quantified integer arithmetic (integers -> bits). See
Symbolic automata that manage first-order formulas by seamlessly using binary decision diagrams (BDDs) underneath. You can:
- declare variables and constants
- formulas to BDDs and
- BDDs to minimal formulas via minimal covering
- prime/unprime variables
- get the support of predicates
- pick satisfying assignments (or work with iterators)
- define operators
omega.symbolic.folfor more details.
Facilities to write symbolic fixpoint algorithms. See
omega.symbolic.prime, and the example
Conversion from graphs annotated with formulas to temporal logic formulas. These graphs can help specify transition relations. The translation is in the spirit of predicate-action diagrams.
omega.automatafor more details, and the example
Enumeration and plotting of state predicates and actions represented as BDDs. See
pip install omega
python setup.py install
The package and its dependencies are pure Python.
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.