Extending the Proof Obligation Generator (How to extend Rodin Tutorial)
From Event-B
In this part
We will see how to proof obligations to discharge for machines after having added our extensions for Probabilistic Reasoning and 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 file 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.
