Difference between pages "Code Generation Activity" and "Extending the Static Checker (How to extend Rodin Tutorial)"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Andy
 
imported>Pascal
 
Line 1: Line 1:
Tasking Event-B is the extension of Event-B for defining concurrent systems sharing data, for details see the [[Tasking Event-B Overview]] page. For more information contact Andy Edmunds - University of Southampton - mailto:ae2@ecs.soton.ac.uk, or Chris Lovell mailto:cjl3@ecs.soton.ac.uk
+
{{Navigation|Previous= [[Extending_the_Static_Checker(How_to_extend_Rodin_Tutorial)]] | Up= [[Plug-in_Tutorial|How to extend Rodin Tutorial (Index)]] | Next= }}
=== Code Generation Feature - Version 0.2.2 For Rodin 2.4===
 
<13th MARCH 2012> THIS PAGE, AND IT'S CONTENT IS UNDERGOING MAINTENEANCE
 
  
The release is imminent !!!
+
=== In this part ===
  
Changes made to the interface and translation from theories.
+
We will see how to add rules to statically check the machines after our extension. The Static Checker (SC) is one dedicated part of the Proof Obligation (PO) generation process. Indeed, the POs are generated from the statically checked version of the model taken into account. Hence, we have to ensure before creating POs, that the model is correctly expressed (i.e. POs are generated for a model which "''could'' have some sense"). This means that we have to verify some additional properties on the newly added elements. <br>
 +
The question addressed here is: " '''Under which conditions (about the model well-formedness) the PO generation means something?''' ".<br>
  
* The Code Generation feature is available by accessing the main Rodin Update Site. In Eclispe click on Help/Install new Software. Find the Rodin update site from the list. In Utilities add Code Generation.
+
=== Principles ===
The approach makes use of the following:
 
*Model Decomposition: Download from the main Rodin Update Site, in the Decomposition section.
 
*Shared Event Composition: Download from the main Rodin Update Site, in the Decomposition section.
 
*Theory Plug-in: Download from the main Rodin Update Site, in the Modelling Extensions section.
 
  
Examples available at:
+
1. To extend the static checker in order to verify some conditions, one has to '''define a static checker module''' using the extension point <tt>org.eventb.core.scModuleTypes</tt>.<br>
+
There are two types of modules: <tt>processorType</tt> and <tt>filterType</tt>. We will detail the way to define such modules later.<br>
* Tutorial, and example, projects are available from the Examples directory: [https://codegenerationd.svn.sourceforge.net/svnroot/codegenerationd/Examples/v0.2.2/ SVN].
+
2. Then, one has to '''set up a configuration''' involving these modules and giving them a hierarchy. In fact, verifying the correctness conditions about added elements can be separated in several processor and filter modules; the configuration is then used to organise them.<br>
* Test projects are also available from the Examples directory [https://codegenerationd.svn.sourceforge.net/svnroot/codegenerationd/Examples/v0.2.1/CG_v0.2.0_Tests SVN].
+
3. Finally, it is needed to '''add this configuration''' to the default one, so our checks can be performed.<br>
* Sources at: [https://rodin-b-sharp.svn.sourceforge.net/svnroot/rodin-b-sharp/trunk/CodeGeneration SVN]
 
* Example Theories at: [https://codegenerationd.svn.sourceforge.net/svnroot/codegenerationd/Examples/TheoriesForCG SVN]
 
  
=== Code Generation Feature - Version 0.2.1 For Rodin 2.3===
+
=== Step 1 : Extending the database to introduce the static checked version of the element ''Bound'' (a.k.a. SCBound) ===
Contains Bug Fixes for previous release. 14-12-2011
 
  
=== Code Generation Feature - Version 0.2.0 For Rodin 2.3===
+
The aim of static checking is to produce a static checked version of the model upon consideration. Hence, every element ("unchecked") shall have its statically checked counterpart. We will then add the counterpart of the element <tt>Bound</tt>, following the same steps as when we added our element <tt>Bound</tt> in the database (See step 4 [[Extend_Rodin_database_(How_to_extend_Rodin_Tutorial)|here]]).
We have release a new version of the code generator on 30-11-2011, and updated documentation.
 
===== Changes to the Tooling and Approach =====
 
The main changes are:
 
* The code generators have been completely re-written. The translators are now implemented in Java, i.e. there is no longer a dependence on the Epsilon tool set. This was undertaken for code maintenance reasons.
 
* Tasking Event-B is now integrated with the Event-B explorer.
 
* The Rose Editor is used for editing the Tasking Event-B, and
 
* a text-based editor is provided, using the Rose extension, for editing the TaskBody. This feature has been added to address some of the usability concerns. It also overcomes the 'problem' experienced with duplicate event names in a development, since the parser-builder that has been implemented automatically selects the correct event.
 
* The EMF tree editor in Rose is only used minimally; we plan enhancements to further reduce its use.
 
* Composed machines are used to store event 'synchronizations'; these are generated automatically during the decomposition process. This reduces the amount of typing in the TaskBody editor, since we no longer need to specify both local and remote (synchronizing) events.
 
* The code generation approach is now extensible; new target language constructs can be added using the Eclipse extension mechanism.
 
* The translation of target's mathematical language is now specified in the theory plug-in. This improves clarity since the the translation from source to target is achieved by specifying pattern matching rules. Extensibility is also improved; the theory plug-in is used to specify new data-types, and how they are implemented.
 
* Translated code is deposited in a directory in the appropriate files. An Ada project file is generated for use with AdaCore's GPS workbench. Eventually this could be enabled/disabled in a preferences dialog box.
 
* The Tasking Event-B to Event-B translator is now properly integrated. Control variable updates to the Event-B model are made in a similar way to the equivalent updates in the state-machine plug-in. The additional elements are added to the Event-B model and marked as 'generated'. This prevents users from manually modifying them, and allows them to be removed through a menu choice.
 
  
===== Changes to the Documentation =====
+
To do so, create a new extension <tt>internalElementType</tt> from <tt>org.rodinp.core.internalElementTypes</tt> with:<br>
The following Pages have been updated:
+
- id: <tt>scBound</tt>,<br>
* [http://wiki.event-b.org/index.php/Tasking_Event-B_Overview Tasking Event-B Overview]
+
- a name such as "Event-B Static Checked Bound Element",<br>
* [http://wiki.event-b.org/index.php/Tasking_Event-B_Tutorial Tutorial]
+
- a class for this element that extends <tt>SCExpressionElement</tt> and implements a freshly created interface <tt>ISCBound</tt> defined as follows:
  
TODO
+
public interface ISCBound extends ISCExpressionElement{
* Add addressed variables (for direct read/write access to memory)
+
* Flattening of composed machines/implementation machines.
+
IInternalElementType<ISCBound> ELEMENT_TYPE =
* Interrupts
+
RodinCore.getInternalElementType(QualProbPlugin.PLUGIN_ID + ".scBound");
 +
}
  
=== Sensing and Actuating for Tasking Event-B ===
+
=== Step 2 : Adding modules===
Version 0.1.5. Sensing and actuating events, and an Environ Machine have been added to allow simulation of the environment and implementation using memory mapped IO.
 
  
* The new v0.1.5 feature is available from the Rodin Update Site, it resides in the Utilities Category.
+
==== Generalities ====
 +
In our case of probabilistic reasoning, the following '''well-formedness conditions should be held''' for a model ''containing probabilistic events'':
 +
# The variant V (declared as usual) shall be either of type integer or some set.
 +
# There is exactly one bound for a model where the probabilistic convergence is proved. The Bound element B shall be of the same type as the declared variant.
 +
# Every probabilistic event shall be refined by a probabilistic event.
 +
# The result of merging a probabilistic event and a convergent event is a probabilistic event.
  
* As in previous releases, the code generation plug-in relies on the Epsilon tool suite. Add the following Epsilon interim update site to the list of available update sites in the Eclipse menu ''help/install new software'': http://download.eclipse.org/modeling/gmt/epsilon/interim/
+
We can face two types of situations during the static checking:
 +
# We encounter a problem which doesn't affect the PO generation: it leads to a '''warning''' (fixed by a default assumption or not).
 +
# We encounter a problem which affects the PO generation: it leads to an '''error''' (The element, added with our extension and under consideration, is not added in the statically checked model).
  
* Select 'the Epsilon Core (Incubation)' component, this is the only component that is required for Tasking Event-B.
+
We have previously said that there is two types of modules. We first define a <tt>processorModule</tt>. Processor modules literally process the elements, storing them once validated in the statically checked file.
 +
In parallel, a <tt>filterModule</tt>s performs only some verifications (i.e. a <tt>filtermodule</tt> cannot do anything with the statically checked file). Furthermore, the filters are called (in group) from processors, and as soon as one filter rejects one element (i.e. "does not accept the element"), the other filters will not be evaluated for this element.  
  
A new [http://wiki.event-b.org/index.php?title=Tasking_Event-B_Tutorial Code Generation Tutorial] has been produced, that makes use of these new features. There is an explanation of the heating controller, upon which it is based, [http://wiki.event-b.org/index.php/Development_of_a_Heating_Controller_System here].
+
In a <tt>processorModule</tt>, if the static check fails for the considered element, the module '''must not add such element''' to the statically checked file that it holds, and which is used for PO generation. Processors are also responsible of running sub-processors, and filters, as well as adding states to the repository if required.<br>
 +
The developer is responsible of its module configuration lifecycle. He has to be aware, at any time, of his module's hierarchy, and has to call sub-modules explicitly when meaningful. Furthermore, a system of state sharing (via a state repository) is available so that a processor can provide informations about its checking results to its sub-modules. See <tt>org.eventb.core.sc.state.ISCStateRepository</tt> and <tt>org.eventb.core.sc.state.ISCState</tt>. Remember that it is only allowed to share informations within a module/sub-module hierarchy and that a policy should be established so that concurrent access to these states is taken into account, and that informations stored in the state repository are still coherent through sub-processors and filters computations.<br>
  
The example/tutorial projects, and also and a Bundled Windows 7 version, are available in the [http://deploy-eprints.ecs.soton.ac.uk/304/ Deploy E-Prints archive] or [https://codegenerationd.svn.sourceforge.net/svnroot/codegenerationd/Examples/HeatingController_Tutorial_v0.1.4/ Examples SVN site].
+
Three methods can be used (e.g. overridden) in a <tt>processorModule</tt>:
 +
* <tt>void initModule(IRodinElement element, ISCStateRepository repository, IProgressMonitor monitor) throws CoreException</tt>, which by default does nothing, but should be used in order to initialise the state (e.g. information) sharing.
 +
* <tt>void process(IRodinElement element, IInternalElement target, ISCStateRepository repository, IProgressMonitor monitor) throws CoreException</tt>, which MUST be implemented to perform static checking.
 +
* <tt>void endModule(IRodinElement element, ISCStateRepository repository, IProgressMonitor monitor) throws CoreException</tt>, which by default does nothing, but should be used if <tt>initModule()</tt> was used, to release the states locally created.<br>
  
=== The Code Generation Demonstrator for Rodin 2.1.x ===
+
==== Adding a processor module ====
 +
The processor that we will create will perform checks, and eventually add the statically checked version of the Bound element to the statically checked machine. As we don't really need to share information to our sub-modules, only the <tt>process()</tt> method will be overridden.
  
Released 24 January 2011.
+
For the extension point <tt>org.eventb.core.scModuleTypes</tt> create an extension <tt>processorType</tt>.<br>
 +
1. Enter a unique ID (like here <tt>machineBoundModule</tt>).<br>
 +
2. Enter a human readable name such as "Machine SC Bound Module" as we will start to check bound elements.<br>
 +
3. Enter the parent ID of the module we want to extend. Here as we want to make checks on bounds, variants and events, we will take <tt>org.eventb.core.machineModule</tt> as parent.<br>
 +
4. Create the module class that <tt>extends SCProcessorModule</tt> (we called it "MachineBoundModule" and we used the "new class wizard").
  
The Rodin 2.1.x compatible code generation demonstrator plug-ins have been released into the Rodin Sourceforge repository at:
+
The module class we created has to be implemented.<br>
 +
Two methods inherited from the interface <tt>ISCProcessorModule</tt> have to be defined (e.g. <tt>@Override</tt>):
  
  https://rodin-b-sharp.svn.sourceforge.net/svnroot/rodin-b-sharp/trunk/CodeGeneration
+
''A . <tt>public IModuleType<?> getModuleType()</tt>''
  
The update-site is available through the Rodin update site in the ''Utilities'' category.
+
This method shall return the type of our module, built from its extension's ID. In order to do that, we use the static method in <tt>org.eventb.core.sc.SCCore.getModuleType()</tt> with the complete identifier of our module extension: <tt>QualProbPlugin.PLUGIN_ID + ".machineBoundModule"</tt>.<br>
 +
Thus, let's use the constant below in our code:
  
The code generation tutorial examples are available for download at:
+
public static final IModuleType<MachineBoundModule> MODULE_TYPE = SCCore.getModuleType(QualProbPlugin.PLUGIN_ID + ".machineBoundModule");
  
  https://sourceforge.net/projects/codegenerationd/files/DemoFiles/
+
So we can write:
  
The code generation plug-in relies on the Epsilon tool suite. Install Epsilon manually, since the automatic install utility does not seem to work for this feature. We currently use the Epsilon interim update site available at:
+
@Override
 +
public IModuleType<?> getModuleType() {
 +
return MODULE_TYPE;
 +
}
  
  http://download.eclipse.org/modeling/gmt/epsilon/interim/
+
''B . <tt>public void process(IRodinElement element, IInternalElement target, ISCStateRepository repository, IProgressMonitor monitor) throws CoreException</tt>''
  
Select 'the Epsilon Core (Incubation)' component, this is the only component that is required for Tasking Event-B.
+
This method is the place where checks are performed. Thus, it is where we will code all the conditions to check and finally produce a statically checked Bound element if all the conditions are respected.
 +
The implementation is "huge" and pure Java, and it is not relevant in this tutorial to detail the full code. We will rather explain which are the main operations performed by the <tt>process</tt> method and give some hints about how to use the Rodin API to retrieve the information required in our checks. Full implementation is let to the reader as an exercise.
  
== Code Generation Status ==
+
Here are some explanations about the <tt>process()</tt> method arguments:
=== Latest Developments ===
 
* Demonstrator plug-in feature version 0.1.0
 
** for Rodin 2.1.x version is available.
 
  
* The Code Generation feature consists of,
+
The <tt>element</tt> passed as argument here is the element propagated by the parent of this module. It may be useful in case of systematic element checking, to retrieve the elements to check in a parent processor module, and then manage each element one by one, calling sub-processor modules.<br>
** a tasking Development Generator.
+
The <tt>IInternalElement</tt> target is the statically checked file where our elements, after successful well-formedness verification, will be stored. This file will be used as an input for the PO generation.<br>
** a tasking Development Editor (Based on an EMF Tree Editor).
+
The parameter <tt>ISCStateRepository</tt> repository is the global repository used by the module to get shared information. (//FIXME complete the static checker page, to add infos about states and link it here).<br>
** a translator, from Tasking Development to Common Language Model (IL1).
+
Finally, <tt>IProgressMonitor</tt> monitor is the progress monitor used while performing the static checks. Sub-tasks can be created for it.
** a translator, from the Tasking Development to Event-B model of the implementation.
 
** a pretty-printer for the Tasking Development.
 
** a pretty-printer for Common Language Model, which generates Ada Source Code.
 
  
* A tutorial is available [[Code Generation Tutorial]]
+
In our case, we have to refine the well-formedness conditions into a verification algorithm. We choose to retrieve the bound and variant values from the machine root directly using the following code in the <tt>process</tt> method:
** Step 1 - Create the tasking development.
 
** Step 2 - Add annotations.
 
** Step 3 - Invoke translators.
 
  
=== Ongoing Work ===
+
final IRodinFile machineFile = (IRodinFile) element;
 +
final IMachineRoot machineRoot = (IMachineRoot) machineFile.getRoot();
 +
final IBound[] bounds = machineRoot.getChildrenOfType(IBound.ELEMENT_TYPE);
 +
final IVariant[] variants = machineRoot.getVariants();
  
* Full Rodin Integration
+
Warnings and errors will be created using the method <tt>createProblemMarker</tt> (see <tt>org.eventb.core.sc.SCModule</tt>).
* Sensed Variables
 
* Branching in Shared Machines
 
  
=== Future Work ===
+
==== Exercise 1 - Implement the proposed algorithm (among others) ====
* Support for Interrupts.
 
* Richer DataTypes.
 
* Accommodation of duplicate event names in tasking developments.
 
  
== Metamodels ==
+
If the machine does not contain a probabilistic event, but there is a bound,
* In the plug-in we define several meta-models:
+
then we add a warning informing that the bound is ignored.
** CompositeControl: for the control flow (algorithmic) constructs such as branch, loop and sequence etc. These constructs may be used in the specification of either  sequential or concurrent systems.
+
** Tasking Meta-model: defines the tasking model where we attach tasking specific details, such as task priority, task type. The tasking structures provide the ability to define single tasking or multi-tasking (concurrent) systems. We make use of the composite control plug-in to specify the flow of control.  
+
If the machine contains at least a probabilistic event (i.e. "the model is probabilistic"), but there are more than one bound,
** Common Language (IL1) Meta-model: defines an abstraction of common programming language constructs for use in translations to implementations.
+
then we create an error telling that there are too many bounds, nothing is created an we return immediately.
 +
 +
// We are now sure that there a single bound
 +
If the model is probabilistic
 +
   
 +
    If the variant is not a set or a constant, we create an error and return.
 +
      The following code may serve as a basis:
 +
 +
      private boolean assertIsASetOrConstant(IExpressionElement element)
 +
throws RodinDBException {
 +
              final String formula = element.getExpressionString();
 +
              final IParseResult result = factory.parseExpression(formula, LanguageVersion.V2, element);
 +
              final Expression boundExpression = result.getParsedExpression();
 +
              return isASetOrConstant(boundExpression.getType());
 +
 +
          with
 +
 +
              private boolean isASetOrConstant(Type type) {
 +
if (type.equals(factory.makeIntegerType())) {
 +
return true;
 +
}
 +
final Type baseType = type.getBaseType();
 +
if (baseType != null) {
 +
return type.equals(factory.makePowerSetType(baseType));
 +
}
 +
return false;
 +
}
 +
   
 +
    If there is no bound, we create an error, and return.
 +
 +
    If the bound is not a set or a constant, we create an error, and return.
 +
 +
    If the bound is not of the same type as the variant, we create an error and return.
 +
      One may check it as follows:
 +
                        if (!getType(bound).equals(getType(variant))) {
 +
createProblemMarker(bound,
 +
EventBAttributes.EXPRESSION_ATTRIBUTE,
 +
ProbabilisticGraphProblem.VariantBoundTypeError);
 +
return;
 +
}
 +
    [...]
 +
// After all checks, we add the bound to the statically checked file.
 +
final ISCBound scBound = target.getInternalElement(ISCBound.ELEMENT_TYPE, BOUND_NAME_PREFIX);
 +
scBound.create(null, monitor);
 +
scBound.setExpression(getExpression(bound), null);
  
== Translation Rules ==
+
In the processor module, one may use the filters to drop a part of the processing with the invocation <tt>filterModules(element, repository, monitor)</tt> which will return a boolean telling if the element has successfully passed all the filtering criteria or not.
* Tasking to IL1/Event-B translation rules [[http://wiki.event-b.org/images/Translation.pdf]]
+
One may also process an element using the child processor modules with the following invocation:<br>
 +
<tt>protected final void processModules(IRodinElement element, IInternalElement target, ISCStateRepository repository, IProgressMonitor monitor) throws CoreException</tt>
  
== Release History ==
+
==== Exercise 2 ====
=== The Code Generation Demonstrator for Rodin 1.3.x ===
+
We used here a filter <tt>machineBoundFreeIdentsModule</tt>, to check that the expression of the ''Bound'' element parses, and no additional free identifier was introduced.
 +
Implement such a filter using the fact that the repository holds a type environment which contains all the usable free identifiers. To use this, we must add a ''prereq'' clause to our filter pointing the id <tt>org.eventb.core.machineVariantModule</tt> of the variant module.
 +
Here is an extract of the filter's <tt>accept()</tt> method :
  
 +
final ITypeEnvironment typeEnv = repository.getTypeEnvironment();
 +
final Expression parsedExpression = parseResult.getParsedExpression();
 +
 +
final FreeIdentifier[] freeIdentifiers = parsedExpression
 +
.getFreeIdentifiers();
 +
 +
boolean ok = true;
 +
for (FreeIdentifier ident : freeIdentifiers) {
 +
if (!typeEnv.contains(ident.getName()))
 +
createProblemMarker(bound,
 +
EventBAttributes.EXPRESSION_ATTRIBUTE,
 +
ProbabilisticGraphProblem.BoundFreeIdentifierError,
 +
ident);
 +
ok = false;
 +
}
 +
return ok;
  
First release: 30 November 2010.
+
=== Step 3 : Set up a static checking configuration ===
  
available from:
+
In order to register our checkings, and because those verifications could be separated in several modules, we need to encapsulate them into a configuration.<br>
 +
The extension point <tt>org.eventb.core.configurations</tt> allows to doing so.<br>
 +
To organise our modules :<br>
 +
1. Create an extension <tt>configuration</tt> from the above mentioned extension point,
 +
:give it an id (for example "qpConfig"),
 +
:give it a human readable name (for example, "Qualitative Probabilistic Reasoning Plug-in SC Configuration").
  
https://sourceforge.net/projects/codegenerationd/files/
+
2. add the modules (full id) previously defined to the configuration, in our example, we implemented two modules :<br>
 +
- <tt>fr.systerel.rodinextension.sample.machineBoundModule</tt><br>
 +
- <tt>fr.systerel.rodinextension.sample.machineBoundFreeIdentsModule</tt><br>
  
The zip file contains a windows XP bundle, and a Windows V7 bundle. Alternatively, if you wish to build using an update-site, this is also included in the zip file, along with some notes on installation. However, note that the demonstrator tool is only compatible with Rodin 1.3.  
+
That's all for configuration creation. Now, we need to add it to machine file configurations so it can run when our plug-in is installed.
  
A simple shared buffer example is provided. This will form the basis of a tutorial (which is work in progress). The WindowsBundles directory contains a Rodin 1.3.1 platform with the Code Generation plug-ins, together with a patch plug-in. The patch plug-in is required to correct an inconsistency in the org.eventb.emf.persistence plug-in. For the bundles, simply extract the appropriate zip file into a directory and run the rodin.exe. The plug-ins are pre-installed - the only configuration necessary may be to switch workspace to ''<installPath>\rodin1.3bWin7\workspace''. When using the update-site the example projects, and the project forming the basis of a simple tutorial, are provided in the accompanying zip file. These should be imported manually.
+
=== Step 4 : Add the configuration so it can run on machine files ===
  
Mac users - no bundled version available at present, but use the update site in the 'advanced' folder.  
+
The best way to add our configuration, is to register a utility class, that will add our configuration to the machine files, when our plug-in is active, and their configuration doesn't contain ours.
 +
To do so, create the following class that implements <tt>org.rodinp.core.IElementChangedListener</tt>:
  
'''A step-by-step [[Code Generation Tutorial]] is available'''
+
/**
 
+
  * Class that updates the configuration of files, to add the static checker
==== About the Initial Release ====
+
  * modules for our qualitative probabilistic reasoning plugin.
The Code Generation (CG) Feature in the initial release is a demonstration tool; a proof of concept, rather than a prototype. The tool has no static checker and, therefore, there will be a heavy reliance on docs and dialogue to facilitate exploration of the tools and concepts.
+
  */
 
+
public class ConfSettor implements IElementChangedListener {
==== Source Code ====
+
 
+
private static final String QUAL_PROB_CONFIG = QualProbPlugin.PLUGIN_ID
The sources are available from,
+
+ ".qpConfig";
 +
 +
public void elementChanged(ElementChangedEvent event) {
 +
 +
final IRodinElementDelta d = event.getDelta();
 +
try {
 +
processDelta(d);
 +
} catch (final RodinDBException e) {
 +
// TODO add exception log
 +
}
 +
}
 +
 +
private void processDelta(final IRodinElementDelta d)
 +
throws RodinDBException {
 +
final IRodinElement e = d.getElement();
 +
 +
final IElementType<? extends IRodinElement> elementType = e
 +
.getElementType();
 +
if (elementType.equals(IRodinDB.ELEMENT_TYPE)
 +
|| elementType.equals(IRodinProject.ELEMENT_TYPE)) {
 +
for (final IRodinElementDelta de : d.getAffectedChildren()) {
 +
processDelta(de);
 +
}
 +
} else if (elementType.equals(IRodinFile.ELEMENT_TYPE)) {
 +
final IInternalElement root = ((IRodinFile) e).getRoot();
 +
 +
if (root.getElementType().equals(IMachineRoot.ELEMENT_TYPE)) {
 +
final IMachineRoot mch = (IMachineRoot) root;
 +
final String conf = mch.getConfiguration();
 +
if (!conf.contains(QUAL_PROB_CONFIG)) {
 +
mch.setConfiguration(conf + ";" + QUAL_PROB_CONFIG, null);
 +
}
 +
}
 +
}
 +
}
 +
}
  
https://codegenerationd.svn.sourceforge.net/svnroot/codegenerationd
+
Where the string constant ''QUAL_PROB_CONFIG'' will refer to our configuration in the machine files, and we check that each machine file that we are manipulating contains our configuration.
 +
Now we need to launch this class at plugin start-up.
  
Note - I used Eclipse 3.5 Galileo, and you will need to install (or have sources from) Epsilon's interim update site. There is also dependency on Camille v2.0.0
+
To do so :<br>
 +
1. open the activator of our plugin,<br>
 +
2. add a method <tt>setProbConfig()</tt> to the <tt>start(BundleContext context)</tt> method of the activator,<br>
 +
3. implement this method the following :<br>
 +
        /**
 +
* Registers a file configuration setter for our plugin.
 +
*/
 +
public static void setProbConfig() {
 +
RodinCore.addElementChangedListener(new ConfSettor());
 +
}
  
  
 +
{{Navigation|Previous= [[Extending_the_Static_Checker(How_to_extend_Rodin_Tutorial)]] | Up= [[Plug-in_Tutorial|How to extend Rodin Tutorial (Index)]] | Next= }}
  
[[Category:Work in progress]]
+
[[Category:Developer documentation|*Index]]
 +
[[Category:Rodin Platform|*Index]]
 +
[[Category:Tutorial|*Index]]

Revision as of 08:32, 31 August 2010

In this part

We will see how to add rules to statically check the machines after our extension. The Static Checker (SC) is one dedicated part of the Proof Obligation (PO) generation process. Indeed, the POs are generated from the statically checked version of the model taken into account. Hence, we have to ensure before creating POs, that the model is correctly expressed (i.e. POs are generated for a model which "could have some sense"). This means that we have to verify some additional properties on the newly added elements.
The question addressed here is: " Under which conditions (about the model well-formedness) the PO generation means something? ".

Principles

1. To extend the static checker in order to verify some conditions, one has to define a static checker module using the extension point org.eventb.core.scModuleTypes.
There are two types of modules: processorType and filterType. We will detail the way to define such modules later.
2. Then, one has to set up a configuration involving these modules and giving them a hierarchy. In fact, verifying the correctness conditions about added elements can be separated in several processor and filter modules; the configuration is then used to organise them.
3. Finally, it is needed to add this configuration to the default one, so our checks can be performed.

Step 1 : Extending the database to introduce the static checked version of the element Bound (a.k.a. SCBound)

The aim of static checking is to produce a static checked version of the model upon consideration. Hence, every element ("unchecked") shall have its statically checked counterpart. We will then add the counterpart of the element Bound, following the same steps as when we added our element Bound in the database (See step 4 here).

To do so, create a new extension internalElementType from org.rodinp.core.internalElementTypes with:
- id: scBound,
- a name such as "Event-B Static Checked Bound Element",
- a class for this element that extends SCExpressionElement and implements a freshly created interface ISCBound defined as follows:

public interface ISCBound extends ISCExpressionElement{
	
	IInternalElementType<ISCBound> ELEMENT_TYPE =
		RodinCore.getInternalElementType(QualProbPlugin.PLUGIN_ID + ".scBound");
}

Step 2 : Adding modules

Generalities

In our case of probabilistic reasoning, the following well-formedness conditions should be held for a model containing probabilistic events:

  1. The variant V (declared as usual) shall be either of type integer or some set.
  2. There is exactly one bound for a model where the probabilistic convergence is proved. The Bound element B shall be of the same type as the declared variant.
  3. Every probabilistic event shall be refined by a probabilistic event.
  4. The result of merging a probabilistic event and a convergent event is a probabilistic event.

We can face two types of situations during the static checking:

  1. We encounter a problem which doesn't affect the PO generation: it leads to a warning (fixed by a default assumption or not).
  2. We encounter a problem which affects the PO generation: it leads to an error (The element, added with our extension and under consideration, is not added in the statically checked model).

We have previously said that there is two types of modules. We first define a processorModule. Processor modules literally process the elements, storing them once validated in the statically checked file. In parallel, a filterModules performs only some verifications (i.e. a filtermodule cannot do anything with the statically checked file). Furthermore, the filters are called (in group) from processors, and as soon as one filter rejects one element (i.e. "does not accept the element"), the other filters will not be evaluated for this element.

In a processorModule, if the static check fails for the considered element, the module must not add such element to the statically checked file that it holds, and which is used for PO generation. Processors are also responsible of running sub-processors, and filters, as well as adding states to the repository if required.
The developer is responsible of its module configuration lifecycle. He has to be aware, at any time, of his module's hierarchy, and has to call sub-modules explicitly when meaningful. Furthermore, a system of state sharing (via a state repository) is available so that a processor can provide informations about its checking results to its sub-modules. See org.eventb.core.sc.state.ISCStateRepository and org.eventb.core.sc.state.ISCState. Remember that it is only allowed to share informations within a module/sub-module hierarchy and that a policy should be established so that concurrent access to these states is taken into account, and that informations stored in the state repository are still coherent through sub-processors and filters computations.

Three methods can be used (e.g. overridden) in a processorModule:

  • void initModule(IRodinElement element, ISCStateRepository repository, IProgressMonitor monitor) throws CoreException, which by default does nothing, but should be used in order to initialise the state (e.g. information) sharing.
  • void process(IRodinElement element, IInternalElement target, ISCStateRepository repository, IProgressMonitor monitor) throws CoreException, which MUST be implemented to perform static checking.
  • void endModule(IRodinElement element, ISCStateRepository repository, IProgressMonitor monitor) throws CoreException, which by default does nothing, but should be used if initModule() was used, to release the states locally created.

Adding a processor module

The processor that we will create will perform checks, and eventually add the statically checked version of the Bound element to the statically checked machine. As we don't really need to share information to our sub-modules, only the process() method will be overridden.

For the extension point org.eventb.core.scModuleTypes create an extension processorType.
1. Enter a unique ID (like here machineBoundModule).
2. Enter a human readable name such as "Machine SC Bound Module" as we will start to check bound elements.
3. Enter the parent ID of the module we want to extend. Here as we want to make checks on bounds, variants and events, we will take org.eventb.core.machineModule as parent.
4. Create the module class that extends SCProcessorModule (we called it "MachineBoundModule" and we used the "new class wizard").

The module class we created has to be implemented.
Two methods inherited from the interface ISCProcessorModule have to be defined (e.g. @Override):

A . public IModuleType<?> getModuleType()

This method shall return the type of our module, built from its extension's ID. In order to do that, we use the static method in org.eventb.core.sc.SCCore.getModuleType() with the complete identifier of our module extension: QualProbPlugin.PLUGIN_ID + ".machineBoundModule".
Thus, let's use the constant below in our code:

public static final IModuleType<MachineBoundModule> MODULE_TYPE = SCCore.getModuleType(QualProbPlugin.PLUGIN_ID + ".machineBoundModule");

So we can write:

	@Override
	public IModuleType<?> getModuleType() {
		return MODULE_TYPE;
	}

B . public void process(IRodinElement element, IInternalElement target, ISCStateRepository repository, IProgressMonitor monitor) throws CoreException

This method is the place where checks are performed. Thus, it is where we will code all the conditions to check and finally produce a statically checked Bound element if all the conditions are respected. The implementation is "huge" and pure Java, and it is not relevant in this tutorial to detail the full code. We will rather explain which are the main operations performed by the process method and give some hints about how to use the Rodin API to retrieve the information required in our checks. Full implementation is let to the reader as an exercise.

Here are some explanations about the process() method arguments:

The element passed as argument here is the element propagated by the parent of this module. It may be useful in case of systematic element checking, to retrieve the elements to check in a parent processor module, and then manage each element one by one, calling sub-processor modules.
The IInternalElement target is the statically checked file where our elements, after successful well-formedness verification, will be stored. This file will be used as an input for the PO generation.
The parameter ISCStateRepository repository is the global repository used by the module to get shared information. (//FIXME complete the static checker page, to add infos about states and link it here).
Finally, IProgressMonitor monitor is the progress monitor used while performing the static checks. Sub-tasks can be created for it.

In our case, we have to refine the well-formedness conditions into a verification algorithm. We choose to retrieve the bound and variant values from the machine root directly using the following code in the process method:

final IRodinFile machineFile = (IRodinFile) element;
final IMachineRoot machineRoot = (IMachineRoot) machineFile.getRoot();
final IBound[] bounds = machineRoot.getChildrenOfType(IBound.ELEMENT_TYPE);
final IVariant[] variants = machineRoot.getVariants(); 

Warnings and errors will be created using the method createProblemMarker (see org.eventb.core.sc.SCModule).

Exercise 1 - Implement the proposed algorithm (among others)

If the machine does not contain a probabilistic event, but there is a bound,
then we add a warning informing that the bound is ignored.

If the machine contains at least a probabilistic event (i.e. "the model is probabilistic"), but there are more than one bound,
then we create an error telling that there are too many bounds, nothing is created an we return immediately.

// We are now sure that there a single bound
If the model is probabilistic 
    
   If the variant is not a set or a constant, we create an error and return.
      The following code may serve as a basis:

      private boolean assertIsASetOrConstant(IExpressionElement element)
			throws RodinDBException {
              final String formula = element.getExpressionString();
              final IParseResult result = factory.parseExpression(formula, LanguageVersion.V2, element);
              final Expression boundExpression = result.getParsedExpression();
              return isASetOrConstant(boundExpression.getType());

          with

              	private boolean isASetOrConstant(Type type) {
		if (type.equals(factory.makeIntegerType())) {
			return true;
		}
		final Type baseType = type.getBaseType();
		if (baseType != null) {
			return type.equals(factory.makePowerSetType(baseType));
		}
		return false;
	}
   
   If there is no bound, we create an error, and return.

   If the bound is not a set or a constant, we create an error, and return.

   If the bound is not of the same type as the variant, we create an error and return.
      One may check it as follows: 
                       if (!getType(bound).equals(getType(variant))) {
				createProblemMarker(bound,
						EventBAttributes.EXPRESSION_ATTRIBUTE,
						ProbabilisticGraphProblem.VariantBoundTypeError);
				return;
			}
   [...]
// After all checks, we add the bound to the statically checked file.
final ISCBound scBound = target.getInternalElement(ISCBound.ELEMENT_TYPE, BOUND_NAME_PREFIX);
scBound.create(null, monitor);
scBound.setExpression(getExpression(bound), null);

In the processor module, one may use the filters to drop a part of the processing with the invocation filterModules(element, repository, monitor) which will return a boolean telling if the element has successfully passed all the filtering criteria or not. One may also process an element using the child processor modules with the following invocation:

protected final void processModules(IRodinElement element, IInternalElement target, ISCStateRepository repository, IProgressMonitor monitor) throws CoreException

Exercise 2

We used here a filter machineBoundFreeIdentsModule, to check that the expression of the Bound element parses, and no additional free identifier was introduced. Implement such a filter using the fact that the repository holds a type environment which contains all the usable free identifiers. To use this, we must add a prereq clause to our filter pointing the id org.eventb.core.machineVariantModule of the variant module. Here is an extract of the filter's accept() method :

		final ITypeEnvironment typeEnv = repository.getTypeEnvironment();
		final Expression parsedExpression = parseResult.getParsedExpression();

		final FreeIdentifier[] freeIdentifiers = parsedExpression
				.getFreeIdentifiers();

		boolean ok = true;
		for (FreeIdentifier ident : freeIdentifiers) {
			if (!typeEnv.contains(ident.getName()))
				createProblemMarker(bound,
						EventBAttributes.EXPRESSION_ATTRIBUTE,
						ProbabilisticGraphProblem.BoundFreeIdentifierError,
						ident);
				ok = false;
			}
		return ok;

Step 3 : Set up a static checking configuration

In order to register our checkings, and because those verifications could be separated in several modules, we need to encapsulate them into a configuration.
The extension point org.eventb.core.configurations allows to doing so.
To organise our modules :
1. Create an extension configuration from the above mentioned extension point,

give it an id (for example "qpConfig"),
give it a human readable name (for example, "Qualitative Probabilistic Reasoning Plug-in SC Configuration").

2. add the modules (full id) previously defined to the configuration, in our example, we implemented two modules :
- fr.systerel.rodinextension.sample.machineBoundModule
- fr.systerel.rodinextension.sample.machineBoundFreeIdentsModule

That's all for configuration creation. Now, we need to add it to machine file configurations so it can run when our plug-in is installed.

Step 4 : Add the configuration so it can run on machine files

The best way to add our configuration, is to register a utility class, that will add our configuration to the machine files, when our plug-in is active, and their configuration doesn't contain ours. To do so, create the following class that implements org.rodinp.core.IElementChangedListener:

/**
 * Class that updates the configuration of files, to add the static checker
 * modules for our qualitative probabilistic reasoning plugin.
 */
public class ConfSettor implements IElementChangedListener {

	private static final String QUAL_PROB_CONFIG = QualProbPlugin.PLUGIN_ID
			+ ".qpConfig";

	public void elementChanged(ElementChangedEvent event) {

		final IRodinElementDelta d = event.getDelta();
		try {
			processDelta(d);
		} catch (final RodinDBException e) {
			// TODO add exception log
		}
	}

	private void processDelta(final IRodinElementDelta d)
			throws RodinDBException {
		final IRodinElement e = d.getElement();

		final IElementType<? extends IRodinElement> elementType = e
				.getElementType();
		if (elementType.equals(IRodinDB.ELEMENT_TYPE)
				|| elementType.equals(IRodinProject.ELEMENT_TYPE)) {
			for (final IRodinElementDelta de : d.getAffectedChildren()) {
				processDelta(de);
			}
		} else if (elementType.equals(IRodinFile.ELEMENT_TYPE)) {
			final IInternalElement root = ((IRodinFile) e).getRoot();

			if (root.getElementType().equals(IMachineRoot.ELEMENT_TYPE)) {
				final IMachineRoot mch = (IMachineRoot) root;
				final String conf = mch.getConfiguration();
				if (!conf.contains(QUAL_PROB_CONFIG)) {
					mch.setConfiguration(conf + ";" + QUAL_PROB_CONFIG, null);
				}
			}
		}
	}
}

Where the string constant QUAL_PROB_CONFIG will refer to our configuration in the machine files, and we check that each machine file that we are manipulating contains our configuration. Now we need to launch this class at plugin start-up.

To do so :
1. open the activator of our plugin,
2. add a method setProbConfig() to the start(BundleContext context) method of the activator,
3. implement this method the following :

        /**
	 * Registers a file configuration setter for our plugin.
	 */
	public static void setProbConfig() {
		RodinCore.addElementChangedListener(new ConfSettor());
	}