Monitoring of Temporal First-Order Properties with Aggregations - Runtime Verification - page 57

proc init ( ϕ )
for each ψ sf ( ϕ ) with ψ = ψ S I ψ do

∈

L ψ ←
for each ψ I ψ do

∈ sf ( ϕ ) with ψ =

case ϕ = ψ ∨ ψ
A ← eval ( ψ , i , τ , Γ )
A ← eval ( ψ , i , τ , Γ )
return A

A ψ ←∅
τ ψ ←

0

A

∪

proc eval ( ϕ , i , τ , Γ )
case ϕ = p ( x 1 ,...,x n )
return Γ p

case ϕ = ∃ x. ψ

A ← eval ( ψ , i , τ , Γ )

s get info exists ( ϕ )

return π s ( A )

←

case ϕ = ψ ∧ p ( t 1 ,...,t n )& kind rig ( ϕ )
case ϕ = ψ ∧¬p ( t 1 ,...,t n )& kind rig ( ϕ )
A ← eval ( ψ , i , τ , Γ )
C ← get info rig ( ϕ )
return σ C ( A )

case ϕ =[ ω t z.ψ ]( y ; g )
A ← eval ( ψ , i , τ , Γ )
H, t ← get info agg ( ϕ )

return ω t ( A )

case ϕ = ψ ∧ p ( t 1 ,...,t n )& kind rig '( ϕ )
A ← eval ( ψ , i , τ , Γ )
k ← get info rig '( ϕ )
R ←∅
for each a ∈ A
R ← R ∪ reval ( p, k, a )
return R

case ϕ = I ψ

A ← A ϕ

A ϕ ← eval ( ψ , i , τ , Γ )

τ ← τ ϕ
τ ϕ ← τ
if i> 0 and ( τ − τ ) ∈ I then
return A
else
return ∅

case ϕ = ψ ∧¬ψ
case ϕ = ψ ∧ ψ
A ← eval ( ψ , i , τ , Γ )
A ← eval ( ψ , i , τ , Γ )

C, s ← get info and ( ϕ )
if ϕ = ψ

case ϕ = ¬ψ S I ψ
case ϕ = ψ S I ψ
A ← eval ( ψ , i , τ , Γ )
A ← eval ( ψ , i , τ , Γ )
return eval since ( ϕ , τ , A , A )

ψ then
return A C,s B
else
return A

∧

C,s B

Fig. 4. The init and eval procedures

proc eval since ( ϕ , τ , A , A )
b ← interval right margin ( ϕ )
drop old ( L ϕ , b , τ )
C, s ← get info and ( ϕ )
case ϕ = ¬ψ S I ψ then
f ← λB.B s,C A
case ϕ = ψ S I ψ then
f ← λB.B s,C A
g ← λ ( κ, B ) . ( κ, f ( B ))
L ϕ ← map ( g , L ϕ )
L ϕ ← L ϕ ++ ( τ,A )
return fold left ( aux since , ∅ , L ϕ )

proc drop old ( L , b , τ )
case L =

return
case L =( κ, B ):: L
if τ b then

return drop old ( L ,b,τ )
else return L

− κ ≥

proc aux since ( R ,( κ, B ))
if ( τ − κ ) ∈ I then return R ∪ B

else return R

Fig. 5. The eval since procedure

assume that ϕ = ψ S I ψ , the other case being similar. The evaluation of ϕ

reflects the logical equivalence ψ S I ψ ≡ d∈I ψ S [ d,d ] ψ . Note that we abuse
notation here, as the right-hand side is not necessarily a formula, because I may
be infinite. The function interval right margin ( ϕ ) returns b ,where I =[ a,b )for
some a ∈ N and b ∈ N ∪{∞} .