Semantics

The transition rule for the await construct is quite straightforward. If, in a fixed interpretation, B evaluates to true, then we can infer the result of the execution of the await construct thus:

This leads us to the following definition:

Definition 128. A configuration is a deadlock, if and there are no transitions starting form that configuration. a program S can deadlock from s if there is a computation sequence starting from and ending in a configuration which is a deadlock. S is deadlock free, if there are no states s such that S can deadlock from s.

The operational semantics for total correctness is modified by reason of deadlock. Hence,

but