A Plan is a finite partially ordered set
of service calls in states
{S1,... Si,...Sn}
where
where service Wl is called in
state Sl and
The values of the instantiations of each property in the
propositions in E(Wi), including Outputs,
are used for the the same
properties in the call of each of the properties
in the propositions
of P(Wj), including Inputs, and
(Si < Sj) ∧
( ∀ k | Si <Sk <
Sj, Pp(Wj) ∉ Ep(Wk)) ,
This last condition is too strong and will be refined in
composition lectures.
A Plan defines a virtual action with P(Plan) being
those propositions true in S1 and in any
P(Wi) and E(Plan)
being those conditions true in
Sn and in any E(Wi).