A Denotational Semantics for Handel-C - Formal Methods and Hybrid Real-Time Systems - page 51

The semantics of a Handel-C program is mapped to a set of these traces, which
conform to a set of healthiness conditions to be mentioned later.
Slots have internal structure, and are divided into two components: the de-
cision actions which occur early in the clock cycle to determine the course of
action to take; and the permanent state-change actions which all occur simul-
taneously at the end of the clock cycle. The former are modelled as sequences
of “microslots” ( MS ), whilst the latter can simply be represented as a single
(merged) guarded action. We shall refer to the second component as the “final
action” of the slot

Slot = MS ∗

s, ( μ, a ) ∈ × GA

Amicroslot( m ) captures the actions in one cycle of selection-request-response
and hence is is a triple of guarded actions ( s, q, r ), where the first ( s )areoftype
sel , the second ( q )areoftype req ,andthelast( r )areoftype res :

MS = GA 3 m, ( s, q, r ) ∈

We expect that any microslot has at least one non-null action present.
We need to be careful how traces and slots are interpreted: In essence, a slot
where the final action is null denotes the case were the clock-tick which ends the
slot has yet to happen. As a consequence of this interpretation, only the last slot
in a trace can be “tick-free” in this manner. T
We need to be able to identify a null slot, as one with no microslots, and a
null final-action:

nils : Slot

nils =( , true )

A trace in which no actions, not even a clock-tick, have occurred, is denoted by a
singleton sequence consisting of one null slot. The reason for not admitting empty
trace sequences is that it introduces ambiguity over interpreting null traces, and
complicates the definition of various concatenation operators.
We also need to identify a slot whose only action is an final-action which
denotes a clock-tick — we overload the notation to denote both such a clock-

tick action, and the corresponding slot. We also expect that merging this action
with any non-null action will result in that non-null action:

‡

‡ : Act ‡ ♦ a = a, a = nop

‡ : Slot ‡ =( , ‡ )

Typing. The typing of actions in slots and microslots is implicitly given by the
actions' position. We can extend the notion of typing to cover both microslots
and slots themselves.
Transition types fall into four categories, with an ordering as indicated:

t ∈ TType = { }

sel < req < res < act

sel, req, res, act