Information Technology Reference
In-Depth Information
and to be able to merge these, and detect if they are both trying to modify the
same variable. With the action model as just described, this is hard to do, so
we adopt an alternative model, were we view an action as simply being a partial
environment which records the part that changes. The null action is simply the
null map (
θ
), and two actions are merged by simply merging the maps together.
Any variable conflict is recognised because the variable occurs in the domain of
both maps — in this case we map the value to ? to denote the (runtime) error.
Evt
=
Env
nop
=
θ
e
1
♦
e
2
=
e
1
∪
e
2
,
if
dom
e
1
∩
dom
e
1
=
∅
{
v
→
e
1
}
♦
{
v
→
e
2
}
=
{
v
→
?
}
The one exception to map conflicts has to do with the way the communication
parts are treated (
,γ,B
). Here we find that the basic action involves lodging
a
prialt
asarequest,intothe
B
component, which is a set of such
prialt
s.
Multiple references to
B
are resolved by applying set union (remember that
P
1
and
P
2
are of type
PriSet
):
{
B
→
P
1
}
♦
{
B
→
P
2
}
=
{
B
→
P
1
∪
P
2
}
The clock-tick action is simply represented by an environment where the sole
identifer in its domain is
τ
, and the datum to which it maps is immaterial:
‡
:
Evt
‡
{
τ
→
}
=
?
State Change.
We use such partial maps to change the state by simply over-
riding the state with a mapping in which any expressions (as
Fun
in
Datum
)
have been first evaluated w.r.t that state:
St
=
Env
†E
ρ
(
e
1
)
(
e
1
)
ρ
=
ρ
E
ρ
{
v
→
f
}
=
{
v
→
f
(
ρ
)
}
It is this model of actions which motivated the particular form of the abstract
action model used when typed assertion traces where described previously, and
why in that model we used
, rather than simply viewing actions there directly
as state-transformers themselves.
State Predicates.
Any boolean-valued expression in Handel-C provides us with
a predicate, simply by evaluating that expression against the state environment
in the usual way.
Search WWH ::
Custom Search