Page 209 -

200 M. Pesic
!curse
!pray
curse

S0 S1

pray

Fig. 6.20 The automaton generated for the mandatory formula of the religion model after
removing task become holy and the constraint specifying that one should pray at least once

!become holy !curse !pray
curse
pray
S0 S1 S2
pray pray

Fig. 6.21 The automaton generated for the mandatory formula of the religion model after adding
a constraint specifying that task become holy cannot be executed before task pray

(a) Develop a ConDec mode for the new model using the appropriate constraint
templates from Fig. 6.5 on page 182.
(b) 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.21.

Exercise 6. Develop a ConDec model for the process containing tasks bless, pray,
curse,and become holy, where three rules must be followed:
(a) One should become holy at least once.
(b) Every time one curses, one must eventually pray for forgiveness afterwards.
(c) Tasks become holy and curse cannot both be executed in the same instance.
Does this model have errors? Explain why. Hint: use the automata generated for the
mandatory formula of this model shown in Fig. 6.22.

Exercise 7. Develop a ConDec model for the process containing tasks bless, pray,
curse,and become holy, where four rules must be followed:
(a) One should become holy at least once.
(b) Every time one curses, one must eventually pray for forgiveness afterwards.
(c) Tasks become holy and curse cannot be both executed in the same instance.
(d) One should curse at least once.
Does this model have errors? Explain why. Hint: the automata generated for the
mandatory formula of this model is empty, that is, it does not have any states or
transitions.