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.3.0.dev0+00ba1eb782880c84538e7847c1863be01fecc44f

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.gridworld: Routines for working with gridworlds.
tulip.hybrid: Classes representing hybrid dynamical systems.
tulip.interfaces: Minimal bindings to external entities.
- tulip.interfaces._inspect: Collect and print environment information.
- tulip.interfaces.gr1c: Interface to gr1c
- tulip.interfaces.gr1py: Interface to gr1py.
- 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.omega: Interface to `omega` package.
- 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'`