3.1.8 Preferences

Rodin provides several options to set the preferences of the Event-B editor. You can access the preferences via Window $\rangle $ Preferences $\rangle $ Event-B in the menu bar. The following subsections describe the different preference options.

3.1.8.1 Appearance

This section provides settings for the Event-B editor appearance.

3.1.8.1.1 Colours and Fonts

The colour and fonts preference page allows you to set the text and comment colour of the Event-B editor. Furthermore, it allows you to turn the borders of the different fields in the Event-B editor on or off. Figure 3.41 shows the Colours and Fonts preference page.

\includegraphics{img/reference/ref_01_preferences13.png}
Figure 3.41: Colours and Fonts preferences

3.1.8.2 Modelling UI

The modelling UI preference pages allows you to customize the visible tabs of the context and machine editor for the Event-B Structural Editor.

3.1.8.3 Prefix Settings

This page describes the default values that are used for the prefixes of the different elements of contexts and machines. Note that prefixes are used for automatic renaming when elements should be alphanumerically ordered in addition to when new elements are created.

Figure 3.42 shows that modifying prefixes on the workspace level or on the project level will affect the names used at creation of new Event-B elements. One can see that the prefixes for variables and invariants, which were originally set to “var" or “inv”, have been replaced by “variable" and “invariant". New elements are then named using those prefixes.

\includegraphics{img/reference/ref_01_preferences1.png}
Figure 3.42: Prefix Settings

3.1.8.3.1 How to set prefixes

Prefix settings can be accessed in two different ways depending on the scope of their application: via Window $\rangle $ Preferences $\rangle $ Event-B $\rangle $ Modelling UI $\rangle $ Prefix settings or via Rename $\rangle $ Customize prefixes....

3.1.8.3.2 Project specific settings

The user can select profiles locally for a project. To do so, select the Properties item in the menu that pops up after right-clicking on a project in the Event-B Explorer. Then open the Prefix Settings tab and check the box to enable project specific settings. You can also click access this page by selecting Window $\rangle $ Preferences and then viewing the Event-B $\rangle $ Modelling UI $\rangle $ Prefix Settings page. Now select the Configure project specific settings link and select the desired project.

A window (see Figure 3.43) appears that allows a user to customize prefixes for a chosen project. On this page, the user can toggle the button Enable project specific settings:

\includegraphics{img/reference/ref_01_preferences2.png}
Figure 3.43: Project specific prefix settings

3.1.8.4 Sequent Prover / Auto/Post Tactic

3.1.8.4.1 Preferences for the selected auto and post tactic profile

There are multiple ways to access the preferences of the auto and post tactics at workspace or project scope:

from the Window $\rangle $ Preferences and then viewing the Event-B $\rangle $ Sequent Prover $\rangle $ Auto/Post Tactic page.

from the properties of a project to set project specific preferences for the Auto/Post Tactic.

from the drop-down menu in the Proof Control view.

The Proof Control view menu shows whether there are sequent prover preferences set for the project containing the current proof obligation 3.44 or not 3.45. Indeed, the command label in the menu tells if project specific settings are set, or if the workspace settings are considered. The command opens the corresponding Auto/Post Tactic page.

\includegraphics[width=1.0\textwidth ]{img/reference/ref_01_proving_perspective13.png}
Figure 3.44: (a) direct access to the Celebrity project specific settings
\includegraphics[width=1.0\textwidth ]{img/reference/ref_01_proving_perspective14.png}
Figure 3.45: (b) no project settings exist for the current PO, direct access to workspace settings

This section describes the Auto/Post Tactic tab of the Auto/Post Tactic preference page.

There are two scopes for the preferences of auto and post tactics: the workspace level and the project level. Note that if the automatic application of tactics is declared only at the workspace level, this option will also be set for the project level.

To access these preferences, open the “Auto/Post Tactic" preference page that can be found after Window $\rangle $ Preference $\rangle $ Sequent Prover.

Figure 3.46 shows the Auto/Post Tactic preference page.

\includegraphics[width=1.0\textwidth ]{img/reference/ref_01_preferences7.png}
Figure 3.46: The “Auto/Post Tactic" preference page

The options shown by (1) and (2) allow you to activate/deactivate the automatic use of auto- and post-tactics. Here you can also choose the profile that should be used for auto- and post-tactics. Note that there is always a profile selected, and this profile can be changed regardless of whether the tactics are automatically launched or not because there is always a way to manually launch auto- and post-tactics. On the previously referenced figure, the Default Auto Tactic Profile is used for the automatic tactic, and the Default Post Tactic Profile is used for the post-tactic.

3.1.8.4.2 Preferences for available profiles

This section describes the Profile tab of the Auto/Post Tactic preference page.

Figure 3.47 shows the contents of the profile tab. There are two visible lists: a list of profiles on the left and the tactics or provers that make up these profiles (Profile Details). Here one can see the contents of the default Auto Tactic Profile.

\includegraphics[width=1.0\textwidth ]{img/reference/ref_01_preferences9.png}
Figure 3.47: Selecting a profile for the Auto-Tactics

There are 4 buttons available to the user:

Default profiles can not be edited nor removed. That is why these options are coloured in gray in the previously referenced figure.

Figure 3.48 shows the dialog available to edit or create a profile. For instance, here we create a profile named “MyFirstTacticProfile".

\includegraphics[width=1.0\textwidth ]{img/reference/ref_01_preferences10.png}
Figure 3.48: Selecting a profile for the Auto-Tactics

In the box labelled Tactics on the left, there is a list of all the different tactics that can be applied to a proof (tactics are explained in more detail in Section 3.4.3). In the box labelled Combinators (combinators are explained in more detail below in Section 3.1.8.5), there is a list of all the combinators that can be used for the proof tactic. To create your proof tactic, drag and drop one of the combinators into the center box. Then drag the proof tactics and drop them on top of the combinator that you just added. This will add the proof tactic to the combinator. You can also add more combinators or even other profiles (available in the Profiles box on the right side) to the combinator that you are working on. If you aren’t certain what a proof tactic or combinator does, select it, and a description of the proof tactic or combinator will be be shown in the Description box that is shown in the lower right hand corner. If the tactic profile that you have created is valid, you will be able to hit the Finish button in the lower right hand corner in order to save it.

3.1.8.4.3 Project specific settings

The user can select profiles locally for each project. To do so, select the Auto/Post Tactic property page in the window that pops up when right-clicking on a project and selecting the Properties item, or selecting the Configure project specific settings link on the Auto/Post Tactic preference page. Figure 3.49 shows what this Auto/Post Tactic tab looks like.

\includegraphics[width=1.0\textwidth ]{img/reference/ref_01_preferences11.png}
Figure 3.49: Auto/Post Tactic Tab for project specific settings for Auto/Post Tactic

Note that the enablement of automatic use of post and auto tactics is decided at the workspace level. Figure 3.50 shows the Profiles tab of the Auto/Post Tactic page for a project specific setting. At the project level, there is a contextual menu available via right click from the list of defined profiles.

\includegraphics[width=1.0\textwidth ]{img/reference/ref_01_preferences12.png}
Figure 3.50: Profiles Tab for project specific settings for Auto/Post Tactic

This contextual menu offers two options to the user:

3.1.8.5 Preferences for Tactic Profiles

3.1.8.5.1 Introduction

The purpose of this section is to give a more detailed preferences to the user so he can build his own automated tactics. More precisely, the user should have a way to specify which parameters have to be passed to the reasoners and have a way to construct complex proof strategies.

3.1.8.5.2 User Documentation

Here is the documentation about the current implementation of the Auto-tactic and Post-tactic preferences.

3.1.8.5.3 Tactic Combinators

Tactic combinators can be used to construct complex proof strategies.

Historically, one combinator has existed since the beginning of auto tactic preferences: the “loop on all pending". It takes one or more tactics and loops them over every pending child until all tactic fail. Until Rodin 2.3 was released, this was the only combinator in Rodin. It is used on the configurable list of auto and post tactics. Rodin 2.3 is easier to configure because there are several other combinators and auto tactic editors.

The following is a list of combinators present by default.

One may notice the absence of child-specific combinator (i.e. combinators that apply tactic T1 on the first child, T2 on the second child, etc.) even though this kind of combinator exists in other provers. The reason is that these tactic profiles are applied automatically and therefore are only used in a general context. Provers with child-specific combinators are used to make manual proofs because they require proof-specific adaptation.

3.1.8.5.3.1 Composers

A composer combinator applies its given tactic(s) to the given node. The given node may be open or closed. It succeeds if at least 1 tactic application is successful.

Name

Arity

Description

Stops when

Sequence

1..n

applies given tactics in given order

all tactics have been applied

Compose until Success

1..n

applies given tactics in given order

a tactic application succeeds

Compose until failure

1..n

applies given tactics in given order

a tactic application fails

Loop

1

applies given tactic repeatedly

the child tactic application fails

3.1.8.5.3.2 Selectors

A selector combinator applies its given tactic to the set of nodes it selects. Selected nodes are computed from the given node. The given node may be open or closed. It succeeds if the tactic application is successful for at least 1 selected node.

Name

Arity

Selects

On all pending

1

all pending children of the given node (the given node itself if it is open)

3.1.8.5.3.3 Post Actions

A post actions applies its given tactic to the given node. The given node must be open (otherwise it fails). Then it performs a specific treatment which is guarded by a trigger condition.

Name

Arity

Trigger Condition

Post Action

Attempt

1

the given node still has pending children (subtree not closed)

prune proof tree at given node

3.1.8.5.3.4 Loop on All pending
  \[  \begin{array}{rl}&  loopOnAllPending(T_1 \ldots T_ n) \\ \mathrel {\widehat=}&  loop(onAllPending(composeUntilSuccess(T_1 \ldots T_ n))) \end{array}  \]    

3.1.8.5.4 Other Ideas

timeout: a post action of arity 1 (with duration as input): limits the time allocated for the tactic that it is applied to (fails after time has gone out)

limitDepth: a post action of arity 1 (with depth as input): limits the proof tree depth for the tactic that it is applied to (prevents tree from growing beyond a given depth)