Saving a Context or a Machine (Rodin User Manual)
From Event-B
Once a machine or context is (possibly partly only) edited, you can save it by using the following button:
Automatic Tool Invocations
Once a "Save" is done, three tools are called automatically, these are:
- the Static Checker
- the Proof Obligation Generator
- the Auto-Prover
This can take a certain time. A "Progress" window can be opened at the bottom right of the screen to see which tools are working (most of the time, it is the auto-prover).
Errors. The Problems Window
When the Static Checker discovers an error in a project, a little "x" is added to this project and to the faulty component in the "Project Explorer" window as shown in the following screen shot:
The error itself is shown by opening the "Problems" window.
By double-clicking on the error statement, you are transferred automatically into the place where the error has been detected so that you can correct it easily as shown below:
Preferences for the Auto-prover
The auto-prover can be configured by means of a preference page, which can be obtained as follows: press the "Window" button on the top tooolbar. On the coming menu, press the "Preferences" button. On the coming menu, press the "Event-B" menue, then the "Sequent Prover’, and finally the "Auto-Tactic" button. This yields the following window:
On the left part you can see the ordered sequence of individual tactics composing the auto-prover, whereas the right part contains further tactics you can incorporate in the left part. By selecting a tactic you can move it from on part to the other or change the order in the left part.