Page 337 -

12 The Declare Service 333
12.5 Verification of Constraint Models

DECLARE uses the methods presented in Chap. 6 to detect dead tasks, conflicts,
and the smallest set of constraints that cause them. To illustrate this, we use the
example for a ConDec model with a conflict from Chap. 6. Figure 12.7a shows this
model in DECLARE:the two 1..* constraints specify that each of the tasks deliv-
ery and bill must be executed at least once. The two precedence constraints specify
that (1) task bill cannot be executed before task pickup and (2) task pickup can-
not be executed before task bill. Besides, for detecting error(s) in models, for each
error DECLARE searches through (the powerset) mandatory constraints to find the
smallest group of constraints that causes the error. DECLARE applies the verification
methods described in Chap. 6 for each group of constraints to detect the smallest
group of constraints that causes the error.
Figure 12.7b–d shows that the DECLARE verification procedure reports three
errors in this model. First, the two precedence constraints cause the bill task to
be dead (cf. Fig. 12.7b). Second, the two precedence constraints cause the pickup
task to be dead (cf. Fig. 12.7c). Finally, the two precedence constraints and the 1..*
constraint on task bill cause a conflict (cf. Fig. 12.7d). Because of this conflict, it
is not possible to satisfy all constraints at the same time. At least one of the three
related constraints mentioned needs to be dropped.
Detailed verification reports in DECLARE aim at helping model developers to
understand error(s) in the model. The goal is to assist the resolution of such prob-
lems. As discussed in Chap.6, errors can be eliminated from a model by removing
at least one constraint from the group of constraints that together cause the error.
For example, if one of the two precedence constraints would be removed from the
DECLARE model in Fig. 12.7a, there would no longer be errors in this model. Also,
removing the 1..* constraint on task bill would remove the conflict, but tasks bill
and pickup would still be dead.

12.6 Execution of Constraint Model Instances

DECLARE determines which tasks can be executed next, that is, determining the
enabled tasks, the state of an instance, and states of constraints using the approach
presented in Chap. 6. Each instance is launched (i.e., created) in the Framework
tool and users can work on instances via their Worklists (cf. Fig. 12.3 on page 329).
A user can work on instances from his/her Worklist. Figure 12.8 shows a screenshot
of a Worklist. All available instances are shown in the list on the left side of the
screen, underneath the “instances” header. In Fig. 12.8, there are two instances of
the Less than Truck Load model presented in Fig. 12.5 on page 332: “(1) Less than
Truck Load” and “(2) Less than Truck Load.” The model of the selected instance is
shown on the right side of the screen. After the user starts a task by double-clicking
it, the task will be opened “in the task panel” under the model.