Information Technology Reference
In-Depth Information
∧
∧
[
α
]
[
α
]
[
α
]
[
α
]
[
α
]
∧
[
α
]
X
→ ϕ
[
β
]
[
α
]
[
α
]
[
β
]
[
α
]
∧
ff
ff
[
β
]
.
.
.
.
.
.
ff
(a) Denotation of
ϕ
safe
defined in (2)
(b) Constructed concurrent
monitors for
ϕ
safe
where
ϕ=
[
α
][
α
][
β
]
ff
∧
[
α
]
X
∧
[
α
]
[
α
]
[
α
]
∧
[
β
]
[
α
]
[
α
]
[
α
]
X
→ ϕ
ff
[
β
]
ff
(c) First expansion of the
constructed monitor for
ϕ
safe
Fig. 3.
Monitor Combinator generation for
ϕ
safe
of Ex. 2
