Page 202 -

6 Declarative Workflow 193

satisfied temporarily violated satisfied

1 2
precedence
A B
<C,A,B>
violated
C

Fig. 6.13 An instance of ConDec model with trace hC; A; Bi

Constraint 1, which specifies that task A must be executed exactly once, is also
satisfied. Constraint 2, which specifies that task A must be executed exactly twice,
is temporarily violated, and would become satisfied if task A would be executed
once again. However, if task A would be executed once again, then the 1 constraint
would become violated. As it is not possible to satisfy the mandatory constraints,
the instance state is violated.
Note that the instance presented in Fig. 6.13 cannot be satisfied because the
instance model contains a conflict. Recall from Sect. 6.2.6 that when the model con-
tains a conflict, then there is no execution that will satisfy the constraints from the
model. The cause of the error is the combination of constraints 1 and 2. Verification
can be used to detect and correct such errors. In the next section, we explain how
instances of correct constraint models can be executed without becoming violated.

6.3.4 Enforcing Correct Instance Execution

The goal of instance execution is to finish the execution in such a way that the
instance is satisfied. In order for an instance to be executed in a correct man-
ner, the execution of tasks that would eventually lead to the violated state of the
instance should be prohibited. This can be done using the automaton generated for
the mandatory formula of the instance. During execution, the automaton changes
state when tasks are executed. Given the current state in the automaton, tasks that
are not implied by labels on transitions from this state are prohibited, and other tasks
are allowed.

Example 8 (Instance execution). Again, consider the ConDec model shown in
Fig. 6.9 on page 188. The automaton represents exactly all traces that satisfy this
model. Initially, no tasks have been executed and the automaton is in state S 0 .
Because of the precedence constraint, only task bill should be prohibited, and other
tasks should be allowed to execute. This can be detected in the automaton by
the absence of a bill transition from S 0 and the presence of pickup and delivery