Tutorial Symbolic Constants - Revision history

Michael Leuschel at 08:18, 28 October 2015

2015-10-28T08:18:48Z

← Older revision		Revision as of 08:18, 28 October 2015
Line 20:		Line 20:
	* not symbolic, which is the default setting. Please note that in certain cases ProB might auto detect that a constant should be stored symbolically (i.e. an infinite set). In this case the "not symbolic" setting is overridden.		* not symbolic, which is the default setting. Please note that in certain cases ProB might auto detect that a constant should be stored symbolically (i.e. an infinite set). In this case the "not symbolic" setting is overridden.

	See "[[Recursively_Defined_Functions#When_does_ProB_treat_a_set_comprehension_or_lambda_abstraction_symbolically_.3F\|the wiki page on infinite and recursive functions]]" for more details.		See [[Recursively_Defined_Functions#When_does_ProB_treat_a_set_comprehension_or_lambda_abstraction_symbolically_.3F\|the wiki page on infinite and recursive functions]] for more details.

Michael Leuschel at 08:18, 28 October 2015

2015-10-28T08:18:32Z

← Older revision		Revision as of 08:18, 28 October 2015
Line 19:		Line 19:
	* symbolic, which will keep the constant stored as a predicate as long as possible. Please note, that some operations might trigger a full evaluation of the constant and thus discard the symbolic representation.		* symbolic, which will keep the constant stored as a predicate as long as possible. Please note, that some operations might trigger a full evaluation of the constant and thus discard the symbolic representation.
	* not symbolic, which is the default setting. Please note that in certain cases ProB might auto detect that a constant should be stored symbolically (i.e. an infinite set). In this case the "not symbolic" setting is overridden.		* not symbolic, which is the default setting. Please note that in certain cases ProB might auto detect that a constant should be stored symbolically (i.e. an infinite set). In this case the "not symbolic" setting is overridden.

			See "[[Recursively_Defined_Functions#When_does_ProB_treat_a_set_comprehension_or_lambda_abstraction_symbolically_.3F\|the wiki page on infinite and recursive functions]]" for more details.

Sebastian Krings: Created page with 'Category:User Manual == Introduction == ProB Tcl/Tk as well as the probcli command-line version are able to store units symbolic…'

2013-12-09T08:08:37Z

Created page with 'Category:User Manual == Introduction == ProB Tcl/Tk as well as the probcli command-line version are able to store units symbolic…'

New page

[[Category:User Manual]]

== Introduction ==

ProB Tcl/Tk as well as the [[Using_the_Command-Line_Version_of_ProB|probcli command-line version]] are able to store units symbolically (i.e. as a predicate) instead of evaluating them. For constants that contain large sets or relations, this might speed up computations or even facilitate more complex ones.

Through a plugin, this behaviour is extended to ProB for Rodin.

== Installing the ProB Symbolic Constants Plugin ==

The plugin is available from the ProB for Rodin Updatesite. The package is called "ProB for Rodin2 - Symbolic Constants Support". It is not bundled with ProB for Rodin itself.

== Marking Constants to be kept symbolic ==

Once the plugin is installed, a toggle button "symbolic" / "not symbolic" should appear next to each constant in the Rodin editor.

You can select between the two behaviours:
* symbolic, which will keep the constant stored as a predicate as long as possible. Please note, that some operations might trigger a full evaluation of the constant and thus discard the symbolic representation.
* not symbolic, which is the default setting. Please note that in certain cases ProB might auto detect that a constant should be stored symbolically (i.e. an infinite set). In this case the "not symbolic" setting is overridden.