|
|
| Line 19: |
Line 19: |
|
| |
|
| [[Image:tulip-planning_23May13.png|640px]] | | [[Image:tulip-planning_23May13.png|640px]] |
|
| |
| === TransitionSystem ===
| |
|
| |
| A transition system consists of
| |
| * states - a list of elements that correspond to the states of the system. Elements are nominally strings
| |
| * transitions - optional subset of states x states indicating allowable transitions (doesn't have to be deterministic)
| |
| * actions - list of actions and what transitions they enable. If empty
| |
| * labels - list of atomic propositions for any subsets of states. Atomic propositions are given by set of all label outputs
| |
| * initial states
| |
| * acceptance sets - for Buchi and Rabin automata
| |
|
| |
| Available functions
| |
|
| |
| === Specification ===
| |
| A specification is a temporal logic formula. Specifications can be input and output as strings using the following symbols:
| |
| * state - evaluates to true if the system is in the discrete state
| |
| * atomic - evaluates to true if the atomic proposition is true
| |
| * logical operators: and, or, not, implies, &, ^, !, ->
| |
| * comparison operators: =, <=, >=, !=
| |
| * temporal operators: always, eventually, until, next, [], <>, U, X
| |
| * path operators: forall, exists, F, E
| |
| * probability operators?
| |
|
| |
| === HybridSystem ===
| |
|
| |
| The HybridSystem class is used to define systems that have continuous time dynamics. The state space of a hybrid system can be continuous, discrete or both.
| |
|
| |
| A space system consists of
| |
| * discrete state space - set of discrete states
| |
| * continuous state space - list of polygonal regions that are each subsets of R^n
| |
| * discrete inputs - set of discrete inputs that affect evolution of the system
| |
| * continuous inputs - set of continuous inputs that affect evolution of the system
| |
| * discrete transitions - set of guarded commands
| |
| * continuous dynamics - for each polygonal region, a set of dynamics that define the evolution of the system (given values for the inputs)
| |
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:
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 classes
Notes from 23 May meeting:
