FAQ - Revision history

Michael Leuschel: /* How can I reduce the memory consumption for model-checking */

2017-05-18T16:45:09Z

How can I reduce the memory consumption for model-checking

← Older revision		Revision as of 16:45, 18 May 2017
Line 17:		Line 17:
	SET_PREF_COMPRESSION == TRUE		SET_PREF_COMPRESSION == TRUE
	to your B machine to set the preference.		to your B machine to set the preference.
			There is also the possibility to forget the state space of already visited states by setting the preferences FORGET_STATE_SPACE and IGNORE_HASH_COLLISIONS to TRUE.

	2) you can try reduce the state space, e.g., via [[Symmetry_Reduction symmetry]].		2) you can try reduce the state space, e.g., via [[Symmetry_Reduction symmetry]].

Michael Leuschel: /* Can I use transitive closure for Event-B models */

2017-05-18T16:43:33Z

Can I use transitive closure for Event-B models

@@ Line 6: / Line 6: @@
 Yes, you need to use a theory of the transitive closure which contains a special mapping file.
 See [[Event-B_Theories|the page on supporting Event-B theories]] along with the links to theories that can be used efficiently with ProB.
 = How do I perform a self-check of ProB? =

Michael Leuschel: /* How do I perform a self-check of ProB? */

2016-02-03T15:03:03Z

How do I perform a self-check of ProB?

← Older revision		Revision as of 15:03, 3 February 2016
Line 8:		Line 8:

	= How do I perform a self-check of ProB? =		= How do I perform a self-check of ProB? =
	If you suspect something is wrong with your ProB installation, run the "Perform Self Check" command in the "Debug Menu". Note: run this command immediately after startup before opening new machines (otherwise you may get some errors because the machine will override some default definitions used for the tests). Normally, the console window should look like this (you may get some multiple solutions warnings; but you should not get errors):		If you suspect something is wrong with your ProB Tcl/Tk installation, run the "Perform Self Check" command in the "Debug Menu". Note: run this command immediately after startup before opening new machines (otherwise you may get some errors because the machine will override some default definitions used for the tests). Normally, the console window should look like this (you may get some multiple solutions warnings; but you should not get errors):

	---------------------		---------------------

Michael Leuschel at 15:02, 3 February 2016

2016-02-03T15:02:24Z

← Older revision		Revision as of 15:02, 3 February 2016
Line 1:		Line 1:
	[[Category:User Manual]]		[[Category:User Manual]]
	{{Revision}}		{{Revision}}

			= Can I use transitive closure for Event-B models =

			Yes, you need to use a theory of the transitive closure which contains a special mapping file.
			See [[Event-B_Theories\|the page on supporting Event-B theories]] along with the links to theories that can be used efficiently with ProB.

	= How do I perform a self-check of ProB? =		= How do I perform a self-check of ProB? =
	If you suspect something is wrong with your ProB installation, run the "Perform Self Check" command in the "Debug Menu". Note: run this command immediately after startup before opening new machines (otherwise you may get some errors because the machine will override some default definitions used for the tests). Normally, the console window should look like this (you may get some multiple solutions warnings; but you should not get errors):		If you suspect something is wrong with your ProB installation, run the "Perform Self Check" command in the "Debug Menu". Note: run this command immediately after startup before opening new machines (otherwise you may get some errors because the machine will override some default definitions used for the tests). Normally, the console window should look like this (you may get some multiple solutions warnings; but you should not get errors):

Michael Leuschel: /* ProB User Group */

2015-09-18T15:39:58Z

ProB User Group

← Older revision		Revision as of 15:39, 18 September 2015
Line 68:		Line 68:

	They can then all be checked using the "Check LTL Assertions" command.		They can then all be checked using the "Check LTL Assertions" command.

	~~= ProB User Group =~~
	~~<html>~~
	~~<iframe id="forum_embed"~~
	~~src="javascript:void(0)"~~
	~~scrolling="no"~~
	~~frameborder="0"~~
	~~width="900"~~
	~~height="700">~~
	~~</iframe>~~
	~~<script type="text/javascript">~~
	~~document.getElementById('forum_embed').src =~~
	~~'https://groups.google.com/forum/embed/?place=forum/prob-users'~~
	~~+ '&showsearch=true&showpopout=true&showtabs=false'~~
	~~+ '&parenturl=' + encodeURIComponent(window.location.href);~~
	~~</script>~~
	~~</html>~~

Michael Leuschel: /* Checking Multiple LTL Formulas */

2015-09-18T15:39:34Z

Checking Multiple LTL Formulas

← Older revision		Revision as of 15:39, 18 September 2015
Line 68:		Line 68:

	They can then all be checked using the "Check LTL Assertions" command.		They can then all be checked using the "Check LTL Assertions" command.

			= ProB User Group =
			<html>
			<iframe id="forum_embed"
			src="javascript:void(0)"
			scrolling="no"
			frameborder="0"
			width="900"
			height="700">
			</iframe>
			<script type="text/javascript">
			document.getElementById('forum_embed').src =
			'https://groups.google.com/forum/embed/?place=forum/prob-users'
			+ '&showsearch=true&showpopout=true&showtabs=false'
			+ '&parenturl=' + encodeURIComponent(window.location.href);
			</script>
			</html>

Michael Leuschel: /* What do the funny question marks in the "Operations" pane mean? */

2015-02-11T18:04:22Z

What do the funny question marks in the "Operations" pane mean?

← Older revision		Revision as of 18:04, 11 February 2015
Line 24:		Line 24:
	= Is there support for refinement? =		= Is there support for refinement? =
	For the moment, you have to give types to operation arguments in refinements; the types are not always extracted from the ancestor specification. Furthermore, the precondition of the operations again are not extracted from ancestor machines and are not propagated down. This is an important difference with classical B: it means that ProB may find an invariant violation in the refinement machine even though the Refinement can be proven correct with B4Free or AtelierB. This is because in those tools you only need to prove consistency within the precondition of all ancestor machines ! ProB checks the refinement machine on its own. Anyway, we believe that it is probably bad style to rely on preconditions from ancestor machines for correctness (as they may be expressed in terms of abstract variables no longer present,...). Finally, as ProB treats top-level PRE conditions as SELECTS, this also affects refinement checking. [ProB's refinement checker is more suited for EventB than classical B, but we are working to fully support both styles of refinement.]		For the moment, you have to give types to operation arguments in refinements; the types are not always extracted from the ancestor specification. Furthermore, the precondition of the operations again are not extracted from ancestor machines and are not propagated down. This is an important difference with classical B: it means that ProB may find an invariant violation in the refinement machine even though the Refinement can be proven correct with B4Free or AtelierB. This is because in those tools you only need to prove consistency within the precondition of all ancestor machines ! ProB checks the refinement machine on its own. Anyway, we believe that it is probably bad style to rely on preconditions from ancestor machines for correctness (as they may be expressed in terms of abstract variables no longer present,...). Finally, as ProB treats top-level PRE conditions as SELECTS, this also affects refinement checking. [ProB's refinement checker is more suited for EventB than classical B, but we are working to fully support both styles of refinement.]

	~~= What do the funny question marks in the "Operations" pane mean? =~~
	A question mark signifies a pending constraint or co-routine. This should not happen in normal mode of operations but can happen if a variable is not given a type (ProB needs the type to enumerate the variable in case it is not bound). Try type-checking your machine (e.g., using B4Free). If there is not type error, please send a bug report.

	= The constraint based checker is very slow and does not always work =		= The constraint based checker is very slow and does not always work =

Michael Leuschel: /* The animator seems slow */

2015-02-11T18:03:54Z

The animator seems slow

← Older revision		Revision as of 18:03, 11 February 2015
Line 24:		Line 24:
	= Is there support for refinement? =		= Is there support for refinement? =
	For the moment, you have to give types to operation arguments in refinements; the types are not always extracted from the ancestor specification. Furthermore, the precondition of the operations again are not extracted from ancestor machines and are not propagated down. This is an important difference with classical B: it means that ProB may find an invariant violation in the refinement machine even though the Refinement can be proven correct with B4Free or AtelierB. This is because in those tools you only need to prove consistency within the precondition of all ancestor machines ! ProB checks the refinement machine on its own. Anyway, we believe that it is probably bad style to rely on preconditions from ancestor machines for correctness (as they may be expressed in terms of abstract variables no longer present,...). Finally, as ProB treats top-level PRE conditions as SELECTS, this also affects refinement checking. [ProB's refinement checker is more suited for EventB than classical B, but we are working to fully support both styles of refinement.]		For the moment, you have to give types to operation arguments in refinements; the types are not always extracted from the ancestor specification. Furthermore, the precondition of the operations again are not extracted from ancestor machines and are not propagated down. This is an important difference with classical B: it means that ProB may find an invariant violation in the refinement machine even though the Refinement can be proven correct with B4Free or AtelierB. This is because in those tools you only need to prove consistency within the precondition of all ancestor machines ! ProB checks the refinement machine on its own. Anyway, we believe that it is probably bad style to rely on preconditions from ancestor machines for correctness (as they may be expressed in terms of abstract variables no longer present,...). Finally, as ProB treats top-level PRE conditions as SELECTS, this also affects refinement checking. [ProB's refinement checker is more suited for EventB than classical B, but we are working to fully support both styles of refinement.]

	~~= The animator seems slow =~~
	Be sure you have the "Runtime Type Checking" and "Debugging Info" flags set to off in the Debug menu. The next release of ProB will hopefully make use of the LOGEN partial evaluator to pre-compile B machines; this should make the animator much, much faster.

	= What do the funny question marks in the "Operations" pane mean? =		= What do the funny question marks in the "Operations" pane mean? =

Michael Leuschel: /* Which features of B are covered? */

2015-02-11T18:03:13Z

Which features of B are covered?

← Older revision		Revision as of 18:03, 11 February 2015
Line 20:		Line 20:

	= Which features of B are covered? =		= Which features of B are covered? =
	ProB covers a large part of B, and we are striving towards full coverage. ProB supports B features such as non-deterministic operations, ANY statements, operations with complex arguments, sets, sequences, functions, lambda abstractions, set comprehensions, constants and properties, and many more. It has limited support for multiple machines and refinements (see FAQ entry about refinements below).		ProB covers a large part of B, and we are striving towards full coverage. ProB supports B features such as non-deterministic operations, ANY statements, operations with complex arguments, sets, sequences, functions, lambda abstractions, set comprehensions, constants and properties, and many more. It has limited support for multiple machines and refinements (see the [[Current_Limitations ]] section and the FAQ entry about refinements below).

	= Is there support for refinement? =		= Is there support for refinement? =

Joy Clark: "", s to z

2011-04-18T12:06:31Z

"", s to z

← Older revision		Revision as of 12:06, 18 April 2011
Line 2:		Line 2:
	{{Revision}}		{{Revision}}
	= How do I perform a self-check of ProB? =		= How do I perform a self-check of ProB? =
	If you suspect something is wrong with your ProB installation, run the Perform Self Check command in the Debug Menu. Note: run this command immediately after startup before opening new machines (otherwise you may get some errors because the ~~Machine~~ will override some default definitions used for the tests). Normally, the console window should look like this (you may get some multiple solutions warnings; but you should not get errors):		If you suspect something is wrong with your ProB installation, run the "Perform Self Check" command in the "Debug Menu". Note: run this command immediately after startup before opening new machines (otherwise you may get some errors because the machine will override some default definitions used for the tests). Normally, the console window should look like this (you may get some multiple solutions warnings; but you should not get errors):

	---------------------		---------------------
Line 28:		Line 28:
	Be sure you have the "Runtime Type Checking" and "Debugging Info" flags set to off in the Debug menu. The next release of ProB will hopefully make use of the LOGEN partial evaluator to pre-compile B machines; this should make the animator much, much faster.		Be sure you have the "Runtime Type Checking" and "Debugging Info" flags set to off in the Debug menu. The next release of ProB will hopefully make use of the LOGEN partial evaluator to pre-compile B machines; this should make the animator much, much faster.

	= What do the funny question marks in the Operations ~~Pane~~ mean? =		= What do the funny question marks in the "Operations" pane mean? =
	A question mark signifies a pending constraint or co-routine. This should not happen in normal mode of operations but can happen if a variable is not given a type (ProB needs the type to enumerate the variable in case it is not bound). Try ~~typechecking~~ your machine (e.g., using B4Free). If there is not type error, please send a bug report.		A question mark signifies a pending constraint or co-routine. This should not happen in normal mode of operations but can happen if a variable is not given a type (ProB needs the type to enumerate the variable in case it is not bound). Try type-checking your machine (e.g., using B4Free). If there is not type error, please send a bug report.

	= The constraint based checker is very slow and does not always work =		= The constraint based checker is very slow and does not always work =
Line 40:		Line 40:
	All variables should be given a type even though ProB may still work without them (but you are living dangerously). In the latest release, typing has become more flexible and previously defined variables are also recognized as a type. aa: POW(myset) & bb: POW(aa) is now ok (previously it was required to type aa: POW(myset) & bb: POW(aa) & bb: POW(POW(myset)) ). One can now also use subset for typing: bb <: COLOURS.		All variables should be given a type even though ProB may still work without them (but you are living dangerously). In the latest release, typing has become more flexible and previously defined variables are also recognized as a type. aa: POW(myset) & bb: POW(aa) is now ok (previously it was required to type aa: POW(myset) & bb: POW(aa) & bb: POW(POW(myset)) ). One can now also use subset for typing: bb <: COLOURS.

	= I cannot ~~visualise~~ the state space =		= I cannot visualize the state space =
	Be sure to set up the viewer preferences and use / (even on Windows!) Be sure to have dot installed and either dotty or a Postscript viewer. Also, on Windows the path to the machine files should not contain spaces. A good example directory would be C:/Machines/		Be sure to set up the viewer preferences and use / (even on Windows!) Be sure to have dot installed and either dotty or a Postscript viewer. Also, on Windows the path to the machine files should not contain spaces. A good example directory would be C:/Machines/

Line 61:		Line 61:
	I want to generate multiple assertion violations in ProB in order to generate the customized test cases for a particular B specfication according to various test coverage criteria. But ProB can only produce a single assertion violation at one time. Is there any option in ProB that can help in producing multiple assertion violations at one goal/command?		I want to generate multiple assertion violations in ProB in order to generate the customized test cases for a particular B specfication according to various test coverage criteria. But ProB can only produce a single assertion violation at one time. Is there any option in ProB that can help in producing multiple assertion violations at one goal/command?

	For the moment the solution would be to put the assertions into the invariant and then model check the entire state space by disabling "Find Invariant Violations" in the dialog box for the Temporal Model Check command. Afterwards, you can use "Compute Coverage" in the ~~analyse~~ menu to see how many states have violated the invariant. Another solution is to write a "dummy" operation for every assertion: my_assertion_N = SELECT not(Assertion_N) THEN skip END		For the moment the solution would be to put the assertions into the invariant and then model check the entire state space by disabling "Find Invariant Violations" in the dialog box for the Temporal Model Check command. Afterwards, you can use "Compute Coverage" in the "Analyse" menu to see how many states have violated the invariant. Another solution is to write a "dummy" operation for every assertion: my_assertion_N = SELECT not(Assertion_N) THEN skip END
	After model checking, you can again use "Compute Coverage" to see how often every assertion has been violated.		After model checking, you can again use "Compute Coverage" to see how often every assertion has been violated.