extensions(x) the set of values which will `complete' x productions(x) the set of values which begin with x {|x1 , x2|} the productions of x1 and x2
productions(x) = {x.z<-extensions(x) } {| x | ...|} = Union( { productions(x) | ...} )
The main use for the `{| |}' syntax is in writing communication sets as part of the various parallel operators. For example, given
channel c : {0..9}
P = c!7->SKIP [| {| c |} |] c?x->Q(x)
we cannot use {c} as the synchronisation set; it denotes the
singleton set containing the channel c, not the set of events
associated with that channel.
All of the closure operations can be used on datatype values as well as channels.
The closure operations are defined even when the supplied values are
complete.
(In that case extensions will supply the singleton set consisting
of the identity value for the `.' operation.)
Go to the Next or Previous section, the Detailed Contents, or the FS(E)L Home Page.