B Semantics
The section describes the semantics of Sequential Function Charts
(SFC's), as (to be) realized in the tool Slime. The semantics is
defined for successfully checked SFC's (cf.
Section 4); unchecked SFC's don't have a meaning.
Especially, the simulator, which realizes the semantics, can assume checked
syntax.
B.1 Informal semantics
We start informally and explain the semantics with the help of the example
from Figure 1.
The SFC's consist of nodes, called steps, to which actions are
associated, and transitions between steps, decorated with boolean
guards. Always, one ore more of the steps are active and the actions
associate with this active steps are executed within one cycle. The
transition from s1 to both s2 and s3 (with double horizontal line) is
a parallel branching: if this transition is taken, s1 is deactivated
and both s2 and s3 get activated. Since this is one transition, and
each transition has exactly one guard, the guard is labeled on the upper part
of the transition.
In contrast, the ``branching'' from s3 to s5 and s6 is no real
branching, it is just an abbreviation for two different transitions: one
leading from s3 to s5, the other leading from s3 to s6.
Therefore, the guards are labeled to the lower parts, since each transition
has exactly one guard.
The topmost step (marked specifically) is initial. The ''N'' on the
left-hand side of the actions is a qualifier, stating that the action
is to be executed in each cycle in which the step is active. There are other
qualifiers, too, but we will neglect them unless we find good reasons for
taking them into account.
The behavior of an SFC during one cycle is as follows.
-
Reading inputs from the environment.
- Executing the actions from the active steps. This is done in two steps
as follows:
-
Assemble all active actions (as a set, so each action appears at most
one time).
- Execute the assembled actions in an arbitrary order.
- Evaluate the guards.2
- Take transition(s) (if possible).
- Write outputs.
Each transition is equipped by a guard, i.e., a boolean expression.
A transition can be taken only if the guard evaluates to true, and, if all
the source steps of the transition are active. We do not enforce the
target steps to be disabled.3
If more than one step is active in a parallel branch, the execution of the
corresponding action is chosen non-deterministically. This means,
they can be executed in an arbitrary order (interleaving semantics).
There is a second source of non-determinism, namely the set of actions
associated to the active steps. These actions will be first assembled, and
then non-deterministically executed. Each action will only be executed once,
even if an action is associated to two different active steps.
Consequently, a program may have a number of different execution runs. The
simulator could realize the different runs in that it asks the user, in which
order the actions should be performed, and which transition should be taken if
several are possible. An alternative is, to determine the order by a random
generator.
The transition from s4 and s7 to s8 closes the parallel branch again.
Such a transition can be taken only, if all source steps are active. In
other words, this transition can be taken if it's guard evaluates to true and
furthermore both s4 and s7 are active.
last generated July 10, 2002 (©Public License)