Page 195 -

186 M. Pesic
C O C is a set of optional constraints, where every element c 2 C O is a well-
formed LTL formula over T
Note that each mandatory and optional constraint is a well-formed LTL formula over
tasks from cm, that is, a constraint cannot involve tasks that are not in the model.
During execution, mandatory constraints must be followed. Therefore, the set of
traces that satisfy constraint model cm contains all traces that satisfy all manda-
tory constraints in cm. The conjunction of all mandatory formulas is defined as the
mandatory formula of the model.
Definition 6 (Mandatory formula f cm ). Let cm 2 U cm be a constraint model
where cm D .T; C M ; C O /, then the mandatory formula for model cm is defined
as
(
true if C M D ∅I
V
f otherwise:
f cm D
f 2C M
The automaton generated for the mandatory formula (f cm) of a model cm gen-
erates the language T , that is, the set of traces that satisfy cm. In the absence of
cm
mandatory constraints, all traces over tasks in the model are allowed.
Definition 7 (Constraint model satisfying traces). Let f cm be the mandatory
formula for constraint model cm.

(
T if C M D ∅I
T
cm D
T otherwise:
f cm
Furthermore, we say a trace 2 T satisfies model cm, if and only if, 2 T ,
cm
and violates cm, if and only if, … T .
cm
Consider, for example, the Carrier Appointment subprocess of the Order Fulfill-
ment process model described in Appendix A. In particular, consider the parts (i.e.,
branches) of the Carrier Appointment net for handling the shipments that require
1
the truck load (TL) and less than truck load (LTTL). Figure 6.8a shows the the
truck load part, and Fig. 6.8b shows the less than the truck load part of the Carrier
Appointment net. For the purpose of simplicity, in the remainder of this chapter, we
will use shorter names for the relevant tasks: pickup for Arrange Pickup Appoint-
ment, delivery for Arrange Delivery Appointment, bill for Create Bill of Lading
and shipment for Create Shipment Information Document.Examples 3 and 4 show
ConDec models for these two parts of the Carrier Appointment net.
Example 3 (The ConDec model for the LTTL process (cm LT TL )). In the LTTL
branch of the process, the goal is to execute tasks pickup, delivery,and bill in such

1
Note that in the original Carrier Appointment net, this branch of the net is called LTL. In this
chapter we will use the LTTL abbreviation to avoid confusion with Linear Temporal Logic (LTL).