Difference between pages "Event Model Decomposition" and "The Proving Perspective (Rodin User Manual)"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Pascal
 
imported>Tommy
 
Line 1: Line 1:
 +
{{Navigation|Previous= [[The_Event-B_Explorer_(Rodin_User_Manual)|The Event-B Explorer]]|Next= [[The_Mathematical_Language_(Rodin_User_Manual)|The Mathematical Language]]|Up= [[index_(Rodin_User_Manual)|User_Manual_index]]}}
 
{{TOCright}}
 
{{TOCright}}
 +
== Overview ==
 +
When proof obligations (POs) are not discharged automatically the user can attempt to discharge them interactively using the Proving Perspective. This page provides an overview of the Proving Perspective and its use. If the Proving Perspective is not visible as a tab on the top right-hand corner of the main interface, the user can switch to it via "Window -> Open Perspective".
  
−
== Introduction ==
+
The Proving Perspective consists of a number of views: the Proof Tree, the Goal, the Selected Hypotheses, the Proof Control, the Search Hypotheses, the Cache Hypotheses and the Proof Information. In the discussion that follows we look at each of these views individually. Below is a screenshot of the Proving Perspective:
−
One of the most important feature of the Event-B approach is the possibility to introduce new events during refinement steps, but a consequence is an increasing complexity of the refinement process when having to deal with many events and many state variables.
 
  
−
The main idea of the decomposition is to cut a model <math>A</math> into sub-models <math>A_1, ..., A_n</math>, which can be refined separately and more comfortably than the whole.  
+
[[Image:ProvPers.png|center]]
  
−
The constraint that shall be satisfied by the decomposition is that these refined models might - the recomposition will never be performed in practice - be recomposed into a whole model <math>C</math> in a way that guarantees that <math>C</math> refines <math>A</math>. An event-based decomposition of a model is detailed in the [[#ancre_1|Event Model Decomposition]] article: the events of a model are partitioned to form the events of the sub-models. In parallel, the variables on which these events act are distributed among the sub-models.
+
== Loading a Proof ==
 +
To work on an un-discharged PO it is necessary to load the proof into the Proving Perspective. To do this switch to the Proving Perspective; select the project from the Event-B Explorer; select and expand the component (context or machine); and finally select (double-click) the proof obligation of interest. A number of views will be updated with details of the corresponding proof.
 +
[[Image:ExplorerView.png|center]]
  
−
The purpose is here to precisely describe what is required at the Rodin platform level to integrate this event model decomposition, and to explain why. The details of how it could be implemented are out of scope.
+
Note that pressing [[Image:Discharged.gif]] button on the top left hand side of the Event-B Explorer will remove all discharged proof obligations (PO's) from the view.
  
−
== Terminology ==
+
== The Proof Tree ==
−
* Event model decomposition: The decomposition of a model, as defined in [[Machines_and_Contexts_(Modelling_Language)|the modelling language]], in sub-models. Other [[#ancre_2|decomposition structures for Event-B]] are not considered here.
+
The proof tree view provides a graphical representation of each individual proof step, as seen in the following screenshot:
−
A model can contain contexts, machines, or both. The notion of model decomposition covers on the one hand the machine decomposition, and on the other hand the context decomposition, both being interdependent.
 
−
* Sub-machine: A machine built from a non-decomposed machine during the event model decomposition.
 
−
* Sub-context: A context built from a non-decomposed context during the event model decomposition.
 
−
* ''Shared'' variable: A variable of a given machine which is accessed by events distributed in distinct sub-machines (by opposition to ''private'' variable).
 
−
* ''Private'' variable: A variable of a given machine which is only accessed by events of the same sub-machine (by opposition to ''shared'' variable).
 
−
* ''External'' event: An event of a sub-machine which is built from an event of the non-decomposed machine, and which simulates the way the ''shared'' variables (between this sub-machine and another sub-machine) are handled in the non-decomposed machine (by opposition to ''internal'' event).
 
−
* ''Internal'' event: An event copied from the non-decomposed machine to a sub-machine, according to the end-user specified distribution (by opposition to ''external'' event).
 
  
−
Note that a variable is said to be ''accessed'' when it is read or written. More precisely, such an access may be performed by a predicate (invariant, guard, witness) or in an assignment (action).
+
[[Image:ProTree.png|center]]
  
−
[[Image:Models.png]]
+
Each node in the tree corresponds to a sequent. A line is right shifted when the corresponding node is a direct descendant of the node of the previous line. Each node is labelled with a comment which indicates which rule has been applied, or which prover discharged the proof. By selecting a node in the proof tree, the corresponding sequent is loaded: the hypotheses of the sequent are loaded to the Selected Hypotheses window, and the goal of the sequent is loaded to the Goal view.
  
−
== Low-level Specification ==
+
=== Decoration===
−
The low-level specification details through several steps how the event model decomposition shall be performed, and in which order. It establishes a distinction between the steps performed on the end-user's initiative, and the computed ones. It links when possible to the already implemented features of the Rodin platform which can be used at some steps.
+
The leaves of the tree are decorated with one of three icons:
  
−
=== <font id="machine_decomposition">Decomposition of a machine in sub-machines</font> ===
+
* [[Image:Discharged.gif]] means that this leaf is discharged,
−
The purpose of this paragraph is to specify how to decompose a machine in sub-machines.  
+
* [[Image:Pending.gif]] means that this leaf is not discharged,
 +
* [[Image:Reviewed.gif]] means that this leaf has been reviewed.
  
−
The hierarchy of machines (see the <math>REFINES</math> clauses) shall be first flatten (virtually or not), as illustrated below. The resulting machine is considered as being the non-decomposed machine from which the sub-machines shall be built.
+
Internal nodes in the proof tree are decorated in reverse colours. Note that a "reviewed" leaf is one that is not discharged yet by the prover. Instead, it has been "seen" by the user who decided to postpone the proof. Marking nodes as "reviewed" is very convenient since the provers will ignore these leaves and focus on specific areas of interest. This allows interactive proof in a gradual fashion. In order to discharge a "reviewed" node, select it and prune the tree at that node: the node will become "brown" again (undischarged) and you can now try to discharge it.
−
<br>Note that it may be necessary to rename some variables or invariants.
 
  
−
<center>
+
=== Navigation within the Proof Tree===
−
[[Image:Flattening_machines.png]]
+
On top of the proof tree view, one can see three buttons:
−
</center>
 
  
−
==== About the variables ====
+
* the "'''G'''" buttons allows you to see the goal of the sequent corresponding to each node,
−
Some variables are needed by several sub-machines of the decomposition. As a consequence, these variables shall be replicated in the sub-machines. Beyond that, since it is not possible to ensure that such a variable will be refined in the same way in each sub-machine, they shall be given a special status (''shared'' variable), with the limitation that they cannot be refined.  
+
* the "'''+'''" button allows you to fully expand the proof tree,
 +
* the "'''-'''" allows you to fully collapse the tree: only the root stays visible.
  
−
We will specify in this section how to introduce the notion of ''shared'' variable in the Rodin platform, and how to check the associated rules.
+
=== Manipulating the Proof Tree===
  
−
===== Defining a variable as shared =====
+
==== Hiding ====
−
The following DTD excerpt describes the structure of a variable in the Rodin database:
+
The little square (with a "+" or "-" inside) next to each node in the proof tree allows you to expand or collapse the subtree starting at that node.
  
−
<!ENTITY % NameAttDecl "name CDATA #REQUIRED">
+
==== Pruning ====
−
<!ENTITY % CommentAttDecl "org.eventb.core.comment CDATA #IMPLIED">
+
The proof tree can be pruned at a selected node; the subtree of the selected node is removed from the proof tree. The selected node becomes a leaf and is decorated with [[Image:Pending.gif]] . The proof activity can then be resumed from this node. After selecting a node in the proof tree pruning can be performed in two ways:
−
<!ENTITY % IdentAttDecl "org.eventb.core.identifier CDATA #REQUIRED">
+
* by right-clicking and then selecting "Prune",
−
+
* by clicking on the [[Image:Pn_prover.gif]] button in the proof control view.
−
<!ELEMENT %variable; EMPTY>
 
−
<!ATTLIST %variable;
 
−
  %NameAttDecl;
 
−
  %CommentAttDecl;
 
−
  %IdentAttDecl;
 
−
  >
 
  
−
A first possibility to tag a variable as ''shared'' would be to add a <tt>shared</tt> specific attribute, which would be set to <tt>true</tt> if and only if the variable is ''shared'':
+
Note that after pruning, the post-tactic is not applied to the new current sequent. The post-tactic should be applied manually, if required, by clicking on the post-tactic button in the Proof Control view. This is useful, in particular, when you want to redo a proof from the beginning. The proof tree can be pruned at its root node and then the proof can proceed again, with invocation of internal or external provers; or with interactive proof.
  
−
<ENTITY % shared "org.eventb.core.shared CDATA #REQUIRED">
+
Before pruning a particular node, the node (and its subtree) can be copied to the clipboard. If the new proof strategy subsequently fails, the copied version can be pasted back into the pruned node (see the next section).
−
 
−
<!ELEMENT %variable; EMPTY>
 
−
<!ATTLIST %variable;
 
−
  ...
 
−
  %shared; (false|true) #REQUIRED
 
−
  >
 
  
−
Another possibility would be to define a more generic attribute, which could take different values, according to the nature of the variable:
+
==== Copy/Paste ====
  
−
<ENTITY % nature "org.eventb.core.nature CDATA #REQUIRED">
+
By selecting a node in the proof tree and then right-clicking with the mouse, you can copy the part of the proof tree starting at that sequent (the node and its subtree). Pasting the node and subtree back in is done in a similar manner, with a right mouse click on a proof node. This allows reuse of part of a proof tree in the same, or even in another, proof.
−
 
−
<!ATTLIST %variable;
 
−
  ...
 
−
  %nature; (0|1) #REQUIRED
 
−
  >
 
−
 
−
<!-- The nature attribute encodes the kind of variable:
 
−
      0: private variable
 
−
      1: shared variable
 
−
-->
 
  
−
The second option, which has the main advantage to be more scalable, is retained here.
+
== Goal and Selected Hypotheses ==
 +
The nodes in the proof tree view correspond to sequents. A user will work with one selected node, and thus one sequent, at a time; attempting various strategies in an effort to show that the sequent goal is true. The "Goal" and "Selected Hypotheses" views provide information to the user about the currently selected sequent. Here is an example:
 +
[[Image:GoalHyp.png|center]]
  
−
===== Ensuring that a shared variable is not data-refined =====
+
A hypothesis can be removed from the list of selected hypotheses by selecting the check the box situated next to it (you can click on several boxes) and then by clicking on the [[Image:remove.gif]] button at the top of the selected hypotheses window:
−
A shared variable shall always be present in the state space of any refinement of the component.
 
−
The verification shall be added to those already performed by the static checker. The static checker shall have a way to determine if a given variable is ''shared'' or not.
 
  
−
===== <font id="var_partition">Partitioning the variables in the sub-machines of the decomposition</font> =====
+
[[Image:GoalHypSelect.png|center]]
−
The first question raised by the partition of the variables is whether it shall be the first stage of the decomposition, or not. Let's first suppose that the answer is "yes". The case where <math>e</math> is an event that accesses a variable <math>v1</math> associated to a sub-machine <math>M1</math> and a variable <math>v2</math> associated to a sub-machine <math>M2</math> cannot be successfully handled: should <math>e</math> be associated to <math>M1</math> or to <math>M2</math>? Moreover, contrary to the events, the variables are not essentially bearers of meanings, and they cannot by themselves guide the decomposition.
 
  
−
As a consequence, it is pertinent to assume that the events have been first partitioned. The following cases have then to be taken into consideration when dealing with the variable distribution:
+
Here is the result:
−
* If <math>v</math> is a variable that is only accessed by events of a given sub-machine <math>m</math>, then <math>v</math> is a ''private'' variable of <math>m</math>. It shall be moved to <math>m</math>.
 
−
* If <math>v</math> is a variable that is accessed by events of distinct sub-machines <math>m_1, ..., m_n</math>, then <math>v</math> is a ''shared'' variable. It shall be tagged as such and duplicated in all sub-machines.
 
  
−
If all the variables are ''shared'' at the conclusion of the partition, the end user shall be notified (it certainly means that the decomposition was not judicious!).
+
[[Image:GoalHypSelectRes.png|center]]
  
−
==== About the events ====
+
Note that the deselected hypotheses are not lost: you can find them again using the Search Hypotheses [[Image:sh_prover.gif]] button in the Proof Control view. Other buttons are used as follows:
−
It shall be possible to simulate the way the ''shared'' variables are handled in the non-decomposed machine. This is precisely the purpose of the so-called ''external'' events.  
 
  
−
We will examine in this section how to define such events in the Rodin platform, how to construct them, and how to enforce the rules that apply (in particular, these events cannot be refined).
 
  
−
===== Identifying an event as external =====
+
* [[Image:select_all_prover.gif]] select all hypotheses.  
−
An attribute is already defined, which is introduced below, to precise the nature of an event. A first solution would be to add another masked value (''eg.'' 4) to encode the ''external'' status.  
 
  
−
<!ENTITY % convergence "org.eventb.core.convergence">
 
−
 
−
<!ATTLIST %event;
 
−
  ...
 
−
  %convergence; (0|1|2) #REQUIRED
 
−
  ...
 
−
  >
 
−
  <!--
 
−
    The convergence attribute specifies which PO should be generated
 
−
    for the combination event / variant:
 
−
      0: ordinary event, no PO
 
−
      1: convergent event, PO to show event decreases variant
 
−
      2: anticipated event, PO to show event doesn't increase variant
 
−
  -->
 
  
−
Another solution would be to add a distinct <tt>external</tt> attribute, which would be set to <tt>true</tt> if and only if the event is ''external'':
+
* [[Image:inv_prover.gif]] invert the selection.
  
−
<ENTITY % external "org.eventb.core.external CDATA #REQUIRED">
 
−
 
−
<!ATTLIST %event;
 
−
  ...
 
−
  %external; (false|true) #REQUIRED
 
−
  >
 
  
−
This solution is preferred because the notion of ''external'' event is totally orthogonal to the notion of convergence.
+
* [[Image:falsify_prover.gif]] next to the goal - proof by contradiction 1: The negation of the '''goal''' becomes a selected hypothesis and the goal becomes "'''⊥'''".  
  
−
===== <font id="build_external">Constructing an external event</font> =====
 
−
The construction of an ''external'' event highly relies on some [[Rewriting_rules_for_event_model_decomposition|rewriting / simplification rules]]. It is recommended to peruse them before reading further.
 
  
−
<math>e</math> is an event of <math>M</math>, <math>v_i</math> are ''private'' variables of <math>M</math>, <math>s_i</math> are ''shared'' variables between <math>M</math> and the destination sub-machine (''i.e.'' the sub-machine where the ''external'' event will be dispatched), <math>P, P_i, Q_i</math> are before-after predicates of <math>M</math>, and <math>G</math> is a predicate of <math>M</math>.
+
* [[Image:falsify_prover.gif]] next to a selected hypothesis - proof by contradiction 2: The negation of the '''hypothesis''' becomes the goal and the negated goal becomes a selected hypothesis.
  
−
<u>Generic construction</u>
 
−
<br>We first focus on the generic construction of an ''external'' event from an event of a sub-machine <math>M</math> whose action is expressed as follows:
 
  
−
  e
+
=== Applying Proof Rules ===
−
  '''WHERE'''
+
A user wishing to attempt an interactive proof has a number of proof rules available, and these may be either rewrite rules or inference rules. In the Goal and the Selected Hypotheses views various operators may appear in red coloured font. The red font indicates that some interactive proof rule(s) are applicable and may be applied as a step in the proof attempt. When the mouse hovers over such an operator a number of applicable rules may be displayed; the user may choose to apply one of the rules by clicking on it.
−
    <math>G(v_1,...,v_n,s_1,...,s_m)~</math>     
 
−
  '''THEN'''                 
 
−
    <math>v_1,...,v_n,s_1,...,s_m \bcmsuch P(v1,...,v_n,s_1,...,s_m, v_1',...,v_n',s_1',...,s_m')</math>
 
  
−
<ol>
+
Other proof rules can be applied when green buttons appear in the Goal and Selected Hypotheses views. Examples are proof by contradiction [[Image:falsify_prover.gif]], that we have already encountered; and [[Image:ConjI_prover.gif]] for conjunction introduction in the goal.
−
<li>The first step of the construction consists in replacing the ''private'' variables by parameters. Note that this step is purely fictive, because assigning an event parameter is not allowed!</li>
 
  
−
  e
+
[[Image:ApplyRewRule.png|center]]
−
  '''ANY''' <math>x_1,...,x_n~</math>
 
−
  '''WHERE'''
 
−
    <math>G(x_1,...,x_n,s_1,...,s_m)~</math>     
 
−
  '''THEN'''                 
 
−
    <math>x_1,...,x_n,s_1,...,s_m \bcmsuch P(x1,...,x_n,s_1,...,s_m, x_1',...,x_n',s_1',...,s_m')</math>
 
  
−
<li>The second step consists in adding guards to define the types of the parameters, if necessary. More precisely, a theorem shall be added for each parameter for which typing is required. The <tt>.bcm</tt> file associated to the non-decomposed machine shall be parsed in order to retrieve the typing information.
+
To instantiate a quantifier the user enters the desired expression in the box behind the quantifier and clicks on the quantifier:
  
−
<li>The third and last step of the construction consists in introducing an existential quantifier to resolve the invalid assignment. <math>external\_e</math> is the newly built external event.</li>
+
[[Image:InstQuantifier.png|center]]
  
−
  external_e
+
==== Rewrite Rules ====
−
  '''ANY''' <math>x_1,...,x_n~</math>
+
Rewrite rules are one-directional equalities (and equivalences) that can be used to simplify formulas (the goal or a single hypothesis). A rewrite rule is applied from left to right when its ''side condition'' holds; it can be applied either in the goal predicate, or in one of the selected hypotheses.
−
  '''WHERE'''
 
−
    <math>G(x_1,...,x_n,s_1,...,s_m)~</math>     
 
−
  '''THEN'''                
 
−
    <math>s_1,...,s_m \bcmsuch \exists y_1,...y_n \qdot P(x1,...,x_n,s_1,...,s_m, y_1,...,y_n,s_1',...,s_m')</math>
 
−
</ol>
 
  
−
<u>Derived constructions</u>
+
A rewrite rule is applied either automatically ('''A''') or manually ('''M'''):
−
<br>Then, it is possible to derivate the construction for other actions:
+
* automatically, when post-tactics are run.
−
# [[Rewriting_rules_for_event_model_decomposition|Rewriting rules 1 to 5]] shall be first applied as many times as possible, from left to right, to get the action into the generic form introduced before.  
+
* automatically, when auto-tactics are run.
−
# Then, the steps detailed for the generic construction shall be followed.
+
* manually, through an interactive command. These rules gather non equivalence laws, definition laws, distributivity laws and derived laws.
−
# Then, the [[Rewriting_rules_for_event_model_decomposition|simplification rules 6 to 8]] shall be enforced.
 
−
# Finally, the [[Rewriting_rules_for_event_model_decomposition|rewriting rules 1 to 4]] shall be applied, from right to left.  
 
  
−
Thus, if <math>P_i(x_1,...,x_n,s_1,...,s_m,s_i')~</math> is equal to <math>s_i' = Q_i(x_1,...,x_n,s_1,...,s_m)~</math>, and if there is no ''private'' variable (''i.e.'' there is no existential quantifier on the right-hand side of the assignments), then <math>s_i \bcmsuch P_{n+i}(x_1,...,x_n,s_1,...s_m,s_i')</math> shall be rewritten as <math>s_i \bcmeq Q_i(x_1,...,x_n,s_1,...,s_m)</math>.
+
Automatic rewrite rules are equivalence simplification laws.
−
<br>
 
−
The proof obligations generated for deterministic actions are indeed more suitable than those generated for non-deterministic actions.  
 
  
−
In the same manner, if <math>P_i(x_1,...,x_n,s_1,...,s_m,s_i')~</math> is equal to <math>s_i' \in Q_i(x_1,...,x_n,s_1,...,s_m)</math>, and if there is no private variable (''i.e.'' there is no existential quantifier on the right-hand side of the assignments), then <math>s_i \bcmsuch P_{n+i}(x_1,...,x_n,s_1,...s_m,s_i')</math> shall be rewritten as <math>s_i \bcmin Q_i(x_1,...,x_n,s_1,...,s_m)</math>.
+
Each rule name indicates the rule's characteristics according to the following convention:
−
<br>
 
−
For a given set <math>S</math>, proving that <math>\exists x \qdot x \in S</math> (FIS proof obligation generated from <math>x \bcmsuch x' \in S</math>) is indeed not as "simple" as proving that <math>S \neq \emptyset</math> (proof obligation generated from <math>x \bcmin S</math>).
 
  
−
<u>Example</u>
+
* the law category: simplification law (SIMP), definition law (DEF), distributivity law (DISTRI), or else derived law (DERIV).
 +
* the root operator of the formula on the left-hand side of the rule, e.g. predicate AND, expression BUNION.
 +
* (optionally) the terminal elements on the left-hand side of the rule: special element (SPECIAL) such as the empty-set, type expression (TYPE), same element occurring more than once (MULTI), literal (LIT). A type expression is either a basic type (<math>\intg, \Bool</math>, any carrier set), or <math>\pow</math>(type expression), or type expression<math>\cprod</math>type expression.
 +
* (optionally) some other description of a characteristic, e.g. left (L), right (R).
  
−
  e
+
Rewrite rules having a symmetric operator on the left-hand side may also describe other rules. eg: the rule:
−
  '''WHERE'''
 
−
    <math>G(v_1,...,v_n,s_1,...,s_m)~</math>     
 
−
  '''THEN'''                 
 
−
    <math>\begin{array}{ll}v_1\!\!\! &\bcmsuch P_1(v_1,...,v_n,s_1,...,s_m,v_1')\\
 
−
    ...\\
 
−
    v_n\!\!\! &\bcmsuch P_n(v_1,...,v_n,s_1,...,s_m,v_n')\\
 
−
    s_1\!\!\! &\bcmsuch P_{n+1}(v_1,...,v_n,s_1,...,s_m,s_1')\\
 
−
    ...\\
 
−
    s_m\!\!\! &\bcmsuch P_{n+m}(v_1,...,v_n,s_1,...,s_m,s_m') \end{array}</math>
 
  
−
  external_e
+
<center><math> \True  = \False  \;\;\defi\;\;  \bfalse </math></center>
−
  '''ANY''' <math>x_1,...,x_n~</math>
 
−
  '''WHERE'''
 
−
    <math>G(x_1,...,x_n,s_1,...,s_m)~</math>     
 
−
  '''THEN'''                 
 
−
    <math>\begin{array}{ll}s_1\!\!\! &\bcmsuch P_{n+1}(x_1,...,x_n,s_1,...,s_m,s_1')\\
 
−
    ...\\
 
−
    s_m\!\!\! &\bcmsuch P_{n+m}(x_1,...,x_n,s_1,...s_m,s_m') \end{array}</math>
 
  
−
In this example, the rules [[Rewriting_rules_for_event_model_decomposition#rule_4|4]], [[Rewriting_rules_for_event_model_decomposition#rule_7|7]] and [[Rewriting_rules_for_event_model_decomposition#rule_8|8]] shall be applied.
+
should also produce the rule:
  
−
===== Partitioning the events in the sub-machines of the decomposition =====
+
<center><math> \False  = \True  \;\;\defi\;\;  \bfalse </math></center>
−
The following sequence shall be followed:
 
−
* The events shall be first partitioned, as indicated by the end-user. More precisely, machines shall be created, according to this partition. At this step, the machines shall only contain the specified events. In particular, the <math>SEES</math> and <math>REFINES</math> clauses shall be empty. Moreover, note that it may be necessary to rename some events when performing the partition.
 
−
* The Rodin platform shall then be able to distribute the variables, according to the event partition (see [[#var_partition|Variable partition]]).
 
−
* The Rodin platform shall be able to distribute the invariants, according to the variable partition (see [[#inv_partition|Invariant partition]]).
 
−
* If <math>e</math> is an event that modifies a ''shared'' variable <math>s</math> (''i.e.'' <math>s</math> is listed among the free identifiers on the left-hand side of an assignment), then an ''external'' event that modifies <math>s</math> shall be built from <math>e</math> in each sub-machine where <math>s</math> is accessed.
 
  
−
''N.B.'' : Note that the construction of an ''external'' event depends on the ''source'' sub-machine (''i.e.'' the sub-machine containing the ''internal'' event <math>e</math> from which the ''external'' event is to be built) and on the ''destination'' sub-machine (''i.e.'' the sub-machine where the ''external'' event is to be built).
+
For associative operators in connection with distributive laws as in:
−
<br>
 
−
Building an ''external'' event from a given event <math>e</math> modifying a ''shared'' variable <math>s</math> and duplicating it in each sub-machine where <math>s</math> is accessed does not indeed entirely fit the requirements, as illustrated below: the sub-machine <math>M3</math> does not know the ''shared'' variable <math>s2</math> and the sub-machine <math>M1</math> does not know the ''shared'' variable <math>s4</math>.
 
  
−
<center>
+
<center><math> P  \land (Q~ {\color{red}{\lor}} \ldots \lor R) </math></center>
−
[[Image:External_events.png]]
 
−
</center>
 
  
−
===== <font id="convergence">Propagating the convergence status</font> =====
+
it has been decided to highlight the first associative/commutative operator (the <math>{\color{red}{\lor}} </math>). A menu is presented when hovering the mouse over the operator: the first menu option distributes all associative/commutative operators, the second option distributes only the first associative/commutative operator. In order to simplify the explanation we write associative/commutative operators with two parameters only. However, ''we must emphasise here'', that generally we may have a sequence of more than two parameters. So, we write <math> Q \lor R </math> instead of <math> Q \lor \ldots \lor R </math>. Rules are sorted according to their purpose.
−
A sub-machine can be seen as a new abstract machine. As a consequence, the convergence status of a given event shall be propagated in the sub-machines as described below:
 
−
* An event tagged as ordinary in the non-decomposed machine shall remain ordinary in the sub-machine.
 
−
* An event tagged as convergent in the non-decomposed machine shall become ordinary in the sub-machine.  
 
−
* An event tagged as anticipated in the non-decomposed machine shall remain anticipated in the sub-machine.
 
−
* An ''external'' event shall always be declared as ordinary.
 
  
−
See [[Events_(Modelling_Language)|the modelling language]] for precisions on the convergence status.
+
Rules marked with a star in the first column are implemented in the current prover.  Rules without a star are planned for implementation.
  
−
===== Propagating the extended status =====
+
Rewrite rules are split into:
−
An event (''external'' or not) of a sub-machine shall always be declared as non-extended.
 
  
−
===== Ensuring that an external event cannot be refined =====
+
* [[Set Rewrite Rules]]
−
The verification shall be performed by the static checker. The static checker shall have a way to determine if a given event is ''external'' or not.
+
* [[Relation Rewrite Rules]]
 +
* [[Arithmetic Rewrite Rules]]
  
−
===== Decomposing the initialization event =====
+
They are also available in a single large page [[All Rewrite Rules]].
−
An initialization event shall be built in each sub-machine from the initialization event of the non-decomposed machine, and according to the distribution of the variables among these sub-machines. The construction is detailed below. <math>initialization</math> is the initial event and <math>e</math> the built event, <math>x_i</math> are variables (''private'' or ''shared'') of the sub-machine containing <math>e</math>, <math>y_i</math> are variables of other sub-machines, <math>P</math> is a before-after predicate and <math>G</math> is a predicate.
 
  
−
  initialization   
+
==== Inference Rules ====
−
  '''THEN'''                 
+
Inference rules (see [[Proof Rules]]) are applied either automatically (A) or manually (M).
−
    <math>x_1,...,x_n,y_1,...,y_m \bcmsuch P(x1,...,x_n,y_1,...,y_m,x_1',...,x_n',y_1',...,y_m')</math>
 
  
−
Only the variables of the considered sub-machine shall appear in the built initialization event; other variables shall become bound:  
+
Inference rules applied automatically are applied at the end of each proof step. They have the following possible effects:
  
−
  e 
+
* they discharge the goal,
−
  '''THEN'''                 
+
* they simplify the goal and add a selected hypothesis,
−
    <math>x_1,...,x_n \bcmsuch \exists z_1,...,z_m \qdot P(x1,...,x_n,y_1,...,y_m,x_1',...,x_n',y_1,...,y_m')</math>
+
* they simplify the goal by decomposing it into several simpler goals,
 +
* they simplify a selected hypothesis,
 +
* they simplify a selected hypothesis by decomposing it into several simpler selected hypotheses.
  
−
The derived cases and simplification rules introduced during [[#build_external|the construction of the external events]] apply here as well.
+
Inference rules applied manually are used to perform an interactive proof. They can be invoked by clicking on the red highlighted operators in the goal or the hypotheses. A menu is presented when there are several options.
  
−
==== <font id="inv_partition">About the invariants</font> ====
+
See [[Inference Rules]] list.
−
We will see in this section how to distribute the invariants among the sub-machines, once the variables have been partitioned.
 
  
−
* Case 1: If <math>i</math> is an invariant only involving ''private'' variables of a given sub-machine, then it shall be copied in this sub-machine.
+
== The Proof Control View==
−
* Case 2: If <math>i</math> is an invariant involving ''private'' variables of distinct sub-machines, then it shall not be copied.
 
−
* Case 3: If <math>i</math> is an invariant only involving ''shared'' variables, then it shall only be copied in the sub-machines containing all these variables.
 
−
* Case 4: If <math>i</math> is an invariant involving ''private'' variables and ''shared'' variables, then it shall only be copied in the sub-machines containing all these variables.
 
  
−
These different cases are illustrated in the figure below, where <math>P1</math>, <math>P2</math>, <math>P3</math> and <math>P4</math> are predicates. <math>A</math> is an abstract machine, <math>C</math> is a concrete machine extending <math>A</math>, <math>M</math> is the flattened machine for <math>C</math> and <math>A</math> (see [[#machine_decomposition|how flattening a hierarchy of machines]]), and <math>M1</math>, <math>M2</math>, and <math>M3</math> are the sub-machines resulting from the decomposition of <math>M</math>. <math>v1</math> is a ''private'' variable of <math>M1</math>, <math>v2</math> is a variable ''shared'' between <math>M1</math> and <math>M2</math>, <math>v3</math> is a variable ''shared'' between <math>M2</math> and <math>M3></math>, and <math>v4</math> is a ''private'' variable of <math>M3</math>.
+
The Proof Control view contains the buttons which you can use to perform an interactive proof.
  
−
<center>
+
[[Image:PControl.png|center]]
−
[[Image:Invariants.png]]  
 
−
</center>
 
  
−
'''To summarize, an invariant based on a <math>P(v_m,...,v_n)~</math> predicate is copied in a sub-machine <math>M_x</math> if and only if <math>M_x</math>  contains the <math>\{v_m,...,v_n\}~</math> variables.'''
+
The Proof Control view offers a number of buttons whose effects we briefly describe next; moving from left to right on the toolbar:
  
−
If an invariant is used for typing but it has not been copied, a theorem shall be added in the sub-machines for each variable for which typing is required (otherwise a problem will be detected by the static checker). Note that there is no contradiction with the requirements on [[#po|proof obligations]]; no proof obligation (PO) is indeed generated for predicates <math>v \in T</math>, where <math>v</math> is a variable and <math>T</math> is a type.
+
* ('''nPP''') invokes the new predicate prover, a drop-down list indicates alternative strategies.
 +
* ('''R''') indicates that a node has been reviewed: in an attempt by the user to carry out proofs in a stepwise fashion, they might decide to postpone the task of discharging some proofs until a later stage. To do this the proofs can be marked as reviewed by choosing the proof node and clicking on this button. This indicates that by visually checking the proof the user is convinced that they can discharge it later, but they do not want to do it right now.
 +
* ('''p0''') the PP and ML provers can be invoked from the drop-down list using different forces.
 +
* ('''dc''') do proof by cases: the proof is split into two branches. In the first branch:- the predicate supplied by the user is added to the Selected Hypotheses, and the user attempts to discharge this branch. In the second branch :- the predicate supplied by the user is negated and added to the Selected Hypotheses; the user then attempts to discharge this branch.
  
−
Beyond that, a workaround exists if an invariant <math>inv</math>, based on a <math>P(v_m,...,v_n)~</math> predicate, seems useful (for example an invariant between a concrete variable and some abstract variable) but it has disappeared in a sub-machine <math>M_x</math> containing variables <math>\{v_p,...,v_q\}~</math> (''eg.'' <math>inv2</math> and <math>inv3</math> have both been excluded from <math>M3</math> machine by application of the stated rules). It is indeed possible to add in the non-decomposed machine a theorem based on <math>P~</math>, but where the variables <math>\{v_m,...,v_n\} \setminus \{v_p,...,v_q\}</math> become bound, and then to perform again the decomposition. It will lead to a new proof obligation in the non-decomposed machine, which does not pose any difficulty.
+
* ('''ah''') add a new lemma: the predicate in the editing area should be proved by the user. It is then added as a new selected hypothesis.
−
<br>For example, if a theorem <math>inv5: P5(v4)~</math>, with <math>P5 \defi \exists v1 \qdot P2(v1,v4)</math>, is added to the <math>C</math> concrete machine, then it will be copied in the sub-machine <math>M3</math> during the decomposition (see case 1). In order to prove the <math>P5~</math> statement, the bound variable <math>v1</math> shall obviously be instantiated with <math>v1</math>.
+
* ('''ae''') abstract expression: the expression in the editing area is given a fresh name.
 +
* '''the robot''': invokes the auto-prover which attempts to discharge the goal. The auto-prover is applied automatically on all proof obligations after a "save" without any intervention of the user. Using this button, you can invoke the auto-prover within an interactive proof.
 +
* the '''post-tactic''' is executed ,
 +
* '''lasoo''': load into the Selected Hypotheses window those hidden hypotheses that contain identifiers in common with the goal, and with the selected hypotheses.
 +
* '''backtrack''' form the current node (i.e., prune its parent),
 +
* '''scissors''': prune the proof tree from the node selected in the proof tree,
 +
* '''Search Hypotheses''': find hypotheses containing the character string in the editing area, and display in the Search Hypothesis view.
 +
* '''Cache Hypotheses''': press this to display the ''"Cache Hypotheses"'' view. This view displays all hypotheses that are related to the current goal.
 +
* load the '''previous''' undischarged proof obligation,
 +
* load the '''next''' undischarged proof obligation,
 +
* '''(i)''' show information corresponding to the current proof obligation in the corresponding window. This information correspond to the elements that directly took part in the proof obligation generation (events, invariant, etc.),
 +
* goto the next '''pending''' node of the current proof tree,
 +
* load the next '''reviewed''' node of the current proof tree.
 +
* '''Disable/Enable Post-tactics''': allows the user to choose whether post-tactics run after each interactive proof step.
 +
=== The Smiley ===
 +
The smiley can be one of three different colors: (1) red, indicates that the proof tree contains one or more undischarged sequents, (2) blue, indicates that all undischarged sequents of the proof tree have been reviewed, (3) green, indicates that all sequents of the proof tree are discharged.
  
−
==== About the variants ====
+
=== The Editing Area ===
−
As mentioned [[#convergence|before]], there is no convergent event in sub-machines. As a consequence, there is no need to take the variants into consideration when performing the decomposition.
+
The editing area allows the user to supply parameters for proof commands. For example, when the user attempts to add a new hypothesis (by clicking on the lemma '''ah''' button), the new hypothesis should have been written by the user in the editing area.
  
−
=== <font id="context_decomposition">Decomposition of a context in sub-contexts</font> ===
+
=== ML/PP and Hypotheses ===
−
The purpose of this paragraph is to specify how to decompose the contexts, according to the decomposition of the machines, and to establish how to link the sub-contexts to the sub-machines.
 
  
−
The hierarchy of contexts (see the <math>EXTENDS</math> clauses) shall be first accumulated in a single context. More precisely, a new context shall be built (virtually or not), which contains all the carrier sets, constants and axioms of the hierarchy. This context is assumed to be the non-decomposed context from which the sub-contexts shall be built.
+
==== ML ====
−
<br>Note that it may be necessary to rename some axioms when flattening the hierarchy.
+
ML (mono-lemma) prover appears in the drop-down list under the button ('''pp''') as M0, M1, M2, M3, ML.
 +
The different configuration (e.g., M0) refer to the proof force of the ML prover. '''All hypotheses''' are passed to ML.
  
−
<center>
+
==== PP ====
−
[[Image:Flattening_contexts.png]]
+
PP (predicate prover) appears in the drop-down list under the button ('''pp''') as P0, P1, PP.  
−
</center>
+
* P0 uses '''all selected hypotheses''' (the ones in '''Selected Hypotheses''' window).
 +
* P1 employs a '''lasoo''' operation to the selected hypotheses and the goal, and uses the resulting hypotheses.
 +
* PP uses '''all hypotheses'''.
  
−
Then, an empty context shall be built for each sub-machine <math>m</math>, by respecting the following sequence: the constants shall be first included, then the carrier sets shall be added, and finally the axioms shall be considered.  
+
== The Search Hypotheses View==
−
<br>This context shall be linked to <math>m</math> through its <math>SEES</math> clause. Note that, at the conclusion of the context decomposition, the sub-contexts that may be empty shall not be kept, and a <math>SEES</math> clause shall not be added to the associated sub-machines.
+
By typing a string in the '''Proof Control''' window and pressing the '''Search Hypotheses''' button a window is provided which contains the hypotheses having a character string in common with the one entered by the user in the editing area. For example, if we search for hypotheses involving the character string "cr", then after pressing the '''Search Hypothesis''' button on the proof control window, we obtain the following:
  
−
==== About the constants ====
+
[[Image:um-0102.png|center]]
−
A constant of a non-decomposed context shall be copied in a sub-context if and only if it appears in a predicate (invariant or guard) or an assignment (action) of the associated sub-machine.
 
  
−
==== About the carrier sets ====
+
This view also integrates a "quick search" area (A), that allows us to search quickly hypotheses involving short character strings such as "cr". A '''search hypothesis button (B)''' that behaves the same as the button of the proving window, a '''refresh button (C)''' that updates the window manually for more control, and a '''drop down menu (D)''' to set the preferences of the view up.  
−
A carrier set shall be visible from any sub-machine that references it, explicitly or implicitly, through a predicate or an assignment. In other terms, a carrier set of a non-decomposed context shall be copied in a sub-context if and only if this set appears in a predicate or assignment of the associated sub-machine, or types a constant previously copied to this sub-context.
 
  
−
==== About the axioms ====
+
By pressing '''return''' key or the button (B) (once a short string has been given in the input area (A)), hypotheses can be searched quickly as if we used the '''Proof Control''' as described before.
−
We will see in this section how to distribute the axioms among the sub-contexts, once the constants and carrier sets have been copied.  
 
  
−
As for the [[#inv_partition|invariants]], an axiom is copied in a sub-machine <math>M_x</math> if and only if <math>M_x</math> contains the referenced constants and sets. If an axiom is used for typing but it has not been copied, a theorem shall be added in the sub-contexts for each constant for which typing is required (otherwise a problem will be detected by the static checker).
+
The drop down menu (D) is accessible to set some preferences over the searched hypotheses :
  
−
== High-level Specification ==
+
[[Image:SearchHyp_view_menu.png|center]]
−
The high-level specification details how the event model decomposition shall be integrated into the Rodin platform as a new feature, by linking to the existing architecture.
 
  
−
=== Definition of the decomposition ===
+
If we change preferences for the search, we might need to "update" manually the view with the button (C).
−
It is necessary to first give a definition of the event model decomposition in the Rodin platform. Is it an Event-B project decomposition? Or, is it a decomposition performed from some well-identified machines and contexts of a given Event-B project?
+
By selecting "Consider hidden hypotheses in search" option, we can review all hypotheses that have been unselected in the selected hypotheses window(more info about[[Rodin_Proving_Perspective#Goal and Selected Hypotheses| selected/hidden hypotheses]]...).
  
−
The entry point for the decomposition is a machine <math>M1</math>, its visible contexts, and its whole parent hierarchy of machines.
+
[[Image:SearchHyp.png|center]]
  
−
<center>
+
To move any of these hypotheses to the '''Selected Hypotheses''' window, select those required (using the check boxes) and press the [[Image:Add.gif]] button. Adding these hypotheses to the selected hypotheses means that they will be visible to the prover. They can then be used during the next interactive proof phase.
−
[[Image:Machine.png]]
 
−
</center>
 
  
−
The machine <math>M1</math> to be taken as input for the decomposition shall be pointed by the end-user. The <math>EXTENDS</math> clauses of contexts and the <math>SEES</math> clauses of machines are used to build the associated hierarchy of contexts. In the same manner, the <math>REFINES</math> clauses allow to build the associated hierarchy of machines.
+
To remove hypotheses from the '''Search Hypotheses''' window use the [[Image:Remove.gif]] button. This button also appears above the selected hypotheses, and allows the user to remove any hypothesis from the '''Selected Hypotheses''' window.  
  
−
=== Configuration of the decomposition ===
+
The other button, situated to the left each hypotheses, is the [[Image:falsify_prover.gif]] button. clicking on this will attempt a proof by contradiction. The effect is the same as if the hypothesis were in the '''Selected Hypotheses'''.
−
The end-user shall be asked to parametrize the decomposition, and more precisely to:
 
−
* identify the machine to be taken as input for the decomposition.
 
−
* identify the sub-machines to be created.
 
−
* partition the events.
 
−
* indicate which invariants, axioms or theorems shall be ignored (because they are not required any longer).
 
  
−
It is more suitable for the end-user to visualize the configuration, and as a consequence it shall preferably be performed through the Graphical User Interface of the Rodin platform.
+
== The Cache Hypotheses Window ==
  
−
The following dialog box, which fills these requirements, is given as an example. The left-hand side displays the non-decomposed model and the right-hand side the decomposed model. The second one is built by the user, by first adding machines and then copying events from left to right. The unchecked invariants are those to be ignored, the checked events are those to be copied (the initialization events are not copied).
+
This window allows the user to keep track of recently manipulated (e.g., used, removed, selected) hypotheses for any PO. For example, when the user applies a rewrite to an hypothesis, a new hypothesis (after the rewriting) is selected, and the original hypothesis is deselected and put in the '''Cache Hypotheses''' window.
  
−
<center>
+
Similar operations (to that of the '''Selected Hypotheses''' and '''Search Hypotheses''' windows) such as removing, selecting and proof by contradiction ('''ct''') are also available for the cached hypotheses. Interactive proof steps (e.g., rewriting) can also be carried out from the '''Cache Hypotheses''' window as well as the '''Search Hypotheses''' window.
−
[[Image:GUI.png]]
 
−
</center>
 
  
−
=== Execution of the decomposition ===
+
== Proof Information View ==
−
A <tt>Decompose</tt> action shall be added. It shall be enabled if and only if a machine is selected. It shall be available from the <tt>Project</tt> menu, from the toolbar, and in the contextual menu displayed when right-clicking on the selected project.
 
  
−
[[Image:Action.png]]
+
This view displays information so that the user can relate a proof obligation to the model. For example, typical information for an event invariant preservation PO includes the event; as well as the invariant in question. In the following example, the hyperlinks 'CreateToken' and 'inv2' can be used to navigate to the containing machine.  
  
−
A new Event-B project shall be created for each sub-machine built during the configuration. The [[#machine_decomposition|decomposition of the sub-machine]] shall first be completed, and then the non-decomposed [[#context_decomposition|context shall be partitioned]], as specified before.
+
[[Image:PInfo.png|center]]
  
−
As far as possible, the developments shall not be performed in the Event-B core; the dedicated extension points shall be used instead (''eg.'' those provided for the static checker. See the <tt>plugin.xml</tt> file of the <tt>org.eventb.core</tt> package).
+
== Rule Details View ==
  
−
=== <font id="po">Generation of the proof obligations</font> ===
+
This view displays the information relative to a given proof tree node, on which a rule was applied.<br>
−
A model to be decomposed is assumed to be proved, ''i.e.'' the proof obligations (PO) have all been handled successfully. The following conditions on PO shall be fulfilled during the decomposition:
+
A command is available when right-clicking on a proof tree node, in order to reveal the Rule Details View (See picture below).
−
* The decomposition shall not generate any new proof obligation.
 
−
* The proof obligations related to the non-decomposed model shall not be "propagated" to the decomposed models to be proved again. As a consequence, the Proof Obligation Generator (POG) shall be temporary disconnected until the decomposition is performed.
 
  
−
== Mathematical Approach ==
+
[[Image:ShowRuleDetailsView.png|center]]
−
The purpose of this section is to mathematically formalize the Event-B decomposition previously specified, and by the way to remove the possible remaining ambiguity.  
 
  
−
Let's define <math>\mathit{MACHINE}</math> as the set of all machine handles, <math>\mathit{EVENT}</math> the set of all events, and <math>\mathit{VAR}</math> the set of all variables.
+
By default, this view is a fast view. A button (identified by the view's icon) is then available at the bottom left of the workbench, to show up this view.
  
−
* The distribution of the events of the non-decomposed machine among the different sub-machines (according to the end-user configuration) can be represented as with a partial function:
+
Here is an overview of the Rule details view :
−
<math>\mathit{partition}\in\mathit{EVENT}\pfun\mathit{MACHINE}</math>
 
−
<br>For a given sub-machine <math>m</math>, <math>partition^{-1}[\{m\}]~</math> is then the set of ''internal'' events of <math>m</math>.
 
−
* The access of a variable by a given event (according to the static-checker) can be expressed as:
 
−
<math>\mathit{access}\in\mathit{EVENT}\rel\mathit{VAR}</math>
 
−
<br>For a given variable <math>v</math>, <math>(partition;access^{-1})[\{v\}]~</math> is then the set of the sub-machines accessing <math>v</math>, and <math>v</math> is a ''private'' variable of a sub-machine <math>m</math> if and only if this set contains a single component (''i.e.'' <math>card((partition;access^{-1})[\{v\}]) = 1~</math>); otherwise, and if and only if this set is not empty, <math>v</math> is ''shared''.
 
−
<br>In parallel, for a given sub-machine <math>m</math>, <math>(access;partition^{-1})[\{m\}]~</math> is the set of variables accessed by the events contained in <math>m</math>.
 
−
* The association of a variable with the events modifying this variable (according to the static-checker) can be specified as:
 
−
<math>\mathit{modify}\in\mathit{VAR}\rel\mathit{EVENT}</math>
 
−
<br>For a given sub-machine <math>m</math> and a variable <math>v \in (access;partition^{-1})[\{m\}]</math>, <math>modify[\{v\}]~</math> is then the set of the events modifying <math>v</math>.
 
−
* The construction of the ''external'' events for a sub-machine can be represented with a relation:
 
−
<math>\mathit{extern}\in\mathit{MACHINE}\rel\mathit{EVENT}</math>
 
−
<br>It is computed as follows: <math>extern = (modify;access;partition^{-1}) \setminus partition^{-1}</math>
 
−
<br>Thus, the ''external'' events of a given sub-machine <math>m</math> are events modifying the variables accessed by the ''internal'' events of <math>m</math>, but they are not ''internal'' events of <math>m</math>.
 
  
−
=== Example ===
+
[[Image:RuleDetailsView.png|center]]
−
The following example is taken from the [[#ancre_1|Event Model Decomposition]].
 
  
−
<center>
+
A quick view on the applied rule contents is provided. On the picture above, we display the contents of the rule named "∀ hyp mp" where an input has been used to instantiate an hypothesis.<br> One can see quickly which was the input used by the instanciation (following '''instantiated with'''), and which was the hypothesis considered by this rule (this is given by the hypothesis of '''Input Sequent''').<br>
−
[[Image:Decomposition.png]]
+
Furthermore, it is possible to view the antecedents created by this rule in details (i.e. child proof tree nodes) and the actions performed on hypotheses : selection, deselection, etc.
−
</center>
 
  
−
A non-decomposed machine has been decomposed in two sub-machines <math>M1</math> and <math>M2</math>, as illustrated by the figure.
+
== Auto-tactic and Post-tactic ==
−
<br>According to the terminology, <math>in\_a</math> and <math>a\_2\_b</math> are ''internal'' events of <math>M1</math>, and <math>b\_2\_c</math> and <math>out\_c</math> are ''internal'' events of <math>M2</math>. Concerning the variables, <math>a</math> and <math>m</math> are ''private'' variables of <math>M1</math>, <math>c</math> and <math>p</math> are ''private'' variables of <math>M2</math>, and <math>b</math>, <math>r</math> and <math>s</math> are ''shared'' variables.
 
−
<br>The variables accessed by the ''internal'' events of <math>M1</math> are <math>a</math>, <math>m</math>, <math>b</math>, <math>r</math> and <math>s</math>. The events modifying these variables are <math>in\_a</math>, <math>a\_2\_b</math>, which both are ''internal'' events of <math>M1</math>, and <math>b\_2\_c</math>, which is an ''internal'' event of <math>M2</math>. Thus, according to the definition given above, <math>b\_2\_c</math> is an ''external'' event for <math>M1</math>. In the same manner, <math>a\_2\_b</math> is an ''external'' event for <math>M2</math>.
 
  
−
''N.B.'': Note that the expression "is an ''external'' event for" is an extrapolation, and shall be literally interpreted as "should lead to the construction of an ''external'' event in".
+
The auto-tactic applies a combination (i.e. ordered list) of ''rewrite'', ''inference'' tactics and ''external provers'' automatically to newly generated proof obligations. However, they can also be invoked by the user by clicking on the [[Image:auto_prover.png]] button in the '''Proof Control''' view. Note that the automatic application of the auto-prover can be quickly toggled with the ''Prove automatically'' menu item available from the ''Project'' menu. See the picture below.
 +
[[Image:AutoPostTactics_Preference_Capture7.png|center]]
  
−
== Bibliography ==
+
The post-tactic is also a combination of ''rewrite'', ''inference'' tactics and ''external provers'', and is applied <u>automatically after each interactive proof step</u>. However, it can also be invoked manually by clicking on the [[Image:Broom_prover.gif]] button in the '''Proof Control''' view.
−
* J.R. Abrial, <font id="ancre_3">''The B-book: assigning programs to meanings''</font>, Cambridge University Press, 1996 (ISBN 0-521-49619-5).
 
−
* J.R. Abrial, Mathematical Models for Refinement and Decomposition, in ''The Event-B Book'', to be published in 2009 ([http://www.event-b.org/abook.html lien externe]).
 
−
* J.R. Abrial, <font id="ancre_1">''Event Model Decomposition''</font>, Version 1.3, April 2009.
 
−
* M. Butler, <font id="ancre_2">Decomposition Structures for Event-B</font>, in ''Integrated Formal Methods iFM2009'', Springer, LNCS 5423, 2009 ([http://eprints.ecs.soton.ac.uk/16965/1/butler.pdf lien externe]).
 
  
−
[[Category:Design]]
+
Note that the post-tactic can be disabled quickly by clicking on the little arrow (marked with an A on the figure below) of the '''Proof Control''' view (right upper corner) and then on "Disable post-tactic" (B):
−
[[Category:Work in progress]]
+
[[Image:Disable_xp_prover.png|center]]
 +
 
 +
=== Principles ===
 +
 
 +
The ordered list of  ''rewrite'', ''inference'' tactics and ''external provers'' that should be applied is called a '''profile'''. There are two default profiles, one for the auto-tactic and one for the post-tactic. These default profiles are immutable in time, but can be duplicated for further modification by the user. Indeed, the user can edit a profile and select it to run as automatic or post tactic. The idea is to have a set of available tactic profiles to be used as needed.
 +
Moreover, these edited profiles are shipped with projects if defined at this scope, or can be imported or exported if defined at a workspace level, which is very useful to share them.
 +
 
 +
There are two ways to run the automatic or post tactics:
 +
* the manual way consists into clicking on the [[Image:auto_prover.png]] button, or the [[Image:Broom_prover.gif]] button in the Proof Control view, to respectively launch the auto-tactic (with the selected auto-tactic profile) and the post-tactic (with the selected post-tactic profile).
 +
* the automatical way if such preference is activated. (Auto-tactic after each proof step, and post-tactic at each step and rebuild) The mandatory condition for post-tactics or auto-tactics to automatically run is that they should be activated from their preference or property.
 +
 
 +
The user can separately define tactic profiles and assign them to post and auto tactics. Therefore, there are two tabs in the "Auto/Post Tactic" preference page to address these choices. These tabs will be descibed in the two next sections.
 +
 
 +
=== Preferences for the selected auto and post tactic profile ===
 +
This section describes the "Auto/Post Tactic" tab of the "Auto/Post Tactic" preference page.
 +
 
 +
There are two scopes to set up preferences for the auto and post tactics : at workspace level, and at project level.
 +
Note that if the automatic application of tactics (auto or post) is decided only at workspace level, and this choice is held at project level.
 +
 
 +
To access these preferences, one as to go open the "Auto/Post Tactic" preference page that can be found after "Window > Preference > Sequent Prover".
 +
 
 +
The figure below shows the "Auto/Post Tactic" preference page:
 +
 
 +
[[Image:AutoPostTactic_Preference_Capture1.png|650px|center]]
 +
 
 +
The buttons 1 and 2 are activating/deactivating the automatic use of respectively auto and post tactics.
 +
One can also see on this picture the selected profile to be use as auto and post tactic.<br>
 +
'''Note that there is always a profile selected, and this profile can be changed whether the tactic are automatically launched or not, as there is alway a way to manually launch auto and post tactics.'''<br>
 +
On the preference appearing above, the ''Default Auto Tactic Profile'' is used to compose the automatic tactic, and the ''Default Post Tactic Profile'' is used to compose the post-tactic.
 +
 
 +
The figure below shows the "Auto/Post Tactic" Preference page with both auto-tactic and post-tactic to automatically run, and where the user selects the profile "MyFirstTacticProfile" to be used as auto-tactic profile.
 +
 
 +
[[Image:AutoPostTactic_Preference_Capture4.png|650px|center]]
 +
 
 +
=== Preferences for available profiles ===
 +
This section describes the "Profile" tab of the "Auto/Post Tactic" preference page.
 +
 
 +
[[Image:AutoPostTactic_Preference_Capture2.png|650px|center]]
 +
The figure above shows the contents of the profile tab.
 +
There are two visible lists : a list of profiles on the left the tactics or provers that compose these profiles (Profile Details). Here one can see the contents of the Defaut Auto Tactic Profile.
 +
 
 +
There are 4 buttons available to the user :
 +
*New : to create a new profile "from scratch", 
 +
*Edit : to edit an existing (editable) profile,
 +
*Remove : to remove a profile definitively,
 +
*Duplicate : to duplicate a selected profile for further slight modification,
 +
 
 +
Default profiles can not be edited nor removed. That is why they are greyed on the image above.
 +
 
 +
On the picture below appears the dialog available to edit or create a profile. Here we create a profile named 'MyFirstTacticProfile'.
 +
[[Image:AutoPostTactic_Preference_Capture3.png|650px|center]]
 +
 
 +
The list of the right represents the available and unselected tactics. The list of the left is the profile contents, and represents the selected tactics to be '''applied from the top to down'''.
 +
The user can select some available tactic from the list of the right using the ">>" button or unselect some tactics from the list of the left using the "<<" button.
 +
The user can re-order contiguous selection of selected tactics using the "Up" and "Down" button.
 +
By clicking on "Finish" the profile will be saved and available for use in the auto and post tactics.
 +
 
 +
=== Project specific settings ===
 +
The user can select profiles locally to project.
 +
To do so, one has to select the "Auto/Post Tactic" property page available from '''right-click > Properties''' on a project, or by clicking the '''Configure project specific settings''' link on the "Auto/Post Tactic" preference page. This property page appears on the picture below, opened on the Auto/Post tactic tab.
 +
[[Image:AutoPostTactic_Preference_Capture5.png|600px|center]]
 +
Note that the enablement of automatic use of post and auto tactics is decided at a workspace level.
 +
 
 +
The picture below 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 on right click from the list of defined profiles.
 +
[[Image:AutoPostTactic_Preference_Capture6.png|600px|center]]
 +
 
 +
This contextual menu offers two options to the user :
 +
*'''Import Workspace Profiles''' to retrieve all the defined profiles in the workspace,
 +
*'''Export to Workspace Profiles''' to push a selected profile up in the list of workspace profiles.
 +
 
 +
[[Category:User documentation|The Proving Perspective]]
 +
[[Category:Rodin Platform|The Proving Perspective]]
 +
[[Category:User manual|The Proving Perspective]]

Revision as of 16:28, 25 July 2011

<prev: The Event-B Explorer >next: The Mathematical Language ^up: User_Manual_index

Overview

When proof obligations (POs) are not discharged automatically the user can attempt to discharge them interactively using the Proving Perspective. This page provides an overview of the Proving Perspective and its use. If the Proving Perspective is not visible as a tab on the top right-hand corner of the main interface, the user can switch to it via "Window -> Open Perspective".

The Proving Perspective consists of a number of views: the Proof Tree, the Goal, the Selected Hypotheses, the Proof Control, the Search Hypotheses, the Cache Hypotheses and the Proof Information. In the discussion that follows we look at each of these views individually. Below is a screenshot of the Proving Perspective:

ProvPers.png

Loading a Proof

To work on an un-discharged PO it is necessary to load the proof into the Proving Perspective. To do this switch to the Proving Perspective; select the project from the Event-B Explorer; select and expand the component (context or machine); and finally select (double-click) the proof obligation of interest. A number of views will be updated with details of the corresponding proof.

ExplorerView.png

Note that pressing Discharged.gif button on the top left hand side of the Event-B Explorer will remove all discharged proof obligations (PO's) from the view.

The Proof Tree

The proof tree view provides a graphical representation of each individual proof step, as seen in the following screenshot:

ProTree.png

Each node in the tree corresponds to a sequent. A line is right shifted when the corresponding node is a direct descendant of the node of the previous line. Each node is labelled with a comment which indicates which rule has been applied, or which prover discharged the proof. By selecting a node in the proof tree, the corresponding sequent is loaded: the hypotheses of the sequent are loaded to the Selected Hypotheses window, and the goal of the sequent is loaded to the Goal view.

Decoration

The leaves of the tree are decorated with one of three icons:

  • Discharged.gif means that this leaf is discharged,
  • Pending.gif means that this leaf is not discharged,
  • Reviewed.gif means that this leaf has been reviewed.

Internal nodes in the proof tree are decorated in reverse colours. Note that a "reviewed" leaf is one that is not discharged yet by the prover. Instead, it has been "seen" by the user who decided to postpone the proof. Marking nodes as "reviewed" is very convenient since the provers will ignore these leaves and focus on specific areas of interest. This allows interactive proof in a gradual fashion. In order to discharge a "reviewed" node, select it and prune the tree at that node: the node will become "brown" again (undischarged) and you can now try to discharge it.

Navigation within the Proof Tree

On top of the proof tree view, one can see three buttons:

  • the "G" buttons allows you to see the goal of the sequent corresponding to each node,
  • the "+" button allows you to fully expand the proof tree,
  • the "-" allows you to fully collapse the tree: only the root stays visible.

Manipulating the Proof Tree

Hiding

The little square (with a "+" or "-" inside) next to each node in the proof tree allows you to expand or collapse the subtree starting at that node.

Pruning

The proof tree can be pruned at a selected node; the subtree of the selected node is removed from the proof tree. The selected node becomes a leaf and is decorated with Pending.gif . The proof activity can then be resumed from this node. After selecting a node in the proof tree pruning can be performed in two ways:

  • by right-clicking and then selecting "Prune",
  • by clicking on the Pn prover.gif button in the proof control view.

Note that after pruning, the post-tactic is not applied to the new current sequent. The post-tactic should be applied manually, if required, by clicking on the post-tactic button in the Proof Control view. This is useful, in particular, when you want to redo a proof from the beginning. The proof tree can be pruned at its root node and then the proof can proceed again, with invocation of internal or external provers; or with interactive proof.

Before pruning a particular node, the node (and its subtree) can be copied to the clipboard. If the new proof strategy subsequently fails, the copied version can be pasted back into the pruned node (see the next section).

Copy/Paste

By selecting a node in the proof tree and then right-clicking with the mouse, you can copy the part of the proof tree starting at that sequent (the node and its subtree). Pasting the node and subtree back in is done in a similar manner, with a right mouse click on a proof node. This allows reuse of part of a proof tree in the same, or even in another, proof.

Goal and Selected Hypotheses

The nodes in the proof tree view correspond to sequents. A user will work with one selected node, and thus one sequent, at a time; attempting various strategies in an effort to show that the sequent goal is true. The "Goal" and "Selected Hypotheses" views provide information to the user about the currently selected sequent. Here is an example:

GoalHyp.png

A hypothesis can be removed from the list of selected hypotheses by selecting the check the box situated next to it (you can click on several boxes) and then by clicking on the Remove.gif button at the top of the selected hypotheses window:

GoalHypSelect.png

Here is the result:

GoalHypSelectRes.png

Note that the deselected hypotheses are not lost: you can find them again using the Search Hypotheses Sh prover.gif button in the Proof Control view. Other buttons are used as follows:


  • Select all prover.gif select all hypotheses.


  • Inv prover.gif invert the selection.


  • Falsify prover.gif next to the goal - proof by contradiction 1: The negation of the goal becomes a selected hypothesis and the goal becomes "⊥".


  • Falsify prover.gif next to a selected hypothesis - proof by contradiction 2: The negation of the hypothesis becomes the goal and the negated goal becomes a selected hypothesis.


Applying Proof Rules

A user wishing to attempt an interactive proof has a number of proof rules available, and these may be either rewrite rules or inference rules. In the Goal and the Selected Hypotheses views various operators may appear in red coloured font. The red font indicates that some interactive proof rule(s) are applicable and may be applied as a step in the proof attempt. When the mouse hovers over such an operator a number of applicable rules may be displayed; the user may choose to apply one of the rules by clicking on it.

Other proof rules can be applied when green buttons appear in the Goal and Selected Hypotheses views. Examples are proof by contradiction Falsify prover.gif, that we have already encountered; and ConjI prover.gif for conjunction introduction in the goal.

ApplyRewRule.png

To instantiate a quantifier the user enters the desired expression in the box behind the quantifier and clicks on the quantifier:

InstQuantifier.png

Rewrite Rules

Rewrite rules are one-directional equalities (and equivalences) that can be used to simplify formulas (the goal or a single hypothesis). A rewrite rule is applied from left to right when its side condition holds; it can be applied either in the goal predicate, or in one of the selected hypotheses.

A rewrite rule is applied either automatically (A) or manually (M):

  • automatically, when post-tactics are run.
  • automatically, when auto-tactics are run.
  • manually, through an interactive command. These rules gather non equivalence laws, definition laws, distributivity laws and derived laws.

Automatic rewrite rules are equivalence simplification laws.

Each rule name indicates the rule's characteristics according to the following convention:

  • the law category: simplification law (SIMP), definition law (DEF), distributivity law (DISTRI), or else derived law (DERIV).
  • the root operator of the formula on the left-hand side of the rule, e.g. predicate AND, expression BUNION.
  • (optionally) the terminal elements on the left-hand side of the rule: special element (SPECIAL) such as the empty-set, type expression (TYPE), same element occurring more than once (MULTI), literal (LIT). A type expression is either a basic type (\intg, \Bool, any carrier set), or \pow(type expression), or type expression\cprodtype expression.
  • (optionally) some other description of a characteristic, e.g. left (L), right (R).

Rewrite rules having a symmetric operator on the left-hand side may also describe other rules. eg: the rule:

\True = \False \;\;\defi\;\; \bfalse

should also produce the rule:

\False = \True \;\;\defi\;\; \bfalse

For associative operators in connection with distributive laws as in:

P \land (Q~ {\color{red}{\lor}} \ldots \lor R)

it has been decided to highlight the first associative/commutative operator (the {\color{red}{\lor}} ). A menu is presented when hovering the mouse over the operator: the first menu option distributes all associative/commutative operators, the second option distributes only the first associative/commutative operator. In order to simplify the explanation we write associative/commutative operators with two parameters only. However, we must emphasise here, that generally we may have a sequence of more than two parameters. So, we write Q \lor R instead of Q \lor \ldots \lor R . Rules are sorted according to their purpose.

Rules marked with a star in the first column are implemented in the current prover. Rules without a star are planned for implementation.

Rewrite rules are split into:

They are also available in a single large page All Rewrite Rules.

Inference Rules

Inference rules (see Proof Rules) are applied either automatically (A) or manually (M).

Inference rules applied automatically are applied at the end of each proof step. They have the following possible effects:

  • they discharge the goal,
  • they simplify the goal and add a selected hypothesis,
  • they simplify the goal by decomposing it into several simpler goals,
  • they simplify a selected hypothesis,
  • they simplify a selected hypothesis by decomposing it into several simpler selected hypotheses.

Inference rules applied manually are used to perform an interactive proof. They can be invoked by clicking on the red highlighted operators in the goal or the hypotheses. A menu is presented when there are several options.

See Inference Rules list.

The Proof Control View

The Proof Control view contains the buttons which you can use to perform an interactive proof.

PControl.png

The Proof Control view offers a number of buttons whose effects we briefly describe next; moving from left to right on the toolbar:

  • (nPP) invokes the new predicate prover, a drop-down list indicates alternative strategies.
  • (R) indicates that a node has been reviewed: in an attempt by the user to carry out proofs in a stepwise fashion, they might decide to postpone the task of discharging some proofs until a later stage. To do this the proofs can be marked as reviewed by choosing the proof node and clicking on this button. This indicates that by visually checking the proof the user is convinced that they can discharge it later, but they do not want to do it right now.
  • (p0) the PP and ML provers can be invoked from the drop-down list using different forces.
  • (dc) do proof by cases: the proof is split into two branches. In the first branch:- the predicate supplied by the user is added to the Selected Hypotheses, and the user attempts to discharge this branch. In the second branch :- the predicate supplied by the user is negated and added to the Selected Hypotheses; the user then attempts to discharge this branch.
  • (ah) add a new lemma: the predicate in the editing area should be proved by the user. It is then added as a new selected hypothesis.
  • (ae) abstract expression: the expression in the editing area is given a fresh name.
  • the robot: invokes the auto-prover which attempts to discharge the goal. The auto-prover is applied automatically on all proof obligations after a "save" without any intervention of the user. Using this button, you can invoke the auto-prover within an interactive proof.
  • the post-tactic is executed ,
  • lasoo: load into the Selected Hypotheses window those hidden hypotheses that contain identifiers in common with the goal, and with the selected hypotheses.
  • backtrack form the current node (i.e., prune its parent),
  • scissors: prune the proof tree from the node selected in the proof tree,
  • Search Hypotheses: find hypotheses containing the character string in the editing area, and display in the Search Hypothesis view.
  • Cache Hypotheses: press this to display the "Cache Hypotheses" view. This view displays all hypotheses that are related to the current goal.
  • load the previous undischarged proof obligation,
  • load the next undischarged proof obligation,
  • (i) show information corresponding to the current proof obligation in the corresponding window. This information correspond to the elements that directly took part in the proof obligation generation (events, invariant, etc.),
  • goto the next pending node of the current proof tree,
  • load the next reviewed node of the current proof tree.
  • Disable/Enable Post-tactics: allows the user to choose whether post-tactics run after each interactive proof step.

The Smiley

The smiley can be one of three different colors: (1) red, indicates that the proof tree contains one or more undischarged sequents, (2) blue, indicates that all undischarged sequents of the proof tree have been reviewed, (3) green, indicates that all sequents of the proof tree are discharged.

The Editing Area

The editing area allows the user to supply parameters for proof commands. For example, when the user attempts to add a new hypothesis (by clicking on the lemma ah button), the new hypothesis should have been written by the user in the editing area.

ML/PP and Hypotheses

ML

ML (mono-lemma) prover appears in the drop-down list under the button (pp) as M0, M1, M2, M3, ML. The different configuration (e.g., M0) refer to the proof force of the ML prover. All hypotheses are passed to ML.

PP

PP (predicate prover) appears in the drop-down list under the button (pp) as P0, P1, PP.

  • P0 uses all selected hypotheses (the ones in Selected Hypotheses window).
  • P1 employs a lasoo operation to the selected hypotheses and the goal, and uses the resulting hypotheses.
  • PP uses all hypotheses.

The Search Hypotheses View

By typing a string in the Proof Control window and pressing the Search Hypotheses button a window is provided which contains the hypotheses having a character string in common with the one entered by the user in the editing area. For example, if we search for hypotheses involving the character string "cr", then after pressing the Search Hypothesis button on the proof control window, we obtain the following:

Um-0102.png

This view also integrates a "quick search" area (A), that allows us to search quickly hypotheses involving short character strings such as "cr". A search hypothesis button (B) that behaves the same as the button of the proving window, a refresh button (C) that updates the window manually for more control, and a drop down menu (D) to set the preferences of the view up.

By pressing return key or the button (B) (once a short string has been given in the input area (A)), hypotheses can be searched quickly as if we used the Proof Control as described before.

The drop down menu (D) is accessible to set some preferences over the searched hypotheses :

SearchHyp view menu.png

If we change preferences for the search, we might need to "update" manually the view with the button (C). By selecting "Consider hidden hypotheses in search" option, we can review all hypotheses that have been unselected in the selected hypotheses window(more info about selected/hidden hypotheses...).

SearchHyp.png

To move any of these hypotheses to the Selected Hypotheses window, select those required (using the check boxes) and press the Add.gif button. Adding these hypotheses to the selected hypotheses means that they will be visible to the prover. They can then be used during the next interactive proof phase.

To remove hypotheses from the Search Hypotheses window use the Remove.gif button. This button also appears above the selected hypotheses, and allows the user to remove any hypothesis from the Selected Hypotheses window.

The other button, situated to the left each hypotheses, is the Falsify prover.gif button. clicking on this will attempt a proof by contradiction. The effect is the same as if the hypothesis were in the Selected Hypotheses.

The Cache Hypotheses Window

This window allows the user to keep track of recently manipulated (e.g., used, removed, selected) hypotheses for any PO. For example, when the user applies a rewrite to an hypothesis, a new hypothesis (after the rewriting) is selected, and the original hypothesis is deselected and put in the Cache Hypotheses window.

Similar operations (to that of the Selected Hypotheses and Search Hypotheses windows) such as removing, selecting and proof by contradiction (ct) are also available for the cached hypotheses. Interactive proof steps (e.g., rewriting) can also be carried out from the Cache Hypotheses window as well as the Search Hypotheses window.

Proof Information View

This view displays information so that the user can relate a proof obligation to the model. For example, typical information for an event invariant preservation PO includes the event; as well as the invariant in question. In the following example, the hyperlinks 'CreateToken' and 'inv2' can be used to navigate to the containing machine.

PInfo.png

Rule Details View

This view displays the information relative to a given proof tree node, on which a rule was applied.
A command is available when right-clicking on a proof tree node, in order to reveal the Rule Details View (See picture below).

ShowRuleDetailsView.png

By default, this view is a fast view. A button (identified by the view's icon) is then available at the bottom left of the workbench, to show up this view.

Here is an overview of the Rule details view :

RuleDetailsView.png

A quick view on the applied rule contents is provided. On the picture above, we display the contents of the rule named "∀ hyp mp" where an input has been used to instantiate an hypothesis.
One can see quickly which was the input used by the instanciation (following instantiated with), and which was the hypothesis considered by this rule (this is given by the hypothesis of Input Sequent).
Furthermore, it is possible to view the antecedents created by this rule in details (i.e. child proof tree nodes) and the actions performed on hypotheses : selection, deselection, etc.

Auto-tactic and Post-tactic

The auto-tactic applies a combination (i.e. ordered list) of rewrite, inference tactics and external provers automatically to newly generated proof obligations. However, they can also be invoked by the user by clicking on the Auto prover.png button in the Proof Control view. Note that the automatic application of the auto-prover can be quickly toggled with the Prove automatically menu item available from the Project menu. See the picture below.

AutoPostTactics Preference Capture7.png

The post-tactic is also a combination of rewrite, inference tactics and external provers, and is applied automatically after each interactive proof step. However, it can also be invoked manually by clicking on the Broom prover.gif button in the Proof Control view.

Note that the post-tactic can be disabled quickly by clicking on the little arrow (marked with an A on the figure below) of the Proof Control view (right upper corner) and then on "Disable post-tactic" (B):

Disable xp prover.png

Principles

The ordered list of rewrite, inference tactics and external provers that should be applied is called a profile. There are two default profiles, one for the auto-tactic and one for the post-tactic. These default profiles are immutable in time, but can be duplicated for further modification by the user. Indeed, the user can edit a profile and select it to run as automatic or post tactic. The idea is to have a set of available tactic profiles to be used as needed. Moreover, these edited profiles are shipped with projects if defined at this scope, or can be imported or exported if defined at a workspace level, which is very useful to share them.

There are two ways to run the automatic or post tactics:

  • the manual way consists into clicking on the Auto prover.png button, or the Broom prover.gif button in the Proof Control view, to respectively launch the auto-tactic (with the selected auto-tactic profile) and the post-tactic (with the selected post-tactic profile).
  • the automatical way if such preference is activated. (Auto-tactic after each proof step, and post-tactic at each step and rebuild) The mandatory condition for post-tactics or auto-tactics to automatically run is that they should be activated from their preference or property.

The user can separately define tactic profiles and assign them to post and auto tactics. Therefore, there are two tabs in the "Auto/Post Tactic" preference page to address these choices. These tabs will be descibed in the two next sections.

Preferences for the selected auto and post tactic profile

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

There are two scopes to set up preferences for the auto and post tactics : at workspace level, and at project level. Note that if the automatic application of tactics (auto or post) is decided only at workspace level, and this choice is held at project level.

To access these preferences, one as to go open the "Auto/Post Tactic" preference page that can be found after "Window > Preference > Sequent Prover".

The figure below shows the "Auto/Post Tactic" preference page:

AutoPostTactic Preference Capture1.png

The buttons 1 and 2 are activating/deactivating the automatic use of respectively auto and post tactics. One can also see on this picture the selected profile to be use as auto and post tactic.
Note that there is always a profile selected, and this profile can be changed whether the tactic are automatically launched or not, as there is alway a way to manually launch auto and post tactics.
On the preference appearing above, the Default Auto Tactic Profile is used to compose the automatic tactic, and the Default Post Tactic Profile is used to compose the post-tactic.

The figure below shows the "Auto/Post Tactic" Preference page with both auto-tactic and post-tactic to automatically run, and where the user selects the profile "MyFirstTacticProfile" to be used as auto-tactic profile.

AutoPostTactic Preference Capture4.png

Preferences for available profiles

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

AutoPostTactic Preference Capture2.png

The figure above shows the contents of the profile tab. There are two visible lists : a list of profiles on the left the tactics or provers that compose these profiles (Profile Details). Here one can see the contents of the Defaut Auto Tactic Profile.

There are 4 buttons available to the user :

  • New : to create a new profile "from scratch",
  • Edit : to edit an existing (editable) profile,
  • Remove : to remove a profile definitively,
  • Duplicate : to duplicate a selected profile for further slight modification,

Default profiles can not be edited nor removed. That is why they are greyed on the image above.

On the picture below appears the dialog available to edit or create a profile. Here we create a profile named 'MyFirstTacticProfile'.

AutoPostTactic Preference Capture3.png

The list of the right represents the available and unselected tactics. The list of the left is the profile contents, and represents the selected tactics to be applied from the top to down. The user can select some available tactic from the list of the right using the ">>" button or unselect some tactics from the list of the left using the "<<" button. The user can re-order contiguous selection of selected tactics using the "Up" and "Down" button. By clicking on "Finish" the profile will be saved and available for use in the auto and post tactics.

Project specific settings

The user can select profiles locally to project. To do so, one has to select the "Auto/Post Tactic" property page available from right-click > Properties on a project, or by clicking the Configure project specific settings link on the "Auto/Post Tactic" preference page. This property page appears on the picture below, opened on the Auto/Post tactic tab.

AutoPostTactic Preference Capture5.png

Note that the enablement of automatic use of post and auto tactics is decided at a workspace level.

The picture below 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 on right click from the list of defined profiles.

AutoPostTactic Preference Capture6.png

This contextual menu offers two options to the user :

  • Import Workspace Profiles to retrieve all the defined profiles in the workspace,
  • Export to Workspace Profiles to push a selected profile up in the list of workspace profiles.
Retrieved from ‘https://wiki.event-b.org/index.php?title=Event_Model_Decomposition&oldid=10222’