AnimB roadmap: Difference between revisions
From Event-B
Jump to navigationJump to search
imported>Mathieu |
imported>Mathieu m wording |
||
(2 intermediate revisions by one other user not shown) | |||
Line 1: | Line 1: | ||
The following array describes the features which will be developed. | The following array describes the features which will be developed as soon as possible. | ||
{| border="1" cellpadding="20" cellspacing="0" | {| border="1" cellpadding="20" cellspacing="0" | ||
!Feature | !Feature | ||
Line 10: | Line 10: | ||
|- | |- | ||
|Predicate evaluator | |Predicate evaluator | ||
|Today the predicate evaluator | |Today the predicate evaluator doesn't use type information to infer a set that allow iteration of variable. | ||
| - | | - | ||
|- | |- | ||
|Sorter on event table column | |Sorter on event table column | ||
|The events, constants and variables are listed using the editing order given by the Rodin database. This new feature | |The events, constants and variables are listed using the editing order given by the Rodin database. This new feature would allow the user to manage the order of events, constants and variables. | ||
| - | | - | ||
|- | |- | ||
|Extension of predicate evaluator | |Extension of predicate evaluator | ||
|Today, the predicate evaluator | |Today, the predicate evaluator doesn't allow the variable quantification with function sets (injection, bijection, ...) | ||
| - | |||
|- | |||
|Adding guard evaluation | |||
|Today, the animator stops the guard evaluation on the first wrong guard. It should be possible to continue the evaluation until the first guard that has a non trivial well defined predicate. | |||
| - | | - | ||
|} | |} | ||
[[Category:Work in progress]] | [[Category:Work in progress]] | ||
[[Category:AnimB]] | [[Category:AnimB]] |
Latest revision as of 20:27, 10 March 2009
The following array describes the features which will be developed as soon as possible.
Feature | Description | Date |
---|---|---|
History saving | The history saving allows the user to save and replay a saved history | - |
Predicate evaluator | Today the predicate evaluator doesn't use type information to infer a set that allow iteration of variable. | - |
Sorter on event table column | The events, constants and variables are listed using the editing order given by the Rodin database. This new feature would allow the user to manage the order of events, constants and variables. | - |
Extension of predicate evaluator | Today, the predicate evaluator doesn't allow the variable quantification with function sets (injection, bijection, ...) | - |
Adding guard evaluation | Today, the animator stops the guard evaluation on the first wrong guard. It should be possible to continue the evaluation until the first guard that has a non trivial well defined predicate. | - |