Tutorial Disprover - Revision history

Michael Leuschel: /* Disprover Export Example */

2022-12-19T11:56:35Z

Disprover Export Example

← Older revision		Revision as of 11:56, 19 December 2022
Line 51:		Line 51:


	=== Disprover Export Example ===		== Disprover Export Example ==

	Camille version of context:		Camille version of context:

Michael Leuschel: /* Example */

2022-03-04T11:01:06Z

Example

← Older revision		Revision as of 11:01, 4 March 2022
Line 51:		Line 51:


	=== Example ===		=== Disprover Export Example ===

	Camille version of context:		Camille version of context:
Line 79:		Line 79:
	<pre>		<pre>
	MACHINE ProofObligation_SelectedHyps		MACHINE ProofObligation_SelectedHyps
	/* Exported: 4/3/2022 10:16 */		/* Exported: 4/3/2022 11:59 */
	/* Origin: context : package(event_b_project) */		/* Origin: context : package(event_b_project) */

Line 88:		Line 88:
	&		&
	n : INTEGER		n : INTEGER
			&
			f : 1 .. n --> BOOL
	&		&
	n = 10		n = 10
	&
	~~f : 1 .. 10 --> BOOL~~

	ASSERTIONS /* Proof Goal: */		ASSERTIONS /* Proof Goal: */
Line 97:		Line 97:
	OPERATIONS		OPERATIONS
	CheckRemainingHypotheses = SELECT		CheckRemainingHypotheses = SELECT
	~~not(~~
	~~f(1) = f(n)~~
	)
	&
	f : INTEGER +-> BOOL		f : INTEGER +-> BOOL
	&
	~~f : 1 .. n --> BOOL~~
	&		&
	n : dom(f)		n : dom(f)

Michael Leuschel: /* Example */

2022-03-04T09:32:33Z

Example

← Older revision		Revision as of 09:32, 4 March 2022
Line 67:		Line 67:


	~~If we~~ just select axm0 and axm1 in the hypothesis ~~this~~ will be the ~~generated~~ B machine.		Let us just select axm0 and axm1 in the hypothesis and run the disprover.
			This will result in generating the B machine below.

Michael Leuschel: /* Example */

2022-03-04T09:31:29Z

Example

← Older revision		Revision as of 09:31, 4 March 2022
Line 64:		Line 64:
	end		end
	</pre>		</pre>



	If we just select axm0 and axm1 in the hypothesis this will be the generated B machine.		If we just select axm0 and axm1 in the hypothesis this will be the generated B machine.


			[[File:DisproverExportExample.png]]

	As you can see the selected hypotheses are put into the PROPERTIES and the proof		As you can see the selected hypotheses are put into the PROPERTIES and the proof
	goal into the ASSERTIONS.		goal into the ASSERTIONS.

Michael Leuschel at 09:29, 4 March 2022

2022-03-04T09:29:56Z

← Older revision		Revision as of 09:29, 4 March 2022
Line 45:		Line 45:
	The last preference allows you to export the PO to a classical B machine at a standard location (/tmp/ProB_Rodin_PO_SelectedHyps.mch).		The last preference allows you to export the PO to a classical B machine at a standard location (/tmp/ProB_Rodin_PO_SelectedHyps.mch).
	This file can be loaded with ProB Tcl/Tk or ProB2-UI.		This file can be loaded with ProB Tcl/Tk or ProB2-UI.
	To find counter examples you should run a constraint-based assertion check.		To find counter examples you should run a constraint-based static assertion check.
	If successful, you can inspect the counter example in the state view.		If successful, you can inspect the counter example in the state view.
	You can also inspect which of the non-selected hypotheses are false for this counter example.		You can also inspect which of the non-selected hypotheses are false for this counter example.
Line 111:		Line 111:
	</pre>		</pre>

			You can load this machine for example in ProB2-UI and then run the symbolic constraint-based static assertion check:

	[[File:CBCStaticAssertionCheck.png]]		[[File:CBCStaticAssertionCheck.png]]

			In this case it finds a counter example, which can be inspected in the state view:

	[[File:DisproverProB2UIStateView1.png]]		[[File:DisproverProB2UIStateView1.png]]

			After initialising the machine you can also inspect the guards of the generated operation in the state view:
			[[File:DisproverProB2UIStateView2.png]]

	~~[[File:DisproverProB2UIStateView2~~.~~png]]~~		As you can see there is axm2 which is false for this counter example.
			Adding this to the selected hypotheses will make the goal provable.

Michael Leuschel at 09:25, 4 March 2022

2022-03-04T09:25:58Z

← Older revision		Revision as of 09:25, 4 March 2022
Line 110:		Line 110:
	END		END
	</pre>		</pre>


			[[File:CBCStaticAssertionCheck.png]]

			[[File:DisproverProB2UIStateView1.png]]


			[[File:DisproverProB2UIStateView2.png]]

Michael Leuschel: /* Preferences */

2022-03-04T09:21:19Z

Preferences

← Older revision		Revision as of 09:21, 4 March 2022
Line 49:		Line 49:
	You can also inspect which of the non-selected hypotheses are false for this counter example.		You can also inspect which of the non-selected hypotheses are false for this counter example.
	These hypotheses are good candidates for inclusion in the selected hypotheses.		These hypotheses are good candidates for inclusion in the selected hypotheses.


			=== Example ===

			Camille version of context:
			<pre>
			context ProBDisproverTest
			constants f n
			axioms
			@axm0 n=10
			@axm1 f∈1‥n → BOOL
			@axm2 f(1) ≠ f(n)
			theorem @thm1 ran(f)=BOOL
			end
			</pre>

			If we just select axm0 and axm1 in the hypothesis this will be the generated B machine.
			As you can see the selected hypotheses are put into the PROPERTIES and the proof
			goal into the ASSERTIONS.
			The Disprover also generates the OPERATION CheckRemainingHypotheses which checks the remaining unselected hypotheses.

			<pre>
			MACHINE ProofObligation_SelectedHyps
			/* Exported: 4/3/2022 10:16 */
			/* Origin: context : package(event_b_project) */

			CONSTANTS
			f, n
			PROPERTIES /* Selected Hypotheses: */
			f : POW(INTEGER * BOOL)
			&
			n : INTEGER
			&
			n = 10
			&
			f : 1 .. 10 --> BOOL

			ASSERTIONS /* Proof Goal: */
			ran(f) = BOOL
			OPERATIONS
			CheckRemainingHypotheses = SELECT
			not(
			f(1) = f(n)
			)
			&
			f : INTEGER +-> BOOL
			&
			f : 1 .. n --> BOOL
			&
			n : dom(f)
			&
			1 : dom(f)
			&
			f(1) /= f(n)
			THEN skip
			END /* CheckRemainingHypotheses */
			DEFINITIONS
			SET_PREF_DISPROVER_MODE == TRUE;
			SET_PREF_TRY_FIND_ABORT == FALSE
			END
			</pre>

Michael Leuschel: /* Preferences */

2022-03-04T09:04:12Z

Preferences

← Older revision		Revision as of 09:04, 4 March 2022
Line 43:		Line 43:

	If you wish you can increase the time out in milliseconds using the first preference.		If you wish you can increase the time out in milliseconds using the first preference.
	The last preference allows you to export the PO to a classical B machine.		The last preference allows you to export the PO to a classical B machine at a standard location (/tmp/ProB_Rodin_PO_SelectedHyps.mch).
			This file can be loaded with ProB Tcl/Tk or ProB2-UI.
			To find counter examples you should run a constraint-based assertion check.
			If successful, you can inspect the counter example in the state view.
			You can also inspect which of the non-selected hypotheses are false for this counter example.
			These hypotheses are good candidates for inclusion in the selected hypotheses.

Michael Leuschel: /* Preferences */

2022-03-04T08:44:24Z

Preferences

← Older revision		Revision as of 08:44, 4 March 2022
Line 41:		Line 41:

	[[File:DisproverPrefs.png]]		[[File:DisproverPrefs.png]]

			If you wish you can increase the time out in milliseconds using the first preference.
			The last preference allows you to export the PO to a classical B machine.

Michael Leuschel at 08:42, 4 March 2022

2022-03-04T08:42:02Z

← Older revision		Revision as of 08:42, 4 March 2022
Line 35:		Line 35:

	Unfortunately, sometimes neither a counter example nor a proof can be found.		Unfortunately, sometimes neither a counter example nor a proof can be found.

			== Preferences ==

			The disprover has a variety of preferences, shown below:

			[[File:DisproverPrefs.png]]