Tutorial Troubleshooting the Setup - Revision history

Michael Leuschel: /* A few more tips */

2021-10-06T16:09:31Z

A few more tips

← Older revision		Revision as of 16:09, 6 October 2021
Line 111:		Line 111:


	== ~~A few more tips~~ ==		== Selectively Ignoring Properties/Axioms ==

	~~In classical B you~~ can use a pragma to tell ProB to ignore a certain property:		You can use a pragma to tell ProB to ignore a certain property:

	<pre>		<pre>

Michael Leuschel: /* A few more tips */

2021-10-06T16:08:49Z

A few more tips

← Older revision		Revision as of 16:08, 6 October 2021
Line 125:		Line 125:
	END		END
	</pre>		</pre>
	The second property will be ignored during property setup, but will still be shown in the evaluation view for example		The second property will be ignored during property setup, but will still be shown in the evaluation view for example.

			This feature is available as of version 1.11.0 when the preference <tt>USE_IGNORE_PRAGMAS</tt> is set to TRUE (currently it is FALSE by default).
			Under these circumstances a conjunct of the PROPERTIES will then be ignored:
			* when it is followed by the <tt>/@desc prob-ignore /</tt> pragma
			* when it is preceded by a label which contains prob-ignore in its name, such as <tt>/* @label="axm2-prob-ignore" */</tt>.

			The latter thus also works within Rodin for Event-B contexts.

	An alternative can also be to move a predicate from PROPERTIES to the ASSERTIONS clause.		An alternative can also be to move a predicate from PROPERTIES to the ASSERTIONS clause.
	The latter will not be used during the constant setup.		The latter will not be used during the constant setup.

Michael Leuschel: /* A few more tips */

2021-06-08T12:28:23Z

A few more tips

← Older revision		Revision as of 12:28, 8 June 2021
Line 126:		Line 126:
	</pre>		</pre>
	The second property will be ignored during property setup, but will still be shown in the evaluation view for example		The second property will be ignored during property setup, but will still be shown in the evaluation view for example

			An alternative can also be to move a predicate from PROPERTIES to the ASSERTIONS clause.
			The latter will not be used during the constant setup.

Michael Leuschel at 12:27, 8 June 2021

2021-06-08T12:27:19Z

← Older revision		Revision as of 12:27, 8 June 2021
Line 109:		Line 109:
	After hitting "Select" or typing return we obtain, which shows us why the operation is not enabled:		After hitting "Select" or typing return we obtain, which shows us why the operation is not enabled:
	[[file:ProB_Jukebox_AnalyseGraphicallyOperationPRE3.png\|center]]		[[file:ProB_Jukebox_AnalyseGraphicallyOperationPRE3.png\|center]]


			== A few more tips ==

			In classical B you can use a pragma to tell ProB to ignore a certain property:

			<pre>
			MACHINE Log2
			DEFINITIONS SET_PREF_USE_IGNORE_PRAGMAS == TRUE
			ABSTRACT_CONSTANTS log2
			PROPERTIES
			log2 : NATURAL1 --> INTEGER &
			!(x,y).(x:NATURAL1 & y:NATURAL1 => log2(x*y) = log2(x)+log2(y))
			/@desc prob-ignore /
			END
			</pre>
			The second property will be ignored during property setup, but will still be shown in the evaluation view for example

Joy Clark: "", s to z

2011-04-18T12:26:24Z

"", s to z

Joy Clark: grasped to have grasped

2011-04-12T13:25:24Z

grasped to have grasped

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


	We assume that you grasped the way that ProB setups up the initial states of a B machine as outlined in [[Tutorial Setup Phases]].		We assume that you have grasped the way that ProB setups up the initial states of a B machine as outlined in [[Tutorial Setup Phases]].

	In this lesson, we examine what can go wrong in these phases and how one can find a solution. Indeed, setting up the constants and initial values of a machine is often the most difficult step for an animator. Unfortunately, it is also the very first step an animator has to perform.		In this lesson, we examine what can go wrong in these phases and how one can find a solution. Indeed, setting up the constants and initial values of a machine is often the most difficult step for an animator. Unfortunately, it is also the very first step an animator has to perform.

Joy Clark: /* Simple Inconsistency in the PROPERTIES */

2011-04-12T13:07:10Z

Simple Inconsistency in the PROPERTIES

← Older revision		Revision as of 13:07, 12 April 2011
Line 26:		Line 26:
	[[file:ProB_Jukebox_DebugUnsatProp.png\|center\|400px]]		[[file:ProB_Jukebox_DebugUnsatProp.png\|center\|400px]]

	What ProB does is add conjuncts from the PROPERTIES (and CONSTRAINTS clause) one-by-one, until it can no longer find a solution. This can often give you an indication of what is wrong, and ~~where~~ the trouble (or inconsistency) ~~stems from~~.		What ProB does is add conjuncts from the PROPERTIES (and CONSTRAINTS clause) one-by-one, until it can no longer find a solution. This can often give you an indication of what is wrong, and the source of the trouble (or inconsistency).

	An alternate means to figure out the source of the problem is ProB's graphical formula viewer.		An alternate means to figure out the source of the problem is ProB's graphical formula viewer.

Michael Leuschel at 09:58, 19 January 2010

2010-01-19T09:58:50Z

← Older revision		Revision as of 09:58, 19 January 2010
Line 1:		Line 1:
	[[Category:~~User Manual~~]]		[[Category:Tutorial]]

Michael Leuschel at 08:49, 19 January 2010

2010-01-19T08:49:19Z

← Older revision		Revision as of 08:49, 19 January 2010
Line 5:		Line 5:

	In this lesson, we examine what can go wrong in these phases and how one can find a solution. Indeed, setting up the constants and initial values of a machine is often the most difficult step for an animator. Unfortunately, it is also the very first step an animator has to perform.		In this lesson, we examine what can go wrong in these phases and how one can find a solution. Indeed, setting up the constants and initial values of a machine is often the most difficult step for an animator. Unfortunately, it is also the very first step an animator has to perform.

			We will also learn to use the various predicate analysis features provided by ProB.

	== Simple Inconsistency in the PROPERTIES ==		== Simple Inconsistency in the PROPERTIES ==

Michael Leuschel at 08:48, 19 January 2010

2010-01-19T08:48:00Z

← Older revision		Revision as of 08:48, 19 January 2010
Line 95:		Line 95:
	As we can see, this predicate is true in that particular state of the machine.		As we can see, this predicate is true in that particular state of the machine.
	Note, there is also the option to use "Analyse Predicate/Custom Predicate...". This will result in a simpler (non-graphical) visualisation. Use this if the graphical visualisation is too large or takes too much time to compute.		Note, there is also the option to use "Analyse Predicate/Custom Predicate...". This will result in a simpler (non-graphical) visualisation. Use this if the graphical visualisation is too large or takes too much time to compute.
			The custom predicate analysis commands have one disadvantage: the formula has to be typed into a single line inside the dialog box (and parse errors are not very user-friendly). The alternatives are entering the formula into the ASSERTIONS clause as above. One can also define a special GOAL predicate in the DEFINITIONS:
			<pre>
			DEFINITIONS GOAL == !x.(x<limit => x<99)
			</pre>
			Then one can use "Analyse Predicate/GOAL" or "Analyse Graphically/GOAL". The GOAL predicate can also be used to guide the model checker.

			Finally, the Analyse commands can also be applied to the precondition and guards of operations. This is useful to find out why a particular operation is (maybe) unexpectedly disabled or enabled.
			For this, choose the "Analyse Graphically/Operation PRE..." in the "Analyse" menu and select the "select" operation:
			[[file:ProB_Jukebox_AnalyseGraphicallyOperationPRE.png\|center]]

			After hitting Select or typing return we obtain, which shows us why the operation is not enabled:
			[[file:ProB_Jukebox_AnalyseGraphicallyOperationPRE3.png\|center]]

← Older revision		Revision as of 12:26, 18 April 2011
Line 35:		Line 35:


	This will result in the following ~~visualisation~~:		This will result in the following visualization:

	[[file:ProB_Jukebox_AnalyseGraphicallyUnsatProp.png\|center]]		[[file:ProB_Jukebox_AnalyseGraphicallyUnsatProp.png\|center]]
Line 65:		Line 65:

	We can see that ProB has found the solution <tt>limit=100</tt> for the first two properties and then got stuck.		We can see that ProB has found the solution <tt>limit=100</tt> for the first two properties and then got stuck.
	Using the graphical viewer results the following ~~visualisation~~:		Using the graphical viewer results the following visualization:

	[[file:ProB_Jukebox_AnalyseGraphicallyUnsatProp2.png\|center\|600px]]		[[file:ProB_Jukebox_AnalyseGraphicallyUnsatProp2.png\|center\|600px]]
Line 82:		Line 82:
	[[file:ProB_JukeboxAfterInit3.png\|center\|\|600px]]		[[file:ProB_JukeboxAfterInit3.png\|center\|\|600px]]

	We can now ~~analyse~~ the ASSERTIONS.		We can now analyze the ASSERTIONS.
	For this, choose the "Analyse Graphically/Assertions" in the "Analyse" menu:		For this, choose the "Analyse Graphically/Assertions" in the "Analyse" menu:

Line 89:		Line 89:
	The graphical viewer gives us an instance where the universally quantified formula is false: <tt>x=99</tt>, which hopefully helps us in fixing the problem, e.g., writing <tt>!x.(x<limit => x<=99)</tt>.		The graphical viewer gives us an instance where the universally quantified formula is false: <tt>x=99</tt>, which hopefully helps us in fixing the problem, e.g., writing <tt>!x.(x<limit => x<=99)</tt>.

	Note, that ProB also allows us to inspect custom predicates using the ~~Graphical Viewer~~ (without saving and reopening a machine).		Note, that ProB also allows us to inspect custom predicates using the graphical viewer (without saving and reopening a machine).
	For this, choose the "Analyse Graphically/Custom Predicate..." in the "Analyse" menu and enter <tt>!x.(x<limit => x<=99)</tt>:		For this, choose the "Analyse Graphically/Custom Predicate..." in the "Analyse" menu and enter <tt>!x.(x<limit => x<=99)</tt>:
	[[file:ProB_Jukebox_AnalyseGraphicallyCustomCommand.png\|center]]		[[file:ProB_Jukebox_AnalyseGraphicallyCustomCommand.png\|center]]
Line 96:		Line 96:

	As we can see, this predicate is true in that particular state of the machine.		As we can see, this predicate is true in that particular state of the machine.
	Note, there is also the option to use "Analyse Predicate/Custom Predicate...". This will result in a simpler (non-graphical) ~~visualisation~~. Use this if the graphical ~~visualisation~~ is too large or takes too much time to compute.		Note, there is also the option to use "Analyse Predicate/Custom Predicate...". This will result in a simpler (non-graphical) visualization. Use this if the graphical visualization is too large or takes too much time to compute.
	The custom predicate analysis commands have one disadvantage: the formula has to be typed into a single line inside the dialog box (and parse errors are not very user-friendly). The alternatives are entering the formula into the ASSERTIONS clause as above. One can also define a special GOAL predicate in the DEFINITIONS:		The custom predicate analysis commands have one disadvantage: the formula has to be typed into a single line inside the dialog box (and parse errors are not very user-friendly). The alternatives are entering the formula into the ASSERTIONS clause as above. One can also define a special GOAL predicate in the DEFINITIONS:
	<pre>		<pre>
Line 103:		Line 103:
	Then one can use "Analyse Predicate/GOAL" or "Analyse Graphically/GOAL". The GOAL predicate can also be used to guide the model checker.		Then one can use "Analyse Predicate/GOAL" or "Analyse Graphically/GOAL". The GOAL predicate can also be used to guide the model checker.

	Finally, the Analyse commands can also be applied to the precondition and guards of operations. This is useful to find out why a particular operation is (maybe) unexpectedly disabled or enabled.		Finally, the "Analyse" commands can also be applied to the precondition and guards of operations. This is useful to find out why a particular operation is (maybe) unexpectedly disabled or enabled.
	For this, choose the "Analyse Graphically/Operation PRE..." in the "Analyse" menu and select the "select" operation:		For this, choose the "Analyse Graphically/Operation PRE..." in the "Analyse" menu and select the "select" operation:
	[[file:ProB_Jukebox_AnalyseGraphicallyOperationPRE.png\|center]]		[[file:ProB_Jukebox_AnalyseGraphicallyOperationPRE.png\|center]]

	After hitting Select or typing return we obtain, which shows us why the operation is not enabled:		After hitting "Select" or typing return we obtain, which shows us why the operation is not enabled:
	[[file:ProB_Jukebox_AnalyseGraphicallyOperationPRE3.png\|center]]		[[file:ProB_Jukebox_AnalyseGraphicallyOperationPRE3.png\|center]]