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

The active guard expression takes a prialt -request as argument, and returns
the index ( i 1 ...n ) of the guard which is going to be active in this clock-cycle.

It is only defined when w

∈

g i is false, and looks up the channel-prialt map

E [[ a g i ]] ρ =min j

where ∃ c • g i ∈ ρ ( γ )( c )

∧ channel ( g j )= c

Here channel returns the channel associated with a guard.
The channel data expression δ ( c ) returns the data expression associated with
an active channel — this information can be extracted from the channel- prialt
map component, as detailed in [5].
We extend the program syntax to include three new statements — a prialt -
request statement ( rq g i ), a prialt -wait statement ( wait g i ), and a multi-way

conditional branch (or case-statement):

p ∈ Prog ::= ... | rq g i | wait g i | e

[ p i ]

The prialt -request statement simply lodges its guard-list argument into the
input PriSet for resolution. In the semantics we use the B component of the
state to hold both the prialts input to resolution (during the req phase) and the
blocked- prialt result of resolution (available during the res and act phases).
The prialt -wait statement asks if its prialt argument is blocked. If it is, it
then waits one clock cycle, then re-submits the corresponding prialt -request,
before repeating itself. If the prialt is not blocked, it terminates immediately.
The case-statement e [ p i ] evaluates expression e , whose value must lie in

the range 1 ...n . This value is used to select the process to execute.
We also define a function on guards which gives the underlying action as an
equivalent statement:

act () : Grd → Prog

act ( c ! e ) = 1

act ( c ? v ) = v := δ ( c )

act (!?) = 0

We give prialt g i → p i a semantics by translating it to:

rq g i

; wait

g i

; a

g i

[ act ( g i ); p i ]

This captures the notion that a prialt acts in three stages: (i) it submits a
request ( rq ); (ii) it waits until it becomes active, re-submitting the request

on every clock cycle ( wait

g i

); and (iii) once waiting is over, selects and executes
the active guard and corresponding process ( a

g i

g i [ act ( g i ); p i ]).