Deferred Sets - Revision history

Michael Leuschel at 05:09, 1 September 2015

2015-09-01T05:09:33Z

← Older revision		Revision as of 05:09, 1 September 2015
Line 16:		Line 16:
	- AA = {aa,bb} & aa/=bb		- AA = {aa,bb} & aa/=bb
	- …		- …
	* you can add a DEFINITION scope_AA == constant to instruct ProB to set the cardinality of AA to the constant.		* you can add a DEFINITION <tt>scope_AA == constant</tt> to instruct ProB to set the cardinality of AA to the constant.

	=== Using Refinement for Animation Preferences ===		=== Using Refinement for Animation Preferences ===

Michael Leuschel at 05:09, 1 September 2015

2015-09-01T05:09:02Z

← Older revision		Revision as of 05:09, 1 September 2015
Line 9:		Line 9:

	In general (for both probcli and ProB Tcl/Tk) you can set the cardinality of a set AA either by		In general (for both probcli and ProB Tcl/Tk) you can set the cardinality of a set AA either by
	* making it an enumerated set, i.e., adding AA = {v1,v2,…} to the SETS clause		* making it an enumerated set, i.e., adding <tt>AA = {v1,v2,…}</tt> to the SETS clause
	* adding a predicate card(AA) = constant to the PROPERTIES clause		* adding a predicate <tt>card(AA) = constant</tt> to the PROPERTIES clause
	* Note: various other predicates in the PROPERTIES clause will also influence the size used for AA by ProB, for example:		* Note: various other predicates in the PROPERTIES clause will also influence the size used for AA by ProB, for example:
	- card(AA) > 1		- card(AA) > 1

Michael Leuschel at 05:08, 1 September 2015

2015-09-01T05:08:19Z

← Older revision		Revision as of 05:08, 1 September 2015
Line 1:		Line 1:
	A deferred set in B is declared in the SETS Section and is not explicitly enumerated. In the example below, AA is a deferred set and BB is an enumerated set.		A deferred set in B is declared in the SETS Section and is not explicitly enumerated. In the example below, AA is a deferred set and BB is an enumerated set.
	<pre>		<pre>
	MACHINE ~~Test~~		MACHINE M0
	SETS AA; BB={bb,cc,dd}		SETS AA; BB={bb,cc,dd}
	END		END
Line 13:		Line 13:
	* Note: various other predicates in the PROPERTIES clause will also influence the size used for AA by ProB, for example:		* Note: various other predicates in the PROPERTIES clause will also influence the size used for AA by ProB, for example:
	- card(AA) > 1		- card(AA) > 1
			- aa:AA & bb:AA & aa/=bb
	- AA = {aa,bb} & aa/=bb		- AA = {aa,bb} & aa/=bb
	~~- aa:AA & bb:AA & aa/=bb~~
	- …		- …
	* you can add a DEFINITION scope_AA == constant to instruct ProB to set the cardinality of AA to the constant.		* you can add a DEFINITION scope_AA == constant to instruct ProB to set the cardinality of AA to the constant.

			=== Using Refinement for Animation Preferences ===
			Note: instead of adding AA = {aa,bb} to the SETS clause you can also add <tt>AA = {aa,bb} & aa/=bb</tt> to the PROPERTIES clause.
			This can also be done in a refinement. A good idea is then to generate a refinement for animation with ProB (which may contain other important settings for animation):
			<pre>
			REFINEMENT M0_ProB REFINES M0
			CONSTANTS aa,bb
			PROPERTIES
			AA = {aa,bb} & aa/=bb
			END
			</pre>


	=== Setting Deferred Set Cardinalities within probcli ===		=== Setting Deferred Set Cardinalities within probcli ===

Michael Leuschel at 08:26, 31 August 2015

2015-08-31T08:26:49Z

← Older revision		Revision as of 08:26, 31 August 2015
Line 1:		Line 1:

	A deferred set in B is declared in the SETS Section and is not explicitly enumerated. In the example below, AA is a deferred set and BB is an enumerated set.		A deferred set in B is declared in the SETS Section and is not explicitly enumerated. In the example below, AA is a deferred set and BB is an enumerated set.
	<pre>		<pre>
Line 7:		Line 6:
	</pre>		</pre>

	ProB in general requires all deferred sets to be given a finite cardinality before starting animation or model checking. If no cardinality is specified, a default size will be used.		ProB in general requires all deferred sets to be given a finite cardinality before starting animation or model checking. If no cardinality is specified, a default size will be used (which is controlled by the <tt>DEFAULT_SETSIZE</tt> [[Controlling ProB Preferences\|preference]]).

	In general (for both probcli and ProB Tcl/Tk) you can set the cardinality of a set AA either by		In general (for both probcli and ProB Tcl/Tk) you can set the cardinality of a set AA either by

Michael Leuschel: /* Setting Deferred Set Cardinalities within probcli */

2015-08-31T08:22:44Z

Setting Deferred Set Cardinalities within probcli

← Older revision		Revision as of 08:22, 31 August 2015
Line 25:		Line 25:
	Example:		Example:
	probcli my.mch -card PID 5		probcli my.mch -card PID 5
	See [[Using_the_Command-Line_Version_of_ProB#-card_.3CGS.3E_.3CVAL.3E]].		See [[Using_the_Command-Line_Version_of_ProB#-card_.3CGS.3E_.3CVAL.3E\|manual page for probcli]].

Michael Leuschel: Created page with ' A deferred set in B is declared in the SETS Section and is not explicitly enumerated. In the example below, AA is a deferred set and BB is an enumerated set.

 MACHINE Test …'

2015-08-31T08:21:56Z

Created page with ' A deferred set in B is declared in the SETS Section and is not explicitly enumerated. In the example below, AA is a deferred set and BB is an enumerated set. <pre> MACHINE Test …'

New page

A deferred set in B is declared in the SETS Section and is not explicitly enumerated. In the example below, AA is a deferred set and BB is an enumerated set.
<pre>
MACHINE Test
SETS AA; BB={bb,cc,dd}
END
</pre>

ProB in general requires all deferred sets to be given a finite cardinality before starting animation or model checking. If no cardinality is specified, a default size will be used.

In general (for both probcli and ProB Tcl/Tk) you can set the cardinality of a set AA either by
* making it an enumerated set, i.e., adding AA = {v1,v2,…} to the SETS clause
* adding a predicate card(AA) = constant to the PROPERTIES clause
* Note: various other predicates in the PROPERTIES clause will also influence the size used for AA by ProB, for example:
- card(AA) > 1
- AA = {aa,bb} & aa/=bb
- aa:AA & bb:AA & aa/=bb
- …
* you can add a DEFINITION scope_AA == constant to instruct ProB to set the cardinality of AA to the constant.

=== Setting Deferred Set Cardinalities within probcli ===

From the command-line, using probcli you can use the command-line switch:
-card <GS> <VAL>
Example:
probcli my.mch -card PID 5
See [[Using_the_Command-Line_Version_of_ProB#-card_.3CGS.3E_.3CVAL.3E]].