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

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Pascal
(CAUTION! Any modification to this page shall be announced on the User mailing list!)
 
imported>Son
m
 
Line 1: Line 1:
<font color=red>CAUTION! Any modification to this page shall be announced on the [[#Mailing_lists |User]] mailing list!</font>
+
[[User:Son]] at '''ETH Zurich''' is in charge of the plug-in.
 +
{{TOCright}}
  
This page groups together all the rewrite rules implemented (or planned for implementation) in the Rodin prover. The rules themselves can be found in their respective location (for editing purposes):
+
== Introduction ==
 +
Event-B Qualitative Probability plug-in provides supports for reasoning about termination with probability 1 (almost-certain termination).
  
Conventions used in these tables are described in [[The_Proving_Perspective_%28Rodin_User_Manual%29#Rewrite_rules]]
 
  
==[[Set Rewrite Rules]]==
+
== Installing and Updating ==
{{:Set Rewrite Rules}}
+
The plug-in is available through the main Rodin Update Site under '''Modelling Extension''' category.
  
==[[Relation Rewrite Rules]]==
+
== News ==
{{:Relation Rewrite Rules}}
+
* 23.11.2011: Version 0.2.1 released for Rodin 2.3.*
  
==[[Arithmetic Rewrite Rules]]==
+
== Technical References ==
{{:Arithmetic Rewrite Rules}}
+
 
 +
== Usage ==

Revision as of 11:14, 23 November 2011

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

Introduction

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


Installing and Updating

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

News

  • 23.11.2011: Version 0.2.1 released for Rodin 2.3.*

Technical References

Usage