Rodin POs and ProB - Revision history

Jan Gruteser at 12:35, 23 January 2026

2026-01-23T12:35:21Z

← Older revision		Revision as of 12:35, 23 January 2026
Line 38:		Line 38:
	Number of unproven (by ProB) POs: 0 ([])		Number of unproven (by ProB) POs: 0 ([])
	</pre>		</pre>


	== ProB Model Checker ==		== ProB Model Checker ==
Line 56:		Line 55:

	[[File:prob_show_specialized_invariants_result.png]]		[[File:prob_show_specialized_invariants_result.png]]

			== ProB Sequent Prover ==

			Since ProB 1.15.1, ProB includes a [[Sequent_Prover\|Sequent Prover]] based on the inference and rewrite rules implemented in Rodin.

Michael Leuschel: /* ProB Model Checker */

2020-03-05T12:44:31Z

ProB Model Checker

← Older revision		Revision as of 12:44, 5 March 2020
Line 48:		Line 48:
	the invariant checking for Event-B models.		the invariant checking for Event-B models.

	The information about discharged proof obligations is automatically obtained by ProB from Rodin. It is also saved in the [[Tutorial_Rodin_Exporting\|eventb export files]].		The information about discharged proof obligations is automatically obtained by ProB from Rodin. It is also saved in the [[Tutorial_Rodin_Exporting\|.eventb export files]].

	In ProB Tcl/Tk (aka ProB Classic) you can inspect the so obtained specialized (simplified) invariants for each operation, by choosing one of the commands in the Debug menu:		In ProB Tcl/Tk (aka ProB Classic) you can inspect the so obtained specialized (simplified) invariants for each operation, by choosing one of the commands in the Debug menu:

Michael Leuschel: /* ProB Model Checker */

2020-03-05T12:44:15Z

ProB Model Checker

← Older revision		Revision as of 12:44, 5 March 2020
Line 48:		Line 48:
	the invariant checking for Event-B models.		the invariant checking for Event-B models.

	The information about discharged proof obligations is automatically obtained by ProB from Rodin. It is also saved in the [[~~https://www3.hhu.de/stups/prob/index.php/~~Tutorial_Rodin_Exporting .eventb export files]].		The information about discharged proof obligations is automatically obtained by ProB from Rodin. It is also saved in the [[Tutorial_Rodin_Exporting\|eventb export files]].

	In ProB Tcl/Tk (aka ProB Classic) you can inspect the so obtained specialized (simplified) invariants for each operation, by choosing one of the commands in the Debug menu:		In ProB Tcl/Tk (aka ProB Classic) you can inspect the so obtained specialized (simplified) invariants for each operation, by choosing one of the commands in the Debug menu:

Michael Leuschel: /* ProB Model Checker */

2020-03-05T12:43:42Z

ProB Model Checker

← Older revision		Revision as of 12:43, 5 March 2020
Line 48:		Line 48:
	the invariant checking for Event-B models.		the invariant checking for Event-B models.

	In ProB Tcl/Tk you can inspect the so obtained specialized (simplified) invariants for each operation, by choosing one of the commands in the Debug menu:		The information about discharged proof obligations is automatically obtained by ProB from Rodin. It is also saved in the [[https://www3.hhu.de/stups/prob/index.php/Tutorial_Rodin_Exporting .eventb export files]].

			In ProB Tcl/Tk (aka ProB Classic) you can inspect the so obtained specialized (simplified) invariants for each operation, by choosing one of the commands in the Debug menu:

	[[File:prob_show_specialized_invariants_menu.png]]		[[File:prob_show_specialized_invariants_menu.png]]

Michael Leuschel: /* ProB Model Checker */

2020-03-05T12:39:55Z

ProB Model Checker

← Older revision		Revision as of 12:39, 5 March 2020
Line 48:		Line 48:
	the invariant checking for Event-B models.		the invariant checking for Event-B models.

	In ProB Tcl/Tk you can inspect the so obtained specialized (simplified) invariants for each operation:		In ProB Tcl/Tk you can inspect the so obtained specialized (simplified) invariants for each operation, by choosing one of the commands in the Debug menu:

	[[File:prob_show_specialized_invariants_menu.png]]		[[File:prob_show_specialized_invariants_menu.png]]

Michael Leuschel at 12:38, 5 March 2020

2020-03-05T12:38:46Z

← Older revision		Revision as of 12:38, 5 March 2020
Line 38:		Line 38:
	Number of unproven (by ProB) POs: 0 ([])		Number of unproven (by ProB) POs: 0 ([])
	</pre>		</pre>


			== ProB Model Checker ==

			During animation and model checking, ProB will compute its own
			verification conditions for invariants, theorems, etc.
			However, if the PROOF_INFO preference is set to true (which it is by default)
			it will make use of the information about which POs are discharged to simplify
			the invariant checking for Event-B models.

			In ProB Tcl/Tk you can inspect the so obtained specialized (simplified) invariants for each operation:

			[[File:prob_show_specialized_invariants_menu.png]]


			[[File:prob_show_specialized_invariants_result.png]]

Michael Leuschel at 11:29, 5 March 2020

2020-03-05T11:29:57Z

← Older revision		Revision as of 11:29, 5 March 2020
Line 6:		Line 6:
	However, if the PROOF_INFO preference is set to true (which it is by default)		However, if the PROOF_INFO preference is set to true (which it is by default)
	it will make use of the information about which POs are discharged to simplify		it will make use of the information about which POs are discharged to simplify
	the invariant checking.		the invariant checking for Event-B models.

	== ProB Prover Disprover ==		== ProB Prover Disprover ==

Michael Leuschel at 10:30, 5 March 2020

2020-03-05T10:30:15Z

← Older revision		Revision as of 10:30, 5 March 2020
Line 1:		Line 1:

	What is the relationship between Rodin proof obligations (POs) and ProB.		What is the relationship between Rodin proof obligations (POs) and ProB.
			In short, ProB can be made to check individual proof obligations.
			During animation and model checking, ProB will compute its own
			verification conditions for invariants, theorems, etc.
			However, if the PROOF_INFO preference is set to true (which it is by default)
			it will make use of the information about which POs are discharged to simplify
			the invariant checking.

	== ProB Prover Disprover ==		== ProB Prover Disprover ==

Michael Leuschel at 10:27, 5 March 2020

2020-03-05T10:27:06Z

← Older revision		Revision as of 10:27, 5 March 2020
Line 17:		Line 17:

	This will generate a Prolog file (with .pl ending) which can be read by probcli. It will then check the individual proof obligations.		This will generate a Prolog file (with .pl ending) which can be read by probcli. It will then check the individual proof obligations.
			Here is an example run:

			<pre>
			probcli GearDoor1_mch.pl
			...
			Disprover Run Summary: [true-9]
			Project LandingGearNew
			Machine GearDoor1 (exported Sun Feb 08 10:38:51 CET 2015)
			Number of POs: 9 ([INITIALISATION/safety_inv1/INV,env_start_retracting/safety_inv1/INV,env_retract_gear/safety_inv1/INV,env_start_extending/safety_inv1/INV,env_extend_gear/safety_inv1/INV,env_start_open_door/safety_inv1/INV,env_open_door/safety_inv1/INV,env_start_close_door/safety_inv1/INV,env_close_door/safety_inv1/INV])
			Number of proven (within Rodin) POs: 9 ([INITIALISATION/safety_inv1/INV,env_start_retracting/safety_inv1/INV,env_retract_gear/safety_inv1/INV,env_start_extending/safety_inv1/INV,env_extend_gear/safety_inv1/INV,env_start_open_door/safety_inv1/INV,env_open_door/safety_inv1/INV,env_start_close_door/safety_inv1/INV,env_close_door/safety_inv1/INV])
			ProB Disprover Analysis with timeout 300 ms
			Number of proven (by ProB) POs: 9 ([INITIALISATION/safety_inv1/INV,env_start_retracting/safety_inv1/INV,env_retract_gear/safety_inv1/INV,env_start_extending/safety_inv1/INV,env_extend_gear/safety_inv1/INV,env_start_open_door/safety_inv1/INV,env_open_door/safety_inv1/INV,env_start_close_door/safety_inv1/INV,env_close_door/safety_inv1/INV])
			Number of disproven (by ProB) POs: 0 ([])
			Number of unproven (by ProB) POs: 0 ([])
			</pre>

Michael Leuschel at 10:23, 5 March 2020

2020-03-05T10:23:49Z

← Older revision		Revision as of 10:23, 5 March 2020
Line 11:		Line 11:


	One can also export the POs of a particular Event-B machine for use with the command-line version of ProB.		One can also export the POs of a particular Event-B machine for use with the [[Using_the_Command-Line_Version_of_ProB\|command-line version of ProB]].


			[[File:rodin_export_pos.png]]

	This will generate a Prolog file (with .pl ending) which can be read by probcli. It will then check the individual proof obligations.		This will generate a Prolog file (with .pl ending) which can be read by probcli. It will then check the individual proof obligations.