Difference between revisions of "Event-B Statemachines"

From Event-B
Jump to navigationJump to search
imported>Vitaly
imported>Colin
 
(43 intermediate revisions by 4 users not shown)
Line 3: Line 3:
 
==Overview==
 
==Overview==
  
Event-B Statemachines Plug-in is part of the iUML-B experimental tool that focuses on UML-B and Event-B integration. The plug-in provides a way of adding state machines directly to Event-B machines and is capable of translating former to Event-B language. It also offers a UML-like diagram editor for state machines, as well as state machine animation, which can be installed as additional plug-in that runs on top of ProB Animator.
+
The Event-B Statemachines Plug-in provides a way of adding state machines directly in to Event-B machines. The statemachines generate additional guards and actions which are added to the events that exist in the same machine. It offers a UML-like diagram editor for state machines, as well as a state machine animation facility based on the ProB Animator.
  
 
==Installation==
 
==Installation==
  
The Event-B Statemachines plug-in is available for installation from Rodin update site under Modelling Extensions category. Animation plug-in for it is available from Verification and Validation category. Both plug-ins require EMF and GMF frameworks, Event-B EMF framework, ProB, OCL and QVT - all of these dependencies will be installed automatically upon plug-in installation.
+
The iUML-B Statemachines plug-in is available for installation from the Rodin update site (Modelling Extensions category).
 +
Version 2.1.x and greater requires at least Rodin 3.x.x. For Rodin 2.8.x or earlier, install Version 2.0.x.
 +
 
 +
The iUML-B Statemachine Animation plug-in is available from the Rodin update site (Verification and Validation category).
 +
Version 2.1.x and greater requires at least Rodin 3.x.x. For Rodin 2.8.x or earlier, install Version 2.0.x.
 +
 
 +
The plug-ins require EMF and GMF frameworks, Event-B EMF framework, Event-B EMF Extensions framework, Event-B diagrams framework and , for animation, ProB - all of these dependencies will be installed automatically during installation installation.
  
 
==Using the tool==
 
==Using the tool==
Line 13: Line 19:
 
The tool consists of a standard UML-like graphical editor for state machine diagrams, an integration to Event-B Explorer and a translator to Event-B language. Some of these may seem familiar to you if you have experience with UML editors or UML-B plug-in for Rodin.
 
The tool consists of a standard UML-like graphical editor for state machine diagrams, an integration to Event-B Explorer and a translator to Event-B language. Some of these may seem familiar to you if you have experience with UML editors or UML-B plug-in for Rodin.
  
===Event-B Explorer===
+
===Event-B Navigator===
 +
[[Image:IUMLBSM_contextMenu.png|thumbnail|Adding a State machine in Event-B Navigator Context Menu]]
 +
[[Image:New_statemachine.png|thumbnail|State machine in Event-B Navigator]]
  
[[Image:New_statemachine.png|thumbnail|State machine in Event-B Explorer]]
+
To start the modelling all you have to do is to select a machine in the Event-B Navigator that you would like to extend with state machines and right click to get the Context Menu. Then select ''Add Statemachine'' from the context menu. An input dialog will appear asking you to name the new state machine. After that you should see the new state machine appear in the contents of the machine in the navigator. Double click on the statemachine in the navigator in order to open the statemachine diagram editor. In addition, there are ''Open'' and ''Delete'' actions available for state machine in the context menu of the navigator. These allow to open a state machine in editor (shortcut is double-click) and delete a state machine (shortcut is Delete key).
  
To start the modelling all you have to do is to select a machine in Event-B Explorer that you would like to extend with state machines and click on ''Create new statemachine'' from explorer's toolbar. An input dialog will appear asking you for name of a new state machine. After that you should be able to see a new state machine appearing as a child of machine in explorer.
+
===Diagram Editor===
 +
[[Image:Statemachine editor.png|thumbnail|State machine diagram editor]]
  
The explorer also shows the contents of state machines, including states, transitions and annotations. You can customise the amount if information you would like to see by going to explorer's menu (a small triangle at the top right-hand side) ''> Customize View.. > Filters'' tab. There are three filters defined for state machines: ''Annotation Filter, Transition Filter, State Filter'' - that hide corresponding elements in explorer (state filter hides simple states, like initial, final or ANY).
+
To edit a state machine in the diagram editor you simply double-click it in the navigator. The tool creates a diagram file for you with the same name as the root state machine.
  
In addition, there are ''Open'' and ''Delete'' actions available for state machine in context menu of explorer. These allow to open a state machine in editor (shortcut is double-click) and delete a state machine (shortcut is Delete key). In machine's context menu there are two more actions related to state machines: ''Refine with statemachines'' and ''Delete generated'' - which allow correspondingly to create a refinement of machine with state machine refinements (not available yet from standard ''Refine'' action of Rodin) and to delete all Event-B elements generated by state machines (required only for experimental purposes if generated things/diagrams get corrupted).
+
Working with the editor is straightforward. The element creation tools are available from palette, divided into three categories: ''States'', ''State Features'' and ''State Links''. When a diagram element is selected on canvas the Properties View shows its available properties (if you cannot find it, please go to Rodin's menu ''Window > Show View > Properties''). This view allows you to modify important features of each diagram element that will affect its translation.
  
===Diagram Editor===
+
Diagram editing is possible by using either a single editor, as state machines support unbounded level of nesting, or multiple editors - by opening each specific state machine in a separate editor (select ''Open Diagram'' from context menu of a nested state machine after right-clicking it). As nesting depth of state machines and number of states grows and the model becomes large this can be a useful feature.
 +
 
 +
After a state machine is complete it can be validated to make sure it has no semantic errors and translated to Event-B. When translated, it can be animated with ProB.
 +
 
 +
===Toolbar===
 +
 
 +
iUML-B contributes four toolbar buttons which perform the following actions:
 +
* ''Validate'' - Runs the validator to check that the state-machine model is well-formed
 +
* ''Translate to Event-B'' - Generates the Event-B that the State-machine represents. (Automatically runs the Validator first)
 +
* ''Start Animation'' - Animates the state-machine diagram (using ProB)
 +
* ''Stop Animation'' - Stops the state-machine animation and returns to the Event-B editing perspective
 +
 
 +
===Diagram Elements===
  
[[Image:Statemachine editor.png|thumbnail|left|State machine diagram editor]]
+
The diagram allows to create the following ''State'' elements:
 +
* State
 +
* Initial
 +
* Final
 +
* Junction
 +
* Fork/Join
 +
* Any
  
To edit a state machine in diagram editor you simply double-click it. The tool creates a diagram file for you with the same name as root state machine.
+
A state can have nested state machines, added from ''State Features'' (also called parallel (or orthogonal) regions).
 +
A state may own invariants (or theorems) which are defined as Event-B predicates.
 +
States can have transitions from one to another, created from ''State Links''.
  
Working with the editor is straightforward. The element creation tools are available from palette, divided into three categories: ''States'', ''State Features'' and ''State Links''. When a diagram element is selected on canvas the Properties View shows its available properties (if you cannot find it, please go to Rodin's menu ''Window > Show View > Properties''). After a state machine is complete it can be validated to make sure it has no semantic errors and translated to Event-B. When translated, it can be animated with ProB.
+
=====Transition Event Elaboration=====
  
 +
Transitions have a many-valued relation to Events via a property attribute called ''elaborates''. This means that the transition contributes its behaviour (state change as well as any attached property features) to existing events in the same Machine. The relationship is flexible and powerful. A single transition can elaborate many events representing different cases and/or several transitions in different statemachines can elaborate the same event so that the statemachines are forced to synchronise on those transitions. [Note that you should take care not to specify an event that can never be enabled. For example, if two transitions in the same statemachine elaborate the same event].
  
 +
=====Transition Properties=====
  
 +
A transition can be endowed with any of the features that are normally contained in events (i.e. parameters, witnesses, guards, actions). These features are added in the properties view when the transition is selected. They will be copied into the elaborated events when the state-machine is translated. Hence, although the state-machines are envisioned as ancilliary to a regular Event-B model, all modelling can be done from the diagram if so desired. [Note that only guards may be added to transition segments that target a junction (see below)].
  
 +
=====Junctions=====
  
 +
A ''junction'' pseudo state is available from the diagram palette. Incoming transition segments to a junction generate a disjunctive guard. I.e. the transition may fire from either of the incoming transition's source states. Junctions can be cascaded if required in order to build a bigger disjunction.
  
 +
Junctions can also be used to split the transition path so that the incoming disjunction is contributed to all of the outgoing paths
  
 +
Note: transition segments that target a junction may not elaborate events.
  
 +
=====Forks and Joins=====
  
 +
A ''fork''/''Join'' pseudo state is a available from the diagram palette. (The same pseudo state node is used for both fork and join). A fork is used so that a single transition can enter several parallel nested statemachines (which must all have the same parent state). A join is used to exit several parallel nested statemachines.
  
====Elements====
+
=====Any=====
  
The diagram allows to create the following ''State'' elements:
+
An ''any'' pseudo state is a available from the diagram palette. An any state is used to represent all of the states at the same level in the state-machine. Hence a transition whose source is an any state can fire irrespective of the current state of the statemachine. Note that the semantic is the same as a transition whose source is the parent state (statemachine boundary). Hence the any state is mostly used in the root level state-machine where there is no parent state.  
* State
 
* Refined State (shall not be used)
 
* Initial (state)
 
* Final (state)
 
* ANY (state)
 
Note: ANY-state is a convenience element for drawing local transitions which can also be drawn in a standard way - connecting parent state to its internal state.
 
  
A state can have nested state machines, added from ''State Features'', which correspond to UML parallel substates, also called parallel (or orthogonal) regions. As other features it may have invariants, which can also be theorems, and are defined as Event-B expression.
+
=====Lifting=====
  
Finally, states can have transitions from one to another, created from ''State Links''. Transitions can also be created from popup arrows on states and link to either existing states or to ones created from the context menu.
+
A statemachine can be ''lifted'' to a set of instances so that the statemachine represents the behaviour of all of these instances. This is similar to statemachines that are owned by a Class in the classic UML-B. In fact the feature will be used for this purpose when iUML-B class diagrams are available. The generated Event-B is lifted by  adding an extra parameter to each elaborated event in order to represent the contextual instance. The name of this parameter can be specified for the state-machine. The instance set and the self-name are both set in the properties view for the state-machine. [Note that currently instances must be constants or carrier sets, variable instance sets are not yet supported].
  
 
====Semantics====
 
====Semantics====
  
Listed elements, apart from refined versions (which are actually not intended for manual creation), are components of a standard UML state machine diagram notation. The semantics of Event-B state machines therefore compares to that of UML. Nevertheless, there is inevitable coupling between a state machine and Event-B which is important to consider during modelling.
+
The semantics of Event-B state machines differ from those of UML. Like Event-B, UML-B semantics are based on the underlying concept of spontaneous atomic guarded actions that change the state of the variables.
 +
Comparing with other commonly used semantics such as UML, UML-B has no concept of external events that may trigger transitions, no ability whereby one transition may invoke another and, as there is no so-called `big-step', terms such as `run to completion' have no meaning. (All these things can be, and often are, modelled explicitly when required by constructing suitable control variables and guards).  
  
State machines, states and transitions are integrated in Event-B machine and generate new elements in that machine upon translation:
+
====Translation to Event-B====
* States translate into boolean-typed variables (variable and type invariant)
 
* State machines and states translate to their relationship invariants such as substate and partitioning invariant
 
* Transitions and states translate to event guards and actions that describe state change behaviour
 
  
While state machines and states are not related to Event-B, for transitions it is necessary to know the events to which new guards and actions will be added. Thus a transition has an attribute called ''elaboration'' that links it to Event-B event. The relationship between two is rather flexible - a single transition can elaborate multiple events, and at the same time a single event can be elaborated by multiple transitions (you must be careful though not to misuse this feature).
+
State machines, states and transitions are contained within an Event-B machine and generate new elements in that same machine upon translation.
 +
There are two alternative translations available which are selectable from the properties view of the root level statemachine.
 +
* In the ''Enumeration'' translation, a single variable is generated for each statemachine. Its type is an enumerated set which is generated from the states of the statemachine or, for a lifted statemachine, a function from the instances set to this enumeration.  
 +
* In the ''Variables'' translation, a variable is generated for each state of the statemachine. The type of these variables is BOOL or, for a lifted statemachine, a subset of the instances set.  
  
State invariants is another Event-B aspect of state machine diagrams that has no connection with UML. Adding an invariant to a state will be interpreted in terms of Event-B as adding an invariant on state variable's value. State invariants are defined as Event-B expressions.
+
In either case, invariants are generated to ensure that the statemachine (or a particular instance thereof) is only ever in one of its states at a time and that the hierarchy is obeyed.
 +
Transitions contribute guards and actions, representing the state change of the transition in the chosen data representation, to the events that they elaborate.  
 +
An invariant in a state will be translated into Event-B by adding an anticedent that the state is active (i.e. the statemachine is in that state).
  
There are some semantic rules that must be obeyed in order for a state machine model to be valid and translatable to Event-B. These rules are implemented in the validation framework and are checked either when validation is called explicitly from context menu, or before the translation. Note that the set of rules is currently not complete thus not guaranteeing full correctness of the model.
+
===Validation===
 +
 
 +
There are some semantic rules that must be obeyed in order for a state machine model to be valid and translatable to Event-B. These rules are implemented in the validation framework and are checked either when validation is called explicitly from the context menu, or before the translation. Note that the set of rules is currently not complete thus not guaranteeing full correctness of the model.
  
 
[[Image:Statemachine markers.png|thumbnail|State machine error and warning markers]]
 
[[Image:Statemachine markers.png|thumbnail|State machine error and warning markers]]
  
Rules:
+
Rules:   [NEEDS UPDATING]
* Transition cannot go to initial state
+
==== State machine ====
* Transition cannot go from final state
+
* Name must be valid (not ''null'', nor empty string)
* Transition cannot go directly from initial to final state
+
* When ''Instances'' is defined, the self-name must be valid
* Transition should elaborate an event if
+
* Must have exactly one initial state if it is a root-level state machine
** it is on the root state machine (its source/target belongs to root)
+
* Must have exactly one initial state if it is a nested state machine with outgoing local transitions (going from a state to parent state or ANY state)
** it is in nested state machine and not initial or final (its source/target is initial or final state)
+
* Cannot have more than one final state.
* Initial state should have outgoing transitions
 
* Final state should have incoming transitions
 
* Root state machine must have an initial state
 
* State machine can only have one initial state
 
* State machine can only have one final state
 
* State machine must have an initial state if
 
** its parent state has incoming transitions
 
** it has outgoing local transitions (going from a state to parent state or ANY state)
 
* Concrete state cannot contain refined state machines
 
 
* Concrete state machine cannot have refined states
 
* Concrete state machine cannot have refined states
 
* Refined state machine cannot have concrete states
 
* Refined state machine cannot have concrete states
  
Not all the rules are strict i.e. violation of certain rules is not considered as error as it doesn't cause translation problems, but keeping a model semantically correct means everything will be translated as intended.
+
==== Initial state and transition ====
 +
* Initial state must have at least one outgoing transition
 +
* Initial state cannot have any incoming transition
 +
* Transition cannot go directly from initial state to final state.
 +
 
 +
==== Final state ====
 +
* Final state must have at least one incoming transition.
 +
* Final state cannot have any outgoing transition.
 +
 
 +
==== State (not initial nor final) ====
 +
* State name must be valid (e.g., not ''null'' nor empty string)
 +
* Any invariants' name must be valid (e.g., not ''null'' nor empty string)
 +
* There cannot be two invariants with the same name.
 +
* Invariants' predicate must not be ''null''
 +
* Concrete state cannot contain refined state machines
 +
 
 +
==== Transition ====
 +
* Source and target states must not be ''null''
 +
* Source and target states must not be dangling states.
 +
* Source and target states must be valid states.
 +
* Must elaborate and event if it is on the root-level state machine (either its source or target belongs to a root-level state machine).
 +
* It is in a nested state machine and not initial or final (its source/target is not initial and final state).
  
The diagram editor, as mentioned, has two ways of checking the diagram model against these rules: selecting ''Validate'' from diagram context menu or running a translation. After validation completes, it produces feedback in the form of a dialog, telling whether model is valid or has errors. The elements that violate specific rules are marked with error/warning markers, which are listed in Rodin Problems view, as well as displayed on the diagram.
 
  
====Context Menu====
+
Not all the rules are strict i.e. violation of certain rules is not considered an error as it doesn't cause translation problems, but keeping a model semantically correct means everything will be translated as intended.
  
The context menu of a diagram includes four specific actions:  
+
The diagram editor, as mentioned, has two ways of checking the diagram model against these rules: selecting ''Validate'' from the diagram context menu or running a translation. After validation completes, it produces feedback in the form of a dialog, which lists any warnings or errors. The elements that violate specific rules are marked with error/warning markers, which are listed in the Rodin Problems view, as well as displayed on the diagram.
* ''Validate'' - to run the validation check on state machine model
 
* ''Translate to Event-B'' - to run the translation of a state machine to Event-B language
 
* ''Start Animation'' - to run ProB animation and animate the diagram
 
* ''Stop Animation'' - to stop the animation and return to Event-B perspective
 
  
 
===Known Problems===
 
===Known Problems===
  
The tool is at the experimental development stage and has some known, and likely some unknown issues. Amongst the former ones:
+
'''Implicit Context extends chain becomes broken'''. This only applies when using the ''Enumerated'' Translation which generates an implicit context to define the enumeration set of states]. If you refine a machine containing a State-Machine without translating the refined statemachine (i.e. because your refinement didn't alter the statemachine) then subsequent refinements that do alter the statemachine introduce errors because the link to the abstract implicit context is not maintained. A work-around is to translate the statemachine of the middle refinement even though you didn’t change the statemachine. This will create an empty context to maintain the chain. Alternatively you can manually edit the extends of the implicit context in the refined level to link to the abstract implicit context. However, you can only do this using the ''Rose'' editor's Advanced tab because the generated implicit context is read-only to other editors.
* Renaming of machine or event causes existing diagrams to lose references to renamed element and thus become corrupted. Therefore it is recommended not to rename existing elements after you have created state machines.
 
* Refinement of machine is refining contained state machines only if you use the custom action from context menu ''Refine with statemachines''. Standard Rodin refinement mechanism is not supporting yet (though planned in the nearest release) extensions and thus ignore any non-Rodin elements including state machines.
 
* Refinement of state machines creates their refined versions in refined machine, but does not create corresponding diagram files. Thereby on opening a refined state machine a new diagram will be created with default layout, in other words the layout from abstract state machine diagram is not persisted in refinement.
 
* Animation of state machine diagrams works only on a single diagram
 
  
 
[[Category:Plugin]] [[Category:User documentation]]
 
[[Category:Plugin]] [[Category:User documentation]]

Latest revision as of 08:04, 6 October 2015

IUMLB big.png

Overview

The Event-B Statemachines Plug-in provides a way of adding state machines directly in to Event-B machines. The statemachines generate additional guards and actions which are added to the events that exist in the same machine. It offers a UML-like diagram editor for state machines, as well as a state machine animation facility based on the ProB Animator.

Installation

The iUML-B Statemachines plug-in is available for installation from the Rodin update site (Modelling Extensions category). Version 2.1.x and greater requires at least Rodin 3.x.x. For Rodin 2.8.x or earlier, install Version 2.0.x.

The iUML-B Statemachine Animation plug-in is available from the Rodin update site (Verification and Validation category). Version 2.1.x and greater requires at least Rodin 3.x.x. For Rodin 2.8.x or earlier, install Version 2.0.x.

The plug-ins require EMF and GMF frameworks, Event-B EMF framework, Event-B EMF Extensions framework, Event-B diagrams framework and , for animation, ProB - all of these dependencies will be installed automatically during installation installation.

Using the tool

The tool consists of a standard UML-like graphical editor for state machine diagrams, an integration to Event-B Explorer and a translator to Event-B language. Some of these may seem familiar to you if you have experience with UML editors or UML-B plug-in for Rodin.

Event-B Navigator

Adding a State machine in Event-B Navigator Context Menu
State machine in Event-B Navigator

To start the modelling all you have to do is to select a machine in the Event-B Navigator that you would like to extend with state machines and right click to get the Context Menu. Then select Add Statemachine from the context menu. An input dialog will appear asking you to name the new state machine. After that you should see the new state machine appear in the contents of the machine in the navigator. Double click on the statemachine in the navigator in order to open the statemachine diagram editor. In addition, there are Open and Delete actions available for state machine in the context menu of the navigator. These allow to open a state machine in editor (shortcut is double-click) and delete a state machine (shortcut is Delete key).

Diagram Editor

State machine diagram editor

To edit a state machine in the diagram editor you simply double-click it in the navigator. The tool creates a diagram file for you with the same name as the root state machine.

Working with the editor is straightforward. The element creation tools are available from palette, divided into three categories: States, State Features and State Links. When a diagram element is selected on canvas the Properties View shows its available properties (if you cannot find it, please go to Rodin's menu Window > Show View > Properties). This view allows you to modify important features of each diagram element that will affect its translation.

Diagram editing is possible by using either a single editor, as state machines support unbounded level of nesting, or multiple editors - by opening each specific state machine in a separate editor (select Open Diagram from context menu of a nested state machine after right-clicking it). As nesting depth of state machines and number of states grows and the model becomes large this can be a useful feature.

After a state machine is complete it can be validated to make sure it has no semantic errors and translated to Event-B. When translated, it can be animated with ProB.

Toolbar

iUML-B contributes four toolbar buttons which perform the following actions:

  • Validate - Runs the validator to check that the state-machine model is well-formed
  • Translate to Event-B - Generates the Event-B that the State-machine represents. (Automatically runs the Validator first)
  • Start Animation - Animates the state-machine diagram (using ProB)
  • Stop Animation - Stops the state-machine animation and returns to the Event-B editing perspective

Diagram Elements

The diagram allows to create the following State elements:

  • State
  • Initial
  • Final
  • Junction
  • Fork/Join
  • Any

A state can have nested state machines, added from State Features (also called parallel (or orthogonal) regions). A state may own invariants (or theorems) which are defined as Event-B predicates. States can have transitions from one to another, created from State Links.

Transition Event Elaboration

Transitions have a many-valued relation to Events via a property attribute called elaborates. This means that the transition contributes its behaviour (state change as well as any attached property features) to existing events in the same Machine. The relationship is flexible and powerful. A single transition can elaborate many events representing different cases and/or several transitions in different statemachines can elaborate the same event so that the statemachines are forced to synchronise on those transitions. [Note that you should take care not to specify an event that can never be enabled. For example, if two transitions in the same statemachine elaborate the same event].

Transition Properties

A transition can be endowed with any of the features that are normally contained in events (i.e. parameters, witnesses, guards, actions). These features are added in the properties view when the transition is selected. They will be copied into the elaborated events when the state-machine is translated. Hence, although the state-machines are envisioned as ancilliary to a regular Event-B model, all modelling can be done from the diagram if so desired. [Note that only guards may be added to transition segments that target a junction (see below)].

Junctions

A junction pseudo state is available from the diagram palette. Incoming transition segments to a junction generate a disjunctive guard. I.e. the transition may fire from either of the incoming transition's source states. Junctions can be cascaded if required in order to build a bigger disjunction.

Junctions can also be used to split the transition path so that the incoming disjunction is contributed to all of the outgoing paths

Note: transition segments that target a junction may not elaborate events.

Forks and Joins

A fork/Join pseudo state is a available from the diagram palette. (The same pseudo state node is used for both fork and join). A fork is used so that a single transition can enter several parallel nested statemachines (which must all have the same parent state). A join is used to exit several parallel nested statemachines.

Any

An any pseudo state is a available from the diagram palette. An any state is used to represent all of the states at the same level in the state-machine. Hence a transition whose source is an any state can fire irrespective of the current state of the statemachine. Note that the semantic is the same as a transition whose source is the parent state (statemachine boundary). Hence the any state is mostly used in the root level state-machine where there is no parent state.

Lifting

A statemachine can be lifted to a set of instances so that the statemachine represents the behaviour of all of these instances. This is similar to statemachines that are owned by a Class in the classic UML-B. In fact the feature will be used for this purpose when iUML-B class diagrams are available. The generated Event-B is lifted by adding an extra parameter to each elaborated event in order to represent the contextual instance. The name of this parameter can be specified for the state-machine. The instance set and the self-name are both set in the properties view for the state-machine. [Note that currently instances must be constants or carrier sets, variable instance sets are not yet supported].

Semantics

The semantics of Event-B state machines differ from those of UML. Like Event-B, UML-B semantics are based on the underlying concept of spontaneous atomic guarded actions that change the state of the variables. Comparing with other commonly used semantics such as UML, UML-B has no concept of external events that may trigger transitions, no ability whereby one transition may invoke another and, as there is no so-called `big-step', terms such as `run to completion' have no meaning. (All these things can be, and often are, modelled explicitly when required by constructing suitable control variables and guards).

Translation to Event-B

State machines, states and transitions are contained within an Event-B machine and generate new elements in that same machine upon translation. There are two alternative translations available which are selectable from the properties view of the root level statemachine.

  • In the Enumeration translation, a single variable is generated for each statemachine. Its type is an enumerated set which is generated from the states of the statemachine or, for a lifted statemachine, a function from the instances set to this enumeration.
  • In the Variables translation, a variable is generated for each state of the statemachine. The type of these variables is BOOL or, for a lifted statemachine, a subset of the instances set.

In either case, invariants are generated to ensure that the statemachine (or a particular instance thereof) is only ever in one of its states at a time and that the hierarchy is obeyed. Transitions contribute guards and actions, representing the state change of the transition in the chosen data representation, to the events that they elaborate. An invariant in a state will be translated into Event-B by adding an anticedent that the state is active (i.e. the statemachine is in that state).

Validation

There are some semantic rules that must be obeyed in order for a state machine model to be valid and translatable to Event-B. These rules are implemented in the validation framework and are checked either when validation is called explicitly from the context menu, or before the translation. Note that the set of rules is currently not complete thus not guaranteeing full correctness of the model.

State machine error and warning markers

Rules: [NEEDS UPDATING]

State machine

  • Name must be valid (not null, nor empty string)
  • When Instances is defined, the self-name must be valid
  • Must have exactly one initial state if it is a root-level state machine
  • Must have exactly one initial state if it is a nested state machine with outgoing local transitions (going from a state to parent state or ANY state)
  • Cannot have more than one final state.
  • Concrete state machine cannot have refined states
  • Refined state machine cannot have concrete states

Initial state and transition

  • Initial state must have at least one outgoing transition
  • Initial state cannot have any incoming transition
  • Transition cannot go directly from initial state to final state.

Final state

  • Final state must have at least one incoming transition.
  • Final state cannot have any outgoing transition.

State (not initial nor final)

  • State name must be valid (e.g., not null nor empty string)
  • Any invariants' name must be valid (e.g., not null nor empty string)
  • There cannot be two invariants with the same name.
  • Invariants' predicate must not be null
  • Concrete state cannot contain refined state machines

Transition

  • Source and target states must not be null
  • Source and target states must not be dangling states.
  • Source and target states must be valid states.
  • Must elaborate and event if it is on the root-level state machine (either its source or target belongs to a root-level state machine).
  • It is in a nested state machine and not initial or final (its source/target is not initial and final state).


Not all the rules are strict i.e. violation of certain rules is not considered an error as it doesn't cause translation problems, but keeping a model semantically correct means everything will be translated as intended.

The diagram editor, as mentioned, has two ways of checking the diagram model against these rules: selecting Validate from the diagram context menu or running a translation. After validation completes, it produces feedback in the form of a dialog, which lists any warnings or errors. The elements that violate specific rules are marked with error/warning markers, which are listed in the Rodin Problems view, as well as displayed on the diagram.

Known Problems

Implicit Context extends chain becomes broken. This only applies when using the Enumerated Translation which generates an implicit context to define the enumeration set of states]. If you refine a machine containing a State-Machine without translating the refined statemachine (i.e. because your refinement didn't alter the statemachine) then subsequent refinements that do alter the statemachine introduce errors because the link to the abstract implicit context is not maintained. A work-around is to translate the statemachine of the middle refinement even though you didn’t change the statemachine. This will create an empty context to maintain the chain. Alternatively you can manually edit the extends of the implicit context in the refined level to link to the abstract implicit context. However, you can only do this using the Rose editor's Advanced tab because the generated implicit context is read-only to other editors.