View source for Plug-in Wishlist

== Introduction ==

This page has been created to give a wish list of tool plug-ins that cannot be resourced by [[Deploy]].
These plug-ins could be developed by [[Deploy]] partners or by external partners.

== The Rodin Workshop 2009 Wishlist ==
The following list has been established during the [[Rodin_Workshop_2009 | Rodin User and Developer Workshop 2009]] (July 15-17 2009): 

* Enabledness POs
* Automatic refinement
* Support for probability
* Automated provers / SMT for set theory
** common context
** used hypothesis
** extensible operator
* Reasoned modeling support
* Flexible document management

== Structural Checker Plug-in ==
The idea of such a plug-in is to perform structural checks on Event-B models.

It could for example ensure that some good-usage rules are enforced, or produce a list of warnings to provide help when modeling (''eg.'' an anticipated event has been found in last refinement).

== Other items ==

* Support for re-play of proofs on other POs.