Page 207 -

198 M. Pesic
models provides an automated mechanism for detecting dead tasks and conflicts,
as described in Sect. 6.2.6. In addition to the automated verification of constraint
models, it is also possible to detect the exact combination of constraints that causes
(each of) the error(s), which helps developing error-free ConDec models.
Execution of instances of constraint models is driven by constraints. To execute
an instance in a correct way, it is necessary that, at the end of the execution, all
mandatory constraints are satisfied, that is, that the instance is satisfied. Execut-
ing activities in an instance may change the state of one or more constraints and
the instance itself. It is important that the instance state and states of all its con-
straints are constantly monitored and presented to users throughout the execution of
the instance (cf. Sects. 6.3.2 and 6.3.3). This helps users who execute instances of
ConDec models to understand what is going on and which actions are necessary in
order to execute the instance in a correct way. Also, to ensure a correct instance
completion, it is necessary to allow completion only if the instance is satisfied
(cf. Sect. 6.3.5).
Some actions of users might cause an instance (and its constraints) to leave the
satisfied state. In some of these cases it is possible to take some actions that will
eventually lead to a correct, that is, satisfied, instance. We refer to this type of vio-
lations as temporary violations. In other cases, the instance becomes permanently
violated, that is, it becomes impossible to satisfy the instance in the future. Espe-
cially, for instances with multiple constraints, it is very difficult for users to be aware
of actions that will permanently violate the instance. Therefore, it is important to
prevent users from taking actions that lead to permanent violation of instances of
ConDec models (cf. Sect. 6.3.4).

Exercises

Exercise 1. Tasks bless, pray, curse,and become holy are four tasks in the Reli-
gion process. Users of this process must obey two important rules. First, one should
pray at least once. Second, every time one curses, one must eventually pray for
forgiveness afterwards.
(a) Develop a ConDec model for this process using the constraint templates shown
in Fig. 6.5 on page 182.
(b) Write down the mandatory LTL formula for the Religion model.

Exercise 2. Figure 6.18 shows the automaton generated for the mandatory formula
of the Religion model described in the previous exercise. Using this automaton,
mark which of the following execution alternatives are possible in instances of the
Religion model:

(a) hbecome holy; curse; blessi
(b) hpray; bless; prayi
(c) hcurse; bless; curse; bless; prayi