Qualitative Probability

From Event-B
Jump to navigationJump to search

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).


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.