Binary decision diagrams implemented in pure Python, as well as Cython wrappers of CUDD, Sylvan, and BuDDy.
Include Inkscape graphics in LaTeX.
Create C call graphs from multiple source files using Cflow, producing linked PDF.
Parser and abstract syntax tree for TLA+, the temporal logic of actions.
Parser and abstract syntax tree for the Promela modeling language.
Symbolic algorithms for solving games of infinite duration.
Utilities for abstract syntax trees and parsing with PLY.
Python tools for working with TLA+ specifications.
Generalized reactive(1) synthesis from Promela specifications.