Tutorial Complete Model Checking - Revision history

David Geleßus at 08:47, 17 June 2022

2022-06-17T08:47:17Z

← Older revision		Revision as of 08:47, 17 June 2022
Line 6:		Line 6:
	In this part we use the following B Machine:		In this part we use the following B Machine:
	<pre>		<pre>
	~~DEFINITIONS~~
	MACHINE SimpleCounterForMC		MACHINE SimpleCounterForMC
	DEFINITIONS MAX==4; SET_PREF_MAX_OPERATIONS==5		DEFINITIONS MAX==4; SET_PREF_MAX_OPERATIONS==5

Joy Clark: grammar and punctuation edits

2011-04-18T12:18:07Z

grammar and punctuation edits

Michael Leuschel at 13:09, 1 March 2011

2011-03-01T13:09:22Z

Daniel Plagge: fixed typo

2011-03-01T10:34:43Z

fixed typo

← Older revision		Revision as of 10:34, 1 March 2011
Line 23:		Line 23:
	To load this machine into ProB you can select "New..." from the "File" menu, choose a file name (e.g., "SimpleCounterForMC.mch") and then paste the text above into the ProB source pane and choose "Save and Reopen" from the "File" menu.		To load this machine into ProB you can select "New..." from the "File" menu, choose a file name (e.g., "SimpleCounterForMC.mch") and then paste the text above into the ProB source pane and choose "Save and Reopen" from the "File" menu.

	Note that the DEFINITION SET_PREF_MAX_OPERATIONS==5 means that ProB will compute at most 5 possible ways to execute any ~~give~~ operation (i.e., Increase and Reset in this case). We return to this issue below.		Note that the DEFINITION SET_PREF_MAX_OPERATIONS==5 means that ProB will compute at most 5 possible ways to execute any given operation (i.e., Increase and Reset in this case). We return to this issue below.

	== Successful Model Checking ==		== Successful Model Checking ==

Michael Leuschel: /* Model Checking and Proof */

2011-03-01T10:13:07Z

Model Checking and Proof

← Older revision		Revision as of 10:13, 1 March 2011
Line 114:		Line 114:

	Finally, even if ProB was able to successfully check the entire state space of your model, this does not imply that you can prove your machine correct with AtelierB (or Rodin).		Finally, even if ProB was able to successfully check the entire state space of your model, this does not imply that you can prove your machine correct with AtelierB (or Rodin).
	We dedicate another tutorial page to this:		We dedicate another tutorial page to this: [[Tutorial Model Checking, Proof and CBC\|Model Checking, Proof and CBC]]
	[[Tutorial Model Checking, Proof and CBC\|Model Checking, Proof and CBC]]

Michael Leuschel at 10:12, 1 March 2011

2011-03-01T10:12:49Z

← Older revision		Revision as of 10:12, 1 March 2011
Line 99:		Line 99:
	SETS ID={id1,id2,id3,id4,id5}		SETS ID={id1,id2,id3,id4,id5}
	</Pre>		</Pre>

			== Infinite Types ==

			It could be that your B machine makes use of the mathematical integers (INTEGER) or infinite subsets thereof (NATURAL, NATURAL1). Note that some derived types (such as seq(.)) are defined in terms of INTEGER.
			In this case there could be no way to explore all states of your system.
			For example, the following operation
			<Pre>
			Choose = BEGIN x :: NATURAL END
			</Pre>
			can be executed in infinitely many ways. ProB will in this case only find values between 0 and MAXINT for x. As such, a complete model checking does not indicate that your machine's state space has been fully explored.
			Note: ProB prints a warning on the console when an infinite type (like NATURAL) was "expanded" into a finite subset of it. This information is not yet fed back to the graphical user interface (but we are working on it).

			== Model Checking and Proof ==

			Finally, even if ProB was able to successfully check the entire state space of your model, this does not imply that you can prove your machine correct with AtelierB (or Rodin).
			We dedicate another tutorial page to this:
			[[Tutorial Model Checking, Proof and CBC\|Model Checking, Proof and CBC]]

Michael Leuschel at 09:45, 1 March 2011

2011-03-01T09:45:00Z

← Older revision		Revision as of 09:45, 1 March 2011
Line 88:		Line 88:
	If you add this definition, ProB will now find an invariant violation:		If you add this definition, ProB will now find an invariant violation:
	[[file:ProBSimpleCountDefSet_InvViol.png\|center]]		[[file:ProBSimpleCountDefSet_InvViol.png\|center]]

			However, if you remove the above DEFINITION and add the following instead:
			<Pre>
			PROPERTIES card(ID) = 5
			</Pre>
			ProB will give you the message we have already seen:
			[[file:ProBModelCheckNoCounterExampleFound.png\|center]]
			Indeed, you have now explicitly declare ID to be of size 5, and ProB has checked all states for that instantiation of ID. Another solution is to replace the deferred set ID by an enumerated set (this will, however, reduce the potential for symmetry reduction):
			<Pre>
			SETS ID={id1,id2,id3,id4,id5}
			</Pre>

Michael Leuschel at 09:41, 1 March 2011

2011-03-01T09:41:01Z

← Older revision		Revision as of 09:41, 1 March 2011
Line 75:		Line 75:
	</Pre>		</Pre>

	Here model checking with ProB will give you the message ~~we have already seen~~:		Here model checking with ProB will give you the following message:
	[[file:~~ProBModelCheckNoCounterExampleFound~~.png\|center]]		[[file:ProBModelCheckNoCounterExampleFound_Unbounded.png\|center]]

	Unfortunately this does not guarantee that your machine is correct. Indeed, ProB has checked your machine only for one specific cardinality of the deferred set ID (probably 2 or 3).		Unfortunately this does not guarantee that your machine is correct. Indeed, ProB has checked your machine only for one specific cardinality of the deferred set ID (probably 2 or 3).

Michael Leuschel at 09:37, 1 March 2011

2011-03-01T09:37:48Z

← Older revision		Revision as of 09:37, 1 March 2011
Line 70:		Line 70:
	INITIALISATION s := {}		INITIALISATION s := {}
	OPERATIONS		OPERATIONS
	Add(x) = PRE x:ID & x/:s THEN s := s\/{x} END		Add(x) = PRE x:ID & x/:s THEN s := s\/{x} END;
			Remove(x) = PRE x:s THEN s:= s - {x} END
	END		END
	</Pre>		</Pre>

Michael Leuschel at 09:03, 1 March 2011

2011-03-01T09:03:12Z

← Older revision		Revision as of 09:03, 1 March 2011
Line 59:		Line 59:
	Now model checking will find a counter example:		Now model checking will find a counter example:
	[[file:ProBSimpleCounterForMC_InvViol.png\|center]]		[[file:ProBSimpleCounterForMC_InvViol.png\|center]]

			== Deferred Sets ==

			Let us now use the following simple machine:
			<Pre>
			MACHINE SimpleCountDefSet
			SETS ID
			VARIABLES s
			INVARIANT s <: ID & card(s)<10
			INITIALISATION s := {}
			OPERATIONS
			Add(x) = PRE x:ID & x/:s THEN s := s\/{x} END
			END
			</Pre>

			Here model checking with ProB will give you the message we have already seen:
			[[file:ProBModelCheckNoCounterExampleFound.png\|center]]

			Unfortunately this does not guarantee that your machine is correct. Indeed, ProB has checked your machine only for one specific cardinality of the deferred set ID (probably 2 or 3).
			Indeed, if you look at the ProB window after loading the above machine you will see:
			[[file:ProBSimpleCountDefSet_BeforeInit.png\|center]]
			In the "State Properties" pane you can see that the cardinality of ID was set to 3.
			There are various ways you can influence the cardinality chosen by ProB; one is by adding a DEFINITION of the form:
			<Pre>
			DEFINITIONS scope_ID == 10
			</Pre>
			If you add this definition, ProB will now find an invariant violation:
			[[file:ProBSimpleCountDefSet_InvViol.png\|center]]

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


	We assume that you have completed [[Tutorial First Model Checking]]. There we ~~have seen~~ how to find invariant violations using the model checker.		We assume that you have completed [[Tutorial First Model Checking]]. There we saw how to find invariant violations using the model checker.

	In this part we use the following B Machine:		In this part we use the following B Machine:
Line 35:		Line 35:

	Does this mean that the B machine is guaranteed to be correct? Does this mean that the AtelierB provers will be able to prove the B machine correct?		Does this mean that the B machine is guaranteed to be correct? Does this mean that the AtelierB provers will be able to prove the B machine correct?
	In this case yes, but in general we have to be very careful about interpreting a completed model check.		In this case yes, but in general, we have to be very careful about interpreting a completed model check.
	Below we examine several issues that have to be considered.		Below we examine several issues that have to be considered.

Line 44:		Line 44:
	[[file:ProBModelCheckNoCounterExampleFoundTrans.png\|center]]		[[file:ProBModelCheckNoCounterExampleFoundTrans.png\|center]]

	Again no invariant violations or deadlocks were found, but this time ProB warns us that not all transitions were computed. Indeed, the <tt>SET_PREF_MAX_OPERATIONS</tt> definition tells ProB to compute at most 5 ways to execute an operation. In this case, there are 6 ways to execute the Reset operation. As such, ProB may have missed certain states and thus may have missed an invariant violation.		Again no invariant violations or deadlocks were found, but this time ProB warns us that not all transitions were computed. Indeed, the <tt>SET_PREF_MAX_OPERATIONS</tt> definition tells ProB to compute at most 5 ways to execute an operation. In this case, there are 6 ways to execute the "Reset" operation. As such, ProB may have missed certain states and thus may have missed an invariant violation.

	Indeed, when you double click on the "INITIALISATION(1)" entry in the "EnabledOperations" pane, you will see the following:		Indeed, when you double click on the "INITIALISATION(1)" entry in the "EnabledOperations" pane, you will see the following:
Line 82:		Line 82:
	[[file:ProBSimpleCountDefSet_BeforeInit.png\|center]]		[[file:ProBSimpleCountDefSet_BeforeInit.png\|center]]
	In the "State Properties" pane you can see that the cardinality of ID was set to 3.		In the "State Properties" pane you can see that the cardinality of ID was set to 3.
	There are various ways you can influence the cardinality chosen by ProB~~; one~~ is by adding a DEFINITION of the form:		There are various ways you can influence the cardinality chosen by ProB. One is by adding a DEFINITION of the form:
	<Pre>		<Pre>
	DEFINITIONS scope_ID == 10		DEFINITIONS scope_ID == 10

← Older revision		Revision as of 13:09, 1 March 2011
Line 23:		Line 23:
	To load this machine into ProB you can select "New..." from the "File" menu, choose a file name (e.g., "SimpleCounterForMC.mch") and then paste the text above into the ProB source pane and choose "Save and Reopen" from the "File" menu.		To load this machine into ProB you can select "New..." from the "File" menu, choose a file name (e.g., "SimpleCounterForMC.mch") and then paste the text above into the ProB source pane and choose "Save and Reopen" from the "File" menu.

	Note that the DEFINITION SET_PREF_MAX_OPERATIONS==5 means that ProB will compute at most 5 possible ways to execute any given operation (i.e., Increase and Reset in this case). We return to this issue below.		Note that the <tt>DEFINITION SET_PREF_MAX_OPERATIONS==5</tt> means that ProB will compute at most 5 possible ways to execute any given operation (i.e., Increase and Reset in this case). We return to this issue below.

	== Successful Model Checking ==		== Successful Model Checking ==
Line 44:		Line 44:
	[[file:ProBModelCheckNoCounterExampleFoundTrans.png\|center]]		[[file:ProBModelCheckNoCounterExampleFoundTrans.png\|center]]

	Again no invariant violations or deadlocks were found, but this time ProB warns us that not all transitions were computed. Indeed, the SET_PREF_MAX_OPERATIONS definition tells ProB to compute at most 5 ways to execute an operation. In this case, there are 6 ways to execute the Reset operation. As such, ProB may have missed certain states and thus may have missed an invariant violation.		Again no invariant violations or deadlocks were found, but this time ProB warns us that not all transitions were computed. Indeed, the <tt>SET_PREF_MAX_OPERATIONS</tt> definition tells ProB to compute at most 5 ways to execute an operation. In this case, there are 6 ways to execute the Reset operation. As such, ProB may have missed certain states and thus may have missed an invariant violation.

	Indeed, when you double click on the "INITIALISATION(1)" entry in the "EnabledOperations" pane, you will see the following:		Indeed, when you double click on the "INITIALISATION(1)" entry in the "EnabledOperations" pane, you will see the following:
Line 56:		Line 56:
	</Pre>		</Pre>
	and repeat the model checking. We will get the exact same result as above, but this time the machine is actually incorrect.		and repeat the model checking. We will get the exact same result as above, but this time the machine is actually incorrect.
	The only way to solve ensure that ProB checks the entire state space is to increase the "MAX_OPERATIONS" preference to a suitably large value, e.g., SET_PREF_MAX_OPERATIONS==8 in this case.		The only way to solve ensure that ProB checks the entire state space is to increase the "MAX_OPERATIONS" preference to a suitably large value, e.g., <tt>SET_PREF_MAX_OPERATIONS==8</tt> in this case.
	Now model checking will find a counter example:		Now model checking will find a counter example:
	[[file:ProBSimpleCounterForMC_InvViol.png\|center]]		[[file:ProBSimpleCounterForMC_InvViol.png\|center]]
Line 102:		Line 102:
	== Infinite Types ==		== Infinite Types ==

	It could be that your B machine makes use of the mathematical integers (INTEGER) or infinite subsets thereof (NATURAL, NATURAL1). Note that some derived types (such as seq(.)) are defined in terms of INTEGER.		It could be that your B machine makes use of the mathematical integers (<tt>INTEGER</tt>) or infinite subsets thereof (<tt>NATURAL</tt>, <tt>NATURAL1</tt>). Note that some derived types (such as seq(.)) are defined in terms of INTEGER.
	In this case there could be no way to explore all states of your system.		In this case there could be no way to explore all states of your system.
	For example, the following operation		For example, the following operation
Line 108:		Line 108:
	Choose = BEGIN x :: NATURAL END		Choose = BEGIN x :: NATURAL END
	</Pre>		</Pre>
	can be executed in infinitely many ways. ProB will in this case only find values between 0 and MAXINT for x. As such, a complete model checking does not indicate that your machine's state space has been fully explored.		can be executed in infinitely many ways. ProB will in this case only find values between 0 and <tt>MAXINT</tt> for x. As such, a complete model checking does not indicate that your machine's state space has been fully explored.
	Note: ProB prints a warning on the console when an infinite type (like NATURAL) was "expanded" into a finite subset of it. This information is not yet fed back to the graphical user interface (but we are working on it).		Note: ProB prints a warning on the console when an infinite type (like <tt>NATURAL</tt>) was "expanded" into a finite subset of it. This information is not yet fed back to the graphical user interface (but we are working on it).

	== Model Checking and Proof ==		== Model Checking and Proof ==