Page 267 -

9.3 Detect 249

Fig. 9.5 WF-net modeling an additional constraint: d can only be started once b or c has com-
pleted

Fig. 9.6 Declare
specification composed of
four constraints: c1, c2, c3,
and c4

25
26 based on partial trace a 12 ,a 19 ,b start ,d 26 . The alert signals that activity
start
start
complete
d was started without being enabled. For the second case a deviation is detected
28
at time 28; based on the partial trace a 17 ,a 23 ,d start an alert is generated
start
complete
stating that d was started before it was enabled. For the third case a deviation is de-
40
30
32
25
tected at time 62. The prefix a start ,a complete ,c start ,c 35 ,d 35 ,d complete ,e 45 ,
start
start
complete
e 50 ,f 50 ,f 55 ,b 60 ,d 62 cannot be replayed properly because the sec-
complete start complete start start
ond instance of d is started without being enabled. These examples show that the
replay approach from Chap. 7 can also be used at run-time for detecting deviations
the moment they happen.
In Chap. 7 we introduced Declare as an example of a constraint-based language.
We used the Declare model shown in Fig. 9.6 to explain some of basic concepts.
Each of the four constraints shown can be specified in terms of LTL. Constraint c1
is a non-coexistence constraint stating that g and h should not both happen. The
LTL expression for this constraint is !((♦g) ∧ (♦h)). Constraint c2 is a precedence
constraint ((!g) W e) modeling the requirement that g should not happen before e
has happened. Constraint c3 is a similar precedence constraint, but now referring to