TuLiP planning, May 2013

This page contains a draft description of the TuLiP toolbox.

Examples

Load up an example stored in files and synthesize a controller

This example shows how to load up a problem that is specified in files and synthesize a controller.

import tulip

# Load up the system and environment, plus specifications
system = tulip.ts.load("robot-discrete.tsf")
environment = tulip.sp.load("robot-env.spf")
specs = tulip.sp.load("robot-specs.spf")

# Synthesize a controller
controller = tulip.syn.jtlv(system, environment, specs)

# Save the controller in TuLiP and Ptolemy formats
tulip.ts.save("robot-control.tsf")
tulip.ptolemy.savefsm("robot-control.fsm")

Notes:

1. The .tsf (transition system file) and .spf (specification file) formats are the default TuLiP file formats.
2. The tf module contains data types and functions for representing different types of transition systems. Multiple transition systems are supported, including deterministic transition systems, Markov decision processes, Kripke structures, Rabin automata, etc.
3. The sp module contains data types and functions for representing specifications. Multiple temporal logics, including LTL, MTL, CTL, PCTL, TCTL, STL, etc are supported.
4. The syn> module contains interfaces to various synthesis tools. Supported tools include JTLV, gr1c and PRISM. The input arguments must be compatible with the synthesis tool, but all arguments should be core TuLiP objects.
   • Would it make more sense to have a module for each program we support? So this line would become tulip.jtlv.syn?
5. The ptolemy module contains functions for interfacing with Ptolemy.