Proof Obligation Commands: Difference between revisions
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... |
imported>Nicolas |
||
| Line 7: | Line 7: | ||
== Retry Auto Provers == | == Retry Auto Provers == | ||
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 == | ||
Revision as of 16:56, 4 March 2010
In this page are presented various proof obligations commands that can be run from the Event-B Explorer as follows:
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
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
TODO
Proof Replay on Undischarged POs
TODO
TODO: Category
