TuLiP planning, May 2013: Difference between revisions

From Murray Wiki
Jump to navigationJump to search
(Created page with "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...")
 
 
(27 intermediate revisions by 3 users not shown)
Line 1: Line 1:
This page contains a draft description of the TuLiP toolbox.
This page contains a draft description of the TuLiP toolbox.


=== Examples ===
== Architecture ==


==== Load up an example stored in files and synthesize a controller ====
Notes from 30 April 2013 meeting:
This example shows how to load up a problem that is specified in files and synthesize a controller.
<pre>
import tulip


# Load up the system and environment, plus specifications
[[Image:tulip-planning_30Apr13.jpg|640px]]
system = tulip.ts.load("robot-discrete.tsf")
environment = tulip.sp.load("robot-env.spf")
specs = tulip.sp.load("robot-specs.spf")


# Synthesize a controller
== Examples ==
controller = tulip.syn.jtlv(system, environment, specs)
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.


# Save the controller in TuLiP and Ptolemy formats
Notes from 14 May meeting:
tulip.ts.save("robot-control.tsf")
tulip.ptolemy.savefsm("robot-control.fsm")
</pre>


Notes:
[[Image:tulip-planning_14May13.png|640px]]
# The <tt>.tsf</tt> (transition system file) and <tt>.spf</tt> (specification file) formats are the default TuLiP file formats.
# 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>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>?
# The <tt>ptolemy</tt> module contains functions for interfacing with Ptolemy.


==== Create an example from scratch ====
== TuLiP classes ==
 
Notes from 23 May meeting:
 
[[Image:tulip-planning_23May13.png|640px]]

Latest revision as of 15:33, 27 May 2013

This page contains a draft description of the TuLiP toolbox.

Architecture

Notes from 30 April 2013 meeting:

Tulip-planning 30Apr13.jpg

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.

Notes from 14 May meeting:

Tulip-planning 14May13.png

TuLiP classes

Notes from 23 May meeting:

Tulip-planning 23May13.png

Retrieved from "https://murray.cds.caltech.edu/index.php?title=TuLiP_planning,_May_2013&oldid=16005"