Transitions
A transition has the form:
transition trigger: someTrigger guard: booleanExpression do: actions next state: stateName
The parts trigger:, guard:, do: are optional. The "next state:" part must be present, except in an "in all states" construction.
-
A trigger is a command or signal from the signature. For commands and signals with parameters, actual parameters have to be provided with a type e.g.,
Command(int param)
. -
A guard is a boolean expression. Note that equality is denoted by “==”, e.g.,
code == 3
. -
The do part is a sequence of actions. Possible actions are:
-
if .. then .. else .. fi
-
Assignment, for instance
code := 3
-
A notification pattern: a notification defined in the signature plus constraints on the number of occurrences. Occurrences are given with the symbols '?' (optional), '+' (at least once), '*' (zero or more), or giving the expected numbers: [2], [1-3], [2-*]. When the occurrence is not given the notification is expected to happen once. The pattern has to provide the expected values for the parameters as expressions. When the value is not relevant, a "*" can be used. Some examples:
info(23)?, statusChange(param, *)[2-*]
-
A reply to trigger command. This may include a return parameter, e.g.,
reply(code+3)
. If it is not relevant to specify the return value, a “*” can be used, i.e.,reply(*)
. -
A notification or reply with variables and an optional condition on their values. The previous two actions have to specify the exact values that are observed or give a "*". In some cases, a condition on the observed values may be needed, for example, an integer between 1 and 100. In this situation, notifications and replies may use variable declaration in the place of their parameters and may give a condition on their values. For example:
infoTemperature(int x) where x > 0, reply(string answer)
. Variables defined in this way are visible to the subsequent actions. They assume the value of the observed event parameter. -
any order
pattern: a composition of notification patterns and a reply that can happen in any order, for example,any order(reply(Status::OnFailed), info(*), statusChange(*)*)
. In this example, the sequences of events shall contain one reply, one notification info, and zero or more notifications statusChange. All these events can be observed in any order.If an observed event is not accepted by the any order pattern and does not cause an error then the execution continues with the next action. If the any order construct is the last action in the transition then the transition is traversed. Consider the example
any order(a, b*)
. The sequence b, b, c causes an error because the event c is not among the expected events and the event a is not observed yet. The sequence a, c is not an error because a has to be observed exactly once, b is optional. In this case, the event c is possibly indicated by an action after the any order.Sometimes a group of events is repeated in many any order actions thus causing too long and repetitive specifications. Such groups can be defined as named event fragments, can be referred to by name from other fragments and any order actions. Fragment definitions cannot contain replies.
interface iA event fragments FrA = a+, b? FrB = c[1-2], fragment FrA ..... ..... ... any order(fragment FrA) ...
-
To express non-determinism, e.g., because the response to a trigger depends on internal state information, the OR
construct can be used. For instance:
transition trigger: PowerOn do: reply(Status::OnOK) next state: SwitchingOn OR do: reply(Status::OnFailed) next state: Off
An example of a state with transitions:
state on { transition trigger: CurrentTemp(Status st, string info, bool error) guard: 12.0 < temp AND temp < 34.7 do: localstat := st reply(temp) next state: on transition guard: code == 3 do: myMode(Mode::on) next state: on }
If the trigger of a transition is a command that has inout or out parameters, their values should be given in the reply in the following order:
-
the values of inout or out parameters in the order they appear in the signature of the command
-
the return value of the command. If the return type is void then no value is given
For example, assume a command defined in a signature file:
commands bool doSomething(int input, out int r)
The reply in a transition shall be:
transition trigger: doSomething(int input, int r) do: ... reply(2, true)
In this example, true is the return value of the command, 2 is the value of the out parameter r.
In the body of transitions, out parameters are write-only, that is, they can only be assigned with values but their value cannot be read in an expression.
The special value any (*) can be used in reply for inout and out parameters. If an out parameter is not explicitly assigned with a value in a transition body then the default value of the corresponding type will be used.