Difference between pages "Rodin Proving Perspective" and "Tasking Event-B Tutorial"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Im06r
 
imported>Andy
 
Line 1: Line 1:
−
{{Navigation|Previous= [[The_Proof_Obligation_Explorer_(Rodin_User_Manual)|The Proof Obligation Explorer]]|Next= [[The_Mathematical_Language_(Rodin_User_Manual)|The Mathematical Language]]|Up= [[index_(Rodin_User_Manual)|User_Manual_index]]}}
+
For more information contact Andy Edmunds - University of Southampton - mailto:ae2@ecs.soton.ac.uk
−
{{TOCright}}
+
=== Tasking Event-B Tutorial Overview ===
−
== Overview ==
 
−
The Proving Perspective is made of a number of windows (views): the Proof Tree (see [[Rodin_Proving_Perspective#The_Proof_Tree]]), the Goal, the Selected Hypotheses, the Proof Control, the Search Hypotheses, the Cache Hypotheses and the Proof Information. In subsequent sections, we study each of these windows. Below is a screenshot of the proving perspective:
 
  
−
[[Image:ProvPers.png|center]]
+
<span style="color: RED">'''Caution''': This Page is under Construction - some parts are incomplete</span>
  
−
== Loading a Proof ==
+
This tutorial follows on from the abstract development described [http://wiki.event-b.org/index.php/Development_of_a_Heating_Controller_System here].
−
In order to load a proof, switch to the Proving Perspective, select the project from the Event-B Explorer, select and expand the component (context or machine), finally select the proof obligation of interest. The corresponding proof will be loaded.
 
  
−
== The Proof Tree ==
+
This code generation tutorial extends the Heating Controller tutorial example, and makes use of example projects from the download site. The code generation stage produces implementable Ada code, and also an Event-B model. It is a model of the implementation, and contains flow control variables that model the flow of execution through the task body. The Ada code is produced from an intermediate model that is not visible to the user. The Common Language model (CLM), is generated from the Tasking Event-B by a translation tool. Ada (and other implementations) may be generated from the CLM. An overview of Tasking Event-B can be found [http://wiki.event-b.org/index.php/Tasking_Event-B_Overview here].
−
The proof tree describe each individual proof step in the proof. The proof tree can be seen in its corresponding window as seen in the following screenshot:
 
  
−
[[Image:ProTree.png|center]]
+
In the example so far, the Heating Controller has been refined to the point where we wish to add implementation constructs. The Event-B language is not expressive enough to fully describe the implementation. Tasking Event-B facilitates this final step to implementation, by extending Event-B with the necessary constructs. Event-B machines modelling tasks, shared objects and the environment are identified, and  extended with the appropriate implementation details.
  
−
Each line in the tree corresponds to a node which is 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 (description) explaining how it can be discharged. 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 window.
+
The example/tutorial projects are are available in the [http://deploy-eprints.ecs.soton.ac.uk/304/ e-prints archive], or on [https://codegenerationd.svn.sourceforge.net/svnroot/codegenerationd/Examples/Heating_ControllerTutorial_v0.2.0/ SVN].
  
−
=== Decoration===
+
{| border="1"
−
The leaves of the tree are decorated with three kinds of logos:
+
|Heating_ControllerTutorial2_Completed
 +
|An example project with an environment simulation. The environment variables are monitored and controlled using subroutine calls. The project contains a complete Tasking Development with generated Event-B and Ada code.
 +
|-
 +
|Heating_ControllerTutorial2_Partial1
 +
|A project with the final decomposition completed, ready to begin Tasking Event-B Development.
 +
|-
 +
|Heating_ControllerTutorial2_Partial2
 +
|A partially completed tasking specification for the continuation of the tutorial.
 +
|-
 +
|TheoriesForCG
 +
|Contains the mathematical language translations; encoded as rules in a theory plug-in rule-base.
 +
|}
  
−
* a green logo with a "'''<math>\surd </math>'''" in it means that this leaf is discharged,
+
== Using the Tasking Extension ==
−
* a brown logo with a "'''?'''" in it means that this leaf is not discharged,
+
The steps needed to generate code from an Event-B model, in this tutorial, are as follows,
−
* a blue logo with a "'''R'''" in it means that this leaf has been reviewed.
+
* Step 1 - [[Tasking Event-B_Tutorial#Adding the Implementation Level Refinement|Adding the Implementation Level Refinement]]
 +
* Step 2 - [[Tasking Event-B_Tutorial#Pre-processing|Pre-processing]]
 +
* Step 3 - [[Tasking Event-B_Tutorial#Providing the Annotations for Implementations|Add Tasking annotations]].
 +
* Step 4 - [[Tasking Event-B_Tutorial#Invoking the Translation|Invoke translators]].
 +
=== Download and Copy the Theories ===
 +
The translations of the Event-B mathematical language to the target language constructs are specified as rules in the theory plug-in. Two rule files are included for the example, and are available in the [https://codegenerationd.svn.sourceforge.net/svnroot/codegenerationd/Examples/Heating_ControllerTutorial_v0.2.0/ SVN]. The files can be downloaded and copied into an Event-B project called ''MathExtensions''. The theory must then be deployed. Right-Click on the theory file and select deploy to do this. The non-Event-B project, the original download may now be deleted.
  
−
Internal nodes in the proof tree are decorated in the same (but lighter) way. 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 have it discharged later. Marking nodes as "reviewed" is very convenient in order to perform an 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.
+
=== Adding the Implementation Level Refinement ===
 +
The final decomposition generates the machines that are required for code generation. However, it is not possible to edit the machines since they are machine generated, and therefore this is prohibited. In order to be able to modify the models we will refine the generated machines. This is where we begin with the ''Heating_ControllerTutorial2_Partial1'' project. To refine the machines we can use the automatic refinement feature, but this presents us with two problems that are dealt with in the pre-processing step. It is also at this stage that any remaining non-deterministic constructs should be removed by replacing them with deterministic constructs.
  
−
=== Navigation within the Proof Tree===
+
TIP: Non-deterministic constructs cause strange characters to appear in the source code. If you see strange characters in the generated code, check for non-deterministic constructs in the implementation level machines.
−
On top of the proof tree window, one can see three buttons:
 
  
−
* the "'''G'''" buttons allows you to see the goal of the sequent corresponding to the node
+
Alter_Temperature_Sensor1 in Envir1Impl: action becomes ts1 := ts1 + 1
−
* the "'''+'''" button allows you to fully expand the proof tree
+
Alter_Temperature_Sensor2 in Envir1Impl: action becomes ts1 := ts1 + 1
−
* the "'''-'''" allows you to fully collapse the tree: only the root stays visible.
+
Alter_Heater_Status in Envir1Impl: action becomes hss := FALSE
 +
INITIALISATION in Heater_Monitor_TaskImpl: becomes shs := FALSE
  
−
=== Manipulating the Proof Tree===
+
We also need to add a typing flag to an invariant. We need to add it in only one place, and this is where an invariant is used type a variable, in the Heating Controller machine. The flag is used to guide the translator to the typing invariant. This is because there is more than one invariant involving that particular variable. They may also be added to guards where parameters are typed in guards, and the parameters are referred to in more than one guard.
  
−
==== Hiding ====
+
* Go to the ''Heater_Monitor_TaskImpl typing_shs'' invariant.
−
The little triangle (with a "+" or "-" inside) next to each node in the proof tree allows you to expand or collapse the subtree starting at that node.
+
* Add the typing flag, by right-clicking on the invariant and selecting typing from the menu.
  
−
==== Pruning ====
+
=== Pre-processing ===
−
The proof tree can be pruned from a node: it means that the subtree starting at that node is eliminated. The node in question becomes a leaf and is brown decorated. This allows you to resume the proof from that node. After selecting a sequent in the proof tree, pruning can be performed by right-clicking and then selecting "Prune".
 
  
−
Note that after pruning, the post-tactic is not applied to the new current sequent: if needed you have to press the "post-tactic" button in the Proof Control window. This happens in particular when you want to redo a proof from the beginning: you prune the proof tree from the root node and then you have to press the "post-tactic" button in order to be in exactly the same situation as the one delivered automatically initially.
+
The pre-processing step should be a temporary, the solutions can be incorporated into the tool to automatically perform the changes that are required.  
  
−
When you want to redo a proof from a certain node, it might be advisable to do it after copying the tree so that in case your new proof fails you can still resume the previous situation by pasting the copied version (see next section).
+
* The Code Generator requires a flattened version of each machine; all of the Event-B elements should be available in the implementation level machine.
 +
* Composed machines are not currently able to be refined, so anything that requires synchronization of events requires some manual updates.
  
−
==== Copy/Paste ====
+
===== 'Flattening' the Implementation Machines =====
  
−
By selecting a node in the proof tree and then clicking on the right key of the mouse, you can copy the part of the proof tree starting at that sequent: it can later be pasted in the same way. This allows you to reuse part of a proof tree in the same (or even another) proof.
+
The temporary solution for flattening:
 +
* Make events ''not extended''.
 +
* Copy missing invariants.
  
−
== Goal and Selected Hypotheses ==
+
I found the Event-B Machine Editor's synthesis view useful for this. Invariants can be copy-pasted into the implementation machine from the abstraction. (A dummy invariant can be added and selected for pasting)
−
The "Goal" and "Selected Hypotheses" windows display the current sequent you have to prove at a given moment in the proof. Here is an example:
 
−
[[Image:GoalHyp.png|center]]
 
  
−
A selected hypothesis can be deselected (and as a result becomes hidden) by first clicking in the box (check box) situated next to it (you can click on several boxes) and then by pressing the red ('''-''') button at the top of the selected hypothesis window:
+
===== Providing the correct Composed Machine =====
  
−
[[Image:GoalHypSelect.png|center]]
+
The composed machine problem is sub-divided into two sub-problems. Firstly composed machines cannot be refined, and secondly when a machine is further decomposed there is no link between the first composed machine and the newly generated composed machine. So one or both of these problems may occur, depending on the number of decompositions.
  
−
Here is the result:
+
We must manually add the information to the composed machines to address these two problems.
  
−
[[Image:GoalHypSelectRes.png|center]]
+
The temporary solution for composed machines:
 +
* Modify the lowest level decomposed machine, HCtrl_M1_cmp, to ''include'' the implementation level machines (task names ending in *Impl). To do this,
 +
* open the composed machine editor. Open the INCLUDES edit feature.
 +
* Select the second drop-down box and find the *Impl version of each machine.
 +
* Save the composed machine.
 +
* Now add missing synchronizations to the composed machine. Add the ''Envir1Impl'' to the includes of HCtrl_M1_cmp.
 +
* Each composed event in the task, that synchronizes with the Environ machine, must have the remote event synchronization added manually. This can only be done by inspection of each composed event. We need to update Sense_Temperatures, Display_Current_Temperature, Actuate_OverHeat_Alram, Actuate_Heat_Source, Sense_Heater_Status, Actuate_NoHeat_Alarm, Sense_PressIncrease_Target_Temperature, Sense_PressDecrease_Target_Temperature, Display_Target_Temperature. One by one, expand the events in the composed events section of the composed machine editor; add a new event in the combines events section, select ''Envir1Impl'' and add the synchronizing event from the list-box to the right.
  
−
Notice that the deselected hypotheses are not lost: you can get them back by means of the Search Hypotheses window. The other two buttons next to the red ('''-''') button allow the user (in the order of their appearance from left to right) to select all hypotheses as well as inverse the current selection.  
+
=== Adding Tasking Event-B ===
 +
Each Machine should be completed as follows.
 +
==== The Temp_Ctrl_TaskImpl Machine ====
 +
Continuing with the tutorial project ''Heating_ControllerTutorial2_Partial2'', we need to make changes to the following machines. During the tutorial we will cut and paste from ''Heating_ControllerTutorial2_Completed'' model when, specifying the task bodies, to save typing.
  
−
The ('''ct''') button next to the goal allows you to do a proof by contradiction: by pressing it, the negation of the goal becomes a selected hypothesis whereas the goal becomes "'''⊥'''".  
+
*Add the ''Auto Task'' extension.
 +
**Right-Click on the Machine node in the Rose tree-editor,  
 +
**and click on ''New Child Element/Auto Task Machine'' menu option.
  
−
The ('''ct''') button next to a selected hypothesis allows you to do another kind of proof by contradiction: by pressing it, the negation of the concerned hypothesis becomes the goal whereas the negated goal becomes an hypothesis.
+
''Auto Tasks'' are tasks that will be declared and defined in the ''Main'' procedure of the implementation. The effect of this is that the ''Auto Tasks'' are created when the program first loads, and then activated (made ready to run) before the ''Main'' procedure body runs.  
  
−
=== Applying Proof Rules ===
+
*'''Edit the TaskBody'''.
−
The red hyperlinks as well as the ('''ct''') buttons (also occasionally other green filled buttons next to it e.g., AND introduction in goal) allows the user to carry out interactive proofs. They are used to invoke proof rules (rewrite rules as well as inference rules).
+
**Open the properties editor for the task body.
 +
**Copy and paste the task body from ''Heating_ControllerTutorial2_Completed/Temp_Ctrl_Task1Impl''
 +
**Set the task type to ''Periodic'',
 +
**Set a period of 250 milliseconds.  
 +
**Click on the Set Task Body button.
  
−
[[Image:ApplyRewRule.png|center]]
+
The task body is parsed, and if successful will add the structure to the EMF tree. If parsing is not successful an error panel will display the source of the error.
  
−
==== Rewrite Rules ====
+
We now look at the sensing event ''Sense_Temperatures'' event in ''Temp_Ctrl_TaskImpl''. In order to assist with the translation we add the following annotation:
−
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 either in the goal or in one of the selected hypotheses, when its ''side condition'' holds.
 
  
−
A rewrite rule is applied either automatically ('''A''') or manually ('''M'''):
+
*'''Add a Sensed Event Annotation'''.
−
* automatically, when post tactics are enabled. These rules are equivalence simplification laws.
+
** Right-click on the ''Sense_Temperatures'' Event node.
−
* manually, through an interactive command. These rules gathers non equivalence laws, definition laws, distributivity laws and derived laws.
+
** Select ''New Child/Implementation'' from the menu.
 +
** Go to the Implementation properties view and set the ''Implementation Type'' property to ''Sensing''.
  
−
Each rule is named after the following elements:
+
We now look at the actuating event ''Display_Current_Temperatures'' event in ''Temp_Ctrl_TaskImpl''. In order to assist with the translation we add the following annotation:
  
−
* The law category: simplification law (SIMP), definition law (DEF), distributivity law (DISTRI), or else derived law (DERIV).
+
*'''Add an Actuating Event Annotation'''.
−
* Particularity on terminal elements of the left part of the rule (optional): special element (SPECIAL) such as the empty-set, type expression (TYPE), same element occurring more then 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.
+
** Right-click on the ''Display_Current_Temperatures'' Event node.
−
* One or more elements describing from top to down the left part of the rule, eg. predicate AND, expression BUNION.
+
** Select ''New Child/Implementation'' from the menu.
−
* Detail to localize those elements (optional): left (L), right (R).
+
** Go to the Implementation properties view and set the ''Implementation Type'' property to ''Actuating''.
  
−
Rewrite rules having an equivalence operator in their left part may also describe other rules. eg: the rule:
+
==== The Shared Machine ====
  
−
<center><math>  \True  = \False  \;\;\defi\;\;  \bfalse </math></center>
+
The next step is to identify the ''Shared_ObjectImpl'' machine as a ''Shared Machine''.
 +
* Right-click on the ''Shared_Object'' Machine node in the Rose tree-editor.
 +
* Select ''New Child/Shared Machine'' from the menu.
  
−
should also produce the rule:
+
==== The Environ Machine ====
 +
In the prepared machine we have identified the ''Envir1Impl'' as an ''Environ Machine'', by adding the ''Environ Machine'' extension. ''Envir1Impl'' models a task that simulates the environment, and can be used to generate simulation code. For deployment in a non-simulated environment the environ machine's generated code can be ignored; we provide details of non-simulated code using addressed variables later. As before, a screenshot is available [http://wiki.event-b.org/images/Envir1Impl_2.pdf here]. In the prepared Environment Machine we have already set task type to ''Periodic'' extension, and set a period of 100 milliseconds.
 +
 +
We will now complete the sequence that has been partially defined in the task body. The following specification models simulation of a temperature change; the temperature value is represented by a monitored variable in the environment. The generated code simulates the temperature change in the environment by changing the monitored value. 
  
−
<center><math>  \False  = \True  \;\;\defi\;\;  \bfalse </math></center>
+
*'''Model Temperature Change in the environment'''.
 +
??????
  
−
For associative operators in connection with distributive laws as in:
+
* Output to the screen during the simulation can be specified as follows:
 +
??????
  
−
<center><math> P \land (Q \lor \ldots \lor R) </math></center>
+
The generated code will print the text, and the value of the variable, to the screen.
  
−
it has been decided to put the "button" on the first associative/commutative operator (here <math>\lor </math>). Pressing that button will generate a menu: the first option of this menu will be to distribute all associative/commutative operators, the second option will be to distribute only the first associative/commutative operator. In the following presentation, to simplify matters, we write associative/commutative operators with two parameters only, but it must always be understood implicitly that we have a sequence of them. For instance, we shall never write <math> Q \lor \ldots \lor R </math> but <math> Q \lor R </math> instead. Rules are sorted according to their purpose.
+
The final step is to complete the ''ENSense_Temperatures'' event. The event is a sensing event, sensing is a kind of synchronisation, it synchronises with the ''TCSense_Temperatures'' event in the ''Temp_Ctrl_Task1'' tasking machine. We add formal parameters annotations corresponding to the actual parameters that we have already defined in the task.
  
−
Rules marked with a star in the first column are implemented in the current prover. Rules without a star are planned for implementation.
+
*'''Add a Sensed Event Annotation'''.
 +
** Right-click on the ''Sense_Temperatures'' Event node.
 +
** Select ''New Child/Implementation'' from the menu.
 +
** Go to the Implementation properties view and set the ''Implementation Type'' property to ''Sensing''.
  
−
Rewrite rules are split into:
+
*'''Add an Actuating Event Annotation'''.
 +
** Right-click on the ''Display_Current_Temperatures'' Event node.
 +
** Select ''New Child/Implementation'' from the menu.
 +
** Go to the Implementation properties view and set the ''Implementation Type'' property to ''Actuating''.
  
−
* [[Set Rewrite Rules]]
+
=== A Summary of Steps ===
−
* [[Relation Rewrite Rules]]
+
For a Tasking Machine definition:
−
* [[Arithmetic Rewrite Rules]]
+
# Add the Tasking Machine type (Auto etc).
 +
# Set the task type (Periodic etc.).
 +
# Set the task priority.
 +
# Specify the task body.
 +
# For sensing/actuating events, add the Event Type.
  
−
They are also available in a single large page [[All Rewrite Rules]].
+
For a Shared Machine definition:
 +
# Add the ''SharedMachine'' Machine type.
  
−
==== Inference Rules ====
+
For an Environ Machine definition:
−
Inference rules (see [[Proof Rules]]) are applied either automatically (A) or manually (M).
+
# Make the type an Environ Machine type.
 +
# Set the task type Periodic; a shorter period than the shortest task period is best for simulation.
 +
# Set the task priority.
 +
# Specify the task body, it will contain a simulation of changes in the environment.
 +
# For each sensing/actuating event, add the Event Type.
  
−
Inference rules applied automatically are applied at the end of each proof step. They have the following possible effects:
+
== Invoking the Translators ==
  
−
* they discharge the goal,
+
* To generate Ada code,
−
* they simplify the goal and add a selected hypothesis,
+
** Right-Click on the composed machine, or any tasking machine in the development, select ''Code Generation/Translate Event-B to Ada''.
−
* they simplify the goal by decomposing it into several simpler goals,
+
** Open the generated ''code'' directory in the project to view the source files. A refresh will be necessary to make the code visible. The .gpr file has been provided for AdaCore GPS users.
−
* 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 pressing "buttons" which corresponds to emphasized (red) operators in the goal or the hypotheses. A menu is proposed when there are several options.
+
* To create the Event-B model of the implementation,
 +
** Right-Click on the composed machine, or any tasking machine in the development, select ''Code Generation/Translate Tasking Event-B to Event-B''.
 +
** The Event-B model should be updated with the flow control variables. Users are not able to manually edit the generated elements. The additions can be removed using the menu option ''Code Generation/Remove Generated Event-B''
  
−
See [[Inference Rules]] list.
+
== Generated Code ==
 +
The Ada Code generated by the translator is available at the following links:
  
−
== The Proof Control Window ==
+
for simulation of environment without addressed variables, [http://wiki.event-b.org/images/Code_Heating_ControllerTutorial_Completed.pdf Heating_ControllerTutorial_Completed]
  
−
The Proof Control window contains the buttons which you can use to perform an interactive proof.
+
for simulation of environment with addressed variables, [http://wiki.event-b.org/images/Code_Heating_Controller5AddressedSim_Completed.pdf Heating_Controller5AddressedSim_Completed]
  
−
[[Image:PControl.png|center]]
+
Removal of the environment task from the ''Heating_Controller5AddressedSim_Completed'' should be deployable.
  
−
The Proof Control window offers a number of buttons which we succinctly describe from left to right:
+
[[Category:User documentation]]
−
 
 
−
* ('''nPP'''): the new predicate prover.
 
−
* ('''R''') review: in an attempt by the user to carry out proofs in a gradual fashion, they might decide to postpone the task of discharging some interactive proofs for a later stage.  In this case they have the possibility to mark these proofs as reviewed by choosing the proof node and pressing this button.  This means that by visually checking this proof, the user is convinced that they can discharge it later but they do not want to do it right now.
 
−
* ('''p0'''): the prover PP and ML can be invoked from the drop-down list.
 
−
* ('''dc''') proof by cases: the goal is proved first under the predicate written in the editing area and then under its negation.
 
−
* ('''ah''') lemma: the predicate in the editing area is proved and then added as a new selected hypothesis.
 
−
* ('''ae''') abstract expression: the expression in the editing area is given a fresh name.
 
−
* '''the robot''': the auto-prover attempts to discharge the goal. The auto-prover is the one which is applied automatically on all proof obligations (as generated automatically by the proof obligation generator after a "save") without any intervention of the user. With this button, you can call the auto-prover within an interactive proof.
 
−
* the '''post-tactic''' is executed (see section [[The_Proving_Perspective_(Rodin_User_Manual)#The Automatic Post-tactic|6.8]]),
 
−
* '''lasoo''': load in the Selected Hypotheses window those hidden hypotheses containing identifiers which are common with identifiers in the goal and 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,
 
−
* show (in the '''Search Hypotheses''' window) hypotheses containing the character string as in the editing area,
 
−
* '''Cache Hypotheses''' Button: by pressing ''"Cache Hypotheses"'' button the tool displays 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 take three different colors: (1) red, meaning that the proof tree contains one or more undischarged sequents, (2) blue, meaning that all undischarged sequents of the proof tree have been reviewed, (3) green, meaning that all sequents of the proof tree are discharged.
 
−
 
 
−
=== The Editing Area ===
 
−
The editing area allows the user to supply parameters to certain proof commands. For example, when the user attempts to add a new hypothesis (by pressing the lemma '''ah''' button), the new hypothesis should be written by the user in the editing area.
 
−
 
 
−
== The Search Hypotheses Window ==
 
−
 
 
−
By typing a string in the editing area of 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.
 
−
 
 
−
[[Image:SearchHyp.png|center]]
 
−
 
 
−
In the next step, any of these hypotheses can be selected (box checked), and then by pressing the '''(+)''' button, they will be moved to the '''Selected Hypotheses''' window. Adding these hypotheses to the set of selected hypotheses means that they will be visible to the prover. This means that they can be used during the next interactive proof phase.
 
−
 
 
−
Accordingly by selecting any numbers of hypotheses and pressing the '''(-)''' they will be removed from the '''Search Hypotheses''' window. The '''(-)''' button also appears above the selected hypotheses, and allow the user to remove any hypothesis form the '''Selected Hypotheses''' window.
 
−
 
 
−
The other button which is situated in the left-hand-side of all hypotheses is the '''(ct)''' button. Pressing the '''(ct)''' button next to a hypothesis in the '''Search Hypotheses''' window achieves proof by contradiction. This has the same effect as selecting (making it part of the '''Selected Hypothesis''' window) that hypothesis, and then pressing the ('''ct''') button next to it in the '''Selected Hypotheses''' window.
 
−
 
 
−
== 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 that can be used to relate the proof obligation to the model. For example, typical information for an event invariant preservation PO include the event as well as the invariant in question.
 
−
 
 
−
[[Image:PInfo.png|center]]
 
−
 
 
−
== Auto-tactics and Post-tactics ==
 
−
 
 
−
Auto-tactics apply a combination of ''rewrite'', ''inference'' and ''external provers'' to newly generated proof obligations. However, they can also be called upon by the user by pressing the ('''robot''') button in the '''Proof Control''' window.
 
−
 
 
−
Post-tactics are applied automatically after each interactive proof step. However, they can also be invoked manually by the user by pressing the ('''''') button in the '''Proof Control''' window.
 
−
 
 
−
In this section, we present the various rewrite or inference rules which are applied automatically as a systematic post-tactic after each proof step. Note that the post-tactic can be disabled by using the "'''P'''<math>\! \! \! \! /</math>" button situated on the right of the proof control window.
 
−
 
 
−
The post-tactic is made of two different rules: rewrite rules, which are applied on any sub-formula of the goal or selected hypotheses (section [[The_Proving_Perspective_(Rodin_User_Manual)#Rewrite Rules|6.8.1]]) and inference rules which are applied on the current sequent (section [[The_Proving_Perspective_(Rodin_User_Manual)#Automatic Inference Rules|6.8.2]]).
 
−
 
 
−
 
 
−
 
 
−
 
 
−
 
 
−
=== Preferences for the Post-tactic ===
 
−
 
 
−
The post-tactic can be configured by means of a preference page which can be obtained as follows: press the "Window" button on the top tooolbar. On the coming menu, press the "Preferences" button. On the coming menu, press the "Event-B" menue, then the "Sequent Prover’, and finally the "Post-Tactic" button. This yilds the following window:
 
−
 
 
−
[[Image:um-0147.png|center]]
 
−
 
 
−
In the left part you can see the ordered sequence of individual tactics composing the post-tactic, whereas the right part contains further tactics you can incorporate in the left part. By selecting a tactic you can move it from on part to the other or change the order in the left part.
 
−
 
 
−
 
 
−
[[Category:User documentation|The Proving Perspective]]
 
−
[[Category:Rodin Platform|The Proving Perspective]]
 
−
[[Category:User manual|The Proving Perspective]]
 

Revision as of 14:07, 1 December 2011

For more information contact Andy Edmunds - University of Southampton - mailto:ae2@ecs.soton.ac.uk

Tasking Event-B Tutorial Overview

Caution: This Page is under Construction - some parts are incomplete

This tutorial follows on from the abstract development described here.

This code generation tutorial extends the Heating Controller tutorial example, and makes use of example projects from the download site. The code generation stage produces implementable Ada code, and also an Event-B model. It is a model of the implementation, and contains flow control variables that model the flow of execution through the task body. The Ada code is produced from an intermediate model that is not visible to the user. The Common Language model (CLM), is generated from the Tasking Event-B by a translation tool. Ada (and other implementations) may be generated from the CLM. An overview of Tasking Event-B can be found here.

In the example so far, the Heating Controller has been refined to the point where we wish to add implementation constructs. The Event-B language is not expressive enough to fully describe the implementation. Tasking Event-B facilitates this final step to implementation, by extending Event-B with the necessary constructs. Event-B machines modelling tasks, shared objects and the environment are identified, and extended with the appropriate implementation details.

The example/tutorial projects are are available in the e-prints archive, or on SVN.

Heating_ControllerTutorial2_Completed An example project with an environment simulation. The environment variables are monitored and controlled using subroutine calls. The project contains a complete Tasking Development with generated Event-B and Ada code.
Heating_ControllerTutorial2_Partial1 A project with the final decomposition completed, ready to begin Tasking Event-B Development.
Heating_ControllerTutorial2_Partial2 A partially completed tasking specification for the continuation of the tutorial.
TheoriesForCG Contains the mathematical language translations; encoded as rules in a theory plug-in rule-base.

Using the Tasking Extension

The steps needed to generate code from an Event-B model, in this tutorial, are as follows,

Download and Copy the Theories

The translations of the Event-B mathematical language to the target language constructs are specified as rules in the theory plug-in. Two rule files are included for the example, and are available in the SVN. The files can be downloaded and copied into an Event-B project called MathExtensions. The theory must then be deployed. Right-Click on the theory file and select deploy to do this. The non-Event-B project, the original download may now be deleted.

Adding the Implementation Level Refinement

The final decomposition generates the machines that are required for code generation. However, it is not possible to edit the machines since they are machine generated, and therefore this is prohibited. In order to be able to modify the models we will refine the generated machines. This is where we begin with the Heating_ControllerTutorial2_Partial1 project. To refine the machines we can use the automatic refinement feature, but this presents us with two problems that are dealt with in the pre-processing step. It is also at this stage that any remaining non-deterministic constructs should be removed by replacing them with deterministic constructs.

TIP: Non-deterministic constructs cause strange characters to appear in the source code. If you see strange characters in the generated code, check for non-deterministic constructs in the implementation level machines. 

Alter_Temperature_Sensor1 in Envir1Impl: action becomes ts1 := ts1 + 1
Alter_Temperature_Sensor2 in Envir1Impl: action becomes ts1 := ts1 + 1
Alter_Heater_Status in Envir1Impl: action becomes hss := FALSE
INITIALISATION in Heater_Monitor_TaskImpl: becomes shs := FALSE

We also need to add a typing flag to an invariant. We need to add it in only one place, and this is where an invariant is used type a variable, in the Heating Controller machine. The flag is used to guide the translator to the typing invariant. This is because there is more than one invariant involving that particular variable. They may also be added to guards where parameters are typed in guards, and the parameters are referred to in more than one guard.

  • Go to the Heater_Monitor_TaskImpl typing_shs invariant.
  • Add the typing flag, by right-clicking on the invariant and selecting typing from the menu.

Pre-processing

The pre-processing step should be a temporary, the solutions can be incorporated into the tool to automatically perform the changes that are required.

  • The Code Generator requires a flattened version of each machine; all of the Event-B elements should be available in the implementation level machine.
  • Composed machines are not currently able to be refined, so anything that requires synchronization of events requires some manual updates.
'Flattening' the Implementation Machines

The temporary solution for flattening:

  • Make events not extended.
  • Copy missing invariants.

I found the Event-B Machine Editor's synthesis view useful for this. Invariants can be copy-pasted into the implementation machine from the abstraction. (A dummy invariant can be added and selected for pasting)

Providing the correct Composed Machine

The composed machine problem is sub-divided into two sub-problems. Firstly composed machines cannot be refined, and secondly when a machine is further decomposed there is no link between the first composed machine and the newly generated composed machine. So one or both of these problems may occur, depending on the number of decompositions.

We must manually add the information to the composed machines to address these two problems.

The temporary solution for composed machines:

  • Modify the lowest level decomposed machine, HCtrl_M1_cmp, to include the implementation level machines (task names ending in *Impl). To do this,
  • open the composed machine editor. Open the INCLUDES edit feature.
  • Select the second drop-down box and find the *Impl version of each machine.
  • Save the composed machine.
  • Now add missing synchronizations to the composed machine. Add the Envir1Impl to the includes of HCtrl_M1_cmp.
  • Each composed event in the task, that synchronizes with the Environ machine, must have the remote event synchronization added manually. This can only be done by inspection of each composed event. We need to update Sense_Temperatures, Display_Current_Temperature, Actuate_OverHeat_Alram, Actuate_Heat_Source, Sense_Heater_Status, Actuate_NoHeat_Alarm, Sense_PressIncrease_Target_Temperature, Sense_PressDecrease_Target_Temperature, Display_Target_Temperature. One by one, expand the events in the composed events section of the composed machine editor; add a new event in the combines events section, select Envir1Impl and add the synchronizing event from the list-box to the right.

Adding Tasking Event-B

Each Machine should be completed as follows.

The Temp_Ctrl_TaskImpl Machine

Continuing with the tutorial project Heating_ControllerTutorial2_Partial2, we need to make changes to the following machines. During the tutorial we will cut and paste from Heating_ControllerTutorial2_Completed model when, specifying the task bodies, to save typing.

  • Add the Auto Task extension.
    • Right-Click on the Machine node in the Rose tree-editor,
    • and click on New Child Element/Auto Task Machine menu option.

Auto Tasks are tasks that will be declared and defined in the Main procedure of the implementation. The effect of this is that the Auto Tasks are created when the program first loads, and then activated (made ready to run) before the Main procedure body runs.

  • Edit the TaskBody.
    • Open the properties editor for the task body.
    • Copy and paste the task body from Heating_ControllerTutorial2_Completed/Temp_Ctrl_Task1Impl
    • Set the task type to Periodic,
    • Set a period of 250 milliseconds.
    • Click on the Set Task Body button.

The task body is parsed, and if successful will add the structure to the EMF tree. If parsing is not successful an error panel will display the source of the error.

We now look at the sensing event Sense_Temperatures event in Temp_Ctrl_TaskImpl. In order to assist with the translation we add the following annotation:

  • Add a Sensed Event Annotation.
    • Right-click on the Sense_Temperatures Event node.
    • Select New Child/Implementation from the menu.
    • Go to the Implementation properties view and set the Implementation Type property to Sensing.

We now look at the actuating event Display_Current_Temperatures event in Temp_Ctrl_TaskImpl. In order to assist with the translation we add the following annotation:

  • Add an Actuating Event Annotation.
    • Right-click on the Display_Current_Temperatures Event node.
    • Select New Child/Implementation from the menu.
    • Go to the Implementation properties view and set the Implementation Type property to Actuating.

The Shared Machine

The next step is to identify the Shared_ObjectImpl machine as a Shared Machine.

  • Right-click on the Shared_Object Machine node in the Rose tree-editor.
  • Select New Child/Shared Machine from the menu.

The Environ Machine

In the prepared machine we have identified the Envir1Impl as an Environ Machine, by adding the Environ Machine extension. Envir1Impl models a task that simulates the environment, and can be used to generate simulation code. For deployment in a non-simulated environment the environ machine's generated code can be ignored; we provide details of non-simulated code using addressed variables later. As before, a screenshot is available here. In the prepared Environment Machine we have already set task type to Periodic extension, and set a period of 100 milliseconds.

We will now complete the sequence that has been partially defined in the task body. The following specification models simulation of a temperature change; the temperature value is represented by a monitored variable in the environment. The generated code simulates the temperature change in the environment by changing the monitored value.

  • Model Temperature Change in the environment.

??????

  • Output to the screen during the simulation can be specified as follows:

??????

The generated code will print the text, and the value of the variable, to the screen.

The final step is to complete the ENSense_Temperatures event. The event is a sensing event, sensing is a kind of synchronisation, it synchronises with the TCSense_Temperatures event in the Temp_Ctrl_Task1 tasking machine. We add formal parameters annotations corresponding to the actual parameters that we have already defined in the task.

  • Add a Sensed Event Annotation.
    • Right-click on the Sense_Temperatures Event node.
    • Select New Child/Implementation from the menu.
    • Go to the Implementation properties view and set the Implementation Type property to Sensing.
  • Add an Actuating Event Annotation.
    • Right-click on the Display_Current_Temperatures Event node.
    • Select New Child/Implementation from the menu.
    • Go to the Implementation properties view and set the Implementation Type property to Actuating.

A Summary of Steps

For a Tasking Machine definition:

  1. Add the Tasking Machine type (Auto etc).
  2. Set the task type (Periodic etc.).
  3. Set the task priority.
  4. Specify the task body.
  5. For sensing/actuating events, add the Event Type.

For a Shared Machine definition:

  1. Add the SharedMachine Machine type.

For an Environ Machine definition:

  1. Make the type an Environ Machine type.
  2. Set the task type Periodic; a shorter period than the shortest task period is best for simulation.
  3. Set the task priority.
  4. Specify the task body, it will contain a simulation of changes in the environment.
  5. For each sensing/actuating event, add the Event Type.

Invoking the Translators

  • To generate Ada code,
    • Right-Click on the composed machine, or any tasking machine in the development, select Code Generation/Translate Event-B to Ada.
    • Open the generated code directory in the project to view the source files. A refresh will be necessary to make the code visible. The .gpr file has been provided for AdaCore GPS users.
  • To create the Event-B model of the implementation,
    • Right-Click on the composed machine, or any tasking machine in the development, select Code Generation/Translate Tasking Event-B to Event-B.
    • The Event-B model should be updated with the flow control variables. Users are not able to manually edit the generated elements. The additions can be removed using the menu option Code Generation/Remove Generated Event-B

Generated Code

The Ada Code generated by the translator is available at the following links:

for simulation of environment without addressed variables, Heating_ControllerTutorial_Completed

for simulation of environment with addressed variables, Heating_Controller5AddressedSim_Completed

Removal of the environment task from the Heating_Controller5AddressedSim_Completed should be deployable.

Retrieved from ‘https://wiki.event-b.org/index.php?title=Rodin_Proving_Perspective&oldid=10028’