Page 200 -

6 Declarative Workflow 191
6.3.1 Constraint Model Instances

The execution of constraint models is driven by the constraints. These constraints
should ensure the correct execution of instances of the model, that is, it should not
be possible to violate mandatory constraints during execution and all mandatory
constraints should be satisfied after execution. To ensure the correct execution of
an instance, it is necessary to keep track of the execution trace of that instance.
Formally, a constraint workflow model instance is defined as follows.
Definition 10 (Constraint model instance ci). A constraint model instance ci is
defined as a pair ci D . ; cm/,where:
2 T is the instance’s trace

cm 2 U cm is a constraint model
We use U ci to denote the set of all constraint instances.

6.3.2 Monitoring Constraint States

The sequence of executed tasks for an instance is kept in its instance trace. Depend-
2
ing on the instance trace, constraints from the model can be satisfied, violated, and
temporarily violated, which means that the constraint is currently violated, but can
still be satisfied. Consider, for example, the LTTL ConDec model shown in Fig. 6.9
on page 188. Although trace hpickupi violates both 1..* constraints, once pickup and
bill are executed, all constraints will become satisfied. Hence, both 1..* constraints
are temporarily violated. As long as the execution is in progress and more tasks can
be executed, we distinguish these three states.
Definition 11 (Constraint state ). Let c 2 C be a constraint and 2 T an
execution trace. The function W .C T / !fsatisfied; temporarily violated;

violatedg is defined as:

8
< satisfied if 2 T I

c
temporarily violated if . … T / ^ .9 2 T

c
. ; c/ D c W C 2 T /I
violated otherwise:
:
The state of a constraint can continuously be monitored via the automaton generated
for its LTL formula. Every time a user executes a task, a transition in the automaton
is triggered, and the automaton changes state. When the automaton is in an accepting
state, then the constraint is satisfied. If the automaton is in a nonaccepting state from
which an accepting state is reachable, then the constraint is temporarily violated.
Finally, if the trace cannot be “replayed” on the automaton at all, then the constraint
is and will continue to be violated for this instance.

2 In Sect. 6.3.4, we explain how this state is avoided during execution.