Language.adoc

Language description

Your features may use the following step definitions (you may choose to use single or double quotes). The logic of the particular step is also available as a method for the composition in the domain specific steps.

Note: All steps may optionally end with the comment delimited by the whitespace and '#' characters.

Event-B

• Setup constants (optionally with the given constants constraints) and initialize the machine.

  Given machine

  Given machine with "«Formula»"

  Given machine with
    """
      «Formula»
    """

  Available as setupConstantsInitialiseMachine(String formula) method (parameter formula is optional).

• Fire the given event (optionally with the given parameters constraints).

  When fire event "«Event-Name»"

  When fire event "«Event-Name»" with "«Formula»"

  Available as fireEvent(String eventName, String formula) method (parameter formula is optional).

• Fire the given event multiple times with all given parameters constraints (one value from the list for each invocation).

  Then fire event "«Event-Name»" with "«Attr-Name»"="«Value-List»"

  Available as fireEvents(String eventName, String attrName, List<String> values) method.

• Fire the given event multiple times with all given parameters constraints (one data table row for each invocation).

  When fire event "«Event-Name»" with
      | name-1 | name-2 | ... |
      | val-11 | val-12 | ... |
      | val-21 | val-22 | ... |

  Available as fireEvents(String eventName, List<Map<String, String>> maps) method.

• Check if the given event (optionally with the given parameters constraints) is enabled.

  Then is enabled event "«Event-Name»"

  Then is enabled event "«Event-Name»" with "«Formula»"

  Available as isEventEnabled(String eventName, String formula) method (parameter formula is optional).

• Check if the given event is enabled with all given parameters constraints (one value from the list for each check).

  Then is enabled event "«Event-Name»" with "«Attr-Name»"="«Value-List»"

  Available as areEventsEnabled(String eventName, String attrName, List<String> values) method.

• Check if the given event (optionally with the given parameters constraints) is disabled.

  Then is disabled event "«Event-Name»"

  Then is disabled event "«Event-Name»" with "«Formula»"

  Available as isEventDisabled(String eventName, String formula) method (parameter formula is optional).

• Check if the given event is disabled with all given parameters constraints (one value from the list for each check).

  Then is disabled event "«Event-Name»" with "«Attr-Name»"="«Value-List»"

  Available as areEventsDisabled(String eventName, String attrName, List<String> values) method.

• Check if the given formula evaluates to the given value.

  Then is TRUE formula "«Formula»"

  Then is FALSE formula "«Formula»"

  Available as isFormula(String formula, String value) method.

iUML-B Class Diagrams

The class instance identification is the class name followed by the instance, separated by the colon (e.g. ClassName:Instance).

• Preset the given class instance for subsequent steps.

  Given class instance "«Class»"

• Call the given method (optionally with the given parameters constraints) of the preset or given classs instance.

  When call method "«Method-Name»"

  When call method "«Method-Name»" with "«Formula»"

  When call method "«Method-Name»" for class instance "«Class»"

  When call method "«Method-Name»" for class instance "«Class»" with "«Formula»"

  Available as callMethod(methodName, classId, formula) method (parameters classId and formula are optional)

• Check, if the given method (optionally with the given parameters constraints) of the preset or given classs instance is enabled.

  Then is enabled method "«Method-Name»"

  Then is enabled method "«Method-Name»" with "«Formula»"

  Then is enabled method "«Method-Name»" for class instance "«Class»"

  Then is enabled method "«Method-Name»" for class instance "«Class»" with "«Formula»"

  Available as isMethodEnabled(methodName, classId, formula) method (parameters classId and formula are optional).

• Check, if the given method (optionally with the given parameters constraints) of the preset or given classs instance is disabled.

  Then is disabled method "«Method-Name»"

  Then is disabled method "«Method-Name»" with "«Formula»"

  Then is disabled method "«Method-Name»" for class instance "«Class»"

  Then is disabled method "«Method-Name»" for class instance "«Class»" with "«Formula»"

  May also be used without the instance designator in order to check, if the method is disabled for all instances.

  Available as isMethodDisabled(methodName, classId, formula) method (parameters classId and formula are optional).

• Check, if the given attribute of the preset or given class instance has or has not the given value.

  Then attribute "«Attr-Name»" is "«Value»"

  Then attribute "«Attr-Name»" is not "«Value»"

  Then attribute "«Attr-Name»" for class instance "«Class»" is "«Value»"

  Then attribute "«Attr-Name»" for class instance "«Class»" is not "«Value»"

  Available as isAttribute(String classId, String attrName, String value, boolean not) method (parameters classId and not are optional).

iUML-B State Machines (both enumeration and variables translation)

The state machine identification is either the plain state machine name (e.g. StateMachine) or for the lifted state machine the state machine name followed by the instance, separated by the colon (e.g. StateMachine:Instance).

• Preset the given state machine for subsequent steps.

  Given state machine "«State-Machine»"

• Trigger the given transition (optionally with the given parameters constraints) of the preset or given state machine.

  When trigger transition "«Trans-Name»"

  When trigger transition "«Trans-Name»" with "«Formula»"

  When trigger transition "«Trans-Name»" for state machine "«State-Machine»"

  When trigger transition "«Trans-Name»" for state machine "«State-Machine»" with "«Formula»"

  Available as triggerTransition(String transName, String smId, String formula) method (parameters smId and formula are optional).

• Check, if the given transition (optionally with the given parameters constraints) of the preset or given state machine is enabled.

  Then is enabled transition "«Trans-Name»"

  Then is enabled transition "«Trans-Name»" with "«Formula»"

  Then is enabled transition "«Trans-Name»" for state machine "«State-Machine»"

  Then is enabled transition "«Trans-Name»" for state machine "«State-Machine»" with "«Formula»"

  Available as isTransitionEnabled(String transName, String smId, String formula) method (parameters smId and formula are optional).

• Check, if the given transition (optionally with the given parameters constraints) of the preset or given state machine is disabled.

  Then is disabled transition "«Trans-Name»"

  Then is disabled transition "«Trans-Name»" with "«Formula»"

  Then is disabled transition "«Trans-Name»" for state machine "«State-Machine»"

  Then is disabled transition "«Trans-Name»" for state machine "«State-Machine»" with "«Formula»"

  May also be used without the instance designator in order to check, if the method is disabled for all transitions.

  Available as isTransitionDisabled(String transName, String smId, String formula) method (parameters smId and formula are optional).

• Check, if the preset or given state machine is or is not in the given state.

  Then is in state "«State»"

  Then is not in state "«State»"

  Then state machine "«State-Machine»" is in state "«State»"

  Then state machine "«State-Machine»" is not in state "«State»"

  Nested states are separated using the character '.' (e.g. "«State1».«State2»".

  Available as isInState(String smId, String state, boolean not) method (parameters smId and not are optional).

Restrictions

• Only class diagrams within Event-B machines (not within Event-B contexts) are considered

• An association can be referenced as an attribute.

• A lifted state machine and a corresponding class must have the same self names.