Semantics is defined as in 3.2.4. On one hand, things are simpler this
time around because there is no correlation among individual choices. On
the other hand, there is a complication related to attempts to choose an
element of the empty set. Such attempt cannot succeed and the execution
should be aborted. To deal with this complication, we extend the
collection of updates of any state by an ideal element that
symbolizes inconsistency. If an update set
contains
then
firing
does not change the state; we call such
contradictory.
Suppose that a state S is appropriate for a rule R and R is
S -perspicuous. Let V be the collection of bound variables of R such
that the range of v is not empty in state S . Fix a
function
on
V such that, for each
v
V,
(v)
belongs to the range of v in
S . By induction on subrule R' of R define
Updates(R', S',
)
where S' is an expansion of S appropriate for R' and R' is
S'-perspicuous.
The cases of update instructions, sequence rules and conditional rule are
treated as above. Notice that if R' is a sequence of rules
and
some Updates(
, S',
)
is
contradictory then
Updates(R', S',
)
is
so.
Suppose that R' is a choose rule with main existential variable v and
body . If the range of
v is empty then
Updates(R', S',
) =
.
Otherwise let
a =
(v)
and
be the expansion of S' to the auxiliary vocabulary
'
{v}
where
v is interpreted as a . Set
Updates(R', S',
) =
Updates(
,
,
).
Finally, NUpdates(R, S)
is the
set of Updates(R, S, )
where
takes all possible values.