Page 268 -

250 9 Operational Support

h rather than g. Constraint c4 is a branched response constraint stating that every
occurrence of a should eventually be followed by g or h, i.e., (a ⇒ (♦(g ∨ h))).
Consider some case having a partial trace σ p listing the events that have happened
thus far. Each constraint c in Fig. 9.6 is in one of the following states for partial
trace σ p :
• Satisfied: the LTL formula corresponding to c evaluates to true for the partial
trace σ p .
• Temporarily violated: the LTL formula corresponding to c evaluates to false for

σ p , however, there is a longer trace σ that has σ p as a prefix and for which the
p
LTL formula corresponding to c evaluates to true.
• Permanently violated: the LTL formula corresponding to c evaluates to false for

σ p and all its extensions, i.e., there is no σ that has σ p as a prefix and for which
p
the LTL formula evaluates to true.
These three notions can be lifted from the level of a single constraint to the level
of a complete Declare specification. A Declare specification is satisfied for a case
if all of its constraints are satisfied. A Declare specification is temporarily violated
by a case if for the current partial trace at least one of the constraints is violated,
however, there is a possible future in which all constraints are satisfied. A Declare
specification is permanently violated by a case if no such future exists.
None of the cases shown in Table 9.1 violates any of the constraints shown in
Fig. 9.6, i.e., for each trace, at the end, all constraints are satisfied. Let us now
consider a scenario in which for a case the trace σ = a,b,d,g is executed. For
simplicity, we removed timestamps and transactional information. Initially, i.e., for
trace σ 0 = , all constraints are satisfied. After executing a, i.e., for prefix σ 1 = a ,
constraint c4 is temporarily violated. Because there is a possible future in which all
constraints are satisfied, there is no need to generate an alert. However, diagnostic
information stating that constraint c4 is temporarily violated could be provided.
Executing b and d does not change the situation, i.e., both partial traces σ 2 = a,b
and σ 3 = a,b,d temporarily violate c4. However, after executing g the situation
changes. Partial trace σ 4 = a,b,d,g satisfies constraint c4. However, constraint
c2 is permanently violated by σ 4 as there is no “possible future” in which e occurs
before g. Therefore, a deviation is detected and reported.
Figure 9.7 shows another Declare model. Constraint c1 is the same non-
coexistence constraint as before. Constraint c2 is a response constraint stating that
every occurrence of activity e should eventually be followed by g, i.e., (e ⇒ (♦g))
in LTL terms. Constraint c3 is a similar response constraint (every occurrence of ac-
tivity e should eventually be followed by h). Constraint c4 is a precedence constraint
((!g) W a) modeling the requirement that g should not happen before a has hap-
pened. Constraint c5 is also a precedence constraint ((!h) W a). Assume that Fig. 9.7
is the normative model. Let us first consider a scenario in which for a case the trace
σ = a,b,d,g is executed. For all prefixes, all of the constraints are satisfied, i.e.,
no alerts need to be executed during the lifetime of this case. Let us now consider the
scenario σ = a,b,d,e,g . No alerts need to be generated for the first three events.
In fact at any stage all five constraints are satisfied. However, after executing e con-
straints c2 and c3 are temporarily violated. To remove these temporary violations,