Difference between revisions of "Extending the Proof Obligation Generator(How to extend Rodin Tutorial)"

From Event-B
Jump to navigationJump to search
imported>Pascal
m
imported>Tommy
 
(17 intermediate revisions by one other user not shown)
Line 3: Line 3:
 
=== In this part ===
 
=== 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.
+
We will see how to create proof obligations (PO) for the machines relatively to our extensions for Probabilistic Reasoning and after having statically checked these machines. The latter operation is the first part of the proof obligation generation as the proof obligation generator (POG) takes statically checked files as 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?'''".
+
The question here is "'''What needs to be mathematically proved with these newly added elements in hands?'''".
 +
 
 +
We will study here the case of the ''BFN'' proof obligation, which is described in the paper. This PO overrides the ''FIN'' PO. Thus, we will see in this section how to:
 +
* Remove the ''FIN'' PO, which is generated by default.
 +
* Add our new ''BFN'' PO.
  
We will study here, the case of the ''BFN'' 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 ''BFN'' PO.
 
 
 
=== Principles ===
 
=== Principles ===
 +
1. To extend the POG in order to add some POs that have to be discharged, '''define a proof obligation processor module''' using the extension point <tt>org.eventb.core.pogModuleTypes</tt>.<br>
 +
2. Then, '''set up a configuration''' involving these modules and giving them a hierarchy. This is done exactly the same way as for creating a static checker configuration.<br>
 +
3. Finally, '''add this POG configuration''' to the default one, so the proof obligation generation can be performed.<br>
  
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 : <tt>org.eventb.core.pogModuleTypes</tt>.<br>
+
We will here show how to generate one PO. We will add the PO named ''BFN'' to ensure that the Bound is a natural number or is finite. It will be generated once for all for the machine taken into account. Moreover, this PO overrides the default ''FIN'' PO 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.
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.<br>
 
3. Finally, it is needed to '''add this POG configuration''' to the default one, so the proof obligation generation can be performed.<br>
 
 
 
 
 
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'' using informations in the state repository that we will add in step 2, so in step 3 we could create a filter to remove the PO ''FIN'' if our machine contains a probabilistic event.
+
In step 1, we will explain how to create our ''BFN'' PO using information in the state repository, we will add it in step 2, and then in step 3 we will create a filter to remove the ''FIN'' PO if our machine contains a probabilistic event.
  
=== Step 1 : Adding POG modules ===
+
=== Step 1: Adding POG modules ===
  
As we know that the POG takes its 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.
+
As we know that the POG takes its input from the static checker output, the presence of a statically checked Bound element (<tt>ISCBound</tt>) in the statically checked model is a prerequisite to prove the probabilistic convergence of this model. Thus, this information shall be shared through our hierarchy of POG modules, as it triggers the operations that they can perform.
  
We will anticipate using this information (stored in a <tt>IPOGState</tt>) to create the ''BFN'' proof obligation :
+
We will anticipate using this information (stored in a <tt>IPOGState</tt>) to create the ''BFN'' PO.
  
From the extension point <tt>org.eventb.core.pogModuleTypes</tt>, create a <tt>processorModule</tt> extension to implement our first PO generation process using a POG processor :<br>
+
From the extension point <tt>org.eventb.core.pogModuleTypes</tt>, create a <tt>processorModule</tt> extension to implement a first PO generation process using a POG processor.
 
As for a static checker module,<br>
 
As for a static checker module,<br>
1. give the module an id (here fwdMachineBoundModule),<br>
+
1. Give an ID to the module (here fwdMachineBoundModule).<br>
2. a human readable name (here "Machine POG Forward Bound Module"),<br>
+
2. Give it a human readable name (here "Machine POG Forward Bound Module").<br>
3. register a parent in the hierarchy of modules (here we used the machine POG module of the Event-B POG : <tt>org.eventb.core.machineModule</tt>),<br>
+
3. Register a parent in the hierarchy of modules (here we use the machine POG module of the Event-B POG <tt>org.eventb.core.machineModule</tt>).<br>
4. create a class for this module.(here we created the class <tt>fr.systerel.rodinextension.sample.pog.modules.FwdMachineBoundModule</tt>).
+
4. Create a class for this module (here we create the class <tt>fr.systerel.rodinextension.sample.pog.modules.FwdMachineBoundModule</tt>).
  
The above module should share (this is done by <tt>repository.setState()</tt>), at its initialisation, an <tt>IMachineBoundInfo</tt> state that we will implement in step 2.
+
The above module shall share (this is done with <tt>repository.setState</tt>), at its initialisation, an <tt>IMachineBoundInfo</tt> state that we will implement in step 2.
  
 
  @Override
 
  @Override
  public void initModule(IRodinElement element,IPOGStateRepository repository, IProgressMonitor monitor) throws CoreException {
+
  public void initModule(IRodinElement element,IPOGStateRepository repository, IProgressMonitor monitor)  
 +
          throws CoreException {
 
  repository.setState(createMachineBoundInfo(element, repository));
 
  repository.setState(createMachineBoundInfo(element, repository));
 
  }
 
  }
 
   
 
   
  private IMachineBoundInfo createMachineBoundInfo(IRodinElement element, IPOGStateRepository repository) throws CoreException {
+
  private IMachineBoundInfo createMachineBoundInfo(IRodinElement element, IPOGStateRepository repository)  
 +
          throws CoreException {
 
  final IRodinFile machineFile = (IRodinFile) element;
 
  final IRodinFile machineFile = (IRodinFile) element;
 
  final ISCMachineRoot root = (ISCMachineRoot) machineFile.getRoot();
 
  final ISCMachineRoot root = (ISCMachineRoot) machineFile.getRoot();
Line 50: Line 50:
 
  final ISCBound scBound = bounds[0];
 
  final ISCBound scBound = bounds[0];
 
  final ITypeEnvironment typeEnv = repository.getTypeEnvironment();
 
  final ITypeEnvironment typeEnv = repository.getTypeEnvironment();
  final Expression expr = scBound.getExpression(typeEnv.getFormulaFactory(), typeEnv);
+
  final Expression expr = scBound.getExpression(typeEnv);
 
  return new MachineBoundInfo(expr, scBound);
 
  return new MachineBoundInfo(expr, scBound);
 
  }
 
  }
Where <tt>MachineBoundInfo</tt> will be our class representing the state for the bound of the traversed machine.
+
Where <tt>MachineBoundInfo</tt> is the class representing the state for the bound of the traversed machine.
  
To use a registered state of the repository, one can use  
+
To use a registered state of the repository, it is possible to use  
 
  repository.getState(IStateType<? extends IPOGState> stateType)
 
  repository.getState(IStateType<? extends IPOGState> stateType)
  
As we suppose the MachineBoundInfo to be a state available after our module is initialized, we will here use :
+
As we suppose the <tt>MachineBoundInfo</tt> to be a state available after our module is initialized, we will here use
  final IMachineBoundInfo machineBoundInfo = (IMachineBoundInfo) repository.getState(IMachineBoundInfo.STATE_TYPE);
+
  final IMachineBoundInfo machineBoundInfo =  
 +
  (IMachineBoundInfo) repository.getState(IMachineBoundInfo.STATE_TYPE);
  
 
Sub-modules of our module <tt>fwdMachineBoundFinitenessModule</tt> can use this state freely from the repository using the above invocation.
 
Sub-modules of our module <tt>fwdMachineBoundFinitenessModule</tt> can use this state freely from the repository using the above invocation.
What we want to do is creating a ''BFN'' PO if the bound expression is not trivially finite. A trivially finite expression is an integer expression or derived from a boolean type.
+
What we want to do is to create a ''BFN'' PO if the bound expression is not trivially finite. A trivially finite expression is an integer expression or is derived from a boolean type.
  
Here is the code that makes those checkings :
+
Here is the code that makes these checks:
  
 
  private boolean mustProveFinite(Expression expr, FormulaFactory ff) {
 
  private boolean mustProveFinite(Expression expr, FormulaFactory ff) {
Line 83: Line 84:
 
  if (type instanceof ProductType) {
 
  if (type instanceof ProductType) {
 
  final ProductType productType = (ProductType) type;
 
  final ProductType productType = (ProductType) type;
  return derivedFromBoolean(productType.getLeft(), ff) && derivedFromBoolean(productType.getRight(), ff);
+
  return derivedFromBoolean(productType.getLeft(), ff) &&  
 +
                      derivedFromBoolean(productType.getRight(), ff);
 
  }
 
  }
 
  return false;
 
  return false;
 
  }
 
  }
  
Here is the corresponding code that generates the PO ''BFN'' put into the process() method of our module :
+
Here is the corresponding code that generates the ''BFN'' PO put into the <tt>process</tt> method of our module:
  
final IMachineBoundInfo machineBoundInfo = (IMachineBoundInfo) repository.getState(IMachineBoundInfo.STATE_TYPE);
+
final IMachineBoundInfo machineBoundInfo =  
  final ISCBound scBound = machineBoundInfo.getBound();
+
  (IMachineBoundInfo) repository.getState(IMachineBoundInfo.STATE_TYPE);
final Expression expr = machineBoundInfo.getExpression();
+
final ISCBound scBound = machineBoundInfo.getBound();
final FormulaFactory ff = repository.getFormulaFactory();
+
final Expression expr = machineBoundInfo.getExpression();
final IPOGSource[] sources = new IPOGSource[] { makeSource(IPOSource.DEFAULT_ROLE, scBound.getSource()) };
+
final FormulaFactory ff = repository.getFormulaFactory();
final IPORoot target = repository.getTarget();
+
final IPOGSource[] sources = new IPOGSource[] { makeSource(IPOSource.DEFAULT_ROLE, scBound.getSource()) };
final IMachineHypothesisManager machineHypothesisManager = (IMachineHypothesisManager) repository.getState(IMachineHypothesisManager.STATE_TYPE);
+
final IPORoot target = repository.getTarget();
 +
final IMachineHypothesisManager machineHypothesisManager = (IMachineHypothesisManager)
 +
  repository.getState(IMachineHypothesisManager.STATE_TYPE);
 
   
 
   
// if the finitness of bound is not trivial
+
// if the finiteness of bound is not trivial
// we generate the PO
+
// we generate the PO
if (mustProveFinite(expr, ff)) {
+
if (mustProveFinite(expr, ff)) {
final Predicate finPredicate = ff.makeSimplePredicate(Formula.KFINITE, expr, null);
+
  final Predicate finPredicate = ff.makeSimplePredicate(Formula.KFINITE, expr, null);
createPO(target, "BFN",
+
  createPO(target, "BFN",
POGProcessorModule.makeNature("Finiteness of bound"),
+
    POGProcessorModule.makeNature("Finiteness of bound"),
machineHypothesisManager.getFullHypothesis(),
+
    machineHypothesisManager.getFullHypothesis(),
makePredicate(finPredicate, scBound.getSource()), sources,
+
    makePredicate(finPredicate, scBound.getSource()), sources,
machineHypothesisManager.machineIsAccurate(), monitor);
+
    machineHypothesisManager.machineIsAccurate(), monitor);
  
 
Add this module to the configuration created for the static checker by creating an extension <tt>pogModule</tt>.
 
Add this module to the configuration created for the static checker by creating an extension <tt>pogModule</tt>.
  
=== Step 2 : creating the support for sharing bound informations among POG sub-modules ===
+
=== Step 2: Creating the support for sharing bound informations among POG sub-modules ===
  
We will here create the extension to store the informations about the statically checked bound which we want available through sub-modules.  
+
We will here create the extension to store the information about the statically checked bound which shall be available through sub-modules.  
To do this : add the <tt>org.eventb.core.pogStateTypes</tt> extension point to our plugin.
+
To do that, add the <tt>org.eventb.core.pogStateTypes</tt> extension point to the plug-in.
Then create an extension <tt>stateType</tt> :<br>
+
Then, create an extension <tt>stateType</tt>:<br>
- id : machineBoundInfo<br>
+
- ID: machineBoundInfo.<br>
- name : POG Machine Bound Info<br>
+
- Name: POG Machine Bound Info.<br>
- class : a new class that will implement the interface described below (here <tt>MachineBoundInfo</tt>).<br>
+
- Class: a new class that will implement the interface described below (here <tt>MachineBoundInfo</tt>).<br>
  
We want three methods to be available in this interface :
+
Three methods shall be available in this interface:
* <tt>getExpression()</tt> to retrieve the expression of the bound,
+
* <tt>getExpression</tt>, to retrieve the expression of the bound.
* <tt>getBound()</tt> to retrieve the statically checked bound,
+
* <tt>getBound</tt>, to retrieve the statically checked bound.
* <tt>hasMachineBound()</tt> telling if the currently processed machine has a bound or not.
+
* <tt>hasMachineBound</tt>, telling if the currently processed machine has a bound or not.
  
Here is the interface <tt>IMachineBoundInfo</tt> one has to create:  
+
Here is the interface <tt>IMachineBoundInfo</tt>:  
  
 
  public interface IMachineBoundInfo extends IPOGState {
 
  public interface IMachineBoundInfo extends IPOGState {
 
   
 
   
  final static IStateType<IMachineBoundInfo> STATE_TYPE = POGCore.getToolStateType(QualProbPlugin.PLUGIN_ID + ".machineBoundInfo");
+
  final static IStateType<IMachineBoundInfo> STATE_TYPE =  
 +
          POGCore.getToolStateType(QualProbPlugin.PLUGIN_ID + ".machineBoundInfo");
 
 
 
 
 
  /**
 
  /**
Line 155: Line 160:
 
  }
 
  }
  
and here is its implementation class :
+
and here is its implementation class:
  
 
  public class MachineBoundInfo implements IMachineBoundInfo {
 
  public class MachineBoundInfo implements IMachineBoundInfo {
Line 214: Line 219:
 
  }
 
  }
  
=== Step 3 : Removing a PO ===
+
=== Step 3: Removing a PO ===
  
To remove a PO, one has to create a filter module. This can be done the same way as for the static checker. After a small search in the package <tt>org.eventb.internal.core.pog.modules</tt>, we identify that the module responsible of creating the ''FIN'' PO is actually <tt>FwdMachineVariantModule</tt>. The goal is here to register our filter as a submodule of <tt>FwdMachineVariantModule</tt> and prevent it to create the ''FIN'' PO.
+
To remove a PO, it is necessary to create a filter module. This can be done in the same way as for the static checker. After a small search in the package <tt>org.eventb.internal.core.pog.modules</tt>, we identify that the module responsible of creating the ''FIN'' PO is actually <tt>FwdMachineVariantModule</tt>. The goal is here to register the filter as a sub-module of <tt>FwdMachineVariantModule</tt> and 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,  
+
The code is really simple... We first check if the model contains a probabilistic event, in which case we want to override the ''FIN'' PO created by default. Then, we search among the generated POs if one corresponds to ''FIN'' and in that event we reject it.
and then, 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 <tt>finPORejectingModule</tt>),<br>
+
1. Give an ID to the module (here <tt>finPORejectingModule</tt>).<br>
2. a human readable name (here "Machine POG Filter FIN PO Rejecting Module"),<br>
+
2. Give it a human readable name (here "Machine POG Filter FIN PO Rejecting Module").<br>
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: <tt>org.eventb.core.fwdMachineVariantModule</tt>),<br>
+
3. Register a parent in the hierarchy of modules (here we use the variant POG module of the Event-B POG that creates the POG to be suppressed <tt>org.eventb.core.fwdMachineVariantModule</tt>).<br>
4. create a class for this module.(here we created the class <tt>fr.systerel.rodinextension.sample.pog.modules.FinPORejectingModule</tt>).
+
4. Create a class for this module (here we create the class <tt>fr.systerel.rodinextension.sample.pog.modules.FinPORejectingModule</tt>).
  
Here we just retrieve the bound informations in the <tt>initModule()</tt>, so we can check in the <tt>accept()</tt> method that the current machine aims to be proved against probabilistic convergence, and remove the ''FIN'' PO which is about to be created. Here is what the code might look like :
+
Here we just retrieve the bound information in the <tt>initModule</tt>, so we can check in the <tt>accept</tt> method if the current machine has to be proved against probabilistic convergence, and remove the ''FIN'' PO which is about to be created. Here is what the code might look like:
  
 
  public class FinPORejectingFilterModule extends POGFilterModule {
 
  public class FinPORejectingFilterModule extends POGFilterModule {
 
   
 
   
  private static final IModuleType<FinPORejectingFilterModule> MODULE_TYPE = POGCore.getModuleType(QualProbPlugin.PLUGIN_ID + ".finPORejectingModule");
+
  private static final IModuleType<FinPORejectingFilterModule> MODULE_TYPE =
 +
          POGCore.getModuleType(QualProbPlugin.PLUGIN_ID + ".finPORejectingModule");
 
  private IMachineBoundInfo boundInfo;
 
  private IMachineBoundInfo boundInfo;
 
   
 
   
Line 239: Line 244:
 
   
 
   
 
  @Override
 
  @Override
  public boolean accept(String poName, IProgressMonitor monitor) throws CoreException {
+
  public boolean accept(String poName, IProgressMonitor monitor)  
 +
          throws CoreException {
 
  if (! boundInfo.machineHasBound()) {
 
  if (! boundInfo.machineHasBound()) {
 
  return true;
 
  return true;
Line 251: Line 257:
 
   
 
   
 
  @Override
 
  @Override
  public void initModule(IPOGStateRepository repository, IProgressMonitor monitor) throws CoreException {
+
  public void initModule(IPOGStateRepository repository, IProgressMonitor monitor)  
 +
          throws CoreException {
 
  boundInfo = (IMachineBoundInfo) repository.getState(IMachineBoundInfo.STATE_TYPE);
 
  boundInfo = (IMachineBoundInfo) repository.getState(IMachineBoundInfo.STATE_TYPE);
 
  }
 
  }
 
   
 
   
 
  @Override
 
  @Override
  public void endModule(IPOGStateRepository repository, IProgressMonitor monitor) throws CoreException {
+
  public void endModule(IPOGStateRepository repository, IProgressMonitor monitor)  
 +
          throws CoreException {
 
  boundInfo = null;
 
  boundInfo = null;
 
  }
 
  }

Latest revision as of 13:57, 5 September 2013

In this part

We will see how to create proof obligations (PO) for the machines relatively to our extensions for Probabilistic Reasoning and after having statically checked these machines. The latter operation is the first part of the proof obligation generation as the proof obligation generator (POG) takes statically checked files as 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 these newly added elements in hands?".

We will study here the case of the BFN proof obligation, which is described in the paper. This PO overrides the FIN PO. Thus, we will see in this section how to:

  • Remove the FIN PO, which is generated by default.
  • Add our new BFN PO.

Principles

1. To extend the POG in order to add some POs that have to be discharged, define a proof obligation processor module using the extension point org.eventb.core.pogModuleTypes.
2. Then, set up a configuration involving these modules and giving them a hierarchy. This is done exactly the same way as for creating a static checker configuration.
3. Finally, add this POG configuration to the default one, so the proof obligation generation can be performed.

We will here show how to generate one PO. We will add the PO named BFN to ensure that the Bound is a natural number or is finite. It will be generated once for all for the machine taken into account. Moreover, this PO overrides the default FIN PO 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 BFN PO using information in the state repository, we will add it in step 2, and then in step 3 we will create a filter to remove the FIN PO if our machine contains a probabilistic event.

Step 1: Adding POG modules

As we know that the POG takes its input from the static checker output, the presence of a statically checked Bound element (ISCBound) in the statically checked model is a prerequisite to prove the probabilistic convergence of this model. Thus, this information shall be shared through our hierarchy of POG modules, as it triggers the operations that they can perform.

We will anticipate using this information (stored in a IPOGState) to create the BFN PO.

From the extension point org.eventb.core.pogModuleTypes, create a processorModule extension to implement a first PO generation process using a POG processor. As for a static checker module,
1. Give an ID to the module (here fwdMachineBoundModule).
2. Give it a human readable name (here "Machine POG Forward Bound Module").
3. Register a parent in the hierarchy of modules (here we use the machine POG module of the Event-B POG org.eventb.core.machineModule).
4. Create a class for this module (here we create the class fr.systerel.rodinextension.sample.pog.modules.FwdMachineBoundModule).

The above module shall share (this is done with repository.setState), at its initialisation, an IMachineBoundInfo state that we will implement in step 2.

	@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);
		return new MachineBoundInfo(expr, scBound);
	}

Where MachineBoundInfo is the class representing the state for the bound of the traversed machine.

To use a registered state of the repository, it is possible to use

repository.getState(IStateType<? extends IPOGState> stateType)

As we suppose the MachineBoundInfo to be a state available after our module is initialized, we will here use

final IMachineBoundInfo machineBoundInfo = 
  (IMachineBoundInfo) repository.getState(IMachineBoundInfo.STATE_TYPE);

Sub-modules of our module fwdMachineBoundFinitenessModule can use this state freely from the repository using the above invocation. What we want to do is to create a BFN PO if the bound expression is not trivially finite. A trivially finite expression is an integer expression or is derived from a boolean type.

Here is the code that makes these checks:

private boolean mustProveFinite(Expression expr, FormulaFactory ff) {
		final Type type = expr.getType();
		if (type.equals(ff.makeIntegerType()))
			return false;
		if (derivedFromBoolean(type, ff))
			return false;
		return true;
	}
private boolean derivedFromBoolean(Type type, FormulaFactory ff) {
	if (type.equals(ff.makeBooleanType()))
		return true;
	final Type baseType = type.getBaseType();
	if (baseType != null)
		return derivedFromBoolean(baseType, ff);
	if (type instanceof ProductType) {
		final ProductType productType = (ProductType) type;
		return derivedFromBoolean(productType.getLeft(), ff) && 
                      derivedFromBoolean(productType.getRight(), ff);
	}
	return false;
}

Here is the corresponding code that generates the BFN PO put into the process method of our module:

final IMachineBoundInfo machineBoundInfo = 
  (IMachineBoundInfo) repository.getState(IMachineBoundInfo.STATE_TYPE);
final ISCBound scBound = machineBoundInfo.getBound();
final Expression expr = machineBoundInfo.getExpression();
final FormulaFactory ff = repository.getFormulaFactory();
final IPOGSource[] sources = new IPOGSource[] { makeSource(IPOSource.DEFAULT_ROLE, scBound.getSource()) };
final IPORoot target = repository.getTarget();
final IMachineHypothesisManager machineHypothesisManager = (IMachineHypothesisManager)
  repository.getState(IMachineHypothesisManager.STATE_TYPE);

// if the finiteness of bound is not trivial
// we generate the PO
if (mustProveFinite(expr, ff)) {
  final Predicate finPredicate = ff.makeSimplePredicate(Formula.KFINITE, expr, null);
  createPO(target, "BFN",
    POGProcessorModule.makeNature("Finiteness of bound"),
    machineHypothesisManager.getFullHypothesis(),
    makePredicate(finPredicate, scBound.getSource()), sources,
    machineHypothesisManager.machineIsAccurate(), monitor);

Add this module to the configuration created for the static checker by creating an extension pogModule.

Step 2: Creating the support for sharing bound informations among POG sub-modules

We will here create the extension to store the information about the statically checked bound which shall be available through sub-modules. To do that, add the org.eventb.core.pogStateTypes extension point to the plug-in. Then, create an extension stateType:
- ID: machineBoundInfo.
- Name: POG Machine Bound Info.
- Class: a new class that will implement the interface described below (here MachineBoundInfo).

Three methods shall be available in this interface:

  • getExpression, to retrieve the expression of the bound.
  • getBound, to retrieve the statically checked bound.
  • hasMachineBound, telling if the currently processed machine has a bound or not.

Here is the interface IMachineBoundInfo:

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 final Expression boundExpression;
	private final ISCBound bound;
 	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();
	}
 	
	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 3: Removing a PO

To remove a PO, it is necessary to create a filter module. This can be done in the same way as 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 the filter as a sub-module of FwdMachineVariantModule and prevent it to create the FIN PO.

The code is really simple... We first check if the model contains a probabilistic event, in which case we want to override the FIN PO created by default. Then, we search among the generated POs if one corresponds to FIN and in that event we reject it.

1. Give an ID to the module (here finPORejectingModule).
2. Give it a human readable name (here "Machine POG Filter FIN PO Rejecting Module").
3. Register a parent in the hierarchy of modules (here we use the variant POG module of the Event-B POG that creates the POG to be suppressed org.eventb.core.fwdMachineVariantModule).
4. Create a class for this module (here we create the class fr.systerel.rodinextension.sample.pog.modules.FinPORejectingModule).

Here we just retrieve the bound information in the initModule, so we can check in the accept method if the current machine has to be proved against probabilistic convergence, and remove the FIN PO which is about to be created. Here is what the code might look like:

public class FinPORejectingFilterModule extends POGFilterModule {

	private static final IModuleType<FinPORejectingFilterModule> MODULE_TYPE =
         POGCore.getModuleType(QualProbPlugin.PLUGIN_ID + ".finPORejectingModule");
	private IMachineBoundInfo boundInfo;

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

	@Override
	public boolean accept(String poName, IProgressMonitor monitor) 
         throws CoreException {
		if (! boundInfo.machineHasBound()) {
			return true;
		}
		final boolean rejectedFIN = poName.equals("FIN");
		if (QualProbPlugin.DEBUG) {
			System.out.println("PO " + poName + " is "+ (rejectedFIN ? "" : "not ") + "filtered out.");
		}
		return !rejectedFIN;
	}

	@Override
	public void initModule(IPOGStateRepository repository, IProgressMonitor monitor) 
         throws CoreException {
		boundInfo = (IMachineBoundInfo) repository.getState(IMachineBoundInfo.STATE_TYPE);
	}

	@Override
	public void endModule(IPOGStateRepository repository, IProgressMonitor monitor) 
         throws CoreException {
		boundInfo = null;
	}

}