Event-B Statemachines - Revision history

imported>Colin: /* Validation */

2015-10-06T08:04:54Z

Validation

← Older revision		Revision as of 08:04, 6 October 2015
Line 104:		Line 104:
	===Validation===		===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 context menu, or before the translation. Note that the set of rules is currently not complete thus not guaranteeing full correctness of the model.		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]]
Line 115:		Line 115:
	* 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)		* 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.		* 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 and transition ====
Line 130:		Line 132:
	* There cannot be two invariants with the same name.		* There cannot be two invariants with the same name.
	* Invariants' predicate must not be ''null''		* Invariants' predicate must not be ''null''
	* Concrete state ~~machine~~ cannot ~~have~~ refined ~~states~~		* Concrete state cannot contain refined state machines
	* Refined state ~~machine cannot have concrete states~~

	==== Transition ====		==== Transition ====
Line 139:		Line 140:
	* 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).		* 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).		* It is in a nested state machine and not initial or final (its source/target is not initial and final state).
	* Concrete state cannot contain refined state machines

	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.

	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.		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===		===Known Problems===

imported>Son: /* Transition */

2015-09-28T13:26:50Z

Transition

← Older revision		Revision as of 13:26, 28 September 2015
Line 134:		Line 134:

	==== Transition ====		==== 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).		* 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).		* It is in a nested state machine and not initial or final (its source/target is not initial and final state).

imported>Son: /* Validation */

2015-09-28T13:03:19Z

Validation

← Older revision		Revision as of 13:03, 28 September 2015
Line 109:		Line 109:

	Rules: [NEEDS UPDATING]		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~~		==== Initial state and transition ====
	* ~~Root~~ state ~~machine must have an initial~~ state		* Initial state must have at least one outgoing transition
	* ~~State machine can only~~ have one ~~initial~~ state		* Initial state cannot have any incoming transition
	* State ~~machine can only have one~~ final ~~state~~		* Transition cannot go directly from initial state to final state.
	* State ~~machine~~ must ~~have an initial state if~~
	** its parent state has incoming transitions		==== Final state ====
	** it has outgoing local transitions (~~going from a state to parent state or ANY state~~)		* Final state must have at least one incoming transition.
	* ~~Concrete state~~ cannot ~~contain refined state machines~~		* 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 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

			==== Transition ====
			* 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).
			* Concrete state cannot contain refined state machines

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

imported>Colin: /* Installation */

2015-06-26T09:38:21Z

Installation

← Older revision		Revision as of 09:38, 26 June 2015
Line 6:		Line 6:

	==Installation==		==Installation==

	~~PLEASE ADD THE FOLLOWING UPDATE SITE BEFORE INSTALLING:~~
	~~gmp - http://download.eclipse.org/modeling/gmp/gmf-tooling/updates/releases/~~

	The iUML-B Statemachines plug-in is available for installation from the Rodin update site (Modelling Extensions category).		The iUML-B Statemachines plug-in is available for installation from the Rodin update site (Modelling Extensions category).
Line 16:		Line 13:
	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.		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 ~~dduring~~ installation installation.		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==

imported>Colin: /* Installation */

2014-10-20T09:08:06Z

Installation

← Older revision		Revision as of 09:08, 20 October 2014
Line 7:		Line 7:
	==Installation==		==Installation==

	PLEASE ADD THE ~~FOLOWING~~ UPDATE ~~SITES~~ BEFORE INSTALLING:		PLEASE ADD THE FOLLOWING UPDATE SITE BEFORE INSTALLING:
	http://download.eclipse.org/releases~~/kepler~~/		gmp - http://download.eclipse.org/modeling/gmp/gmf-tooling/updates/releases/

	The iUML-B Statemachines plug-in is available for installation from the Rodin update site (Modelling Extensions category).		The iUML-B Statemachines plug-in is available for installation from the Rodin update site (Modelling Extensions category).

imported>Colin: /* Installation */

2014-10-06T07:10:24Z

Installation

← Older revision		Revision as of 07:10, 6 October 2014
Line 16:		Line 16:
	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.		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, ProB~~, OCL and QVT~~ - all of these dependencies will be installed automatically ~~upon plug-in~~ installation.		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 dduring installation installation.

	==Using the tool==		==Using the tool==

imported>Colin: /* Installation */

2014-09-29T16:05:53Z

Installation

← Older revision		Revision as of 16:05, 29 September 2014
Line 8:		Line 8:

	PLEASE ADD THE FOLOWING UPDATE SITES BEFORE INSTALLING:		PLEASE ADD THE FOLOWING UPDATE SITES BEFORE INSTALLING:
	http://download.eclipse.org/~~modeling/gmp/updates~~/~~releases~~/		http://download.eclipse.org/releases/kepler/

	The iUML-B Statemachines plug-in is available for installation from the Rodin update site (Modelling Extensions category).		The iUML-B Statemachines plug-in is available for installation from the Rodin update site (Modelling Extensions category).

imported>Colin: /* Installation */

2014-09-29T13:17:38Z

Installation

← Older revision		Revision as of 13:17, 29 September 2014
Line 8:		Line 8:

	PLEASE ADD THE FOLOWING UPDATE SITES BEFORE INSTALLING:		PLEASE ADD THE FOLOWING UPDATE SITES BEFORE INSTALLING:
	http://download.eclipse.org/modeling/gmp~~/gmf-tooling~~/updates/releases/		http://download.eclipse.org/modeling/gmp/updates/releases/
	~~http://download.eclipse.org/releases/indigo~~

	The iUML-B Statemachines plug-in is available for installation from the Rodin update site (Modelling Extensions category).		The iUML-B Statemachines plug-in is available for installation from the Rodin update site (Modelling Extensions category).

imported>Colin: /* Translation to Event-B */

2014-06-12T16:09:06Z

Translation to Event-B

← Older revision		Revision as of 16:09, 12 June 2014
Line 97:		Line 97:
	====Translation to Event-B====		====Translation to Event-B====

	State machines, states and transitions are ~~integrated in~~ Event-B machine and generate new elements in that machine upon translation.		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.		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 ''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 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.		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.		Transitions contribute guards and actions, representing the state change of the transition in the chosen data representation, to the events that they elaborate.
	~~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

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

imported>Colin at 16:06, 12 June 2014

2014-06-12T16:06:05Z

← Older revision		Revision as of 16:06, 12 June 2014
Line 59:		Line 59:

	A state can have nested state machines, added from ''State Features'' (also called parallel (or orthogonal) regions).		A state can have nested state machines, added from ''State Features'' (also called parallel (or orthogonal) regions).
	A state may ~~have~~ invariants (or theorems) which are defined as Event-B predicates.		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''.		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=====		=====Transition Properties=====
Line 106:		Line 110:
	* Transitions and states translate to event guards and actions that describe state change behaviour		* Transitions and states translate to event guards and actions that describe state change behaviour

	~~====Event Elaboration====~~		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).
	Transitions have a many-valued relation to Events via an 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. 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].

	~~====State Invariants====~~
	An invariant in a state will be ~~interpreted~~ translated into Event-B by adding an anticedent that the state is active (i.e. the statemachine is in that state).

	===Validation===		===Validation===