This page supplies the further definitions needed to complete the basic scheduling example in Chapter 4.
Given a number of activities (i.e. 
, 
, 
and 
), a number of time periods (i.e. 
, 
and 
) chronologically ordered (
) and a set of requirements stating the desired ordering and simultaneity of activities, then a schedule is a set of activity-time pairs assigning to each activity exactly one time period, where the assignements must satisfy all the requirements.
We have four types of requirements on the schedule:
Furthermore, we prefer schedules that assign to each activity a time period that occurs as early as possible. The schedulling process is stated as follows.
We have activities a1, a2, a3 and a4.
We have time points t1, t2 and t3.
The time points are ordered with t1 forst, followed by t2 and then t3.
We can refine a schedule, S, to a new schedule formed from S and an activity, A, started at time, T, if A is an activity; T is a time point; and A has not already been assigned in schedule S.
A schedule, S, is complete if every activity, A, is assigned a time, T in S.
Requirements on the schedule are represented as pairs where the first element is a schedule and the second is a predicate which must hold for that schedule. For our example, these are as follows:
For any schedule, S: a3 must precede a2 in S; a3 must precede a4 in S; and a2 must not occur at the same time as a4 in S.
We next define the tests required above.
Activity, 
, precedes activity, 
, in schedule, S,
if every time point at which 
is assigned in S is earlier
than any to which 
is assigned.
Activity, 
, is simultaneous with activity, 
, in
schedule, S, if both are assigned to the same time point.
Time point, 
, is earlier than time point, 
, if
immediately precedes 
or if 
immediately
precedes some other time point, 
, which is earlier than 
.
Finally we define what we mean by a correct schedule.
A schedule S is correct if all requirements R hold for it.
This completes our definition of the scheduling model. That it is a
model, rather than a specification of a real scheduler, is clear
because it omits many features of practical schedulers (such as an
efficient schedule selection algorithm). Nevertheless, it is
executable and can generate alternative schedules for our test example
by finding solutions for the goal 
. Instances
generated for X by satisfing this goal from our definitions include:
