Page 208 -

6 Declarative Workflow 199
!pray
!curse
pray

S0 S1

curse

Fig. 6.18 The automaton generated for the mandatory formula of the Religion model

!curse
!pray !pray
curse
–
S0 S1
pray
S0 S1
pray
(a) One should pray at least once (b) One must always eventually pray
after cursing

Fig. 6.19 Automata generated for the two constraints from the religion model

(d) hbless; become holyi
Exercise 3. Figure 6.19 shows automata generated for the two constraints from
the Religion model from the first exercise. Using these two automata and the
automaton generated for the mandatory formula of this model (cf. Fig. 6.18), write
down how states of the instance and both constraints change while executing trace
hbless; curse; bless; bless; curse; become holy; pray; curse; prayi.

Exercise 4. Consider an instance of the Religion model described in the first
exercise, where the instance trace is hbless; curse; bless; bless; curse; become holy;
pray; curse; prayi. Assume that we attempt to change the model of this instance in
a way that:

The constraint specifying that one should pray at least once is removed
Task become holy is removed.
Can this dynamic change be applied to the instance at this moment? Explain
why. Hint: use the automata generated for the mandatory formula of the new (i.e.,
changed) model shown in Fig. 6.20.

Exercise 5. Consider an instance of the Religion model described in the first
exercise, were the instance trace is hbless; curse; bless; bless; curse; become holy;
pray; curse; prayi. Assume that we attempt to change the model of this instance in
a way that a constraint specifying that task become holy cannot be executed before
task pray is added.