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. 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 : " Which are the conditions under which the model is correct for proof obligation generation? ".
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
In our case of probabilistic reasoning, the following conditions are checked 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 sorts 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.
