Page 201 -

192 M. Pesic
6.3.3 Monitoring Instance States

During execution, the state of an instance is also monitored. The state of an instance
depends on the satisfaction of the mandatory constraints in the model.

Definition 12 (Instance state !). Let ci 2 U ci be an instance where ci D . ; cm/.
The function ! W U ci !fsatisfied; temporarily violated; violatedg of instance ci is
defined as:
8
< satisfied if 2 T cm I

temporarily violated if . … T / ^ .9 2 T W C 2 T
!.ci/ D cm cm /I
:
violated otherwise:
Recall that T is the set of all traces that satisfy the conjunction of all manda-
cm
tory formulas (cf. Definition 6 on page 186). Similar to the monitoring of constraint
states, the state of an instance can be monitored using the automaton generated for
the mandatory formula of the model.

Example 7 (Instance states). Table 6.2 shows how three instances (ci 1 ; ci 2 ,and ci 3 )
of the model shown in Fig. 6.9 on page 188 change state during execution. The
instance state is always deduced from the automaton’s current state (Fig. 6.9b).
As long as the automaton stays in nonaccepting states (i.e., S 0;S 1 ;::: ;S 4 ), the
instance is temporarily violated (tv). The instance becomes satisfied (s) only when
the automaton reaches its accepting state S 5 . If the instance trace cannot be replayed
in the automaton, the instance is violated (v).
The instance state cannot always be directly induced from the states of its indi-
vidual constraints. When all mandatory constraints are satisfied, the instance is
also satisfied, and if at least one mandatory constraint is violated, the instance is
also violated. However, in the presence of temporarily violated constraints and the
absence of violated constraints, a deeper analysis of the constraints is needed to
induce the instance state. Consider, for example, the instance of the ConDec model
shown in Fig. 6.13. The state of the individual constraints is depicted for execu-
tion trace hC; A; Bi. Observe that none of the mandatory constraints is violated.
The precedence constraint is satisfied, because task A is executed before task B.

Table 6.2 State change for instances of the ConDec model in Fig. 6.9
Instance ci 1 D . ; cm/ Instance ci 2 D . ; cm/ Instance ci 3 D .ı; cm/
i State !.ci 1 / i State !.ci 2 / ı i State !.ci 3 /
initial S 0 tv initial S 0 tv initial S 0 tv
delivery S 2 tv pickup S 1 tv delivery S 2 tv
pickup S 4 tv delivery S 4 tv bill v
bill S 5 s bill S 5 tv
pickup S 5 s
“s”Dsatisfied,“tv”Dtemporarily violated,“v”Dviolated