TuLiP planning, May 2013: Difference between revisions
From Murray Wiki
Jump to navigationJump to search
(→Notes) |
(→Notes) |
||
Line 29: | Line 29: | ||
# The <tt>tf</tt> 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. | # The <tt>tf</tt> 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. | ||
# The <tt>sp</tt> module contains data types and functions for representing specifications. Multiple temporal logics, including LTL, MTL, CTL, PCTL, TCTL, STL, etc are supported. | # The <tt>sp</tt> module contains data types and functions for representing specifications. Multiple temporal logics, including LTL, MTL, CTL, PCTL, TCTL, STL, etc are supported. | ||
# The <tt>syn | # The <tt>syn</tt> 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 <tt>tulip.jtlv.syn</tt>? | #* Would it make more sense to have a module for each program we support? So this line would become <tt>tulip.jtlv.syn</tt>? --[[User:Murray|Richard Murray]] ([[User talk:Murray|talk]]) 15:07, 11 May 2013 (PDT) | ||
# The <tt>ptolemy</tt> module contains functions for interfacing with Ptolemy. | # The <tt>ptolemy</tt> module contains functions for interfacing with Ptolemy. | ||
=== Create an example from scratch === | === Create an example from scratch === |
Revision as of 22:07, 11 May 2013
This page contains a draft description of the TuLiP toolbox.
Examples
This section contains a set of example that illustrate how the TuLiP code should be structured. This goes first so that we focus on the TuLiP interface and functionality and then figure out what is required to support it.
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.
Code
import tulip # Load up the system and environment descriptions, 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
- The .tsf (transition system file) and .spf (specification file) formats are the default TuLiP file formats.
- Alternatively, perhaps we have a single file format .tlp and then use tulip.load and tulip.save to read and write. The type of object would just be part of the file specification. --Richard Murray (talk) 15:07, 11 May 2013 (PDT)
- 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.
- The sp module contains data types and functions for representing specifications. Multiple temporal logics, including LTL, MTL, CTL, PCTL, TCTL, STL, etc are supported.
- 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? --Richard Murray (talk) 15:07, 11 May 2013 (PDT)
- The ptolemy module contains functions for interfacing with Ptolemy.