n
SOC 2 Composition 2 slide-24
Planning Assumptions
The plan consists of a partial order of service calls: states
ordered by the relation subsequent: <. Let (p=a,S) denote that property p
has value a in state S.
Let service WS be called in state Si, and
return in state Sf.
- ∀ p, (input WS p) ∃ a, (p=a, Si)
- ∀ p, (Output WS p a),
(p=a,Sf)
- (Subseqent Si Sf): Si < Sf
No spoiling and
persistance frame
assumptions:
(p=a,Sk) ⇐ (p=a,Si)
∧ (Si < Sk)
∧ ¬ ∃ Sj, (p=b,Sj),
Si < Sj ≤ Sk.
Constraints: Service-specific or global conditions restrict property
values and service calls in state sequences.
Preferences: Some property values and service calls in some state sequences are
preferred.
Meta-Constraint: ¬ (
(p=a, S) ∧ (p=b, S)) .
I.e., properties are single-valued in a state.
©2012
Charles Petrie - permission to reproduce widely with attribution.