// - be on the frontier or
// - have a non-doomed node closer to the frontier than themself
if (phase.isFrontier()) dead = false;
- for(Result r : children)
- if (state.doomed) { if (r.usedByAnyNode()) { dead = false; break; } }
- else { if (r.usedByNonDoomedNode()) { dead = false; break; } }
+ else for(Result r : children)
+ if (state.doomed) { if (r.usedByAnyNode()) { dead = false; break; } }
+ else { if (r.usedByNonDoomedNode()) { dead = false; break; } }
dead |= results.size()==0;
- if (!dead || destroyed) return;
+ if (!dead) return;
destroyed = true;
while(children.size()>0)
for(Result r : children) {