Modes of use of a WACS

In a previous section, we described some modes of use of a WACS. We
will show that most of those modes of use can be modeled in our
approach. The modes of use that cannot be modeled with the tools
developed in this paper are the ones that deal with inter-case
coordination, such as workflow as a scheduler or as a simulator. The
logic developed herein deals only with a single workcase, the logical
model does not distinguish the activity *a* executed in a workcase,
from the same activity performed for another workcase.

WACS as a verifier, would simply check whether a workcase complies
with the process models, policies and the such. If as usual, *F* is
the set of formulas that represent the policies, processes,
constraints, and so on, *wc* is the workcase, and
is the
current time, then the case is consistent with *F* if
.

The WACS as a dispatcher and as a helper are from the point of view of this model similar. They both figure out the activities that can be performed now; the dispatcher actually sends the activity to the appropriate actor, where as the helper only lists them. From the point of view of our approach, what is needed is the ability to discover what are the enabled activities. They are all activities such that

The WACS as a planner cannot be meaningfully modeled in this framework,
since preconditions, and postconditions for each activity where not
modeled. But it is possible to model the WACS as a replanner. If it is
decided that activity *p* must be performed (in the future), then the
set of activities *x* such that
are the activities that must be performed next. After these
activities were performed, the workcase will be *wc*', at a time *t*'.
At this stage one would again determine the set of activities that can
be performed next, and so on successively until at a certain time
*t*'' with the workcase at stage *wc*'' *p* itself would satisfy
.

If one decides to postpone an activity *q* and call an unplanned
activity *p*, say to evaluate if/how *q* will be done, then
for ,
will
compute all activities that can start now so that *p* can start as
soon as possible, but will not include those that are preparation for
*q*.

Recall that
states that all minimal models that
are compressed continuations of *wc* after *t* and which satisfy
satisfy .