TuLiP planning, May 2013 - Revision history

Murray: /* TuLiP classes */

2013-05-27T15:33:29Z

TuLiP classes

← Older revision		Revision as of 15:33, 27 May 2013
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)

Murray: /* Examples */

2013-05-27T15:31:41Z

Examples

@@ Line 9: / Line 9: @@
 == 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:

Murray: /* TuLiP classes */

2013-05-27T15:23:32Z

TuLiP classes

← Older revision		Revision as of 15:23, 27 May 2013
Line 141:		Line 141:
	Notes from 23 May meeting:		Notes from 23 May meeting:

	[[Image:tulip-planning_23May13.~~jpg~~\|640px]]		[[Image:tulip-planning_23May13.png\|640px]]

	=== TransitionSystem ===		=== TransitionSystem ===

Murray: /* Discretize continuous dynamics */

2013-05-27T15:23:21Z

Discretize continuous dynamics

← Older revision		Revision as of 15:23, 27 May 2013
Line 135:		Line 135:
	Notes from 14 May meeting:		Notes from 14 May meeting:

	[[Image:tulip-planning_14May13.~~jpg~~\|640px]]		[[Image:tulip-planning_14May13.png\|640px]]

	== TuLiP classes ==		== TuLiP classes ==

Murray at 15:22, 27 May 2013

2013-05-27T15:22:26Z

← Older revision		Revision as of 15:22, 27 May 2013
Line 133:		Line 133:
	</pre>		</pre>

	~~===~~ Notes from 14 May meeting ~~===~~		Notes from 14 May meeting:

			[[Image:tulip-planning_14May13.jpg\|640px]]

	== TuLiP classes ==		== TuLiP classes ==

	~~===~~ Notes from 23 May meeting ~~===~~		Notes from 23 May meeting:

			[[Image:tulip-planning_23May13.jpg\|640px]]

	=== TransitionSystem ===		=== TransitionSystem ===

Murray: /* TuLiP classes */

2013-05-27T15:21:36Z

TuLiP classes

← Older revision		Revision as of 15:21, 27 May 2013
Line 136:		Line 136:

	== TuLiP classes ==		== TuLiP classes ==

			=== Notes from 23 May meeting ===

	=== TransitionSystem ===		=== TransitionSystem ===

Murray: /* Discretize continuous dynamics */

2013-05-27T15:21:11Z

Discretize continuous dynamics

← Older revision		Revision as of 15:21, 27 May 2013
Line 132:		Line 132:
	tulip.discretize(system, 0.01)		tulip.discretize(system, 0.01)
	</pre>		</pre>

			=== Notes from 14 May meeting ===

	== TuLiP classes ==		== TuLiP classes ==

Slivings: /* Notes */

2013-05-14T20:00:48Z

Notes

← Older revision		Revision as of 20:00, 14 May 2013
Line 33:		Line 33:
	# The <tt>.tsf</tt> (transition system file) and <tt>.spf</tt> (specification file) formats are the default TuLiP file formats.		# The <tt>.tsf</tt> (transition system file) and <tt>.spf</tt> (specification file) formats are the default TuLiP file formats.
	#* Alternatively, perhaps we have a single file format <tt>.tlp</tt> and then use <tt>tulip.load</tt> and <tt>tulip.save</tt> to read and write. The type of object would just be part of the file specification. --[[User:Murray\|Richard Murray]] ([[User talk:Murray\|talk]]) 15:07, 11 May 2013 (PDT)		#* Alternatively, perhaps we have a single file format <tt>.tlp</tt> and then use <tt>tulip.load</tt> and <tt>tulip.save</tt> to read and write. The type of object would just be part of the file specification. --[[User:Murray\|Richard Murray]] ([[User talk:Murray\|talk]]) 15:07, 11 May 2013 (PDT)
	# 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>ts</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</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.		# 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.

Slivings: /* Notes */

2013-05-14T16:09:12Z

Notes

← Older revision		Revision as of 16:09, 14 May 2013
Line 41:		Line 41:
	#* We should be careful about MoC the automaton is synthesized for (event-based, discrete-time, continuous-time etc.) while interfacing. Ptolemy and FMI seem to have better support for certain types. -- Necmiye		#* We should be careful about MoC the automaton is synthesized for (event-based, discrete-time, continuous-time etc.) while interfacing. Ptolemy and FMI seem to have better support for certain types. -- Necmiye
	# It would be nice to have transition system class support symbolic representations (e.g., based on variable tuples as is now instead of listing all states). For instance for a 10x10 grid, one might want to define the problem in terms of x and y coordinates instead of listing 100 states. Another example where listing the states is difficult is vms examples, where we have temperature, ice_level, wind_level, etc. This way we can take better advantage of underlying symbolic computations. -- Necmiye		# It would be nice to have transition system class support symbolic representations (e.g., based on variable tuples as is now instead of listing all states). For instance for a 10x10 grid, one might want to define the problem in terms of x and y coordinates instead of listing 100 states. Another example where listing the states is difficult is vms examples, where we have temperature, ice_level, wind_level, etc. This way we can take better advantage of underlying symbolic computations. -- Necmiye
			#* The <code>gridworld</code> module already provides an example of this. --[[User:Slivings\|Slivings]] ([[User talk:Slivings\|talk]]) 09:09, 14 May 2013 (PDT)

	=== Create a discrete example from scratch ===		=== Create a discrete example from scratch ===

Necmiye at 17:14, 12 May 2013

2013-05-12T17:14:16Z

← Older revision		Revision as of 17:14, 12 May 2013
Line 39:		Line 39:
	# The <tt>ptolemy</tt> module contains functions for interfacing with Ptolemy.		# The <tt>ptolemy</tt> module contains functions for interfacing with Ptolemy.
	#* Should we instead make an FMI interface and then use Ptolemy's FMI capability? --[[User:Murray\|Richard Murray]] ([[User talk:Murray\|talk]]) 15:09, 11 May 2013 (PDT)		#* Should we instead make an FMI interface and then use Ptolemy's FMI capability? --[[User:Murray\|Richard Murray]] ([[User talk:Murray\|talk]]) 15:09, 11 May 2013 (PDT)
			#* We should be careful about MoC the automaton is synthesized for (event-based, discrete-time, continuous-time etc.) while interfacing. Ptolemy and FMI seem to have better support for certain types. -- Necmiye
			# It would be nice to have transition system class support symbolic representations (e.g., based on variable tuples as is now instead of listing all states). For instance for a 10x10 grid, one might want to define the problem in terms of x and y coordinates instead of listing 100 states. Another example where listing the states is difficult is vms examples, where we have temperature, ice_level, wind_level, etc. This way we can take better advantage of underlying symbolic computations. -- Necmiye

	=== Create a discrete example from scratch ===		=== Create a discrete example from scratch ===