Difference between pages "All Rewrite Rules" and "Event-B Qualitative Probability User Guide"

Revision as of 11:14, 23 November 2011

User:Son at ETH Zurich is in charge of the plug-in.

Event-B Qualitative Probability plug-in provides supports for reasoning about termination with probability 1 (almost-certain termination).

The plug-in is available through the main Rodin Update Site under Modelling Extension category.

@@ Line 1: / Line 1: @@
-This page groups together all the rewrite rules implemented (or planned for implementation) in the Rodin prover. The rules themselves can be found in the following locations (for editing purposes):
+[[User:Son]] at '''ETH Zurich''' is in charge of the plug-in.
-* [[Set Rewrite Rules]]
+{{TOCright}}
-* [[Relation Rewrite Rules]]
-* [[Arithmetic Rewrite Rules]]
-Conventions used in these tables are described in [[The_Proving_Perspective_%28Rodin_User_Manual%29#Rewrite_rules]]
+== Introduction ==
+Event-B Qualitative Probability plug-in provides supports for reasoning about termination with probability 1 (almost-certain termination).
-{{:Set Rewrite Rules}}
-{{:Relation Rewrite Rules}}
+== Installing and Updating ==
+The plug-in is available through the main Rodin Update Site under '''Modelling Extension''' category.
-{{:Arithmetic Rewrite Rules}}
+== News ==
+* 23.11.2011: Version 0.2.1 released for Rodin 2.3.*
+== Technical References ==
+== Usage ==