Extending the Static Checker (How to extend Rodin Tutorial)
In this part
We will see how to add rules to statically check the machines after our extension. The Static Checker is one dedicated part of the Proof Obligation generation process. Indeed, the Proof Obligations are generated from the statically checked version of the model taken into account. Hence, we have to ensure before creating Proof Obligations, that the model is correctly expressed (i.e. proof obligations are generated for a model which "could have some sense"). This means that we have to verify some additional proprerties on the newly added elements.
The question addressed here is : " Under which conditions (about the model well-formedness) the proof obligation 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 those modules and giving them a hierachy. In fact, verifying that 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 checkings 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",
- implement 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");
}
Step2 : Adding modules
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) is either of the type integer or some set.
- There is exactly one bound for a model where the probabilistic converge is proved. The bound element B must be of the same type as the declared variant.
- Every probabilistic event must be refined by a probabilistic event.
- 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 :
- we encounter a problem which doesn't affect the PO generation : this leads to a warning (corrected by a default assumption or not).
- we encounter a problem which affects the PO generation : this leads to an error. (the element (added with our extension) under consideration is not added in the statically checked model).
From the two types of modules, we will first use a processorModule. Processor modules literally process the elements, storing them once validated in the static checked file. Whereas filterModules performs only some verifications (i.e. a filtermodule can not 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 proof obligation 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 must be aware, at any time, of his module's hierachy, and call submodules explicitely when this is 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 submodules. 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 those 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. overriden) 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 state informations locally created.
The processor, that we will create, will perform checkings and eventually, add the statically checked version of the bound to the statically checked machine. As we don't really need to share informations to our submodules, only the process() method will be overriden.
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 checkings 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 (e.g. the class we created) needs to be implemented.
Two methods inherited from the interface ISCProcessorModule need 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. To do this we use the static method in org.eventb.core.sc.SCCore.getModuleType() with our module extension complete identifier : 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 checkings are done. Thus it's where we will code all the conditions to check and finally produce a statically checked bound element, if all those conditions are respected. Accorded to the checking implementations which are "huge" and pure java, it is not relevant for this part of the 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 retreive the informations needed in our checkings. Full implementation is let to the reader as an exercise.
Here are some explanations about the process() method arguments:
The element passed as an argument here, is the element passed by the parent of this module. It can be useful in case of systematic element checking, to retrieve the elements to check in a parent processor module, and then, treat each element one by one, calling sub-processor modules.
The IInternalElement target is (e.g. should be) the statically checked file where our elements, after sucessful well-formedness verification, should be stored. This file will be used as an input for the proof obligation generation.
The parameter ISCStateRepository repository is the global repository used by the module to get shared informations. (//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 checking, subtasks can be created for it, so the user interface reflects the checkings which are done.
In our case, we must refine the well-formedness conditions into a verification algorithm. We choosed to retreive 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 a lot of possible other):
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 propabilistic event (i.e. say "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 now know that there is at maximum one bound
if the model is probabilistic
if the variant is not a set or a constant, we create an error and return;
NB: we can use the following code :
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;
NB: one could check it this way :
if (!getType(bound).equals(getType(variant))) {
createProblemMarker(bound,
EventBAttributes.EXPRESSION_ATTRIBUTE,
ProbabilisticGraphProblem.VariantBoundTypeError);
return;
}
[...]
// after all checkings... 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 could use the filters to drop a part of the processings using the invocation : filterModules(element, repository, monitor) which will return a boolean telling if the element successfully passed all the filtering criteria or not.
One can also process an element using the child processor modules using the 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 "qp"),
- 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.
