Difference between revisions of "User:Mathieu/Event-B IDE:Needed use cases"
From Event-B
Jump to navigationJump to searchimported>Mathieu m (new page) |
imported>Mathieu m (A way to quickly jump along an event refinement chain by skipping all extended and unmodified events) |
||
| Line 3: | Line 3: | ||
* 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 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). | * 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 == | == Model refactoring == | ||
Latest revision as of 10:02, 24 February 2009
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).
- 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).
