Tutorial Model Checking, Proof and CBC - Revision history

Joy Clark: grammar and punctuation

2011-04-18T12:39:22Z

grammar and punctuation

← Older revision		Revision as of 12:39, 18 April 2011
Line 48:		Line 48:
	[[file:CBCDoubleCounter2.png\|center]]		[[file:CBCDoubleCounter2.png\|center]]

	As you can see, the Counter has the value 130, which clearly violates the invariant <tt>counter<=128</tt>. However, no value in the state space above ~~did have~~ this value for Counter. So how did we reach this error state? By pressing the left arrow in the "EnabledOperations" pane you will see the previous state that ProB has computed:		As you can see, the Counter has the value 130, which clearly violates the invariant <tt>counter<=128</tt>. However, no value in the state space above had this value for Counter. So how did we reach this error state? By pressing the left arrow in the "EnabledOperations" pane you will see the previous state that ProB has computed:

	[[file:CBCDoubleCounter1.png\|center]]		[[file:CBCDoubleCounter1.png\|center]]

	Now, while this state does not appear in the state space above either. However, this time this state does satisfy the invariant. Thus, if we <em>ignore</em> the ~~initialisation~~ and just look at the INVARIANT <tt>counter:NATURAL & counter<=128</tt> as describing all possible states, then the machine is indeed erroneous: the operation <em>Double</em> lead us outside of the safe states.		Now, while this state does not appear in the state space above either. However, this time this state does satisfy the invariant. Thus, if we <em>ignore</em> the initialization and just look at the INVARIANT <tt>counter:NATURAL & counter<=128</tt> as describing all possible states, then the machine is indeed erroneous: the operation <em>Double</em> lead us outside of the safe states.
	The operation <em>Halve</em> on the other hand is correct: for every possible state satisfying the INVARIANT the resulting successor state will also satisfy the INVARIANT.		The operation <em>Halve</em> on the other hand is correct: for every possible state satisfying the INVARIANT the resulting successor state will also satisfy the INVARIANT.

Line 69:		Line 69:
	More generally, the proof obligation in classical B for an operation with precondition P and body S is:		More generally, the proof obligation in classical B for an operation with precondition P and body S is:
	I & P => [S] I		I & P => [S] I
	In other words, for <b>any</b> state which satisfies the invariant I and the precondition P, the operation must preserve the invariant; not just for the states reachable from the ~~initialisation~~. In particular, the operation must preserve the invariant for the state with counter=65, which it does not.		In other words, for <b>any</b> state which satisfies the invariant I and the precondition P, the operation must preserve the invariant; not just for the states reachable from the initialization. In particular, the operation must preserve the invariant for the state with counter=65, which it does not.

Michael Leuschel: /* How to correct problems found */

2011-03-02T13:58:50Z

How to correct problems found

← Older revision		Revision as of 13:58, 2 March 2011
Line 77:		Line 77:

	{\| border="1"		{\| border="1"
	\|+ align="bottom" style="color:#e76700;" \|''~~Number of distinct solutions~~''		\|+ align="bottom" style="color:#e76700;" \|''Solving Invariant Violation Problems''
	! Potential		! Potential Solution
	! CBC		! CBC
	! Model Check		! Model Check
	\|-
	~~\| Solution~~
	~~\| Invariant Violation~~
	~~\| Invariant Violation~~
	\|-		\|-
	\| Strengthen Invariant		\| Strengthen Invariant

Michael Leuschel at 13:55, 2 March 2011

2011-03-02T13:55:40Z

← Older revision		Revision as of 13:55, 2 March 2011
Line 70:		Line 70:
	I & P => [S] I		I & P => [S] I
	In other words, for <b>any</b> state which satisfies the invariant I and the precondition P, the operation must preserve the invariant; not just for the states reachable from the initialisation. In particular, the operation must preserve the invariant for the state with counter=65, which it does not.		In other words, for <b>any</b> state which satisfies the invariant I and the precondition P, the operation must preserve the invariant; not just for the states reachable from the initialisation. In particular, the operation must preserve the invariant for the state with counter=65, which it does not.


			== How to correct problems found ==

			Below is a small guide on how to correct invariant violations found by constraint-based checking and model checking.

			{\| border="1"
			\|+ align="bottom" style="color:#e76700;" \|''Number of distinct solutions''
			! Potential
			! CBC
			! Model Check
			\|-
			\| Solution
			\| Invariant Violation
			\| Invariant Violation
			\|-
			\| Strengthen Invariant
			\| if start state wrong
			\| NA
			\|-
			\| Weaken Invariant
			\| if destination state ok
			\| If destination state ok
			\|-
			\| Guard Strengthening
			\| if transition should not be allowed
			\| if path not legal
			\|-
			\| Guard Weakening
			\| NA
			\| NA
			\|-
			\| Adapt Substitution
			\| if destination state wrong
			\| if destination (or intermediate) state wrong
			\|}

Michael Leuschel: /* Constraint Based Checking (CBC) for the Invariant */

2011-03-01T16:00:05Z

Constraint Based Checking (CBC) for the Invariant

← Older revision		Revision as of 16:00, 1 March 2011
Line 66:		Line 66:
	[[file:ClicknProveDoubleCounter.png\|center\|\|300px]]		[[file:ClicknProveDoubleCounter.png\|center\|\|300px]]

	Indeed, we have to prove that 2*counter is less or equal to 128, given that counter is less or equal to 99 and less or equal to 128. This is not possible.		Indeed, we have to prove that 2*counter is less or equal to 128, given that counter is less or equal to 99 and less or equal to 128. This is not possible; above ProB has found counter=65 as a counterexample.
	More generally, the proof obligation in classical B for an operation with precondition P and body S is:		More generally, the proof obligation in classical B for an operation with precondition P and body S is:
	I & P => [S] I		I & P => [S] I
	In other words, for <b>any</b> state which satisfies the invariant I and the precondition P, the operation must preserve the invariant; not just for the states reachable from the initialisation. In particular, the operation must preserve the invariant for the state with counter=65, which it does not.		In other words, for <b>any</b> state which satisfies the invariant I and the precondition P, the operation must preserve the invariant; not just for the states reachable from the initialisation. In particular, the operation must preserve the invariant for the state with counter=65, which it does not.

Michael Leuschel: /* Constraint Based Checking (CBC) for the Invariant */

2011-03-01T15:59:13Z

Constraint Based Checking (CBC) for the Invariant

← Older revision		Revision as of 15:59, 1 March 2011
Line 66:		Line 66:
	[[file:ClicknProveDoubleCounter.png\|center\|\|300px]]		[[file:ClicknProveDoubleCounter.png\|center\|\|300px]]

	Indeed, the proof obligation in classical B for an operation with precondition P and body S is:		Indeed, we have to prove that 2*counter is less or equal to 128, given that counter is less or equal to 99 and less or equal to 128. This is not possible.
			More generally, the proof obligation in classical B for an operation with precondition P and body S is:
	I & P => [S] I		I & P => [S] I
	In other words, for <b>any</b> state which satisfies the invariant I and the precondition P, the operation must preserve the invariant; not just for the states reachable from the initialisation. In particular, the operation must preserve the invariant for the state with counter=65, which it does not.		In other words, for <b>any</b> state which satisfies the invariant I and the precondition P, the operation must preserve the invariant; not just for the states reachable from the initialisation. In particular, the operation must preserve the invariant for the state with counter=65, which it does not.

Michael Leuschel at 13:24, 1 March 2011

2011-03-01T13:24:32Z

← Older revision		Revision as of 13:24, 1 March 2011
Line 16:		Line 16:

	Now click the "Model Check" button. After a short while, ProB will give you the following message:		Now click the "Model Check" button. After a short while, ProB will give you the following message:
	[[file:ProBModelCheckNoCounterExampleFound.png\|center]]		[[file:ProBModelCheckNoCounterExampleFound.png\|center\|\|350px]]

	Is this model correct? As you will see, this depends on your point of view.		Is this model correct? As you will see, this depends on your point of view.
Line 64:		Line 64:
	If one tries to use for example Click'n Prove to prove this machine, there is one proof obligation for the Double operation which cannot be discharged:		If one tries to use for example Click'n Prove to prove this machine, there is one proof obligation for the Double operation which cannot be discharged:

	[[file:ClicknProveDoubleCounter.png\|center]]		[[file:ClicknProveDoubleCounter.png\|center\|\|300px]]

	Indeed, the proof obligation in classical B for an operation with precondition P and body S is:		Indeed, the proof obligation in classical B for an operation with precondition P and body S is:
	I & P => [S] I		I & P => [S] I
	In other words, for <b>any</b> state which satisfies the invariant I and the precondition P, the operation must preserve the invariant; not just for the states reachable from the initialisation. In particular, the operation must preserve the invariant for the state with counter=65, which it does not.		In other words, for <b>any</b> state which satisfies the invariant I and the precondition P, the operation must preserve the invariant; not just for the states reachable from the initialisation. In particular, the operation must preserve the invariant for the state with counter=65, which it does not.

Michael Leuschel at 13:22, 1 March 2011

2011-03-01T13:22:56Z

← Older revision		Revision as of 13:22, 1 March 2011
Line 60:		Line 60:
	[[file:DoubleCounterStatespace2.png\|center\|\|300px]]		[[file:DoubleCounterStatespace2.png\|center\|\|300px]]

	As you can see the constraint-based checker has transported us into the state with counter=65, which is not reachable from the initial state of the system. However, as we have said, it does satisfy the invariant and as such the machine cannot be proven using the B provers. Indeed, the proof obligation in classical B for an operation with precondition P and body S is:		As you can see the constraint-based checker has transported us into the state with counter=65, which is not reachable from the initial state of the system. However, as we have said, it does satisfy the invariant and as such the machine cannot be proven using the B provers.

			If one tries to use for example Click'n Prove to prove this machine, there is one proof obligation for the Double operation which cannot be discharged:

			[[file:ClicknProveDoubleCounter.png\|center]]

			Indeed, the proof obligation in classical B for an operation with precondition P and body S is:
	I & P => [S] I		I & P => [S] I
	In other words, for <b>any</b> state which satisfies the invariant I and the precondition P, the operation must preserve the invariant; not just for the states reachable from the initialisation. In particular, the operation must preserve the invariant for the state with counter=65, which it does not.		In other words, for <b>any</b> state which satisfies the invariant I and the precondition P, the operation must preserve the invariant; not just for the states reachable from the initialisation. In particular, the operation must preserve the invariant for the state with counter=65, which it does not.

Michael Leuschel at 13:07, 1 March 2011

2011-03-01T13:07:41Z

← Older revision		Revision as of 13:07, 1 March 2011
Line 60:		Line 60:
	[[file:DoubleCounterStatespace2.png\|center\|\|300px]]		[[file:DoubleCounterStatespace2.png\|center\|\|300px]]

	As you can see the constraint-based checker has transported us into the state with ~~Counter~~=65, which is not reachable from the initial state of the system. However, as we have said, it does satisfy the invariant and as such the machine cannot be proven using the B provers. Indeed, the proof obligation in classical B for an operation with precondition P and body S is:		As you can see the constraint-based checker has transported us into the state with counter=65, which is not reachable from the initial state of the system. However, as we have said, it does satisfy the invariant and as such the machine cannot be proven using the B provers. Indeed, the proof obligation in classical B for an operation with precondition P and body S is:
	I & P => [S] I		I & P => [S] I
	In other words, for <b>any</b> state which satisfies the invariant I and the precondition P, the operation must preserve the invariant; not just for the states reachable from the initialisation.		In other words, for <b>any</b> state which satisfies the invariant I and the precondition P, the operation must preserve the invariant; not just for the states reachable from the initialisation. In particular, the operation must preserve the invariant for the state with counter=65, which it does not.

Michael Leuschel at 13:05, 1 March 2011

2011-03-01T13:05:36Z

← Older revision		Revision as of 13:05, 1 March 2011
Line 24:		Line 24:
	If you look purely at the state space of the machine (choose the View State Space command in the Animate menu) you get the following picture:		If you look purely at the state space of the machine (choose the View State Space command in the Animate menu) you get the following picture:

			[[file:DoubleCounterStatespace.png\|center\|\|300px]]

	Indeed, all reachable states are correct, in the sense that the invariant <tt>counter:NATURAL & counter<=128</tt> holds for all of those states.		Indeed, all reachable states are correct, in the sense that the invariant <tt>counter:NATURAL & counter<=128</tt> holds for all of those states.
	~~[[file:DoubleCounterStatespace.png\|center\|\|300px]]~~


Line 54:		Line 54:
	Now, while this state does not appear in the state space above either. However, this time this state does satisfy the invariant. Thus, if we <em>ignore</em> the initialisation and just look at the INVARIANT <tt>counter:NATURAL & counter<=128</tt> as describing all possible states, then the machine is indeed erroneous: the operation <em>Double</em> lead us outside of the safe states.		Now, while this state does not appear in the state space above either. However, this time this state does satisfy the invariant. Thus, if we <em>ignore</em> the initialisation and just look at the INVARIANT <tt>counter:NATURAL & counter<=128</tt> as describing all possible states, then the machine is indeed erroneous: the operation <em>Double</em> lead us outside of the safe states.
	The operation <em>Halve</em> on the other hand is correct: for every possible state satisfying the INVARIANT the resulting successor state will also satisfy the INVARIANT.		The operation <em>Halve</em> on the other hand is correct: for every possible state satisfying the INVARIANT the resulting successor state will also satisfy the INVARIANT.


			If you look purely at the state space of the machine (choose the View State Space command in the Animate menu) you get the following picture:

			[[file:DoubleCounterStatespace2.png\|center\|\|300px]]

			As you can see the constraint-based checker has transported us into the state with Counter=65, which is not reachable from the initial state of the system. However, as we have said, it does satisfy the invariant and as such the machine cannot be proven using the B provers. Indeed, the proof obligation in classical B for an operation with precondition P and body S is:
			I & P => [S] I
			In other words, for <b>any</b> state which satisfies the invariant I and the precondition P, the operation must preserve the invariant; not just for the states reachable from the initialisation.

Michael Leuschel: /* Constraint Based Checking (CBC) for the Invariant */

2011-03-01T12:59:15Z

Constraint Based Checking (CBC) for the Invariant

← Older revision		Revision as of 12:59, 1 March 2011
Line 35:		Line 35:
	In addition to model checking, ProB also offers constraint-based checking (CBC), which is particularly useful when used in conjunction with proof. This will give us the clue as to why the above machine cannot be proven correct, and why it can also be viewed as incorrect.		In addition to model checking, ProB also offers constraint-based checking (CBC), which is particularly useful when used in conjunction with proof. This will give us the clue as to why the above machine cannot be proven correct, and why it can also be viewed as incorrect.

	Before proceeding, please ensure that you have either set the CLPFD preference to TRUE or have set the MAXINT preference to at least 130. This can be set by going to the "Animation Preferences" command in the Preferences menu or by adding for example the following to your file:		Before proceeding, please ensure that you have either set the CLPFD preference to TRUE or have set the MAXINT preference to at least 130. This can be set by going to the "Animation Preferences" command in the Preferences menu or by adding for example the following to your file and then reloading it:
	<Pre>		<Pre>
	DEFINITIONS SET_PREF_CLPFD == TRUE		DEFINITIONS SET_PREF_CLPFD == TRUE