Tutorial Setup Phases - Revision history

Michael Leuschel: /* 2. SETUP_CONSTANTS */

2023-05-02T13:35:38Z

2. SETUP_CONSTANTS

← Older revision		Revision as of 13:35, 2 May 2023
Line 45:		Line 45:
	Note that ProB will '''not''' (yet) modify the settings from phase 1 for MAXINT, MININT and the size of the deferred sets.		Note that ProB will '''not''' (yet) modify the settings from phase 1 for MAXINT, MININT and the size of the deferred sets.

	ProB will initiate this phase automatically, and as we can see above, ProB has found three distinct ways to setup the constant limit. Observe that a little orange button labeled max has appeared in the "Enabled Operations" pane. This means that there might actually be more than three ways to setup the constants. We will [[Tutorial_Animation_Tips\|return to this issue later]].		ProB will initiate this phase automatically, and as we can see above, ProB has found three distinct ways to setup the constant limit. Observe that a little orange button labeled max has appeared in the "Enabled Operations" pane. This means that there might actually be more than three ways to setup the constants. (If you wish you can right-click in the pane and select "Execute an Operation..." which allows you to choose other values such as limit=4. We will [[Tutorial_Animation_Tips\|return to this issue later]].)

	By double clicking on "SETUP_CONSTANTS(2)" we proceed to the next phase:		By double clicking on "SETUP_CONSTANTS(2)" we proceed to the next phase:

Michael Leuschel: /* 2. SETUP_CONSTANTS */

2023-05-02T13:33:50Z

2. SETUP_CONSTANTS

← Older revision		Revision as of 13:33, 2 May 2023
Line 45:		Line 45:
	Note that ProB will '''not''' (yet) modify the settings from phase 1 for MAXINT, MININT and the size of the deferred sets.		Note that ProB will '''not''' (yet) modify the settings from phase 1 for MAXINT, MININT and the size of the deferred sets.

	ProB will initiate this phase automatically, and as we can see above, ProB has found three distinct ways to setup the constant limit. Observe that a little orange button labeled max has appeared in the "Enabled Operations" pane. This means that there might actually be more than three ways to setup the constants. We will return to this issue later.		ProB will initiate this phase automatically, and as we can see above, ProB has found three distinct ways to setup the constant limit. Observe that a little orange button labeled max has appeared in the "Enabled Operations" pane. This means that there might actually be more than three ways to setup the constants. We will [[Tutorial_Animation_Tips\|return to this issue later]].

	By double clicking on "SETUP_CONSTANTS(2)" we proceed to the next phase:		By double clicking on "SETUP_CONSTANTS(2)" we proceed to the next phase:

Joy Clark: "", s to z

2011-04-18T12:23:12Z

"", s to z

Joy Clark: /* 1. Loading */ added a space

2011-04-12T14:26:21Z

1. Loading: added a space

← Older revision		Revision as of 14:26, 12 April 2011
Line 32:		Line 32:
	Note that these preferences determine the elements of the sets <tt>INT</tt> (implementable integers), <tt>NAT</tt> (implementable natural numbers) and <tt>NAT1</tt>. In addition, they are used to control the enumeration of variables of type <tt>INTEGER</tt> (mathematical integers), in case a definite value cannot be inferred from the machine.		Note that these preferences determine the elements of the sets <tt>INT</tt> (implementable integers), <tt>NAT</tt> (implementable natural numbers) and <tt>NAT1</tt>. In addition, they are used to control the enumeration of variables of type <tt>INTEGER</tt> (mathematical integers), in case a definite value cannot be inferred from the machine.

	Afterwards, ProB will determine the cardinality of all deferred sets (such as <tt>TRACK</tt> in the Jukebox machine).There are several ways you can influence this:		Afterwards, ProB will determine the cardinality of all deferred sets (such as <tt>TRACK</tt> in the Jukebox machine). There are several ways you can influence this:
	* by using "Animation Preferences..." command in the "Preferences" menu and modifying the preference "Size of unspecified deferred sets in SETS section".		* by using "Animation Preferences..." command in the "Preferences" menu and modifying the preference "Size of unspecified deferred sets in SETS section".
	* by including a "DEFINITIONS" section in your machine (if there is not yet one) and then adding a definition of the form <tt>scope_TRACK == 5</tt> (where <tt>TRACK</tt> is the name of the deferred set you wish to influence and 5 is its desired cardinality). This will override the default size.		* by including a "DEFINITIONS" section in your machine (if there is not yet one) and then adding a definition of the form <tt>scope_TRACK == 5</tt> (where <tt>TRACK</tt> is the name of the deferred set you wish to influence and 5 is its desired cardinality). This will override the default size.

Joy Clark at 13:24, 12 April 2011

2011-04-12T13:24:30Z

← Older revision		Revision as of 13:24, 12 April 2011
Line 2:		Line 2:


	We assume that you grasped the first steps of opening and animating a B machine as outlined in [[Tutorial First Step]].		We assume that you have grasped the first steps of opening and animating a B machine as outlined in [[Tutorial First Step]].

	In this lesson, we examine more closely the various steps that ProB undertakes before a machine can be animated.		In this lesson, we examine more closely the various steps that ProB undertakes before a machine can be animated.

Michael Leuschel: /* 1. Loading */

2010-06-02T09:58:14Z

1. Loading

← Older revision		Revision as of 09:58, 2 June 2010
Line 30:		Line 30:
	* by using "Animation Preferences..." command in the "Preferences" menu and modifying the corresponding preferences.		* by using "Animation Preferences..." command in the "Preferences" menu and modifying the corresponding preferences.
	* by including a "DEFINITIONS" section in your machine (if there is not yet one) and then adding a definition of the form <tt>SET_PREF_MAXINT == 5</tt> or <tt>SET_PREF_MININT == -2147483648</tt>.		* by including a "DEFINITIONS" section in your machine (if there is not yet one) and then adding a definition of the form <tt>SET_PREF_MAXINT == 5</tt> or <tt>SET_PREF_MININT == -2147483648</tt>.
	Note that these preferences determine the elements of the sets <tt>INT</tt> (implementable integers), <tt>NAT</tt> (implementable natural numbers) and <tt>NAT1</tt>. In addition, they are used to control the enumeration of variables of type <tt>INTEGER</tt>) (mathematical integers), in case a definite value cannot be inferred from the machine.		Note that these preferences determine the elements of the sets <tt>INT</tt> (implementable integers), <tt>NAT</tt> (implementable natural numbers) and <tt>NAT1</tt>. In addition, they are used to control the enumeration of variables of type <tt>INTEGER</tt> (mathematical integers), in case a definite value cannot be inferred from the machine.

	Afterwards, ProB will determine the cardinality of all deferred sets (such as <tt>TRACK</tt> in the Jukebox machine).There are several ways you can influence this:		Afterwards, ProB will determine the cardinality of all deferred sets (such as <tt>TRACK</tt> in the Jukebox machine).There are several ways you can influence this:

Michael Leuschel: /* 1. Loading */

2010-06-02T09:57:51Z

1. Loading

← Older revision		Revision as of 09:57, 2 June 2010
Line 30:		Line 30:
	* by using "Animation Preferences..." command in the "Preferences" menu and modifying the corresponding preferences.		* by using "Animation Preferences..." command in the "Preferences" menu and modifying the corresponding preferences.
	* by including a "DEFINITIONS" section in your machine (if there is not yet one) and then adding a definition of the form <tt>SET_PREF_MAXINT == 5</tt> or <tt>SET_PREF_MININT == -2147483648</tt>.		* by including a "DEFINITIONS" section in your machine (if there is not yet one) and then adding a definition of the form <tt>SET_PREF_MAXINT == 5</tt> or <tt>SET_PREF_MININT == -2147483648</tt>.
	Note that these preferences determine the elements of the sets <tt>INT</tt> (implementable integers), <tt>NAT</tt> (implementable natural numbers) and <tt>NAT1</tt>. In addition, they are used to control the enumeration of variables of type <tt>INTEGER</tt) (mathematical integers), in case a definite value cannot be inferred from the machine.		Note that these preferences determine the elements of the sets <tt>INT</tt> (implementable integers), <tt>NAT</tt> (implementable natural numbers) and <tt>NAT1</tt>. In addition, they are used to control the enumeration of variables of type <tt>INTEGER</tt>) (mathematical integers), in case a definite value cannot be inferred from the machine.

	Afterwards, ProB will determine the cardinality of all deferred sets (such as <tt>TRACK</tt> in the Jukebox machine).There are several ways you can influence this:		Afterwards, ProB will determine the cardinality of all deferred sets (such as <tt>TRACK</tt> in the Jukebox machine).There are several ways you can influence this:

Michael Leuschel: /* 3. INITIALISATION */

2010-01-18T16:31:22Z

3. INITIALISATION

← Older revision		Revision as of 16:31, 18 January 2010
Line 55:		Line 55:
	As we can see above, ProB has found just one possible way to initialise the variables <tt>credit</tt> and <tt>playset</tt>. Double-clicking on INITIALISATION(0,{}) leads the animator into a state where all constants and variables are valued, and where the <tt>INVARIANT</tt> can be checked and operations can be applied:		As we can see above, ProB has found just one possible way to initialise the variables <tt>credit</tt> and <tt>playset</tt>. Double-clicking on INITIALISATION(0,{}) leads the animator into a state where all constants and variables are valued, and where the <tt>INVARIANT</tt> can be checked and operations can be applied:

	[[file:ProB_JukeboxAfterINITIALISATION.png\|center\|\|700px]]		[[file:ProB_JukeboxAfterINITIALISATION.png\|center\|700px]]




	Let us conclude by choosing the "View Statespace" command in the "Animate" menu:		Let us conclude by choosing the "View Statespace" command in the "Animate" menu:

	[[file:ProB_Jukebox_Statespace.png\|center]]		[[file:ProB_Jukebox_Statespace.png\|center\|500px]]

	As you can see, there is only one root node: in order to change MAXINT, MININT or the deferred set sizes you have to reload the machine. There are, however, three different ways to setup the constants. The model checker will explore all of them. Let us choose the "Model Check..." command in the "Verify" menu and then press on the "Model Check" button.		As you can see, there is only one root node (inverted triangle): in order to change MAXINT, MININT or the deferred set sizes you have to reload the machine. There are, however, three different ways to setup the constants. The model checker will explore all of them. Let us choose the "Model Check..." command in the "Verify" menu and then press on the "Model Check" button.

	If we now choose the "View Statespace" command in the "Animate" menu, we get the following picture:		If we now choose the "View Statespace" command in the "Animate" menu, we get the following picture:
	[[file:ProB_Jukebox_StatespaceFull.png\|center]]		[[file:ProB_Jukebox_StatespaceFull.png\|center]]
	We can see (or guess at least) that ProB has validated the machine and explored the statespace not just for <tt>limit=2</tt> but also for <tt>limit=1</tt> and <tt>limit=3</tt>.		We can see (or guess at least) that ProB has validated the machine and explored the statespace not just for <tt>limit=2</tt> but also for <tt>limit=1</tt> and <tt>limit=3</tt>.

Michael Leuschel: /* 1. Loading */

2010-01-18T16:30:09Z

1. Loading

← Older revision		Revision as of 16:30, 18 January 2010
Line 37:		Line 37:
	* by including a predicate of the form <tt>card(TRACK)=5</tt> in the <tt>PROPERTIES</tt> or <tt>CONSTRAINTS</tt> section of your machine.		* by including a predicate of the form <tt>card(TRACK)=5</tt> in the <tt>PROPERTIES</tt> or <tt>CONSTRAINTS</tt> section of your machine.

	As you can see above, ProB has chosen MAXINT=3, MININT=-1 and card(TRACK)=2. If you wish to change these settings, perform the steps above and reload the machine. Hint: there is a Reopen command in the File menu:		As you can see above in the "State Properties" pane, ProB has chosen MAXINT=3, MININT=-1 and card(TRACK)=2. If you wish to change these settings, perform the steps above and reload the machine. Hint: there is a Reopen command in the File menu:
	[[file:ProB_JukeboxReopenCommand.png\|center]]		[[file:ProB_JukeboxReopenCommand.png\|center]]

Michael Leuschel at 16:29, 18 January 2010

2010-01-18T16:29:29Z

← Older revision		Revision as of 16:29, 18 January 2010
Line 2:		Line 2:


	We assume that you grasped the first steps of opening and animating a B machine as outlined in [[Tutorial First ~~Steps~~]].		We assume that you grasped the first steps of opening and animating a B machine as outlined in [[Tutorial First Step]].

	In this lesson, we examine more closely the various steps that ProB undertakes before a machine can be animated.		In this lesson, we examine more closely the various steps that ProB undertakes before a machine can be animated.
Line 38:		Line 38:

	As you can see above, ProB has chosen MAXINT=3, MININT=-1 and card(TRACK)=2. If you wish to change these settings, perform the steps above and reload the machine. Hint: there is a Reopen command in the File menu:		As you can see above, ProB has chosen MAXINT=3, MININT=-1 and card(TRACK)=2. If you wish to change these settings, perform the steps above and reload the machine. Hint: there is a Reopen command in the File menu:
			[[file:ProB_JukeboxReopenCommand.png\|center]]
	[[file:ProB_JukeboxReopenCommand.png\|center~~\|\|700px~~]]

	== 2. SETUP_CONSTANTS ==		== 2. SETUP_CONSTANTS ==
Line 48:		Line 47:
	ProB will initiate this phase automatically, and as we can see above, ProB has found three distinct ways to setup the constant limit. Observe that a little orange button labelled max has appeared in the "Enabled Operations" pane. This means that there might actually be more than three ways to setup the constants. We will return to this issue later.		ProB will initiate this phase automatically, and as we can see above, ProB has found three distinct ways to setup the constant limit. Observe that a little orange button labelled max has appeared in the "Enabled Operations" pane. This means that there might actually be more than three ways to setup the constants. We will return to this issue later.

	By double clicking on "SETUP_CONSTANTS(2)" we proceed to the next phase:		By double clicking on "SETUP_CONSTANTS(2)" we proceed to the next phase:

	[[file:ProB_JukeboxAfterSETUPCONSTANTS.png\|center\|\|700px]]		[[file:ProB_JukeboxAfterSETUPCONSTANTS.png\|center\|\|700px]]

Line 66:		Line 64:
	[[file:ProB_Jukebox_Statespace.png\|center]]		[[file:ProB_Jukebox_Statespace.png\|center]]

	As you can see, there is only one root node: in order to change MAXINT, MININT or the deferred set sizes you have to reload the machine. There are, however, three different ways to setup the constants. The model checker will explore all of them. ~~If we~~ choose the "Model Check..." command in the "Verify" menu and then press on the "Model Check" button.		As you can see, there is only one root node: in order to change MAXINT, MININT or the deferred set sizes you have to reload the machine. There are, however, three different ways to setup the constants. The model checker will explore all of them. Let us choose the "Model Check..." command in the "Verify" menu and then press on the "Model Check" button.


			If we now choose the "View Statespace" command in the "Animate" menu, we get the following picture:
	[[file:ProB_Jukebox_StatespaceFull.png\|center]]		[[file:ProB_Jukebox_StatespaceFull.png\|center]]
			We can see (or guess at least) that ProB has validated the machine and explored the statespace not just for <tt>limit=2</tt> but also for <tt>limit=1</tt> and <tt>limit=3</tt>.

← Older revision		Revision as of 12:23, 18 April 2011
Line 15:		Line 15:
	* 1. Loading the machine and determining the sizes of the deferred sets, as well as fixing the values of MININT and MAXINT.		* 1. Loading the machine and determining the sizes of the deferred sets, as well as fixing the values of MININT and MAXINT.
	* 2. Setting up the constants of the machine, such that the PROPERTIES and CONSTRAINTS are satisfied.		* 2. Setting up the constants of the machine, such that the PROPERTIES and CONSTRAINTS are satisfied.
	* 3. Performing a valid ~~initialisation~~ of the machine.		* 3. Performing a valid initialization of the machine.
	This process is illustrated in the following picture:		This process is illustrated in the following picture:

Line 37:		Line 37:
	* by including a predicate of the form <tt>card(TRACK)=5</tt> in the <tt>PROPERTIES</tt> or <tt>CONSTRAINTS</tt> section of your machine.		* by including a predicate of the form <tt>card(TRACK)=5</tt> in the <tt>PROPERTIES</tt> or <tt>CONSTRAINTS</tt> section of your machine.

	As you can see above in the "State Properties" pane, ProB has chosen MAXINT=3, MININT=-1 and card(TRACK)=2. If you wish to change these settings, perform the steps above and reload the machine. Hint: there is a Reopen command in the File menu:		As you can see above in the "State Properties" pane, ProB has chosen MAXINT=3, MININT=-1 and card(TRACK)=2. If you wish to change these settings, perform the steps above and reload the machine. Hint: there is a "Reopen" command in the "File" menu:
	[[file:ProB_JukeboxReopenCommand.png\|center]]		[[file:ProB_JukeboxReopenCommand.png\|center]]

Line 45:		Line 45:
	Note that ProB will '''not''' (yet) modify the settings from phase 1 for MAXINT, MININT and the size of the deferred sets.		Note that ProB will '''not''' (yet) modify the settings from phase 1 for MAXINT, MININT and the size of the deferred sets.

	ProB will initiate this phase automatically, and as we can see above, ProB has found three distinct ways to setup the constant limit. Observe that a little orange button ~~labelled~~ max has appeared in the "Enabled Operations" pane. This means that there might actually be more than three ways to setup the constants. We will return to this issue later.		ProB will initiate this phase automatically, and as we can see above, ProB has found three distinct ways to setup the constant limit. Observe that a little orange button labeled max has appeared in the "Enabled Operations" pane. This means that there might actually be more than three ways to setup the constants. We will return to this issue later.

	By double clicking on "SETUP_CONSTANTS(2)" we proceed to the next phase:		By double clicking on "SETUP_CONSTANTS(2)" we proceed to the next phase:
	[[file:ProB_JukeboxAfterSETUPCONSTANTS.png\|center\|\|700px]]		[[file:ProB_JukeboxAfterSETUPCONSTANTS.png\|center\|\|700px]]

	== 3. ~~INITIALISATION~~ ==		== 3. INITIALIZATION ==

	In this phase the values for the constants have been found, but the initial values of the variables still remain to be determined. For this, ProB will try to execute the <tt>INITIALISATION</tt> substitution.		In this phase the values for the constants have been found, but the initial values of the variables still remain to be determined. For this, ProB will try to execute the <tt>INITIALISATION</tt> substitution.
	As we can see above, ProB has found just one possible way to ~~initialise~~ the variables <tt>credit</tt> and <tt>playset</tt>. Double-clicking on INITIALISATION(0,{}) leads the animator into a state where all constants and variables are valued, and where the <tt>INVARIANT</tt> can be checked and operations can be applied:		As we can see above, ProB has found just one possible way to initialize the variables <tt>credit</tt> and <tt>playset</tt>. Double-clicking on INITIALISATION(0,{}) leads the animator into a state where all constants and variables are valued, and where the <tt>INVARIANT</tt> can be checked and operations can be applied:

	[[file:ProB_JukeboxAfterINITIALISATION.png\|center\|700px]]		[[file:ProB_JukeboxAfterINITIALISATION.png\|center\|700px]]