Tutorial Animation Tips - Revision history

Michael Leuschel: /* Using EXTENDS */

2023-05-03T08:37:16Z

Using EXTENDS

← Older revision		Revision as of 08:37, 3 May 2023
Line 172:		Line 172:

	This instance machine acts a bit like a configuration file for ProB.		This instance machine acts a bit like a configuration file for ProB.
			In Event-B you can use the extends concept for contexts to achieve this effect,
			[[Tutorial_Rodin_Parameters#Using_contexts_for_ProB_animation\|as explained here]].

2023-05-03T08:35:41Z

Using EXTENDS

← Older revision		Revision as of 08:35, 3 May 2023
Line 156:		Line 156:
	PROPERTIES root : USERS		PROPERTIES root : USERS
	END		END
	<pre>		</pre>

	In classical B you can use EXTENDS to create an instantiation machine:		In classical B you can use EXTENDS to create an instantiation machine:
Line 169:		Line 169:
	root = mary		root = mary
	END		END
	<pre>		</pre>

	This instance machine acts a bit like a configuration file for ProB.		This instance machine acts a bit like a configuration file for ProB.

2023-05-03T08:35:26Z

Using Trace Replay

← Older revision		Revision as of 08:35, 3 May 2023
Line 144:		Line 144:
	If you wish you can generate such traces programmatically		If you wish you can generate such traces programmatically
	or modify them by hand and try to replay them.		or modify them by hand and try to replay them.

			=== Using EXTENDS ===

			If you have many possible valuations for constants you may want to consider to generate one or more instantiations of your machine for animation or model checking.

			For example, given a machine
			<pre>
			MACHINE Generic
			SETS USERS
			CONSTANTS root
			PROPERTIES root : USERS
			END
			<pre>

			In classical B you can use EXTENDS to create an instantiation machine:

			<pre>
			MACHINE Instance1
			EXTENDS Generic
			CONSTANTS peter, paul, mary
			PROPERTIES
			USERS = {peter,paul,mary} &
			card({peter,paul,mary}) = 3 & // all different
			root = mary
			END
			<pre>

			This instance machine acts a bit like a configuration file for ProB.

2023-05-02T13:42:14Z

Using Constraint-Based Validation Techniques

@@ Line 87: / Line 87: @@
 [[file:ProB_Lift_Randomise.png|center||650px]]
 === Using Constraint-Based Validation Techniques ===
@@ Line 134: / Line 136: @@
 More details are available in the [[Tutorial_Model-Based_Testing]] and [[Tutorial_Model_Checking,_Proof_and_CBC]] sections.

2023-05-02T13:39:43Z

Increasing MAX_OPERATIONS or MAX_INITIALISATIONS

← Older revision		Revision as of 13:39, 2 May 2023
Line 33:		Line 33:

	Note there is another preference "MAX_INITIALISATIONS" which controls how many solutions are computed for SETUP_CONSTANTS and for INITIALISATION.		Note there is another preference "MAX_INITIALISATIONS" which controls how many solutions are computed for SETUP_CONSTANTS and for INITIALISATION.


			Note: you can also set either of these preferences to 0.
			In this case, no solutions will be automatically be pre-computed for you, but
			you can use "Execute an Operation..." below. You can then also double-click on individual operation names for this.

	=== Increasing MAX_OPERATIONS for an individual operation ===		=== Increasing MAX_OPERATIONS for an individual operation ===

2023-05-02T13:37:06Z

Increasing MAX_OPERATIONS

← Older revision		Revision as of 13:37, 2 May 2023
Line 22:		Line 22:
	There are several solutions to overcome this.		There are several solutions to overcome this.

	=== Increasing MAX_OPERATIONS ===		=== Increasing MAX_OPERATIONS or MAX_INITIALISATIONS===
	First, you could increase the "MAX_OPERATIONS" preference of ProB by selecting the "Animation Preferences" command in the "Preferences" menu:		First, you could increase the "MAX_OPERATIONS" preference of ProB by selecting the "Animation Preferences" command in the "Preferences" menu:

Line 30:		Line 30:

	[[file:ProB_Lift_OpPane_WithJump101.png\|center\|\|200px]]		[[file:ProB_Lift_OpPane_WithJump101.png\|center\|\|200px]]


			Note there is another preference "MAX_INITIALISATIONS" which controls how many solutions are computed for SETUP_CONSTANTS and for INITIALISATION.

	=== Increasing MAX_OPERATIONS for an individual operation ===		=== Increasing MAX_OPERATIONS for an individual operation ===

2019-03-21T07:05:01Z

Increasing MAX_OPERATIONS

← Older revision		Revision as of 07:05, 21 March 2019
Line 30:		Line 30:

	[[file:ProB_Lift_OpPane_WithJump101.png\|center\|\|200px]]		[[file:ProB_Lift_OpPane_WithJump101.png\|center\|\|200px]]

			=== Increasing MAX_OPERATIONS for an individual operation ===

			As of version 1.9.0 of ProB you can also set the MAX_OPERATIONS limit individually per operation.
			For this you need to add a declaration in the DEFINITIONS section of your B machine:

			<pre>
			DEFINITIONS
			MAX_OPERATIONS_jump == 101
			</pre>

	=== Executing an Operation by Predicate ===		=== Executing an Operation by Predicate ===

2015-02-11T16:59:41Z

Using Random enumeration

← Older revision		Revision as of 16:59, 11 February 2015
Line 68:		Line 68:
	After reloading the machine you should see a picture similar to the following one:		After reloading the machine you should see a picture similar to the following one:

	[[file:ProB_Lift_Randomise.png\|center\|\|~~550px~~]]		[[file:ProB_Lift_Randomise.png\|center\|\|650px]]

	=== Using Constraint-Based Validation Techniques ===		=== Using Constraint-Based Validation Techniques ===

2015-02-11T16:58:54Z

Constraint-Based Model-Based Testing

← Older revision		Revision as of 16:58, 11 February 2015
Line 113:		Line 113:
	[[file:CBCMBTTreeResult.png \|center\|\|600px]]		[[file:CBCMBTTreeResult.png \|center\|\|600px]]

			Green entries show test cases (traces which cover an operation in the shortest possible way), gray entries are traces which did not contribute to a test case.

	More details are available in the [[Tutorial_Model-Based_Testing]] and [[Tutorial_Model_Checking,_Proof_and_CBC]] sections.		More details are available in the [[Tutorial_Model-Based_Testing]] and [[Tutorial_Model_Checking,_Proof_and_CBC]] sections.

2015-02-11T16:57:18Z

Constraint-Based Model-Based Testing

← Older revision		Revision as of 16:57, 11 February 2015
Line 102:		Line 102:
	Now click on the ok button in the dialog box (which allows you to select the target operations to cover in the generated test cases):		Now click on the ok button in the dialog box (which allows you to select the target operations to cover in the generated test cases):

	[[file:CBCMBTDialog.png \|center\|\|~~300px~~]]		[[file:CBCMBTDialog.png \|center\|\|200px]]

	ProB will then find four test cases for you, one for each operation:		ProB will then find four test cases for you, one for each operation:
Line 111:		Line 111:


	[[file:CBCMBTTreeResult.png \|center\|\|~~500px~~]]		[[file:CBCMBTTreeResult.png \|center\|\|600px]]



	More details are available in the [[Tutorial_Model-Based_Testing]] and [[Tutorial_Model_Checking,_Proof_and_CBC]] sections.		More details are available in the [[Tutorial_Model-Based_Testing]] and [[Tutorial_Model_Checking,_Proof_and_CBC]] sections.