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 $\hat{t}$ is the current time, then the case is consistent with F if $wc, \hat{t}\;\sim\; F$.

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 $x \in A$such that $\Box F, wc, \hat{t}\;\rhd\;x$

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 $\Box F \land \stackrel{\rightarrow}{\Diamond}\!p, wc, \hat{t}\;\rhd\; x$ 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 $\Box F \land \stackrel{\rightarrow}{\Diamond}\!p, wc'', t'' \;\rhd\;p$.

If one decides to postpone an activity q and call an unplanned activity p, say to evaluate if/how q will be done, then $\Box F \land \stackrel{\rightarrow}{\Diamond}\!( p \land \stackrel{\rightarrow}{\Diamond}\!q), wc, \hat{t}\;\rhd\;x$ for $x \in A$, 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 $\alpha, wc, t \;\rhd\;x$ states that all minimal models that are compressed continuations of wc after t and which satisfy $\alpha$ satisfy ${\bf N}x$.