Refinement (Go(Home, SFO),
STEPS: [Drive(Home, SFOLongTermParking ),
Shuttle(SFOLongTermParking, SFO)] )
Refinement (Go(Home, SFO),
STEPS: [Taxi(Home, SFO)] )
Refinement(Navigate([a, b], [x, y]),
PRECOND: a = x ∧ b = y
STEPS: [ ] )
Refinement(Navigate([a, b], [x, y]),
PRECOND: Connected ([a, b], [a − 1, b])
STEPS: [Left , Navigate([a − 1, b], [x, y])] )
Refinement (Navigate([a, b], [x, y]),
PRECOND: Connected ([a, b], [a + 1, b])
STEPS: [Right , Navigate([a + 1, b], [x, y])] )
...
Figure ?? Definitions of possible refinements for two high-level actions: going to San Francisco airport and navigating in the vacuum world. In the latter case, note the recursive nature of the refine- ments and the use of preconditions.