Package tulip

TuLiP toolbox

The Temporal Logic Planning (TuLiP) Toolbox provides functions for verifying and constructing control protocols.

Notes

Citations are used throughout the documentation. References corresponding to these citations are defined in doc/bibliography.rst of the TuLiP source distribution. E.g., [BK08] used in various docstrings is listed in doc/bibliography.rst as the book "Principles of Model Checking" by Baier and Katoen (2008).

Version: 1.2.0-dev-8168668535962dcbe7d434ee136a5296702c3584

Submodules

tulip.abstract: TuLiP Toolbox Abstract subpackage
- tulip.abstract.discretization: Algorithms related to discretization of continuous dynamics.
- tulip.abstract.feasible: Check Linear Discrete-Time-Invariant System reachability between polytopes
- tulip.abstract.find_controller: Algorithms related to controller synthesis for discretized dynamics.
- tulip.abstract.plot: Functions for plotting Partitions.
- tulip.abstract.prop2partition: Proposition preserving partition module.
tulip.dumpsmach: Code generation and exporting of controllers from TuLiP
tulip.hybrid: Classes representing hybrid dynamical systems.
tulip.interfaces: Minimal bindings to external entities
- tulip.interfaces.gr1c: Interface to gr1c
- tulip.interfaces.jtlv: Interface to the JTLV implementation of GR(1) synthesis
- tulip.interfaces.lily: Interface to Lily that solves LTL games.
- tulip.interfaces.ltl2ba: Interface to ltl2ba
- tulip.interfaces.slugs: Interface to the slugs implementation of GR(1) synthesis.
tulip.spec: Specification subpackage of TuLiP
- tulip.spec.ast: Abstract syntax tree classes for LTL.
- tulip.spec.form: Formulae constituting specifications
- tulip.spec.gr1_fragment: Test if given formula belongs to an LTL fragment that is convertible to deterministic Buchi Automata (readily expressible in GR(1) ).
- tulip.spec.lexyacc: PLY-based parser for TuLiP LTL syntax, using AST classes from spec.ast
- tulip.spec.parser: LTL parser supporting JTLV, SPIN, SMV, and gr1c syntax
- tulip.spec.transformation: Syntactic manipulation of trees.
- tulip.spec.translation: AST subclasses to translate to each syntax of:
tulip.synth: Interface to library of synthesis tools, e.g., JTLV, gr1c
tulip.transys: TuLiP Toolbox Transition System subpackage
- tulip.transys.algorithms: Algorithms on Kripke structures and Automata
- tulip.transys.automata: Automata Module
- tulip.transys.export: Export functions for labeled graphs to various file formats.
  - tulip.transys.export.graph2dot: Convert labeled graph to dot using pydot and custom filtering
  - tulip.transys.export.graph2promela: Convert state graphs to promela
  - tulip.transys.export.machine2scxml: Convert Finite State Machines to State Chart XML (SCXML)
  - tulip.transys.export.save_d3: Export html containing d3.js animating SVG
- tulip.transys.labeled_graphs: Base classes for labeled directed graphs
- tulip.transys.machines: Finite State Machines Module
- tulip.transys.mathset: Mathematical Sets and Power Sets
- tulip.transys.products: Products between automata and transition systems
- tulip.transys.transys: Transition System Module

Variables
	__package__ = `'tulip'`