Proof Obligation Commands - Revision history

imported>Nicolas at 10:43, 18 March 2010

2010-03-18T10:43:43Z

← Older revision		Revision as of 10:43, 18 March 2010
Line 4:		Line 4:

	These commands are run on all POs located under the node(s) selected in the explorer. The selection can be a whole project, a model (context/machine), the 'Proof Obligations' node (equivalent to selecting the corresponding model), an element type (Axioms/Invariants/Events), a particular element (axm12, inv314, …), a particular PO (INITIALISATION/inv2/INV, …), or any combination of selectable nodes (multiselection using the CTRL key).		These commands are run on all POs located under the node(s) selected in the explorer. The selection can be a whole project, a model (context/machine), the 'Proof Obligations' node (equivalent to selecting the corresponding model), an element type (Axioms/Invariants/Events), a particular element (axm12, inv314, …), a particular PO (INITIALISATION/inv2/INV, …), or any combination of selectable nodes (multiselection using the CTRL key).

			For Rodin up to version 1.2 included, PO commands apply to all selected POs. From Rodin version 1.3 on, they apply on a subset of selected POs. After-specified behaviour concerns versions 1.3 and more.

	== Retry Auto Provers ==		== Retry Auto Provers ==

	Applies to undischarged POs under selection only.		Applies to undischarged POs under selection only.

	As the name suggests, this command runs the Auto Provers on selected POs. When the 'Prove Automatically' option is turned off, it's a convenient way to manually trigger auto proving on the desired (set of) PO(s).		As the name suggests, this command runs the Auto Provers on selected POs. When the 'Prove Automatically' option is turned off, it's a convenient way to manually trigger auto proving on the desired (set of) PO(s).

Line 13:		Line 16:

	== Recalculate Auto Status ==		== Recalculate Auto Status ==

			Applies to all POs under selection (both discharged and undischarged).

	This command is related to the "auto" or "manual" PO status. This status is visible in the explorer on each PO: it is marked with a 'A' at the upper right corner of the PO icon if it was entirely discharged using the auto prover, else there is no mark, meaning that the user had to edit the proof by hand (even partially).		This command is related to the "auto" or "manual" PO status. This status is visible in the explorer on each PO: it is marked with a 'A' at the upper right corner of the PO icon if it was entirely discharged using the auto prover, else there is no mark, meaning that the user had to edit the proof by hand (even partially).
Line 21:		Line 26:

	== Proof Replay on Undischarged POs ==		== Proof Replay on Undischarged POs ==

			Applies to undischarged POs under selection only.

	It often happens during a model development that, after a given PO has been manually discharged, one makes small changes to the model in such a way that the PO is only slightly altered and would be discharged again if the proof were replayed. However, the platform does not try to replay POs on its own initiative, as this is a potentially long-running operation.		It often happens during a model development that, after a given PO has been manually discharged, one makes small changes to the model in such a way that the PO is only slightly altered and would be discharged again if the proof were replayed. However, the platform does not try to replay POs on its own initiative, as this is a potentially long-running operation.

imported>Nicolas: /* Retry Auto Provers */

2010-03-18T10:34:52Z

Retry Auto Provers

← Older revision		Revision as of 10:34, 18 March 2010
Line 7:		Line 7:
	== Retry Auto Provers ==		== Retry Auto Provers ==

			Applies to undischarged POs under selection only.
	As the name suggests, this command runs the Auto Provers on selected POs. When the 'Prove Automatically' option is turned off, it's a convenient way to manually trigger auto proving on the desired (set of) PO(s).		As the name suggests, this command runs the Auto Provers on selected POs. When the 'Prove Automatically' option is turned off, it's a convenient way to manually trigger auto proving on the desired (set of) PO(s).

imported>Nicolas: /* Proof Replay on Undischarged POs */

2010-03-04T17:50:43Z

Proof Replay on Undischarged POs

← Older revision		Revision as of 17:50, 4 March 2010
Line 21:		Line 21:
	== Proof Replay on Undischarged POs ==		== Proof Replay on Undischarged POs ==

	~~{{TODO}}~~		It often happens during a model development that, after a given PO has been manually discharged, one makes small changes to the model in such a way that the PO is only slightly altered and would be discharged again if the proof were replayed. However, the platform does not try to replay POs on its own initiative, as this is a potentially long-running operation.

			This command provides a convenient way to manually try to replay a selected (set of) undischarged PO(s).



			[[Category:User documentation]]
			[[Category:Proof]]












	~~{{TODO\|~~Category}}

imported>Nicolas: /* Recalculate Auto Status */

2010-03-04T17:19:31Z

Recalculate Auto Status

← Older revision		Revision as of 17:19, 4 March 2010
Line 13:		Line 13:
	== Recalculate Auto Status ==		== Recalculate Auto Status ==

	~~{{TODO}}~~		This command is related to the "auto" or "manual" PO status. This status is visible in the explorer on each PO: it is marked with a 'A' at the upper right corner of the PO icon if it was entirely discharged using the auto prover, else there is no mark, meaning that the user had to edit the proof by hand (even partially).

			Launching 'Recalculate Auto Status' reruns the current auto prover on selected POs. The main aim of this command is to update the "auto"/"manual" status to reflect the current auto prover configuration. In case a proof was previously automatically discharged and is no more, it will be marked as manually created.

			This is intended to be used as a post-development operation to estimate the percentage of automated proofs over a changing auto prover. It is recommended to restore to the default auto provers before running this command.

	== Proof Replay on Undischarged POs ==		== Proof Replay on Undischarged POs ==

imported>Nicolas: /* Retry Auto Provers */

2010-03-04T16:56:31Z

Retry Auto Provers

← Older revision		Revision as of 16:56, 4 March 2010
Line 7:		Line 7:
	== Retry Auto Provers ==		== Retry Auto Provers ==

	~~{{TODO}}~~		As the name suggests, this command runs the Auto Provers on selected POs. When the 'Prove Automatically' option is turned off, it's a convenient way to manually trigger auto proving on the desired (set of) PO(s).

			It may also be used after changing the Auto Prover preferences, in order to check whether the new prover configuration allows to discharge a given (set of) PO(s).

	== Recalculate Auto Status ==		== Recalculate Auto Status ==

imported>Nicolas: New page: In this page are presented various proof obligations commands that can be run from the Event-B Explorer as follows: Image:PO_Commands.png These commands are run on all POs located un...

2010-03-04T16:42:12Z

New page: In this page are presented various proof obligations commands that can be run from the Event-B Explorer as follows: Image:PO_Commands.png These commands are run on all POs located un...

New page

In this page are presented various proof obligations commands that can be run from the Event-B Explorer as follows:

[[Image:PO_Commands.png]]

These commands are run on all POs located under the node(s) selected in the explorer. The selection can be a whole project, a model (context/machine), the 'Proof Obligations' node (equivalent to selecting the corresponding model), an element type (Axioms/Invariants/Events), a particular element (axm12, inv314, …), a particular PO (INITIALISATION/inv2/INV, …), or any combination of selectable nodes (multiselection using the CTRL key).

== Retry Auto Provers ==

{{TODO}}

== Recalculate Auto Status ==

{{TODO}}

== Proof Replay on Undischarged POs ==

{{TODO}}

{{TODO|Category}}