Extending the Proof Obligation Generator (How to extend Rodin Tutorial)
In this part
We will see how to create proof obligations to discharge for the machines relatively to our extensions for Probabilistic Reasoning and after having statically checked the machines. The latter operation is the first part of the proof obligation generation as the proof obligation generator takes statically checked files in input. One will notice that the provided architecture for static checking is really similar to the one for proof obligation generation. Thus, it can be useful for the reader to understand well the previous part of this tutorial, as we will not repeat all the ideas shared by the both processes. The question here is "What needs to be mathematically proved with those newly added elements in hands?".
We will study here, the case of the BNF proof obligation, which is described in the paper. This PO overrides the FIN proof obligation. Thus we will see here, how to :
- remove the FIN PO which is generated by default,
- add our new BNF PO.
Principles
1. To extend the proof obligation generator (POG) in order to add some proof obligations that one has to discharge, one has to define a proof obligation processor module using the extension point : org.eventb.core.pogModuleTypes.
2. Then , one has to set up a configuration involving those modules and giving them a hierachy. This is done exactly the same way as for creating a static checker configuration.
3. Finally, it is needed to add this POG configuration to the default one, so the proof obligation generation can be performed.
We want here to show how to generate one proof obligation. We will add the PO named BFN to ensure that the bound is a natural number or finite. It will be generated once for all for the machine taken into account. Moreover, this PO overrides the default FIN proof obligation which is generated if a convergent event (with the associated variant) is present in the model. If a probabilistic event is in the machine, we want to create our BFN PO, thus we have to remove the FIN PO.
In step 1, we will explain how to create our PO BFN, and add informations in the state repository so that in the second step, we could create a filter to remove the PO FIN if our machine contains a probabilistic event.
Step 1 : Adding POG modules
As we know that the POG takes his input from the static checker, the presence of a statically checked bound (ISCBound) in the statically checked model, means that one aims to prove the probabilistic convergence of this model. Thus, this information shall be shared throught our hierachy of POG modules, as it triggers the operations they could perform.
We will first let the information about the statically checked bound be available through sub-modules via a specific state that we will create. And use this information to create the BFN proof obligation.
From the extension point org.eventb.core.pogModuleTypes, create a processorModule extension to implement our first PO generation process using a POG processor :
As for a static checker module,
1. give the module an id (here fwdMachineBoundModule),
2. a human readable name (here "Machine POG Forward Bound Module"),
3. register a parent in the hierarchy of modules (here we used the machine POG module of the Event-B POG : org.eventb.core.machineModule),
4. create a class for this module.(here we created the class fr.systerel.rodinextension.sample.pog.modules.FwdMachineBoundModule).
The above module should share, at its initialisation, an IMachineBoundInfo state that we should create here too.
@Override
public void initModule(IRodinElement element,
IPOGStateRepository repository, IProgressMonitor monitor)
throws CoreException {
repository.setState(createMachineBoundInfo(element, repository));
}
private IMachineBoundInfo createMachineBoundInfo(IRodinElement element,
IPOGStateRepository repository) throws CoreException {
final IRodinFile machineFile = (IRodinFile) element;
final ISCMachineRoot root = (ISCMachineRoot) machineFile.getRoot();
final ISCBound[] bounds = root.getChildrenOfType(ISCBound.ELEMENT_TYPE);
if (bounds.length != 1) {
return new MachineBoundInfo();
}
final ISCBound scBound = bounds[0];
final ITypeEnvironment typeEnv = repository.getTypeEnvironment();
final Expression expr = scBound.getExpression(
typeEnv.getFormulaFactory(), typeEnv);
return new MachineBoundInfo(expr, scBound);
}
Here is the interface IMachineBoundInfo one has to create :
public interface IMachineBoundInfo extends IPOGState {
final static IStateType<IMachineBoundInfo> STATE_TYPE =
POGCore.getToolStateType(QualProbPlugin.PLUGIN_ID + ".machineBoundInfo");
/**
* Returns the parsed and type-checked bound expression, or null
* if the machine does not have a bound.
*
* @return the parsed and type-checked bound expression, or null
* if the machine does not have a bound
*/
Expression getExpression();
/**
* Returns a handle to the bound, or null if the machine does not have a bound.
*
* @return a handle to the bound, or null if the machine does not have a bound
*/
ISCBound getBound();
/**
* Returns whether the machine has a bound.
*
* @return whether the machine has a bound
*/
boolean machineHasBound();
}
and here is its implementation class :
public class MachineBoundInfo implements IMachineBoundInfo {
private boolean immutable;
/** * Constructor */ public MachineBoundInfo(final Expression expression, final ISCBound bound) { this.boundExpression = expression; this.bound = bound; immutable = false; }
/** * Constructor with no bound attached */ public MachineBoundInfo() { this.boundExpression = null; this.bound = null; immutable = false; }
@Override public String toString() { return boundExpression == null ? "null" : boundExpression.toString(); }
private final Expression boundExpression;
private final ISCBound bound;
public Expression getExpression() { return boundExpression; }
public ISCBound getBound() { return bound; }
public IStateType<?> getStateType() { return IMachineBoundInfo.STATE_TYPE; }
public boolean machineHasBound() { return boundExpression != null; }
@Override public void makeImmutable() { immutable = true; }
@Override public boolean isImmutable() { return immutable; }
}
Step 2 : Removing a PO
To remove a PO, one has to create a filter module. This follows the same way as what is done for the static checker. After a small search in the package org.eventb.internal.core.pog.modules, we identify that the module responsible of creating the FIN PO is actually FwdMachineVariantModule. The goal is here to register our filter as a submodule of FwdMachineVariantModule that will prevent it to create the FIN PO.
The code is really simple... first one has to check if the model contains a probabilistic event, which means that we want to override the FIN PO that will be created by default, and then, in the filter, one has to search from the generated PO if one corresponds to FIN by searching inside PO names and reject it.
1. give the module an id (here finPORejectingModule),
2. a human readable name (here "Machine POG Filter FIN PO Rejecting Module"),
3. register a parent in the hierarchy of modules (here we used the variant POG module of the Event-B POG that creates the POG we want to suppress: org.eventb.core.fwdMachineVariantModule),
4. create a class for this module.(here we created the class fr.systerel.rodinextension.sample.pog.modules.FinPORejectingModule).
