Extending the Static Checker (How to extend Rodin Tutorial)

<prev: Extending_the_Static_Checker(How_to_extend_Rodin_Tutorial)

^up: How to extend Rodin Tutorial (Index)

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. In fact, we have to be sure before creating Proof Obligations, that the model is correctly expressed (i.e. proof obligations are generated for a model which is sound).
The question addressed here is : " Under which conditions (about correctness of the model) the proof obligation generation means something ? ".

Principles

1. To extend the static checker 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.
3. Finally, it is needed to add this configuration to the default one, so our checkings can be performed.

Step1 : Adding modules

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

1. The variant V (declared as usual) is either of the type integer or some set.
2. 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.
3. Every probabilistic event must 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 sorts of situations during the static checking :

1. we encounter a problem which doesn't affect the PO generation : this leads to a warning (corrected by a default assumption or not).
2. we encounter a problem which affects the PO generation : this leads to an error.

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. If the static check fails for the considered element, the module must not add such element. Processors are also responsible of running sub-processors and adding states to the repository if required.
The processor that we will create will perform checkings and eventually, add the statically checked version of the bound to the statically checked machine.

Whereas filterModules performs only some verifications (i.e. a filtermodule must not add the element in the statically checked file). Furthermore, the filters are called (in group) from processors, and as soon as one filter reject one elements, the others will not be evaluated.

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 name. To do this we use the static method in org.eventb.core.sc.SCCore.getModuleType() with our module extension complete id : QualProbPlugin.PLUGIN_ID + ".machineBoundModule".
Thus, let's use the constant below in our module :

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 explainations about 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.

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, threat each element one by one, calling sub-processor modules.

Step2 : Set up a static checking configuration

<prev: Extending_the_Static_Checker(How_to_extend_Rodin_Tutorial)

^up: How to extend Rodin Tutorial (Index)