Menu
▾
▴
#22 Order of generated invariants
Currently the order of generated invariants is not fixed. This should be possible for the modellers to define the order of the state machines to be generated. Moreover, in some cases, the generated Event-B machine cannot be type-checked due to the order of the invariants generated. This is because invariants within a machine A referring state of another machine B, and invariants of A is generated before B. As a result, the invariants generation should be in two phases
1. Generate all "typing" invariants from all state machines.
2. Generate other invariants from all state machines.
Best,
Son
Fixed for next release: Generated elements now contain their position priority as a Rodin Attribute so that the priority of elements generated by other extensions (i.e. diagrams) are respected. Also, generated elements of the same priority follow the order of the extensions that generate them. The navigator now shows the correct order of the extensions in the model instead of sorting to alphabetical.