User:Mathieu/Event-B IDE:Needed use cases

From Event-B
Jump to navigationJump to search
The printable version is no longer supported and may have rendering errors. Please update your browser bookmarks and please use the default browser print function instead.

Model understanding

  • A mean to quickly see which variables are changed from a refinement to another one (new variables, removed one)
  • A mean to follow a slice of a model across refinements. For example, given 2 events, it is useful to be able to see them and only them side by side on several refinement levels (textual export with event markers and sed do the trick)
  • A mean to diff two levels of refinements and quickly see what as change from one level to the next one (textual export and classical diff do the trick).

Model Navigation

  • A way to quickly jump along an event refinement chain by skipping all extended and unmodified events.

Model refactoring

  • Be able to change a guard (given by a formula) by another one in the whole model


Other difficulties

  • It is somewhat difficult to propagate the changes down after inserting a new refinement between two existing levels (a way to diff contiguous levels may be useful).