imported>Nicolas |
imported>Nicolas |
| Line 1: |
Line 1: |
| − | The purpose is to give more flexibility to tactic providers by allowing them to provide as many tactic applications as they will for a given proof node, even they apply to the same predicate and at the same position.
| + | In this page are presented various proof obligations commands that can be run from the Event-B Explorer as follows: |
| | | | |
| − | == Proposed Framework ==
| + | [[Image:PO_Commands.png]] |
| | | | |
| − | The current proposal consists in the following published interfaces: | + | 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). |
| | | | |
| − | public interface ITacticProvider2 {
| + | == Retry Auto Provers == |
| − | List<ITacticApplication> getPossibleApplications(IUserSupport userSupport,
| |
| − | IProofTreeNode node,
| |
| − | Predicate hyp,
| |
| − | String globalInput);
| |
| − | }
| |
| | | | |
| − | public interface ITacticApplication {
| + | 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). |
| − | void apply(String[] inputs,
| |
| − | String globalInput,
| |
| − | IProgressMonitor monitor);
| |
| − | }
| |
| | | | |
| − | public interface IPositionApplication extends ITacticApplication {
| + | 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). |
| − | Point getHyperlinkBounds();
| |
| − | String getHyperlinkLabel();
| |
| − | }
| |
| | | | |
| − | public interface IPredicateApplication extends ITacticApplication {
| + | == Recalculate Auto Status == |
| − | Image getIcon();
| |
| − | String getTooltip();
| |
| − | }
| |
| | | | |
| − | The current extension point "proofTactics" remains unchanged.
| + | {{TODO}} |
| | | | |
| − | All those interfaces are intended to be implemented by clients.
| + | == Proof Replay on Undischarged POs == |
| | | | |
| − | == Explanations ==
| + | {{TODO}} |
| | | | |
| − | The idea is to encapsulate in {{class|ITacticApplication}} all data needed by the UI to display and apply tactics.
| |
| − | Thus, tactic providers, instead of returning just one fixed tactic to apply, can return several possible 'autonomous' applications.
| |
| | | | |
| − | == Example ==
| |
| | | | |
| − | <pre>
| |
| − | // rewrites occurrences of literal 4 into either 2+2 or 2*2
| |
| − | public class ExampleTacticProvider2 implements ITacticProvider2 {
| |
| | | | |
| − | private static class ExampleApplication implements ITacticApplication {
| |
| | | | |
| − | private final IUserSupport userSupport;
| |
| − | private final Predicate hyp;
| |
| − | private final IPosition position;
| |
| − | // 2 Kinds: PLUS (2+2) and MULT (2*2)
| |
| − | private final ExampleReasoner.Kind kind;
| |
| | | | |
| − | public ExampleApplication(IUserSupport userSupport, Predicate hyp, IPosition position, Kind kind) {
| |
| − | this.userSupport = userSupport;
| |
| − | this.hyp = hyp;
| |
| − | this.position = position;
| |
| − | this.kind = kind;
| |
| − | }
| |
| | | | |
| − | public void apply(String[] inputs, String globalInput, IProgressMonitor monitor) {
| |
| − | try {
| |
| − | // ExampleReasoner implements IReasoner and rewrites literal 4
| |
| − | // at given position into:
| |
| − | // . 2+2 if input.kind is PLUS
| |
| − | // . 2*2 if input.kind is MULT
| |
| − | userSupport.applyTactic(BasicTactics.reasonerTac(
| |
| − | new ExampleReasoner(),
| |
| − | new ExampleReasoner.Input(hyp, position, kind)),
| |
| − | true, monitor);
| |
| − | } catch (RodinDBException e) {
| |
| − | // log the problem
| |
| − | }
| |
| − | }
| |
| − | }
| |
| | | | |
| − | private static class ExampleApplicationVisitor extends DefaultVisitor {
| |
| | | | |
| − | private final IUserSupport userSupport;
| |
| − | private final Predicate hyp;
| |
| − | private final Predicate predicate;
| |
| − | // a list to put applications into
| |
| − | private final List<ITacticApplication> applications;
| |
| | | | |
| − | public ExampleApplicationVisitor(IUserSupport userSupport,
| |
| − | Predicate predicate, Predicate hyp,
| |
| − | List<ITacticApplication> applications) {
| |
| − | this.userSupport = userSupport;
| |
| − | this.predicate = predicate;
| |
| − | this.hyp = hyp;
| |
| − | this.applications = applications;
| |
| − | }
| |
| | | | |
| − | @Override
| |
| − | public boolean visitINTLIT(IntegerLiteral lit) {
| |
| − | if (lit.getValue().intValue() == 4) {
| |
| − | final IPosition position = predicate.getPosition(lit.getSourceLocation());
| |
| − | applications.add(new ExampleApplication(userSupport, hyp, position, Kind.MULT));
| |
| − | applications.add(new ExampleApplication(userSupport, hyp, position, Kind.PLUS));
| |
| − | }
| |
| − | return true;
| |
| − | }
| |
| − | }
| |
| | | | |
| − | // the ITacticProvider2 interface method
| |
| − | public List<ITacticApplication> getPossibleApplications(IUserSupport userSupport,
| |
| − | IProofTreeNode node,
| |
| − | Predicate hyp,
| |
| − | String globalInput) {
| |
| | | | |
| − | final Predicate pred = (hyp == null) ? node.getSequent().goal() : hyp;
| |
| | | | |
| − | final List<ITacticApplication> applications = new ArrayList<ITacticApplication>();
| + | |
| − |
| + | |
| − | pred.accept(new ExampleApplicationVisitor(userSupport, pred, hyp, applications));
| + | |
| − |
| + | |
| − | return applications;
| + | {{TODO|Category}} |
| − | }
| |
| − | } | |
| − | </pre>
| |
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
