Information Technology Reference
In-Depth Information
−
m
is defined on the structure of the
sHML
formula:
Definition 6 (Synthesis).
m
def
= λ
ff
x
env
.
fail
!
⎩
y
pid1
=spw
ϕ
m
(x
env
)
,
y
pid2
=spw
ψ
m
(x
env
)
,
λ
x
env
.
m
def
=
ϕ∧ψ
fork
(y
pid1
,
y
pid2
)
rcv
tr(
stop
end
m
m
(x
env
);
def
= λ
[
α
]
ϕ
x
env
.
α
)
→ ϕ
→
m
m
,
y
mon
(
{
X
,
def
= λ
max
(
X
,ϕ
)
x
env
.
y
mon
=
ϕ
y
mon
}
: x
env
)
m
y
mon
=lookUp
(
X
,
def
= λ
X
x
env
.
x
env
)
,
y
mon
(x
env
)
Auxiliary Function definitions and meta-operators:
→
x
pid1
!z
,
x
pid2
!z
end,
y
rec
(x
pid1
,
def
= μ
fork
y
rec
.λ
(x
pid1
,
x
pid2
)
.
rcv
z
x
pid2
)
⎩
μ
y
rec
.λ
(x
var
,
x
map
)
.
case
x
map
of
(
{
x
var
,
z
mon
}
: )
→
z
mon
: z
tl
→
y
rec
(x
var
,
z
tl
)
def
=
lookUp
nil
→
exit
end
In Def. 6, the monitor for the formula
ff
immediately reports a violation to some
supervisor actor identified as
fail
, handling the violation. Conjunction,
ϕ
1
∧ϕ
2
,trans-
ϕ
2
and subsequently forwarding
any trace messages to these spawned monitors through the auxiliary function
fork
.The
translated monitor for [
ϕ
1
and
lates into spawning the respective monitors for
α
ϕ
ϕ
]
behaves as the monitor translation for
once it receives a
trace message encoding the occurrence of action
α
, using the function:
tr(
i
?
v
)
def
tr(
i
!
v
)
def
= {
rv
,
i
,
v
}
= {
sd
,
i
,
v
}
Importantly, the monitor for [
α
]
ϕ
terminates if the trace message does not correspond
to
α
. The translations of
max
(
X
,ϕ
)and
X
are best understood together. The monitor for
max
(
X
,ϕ
) behaves like that for
ϕ
, under the extended map where
X
is mapped to the
max
(
X
,ϕ
monitor for
from Def. 2.
The monitor for
X
retrieves the respective monitor translation bound to
X
in the map
using function
lookUp
, and behaves like this monitor.
Closed
formulas guarantee that
map entries are always found by
lookUp
, whereas
guarded
formulas guarantee that
formula variables,
X
, are guarded by necessity conditions, [
ϕ
,e
ff
ectively modelling the formula unrolling
ϕ{
)
/
X
}
— this implements the
lazy
recursive unrolling of formulas and prevents infinite bound-variable expansions.
α
]
ϕ
z
pid
=spw
m
(
nil
)
, mLoop
(z
pid
)
def
= λ
x
frm
.
x
frm
Mon
rcv
z
msg
→
x
pid
!z
msg
end,
y
rec
(x
pid
)
def
= μ
mLoop
y
rec
.λ
x
pid
.
Monitor instrumentation, performed through the function
Mon
(defined above), spawns
the synthesised function initialised to the empty map,
nil
, and then acts as a message
forwarder to the spawned process, through the function
mLoop
(defined above), for any
trace messages it receives through the tracing semantics discussed in Sec. 2.