Possible error in AngelicSearch

[samagra14]

The last two lines of the angelicSearch algorithm appear a bit incorrect.

for each sequence in REFINEMENTS(hla, outcome, hierarchy) do
   frontier ← INSERT(APPEND(prefix, sequence, suffix), frontier)

1. There is no state defined as outcome in the entire algorithm.
2. We cannot apply the refinements function to a single state as under the angelic semantics we consider an entire set of reachable states.
3. The refinements function should be modified to accept a set of possible states and it should return all those HLAs which are applicable in at least one of the states in the set.

@norvig Please have a look at this. Please correct me if I am wrong.