Qualitative Probability
From Event-B
Return to Rodin Plug-ins
The Qualitative Probability plug-in provides supports for reasoning about termination with probability 1 (almost-certain termination).
Please have a look also at the Qualitative Probability User Guide.
Current version
The Qualitative Probability plug-in version 0.2.4 is available as a separate plug-in from the main Rodin update site (under the Modelling Extensions category).
Principles
Qualitative Probability plug-in provide a new probabilistic attribute for event. When this attribute is set and the event is convergent, the event will be interpreted as probabilistic convergent.
