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

From Event-B
< User:Mathieu
Revision as of 08:34, 24 February 2009 by imported>Mathieu (new page)
(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)
Jump to navigationJump to search

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