14.4 Discussion and Historical Remarks 343
the current AND/OR graph. At some maximal depth, the formula is computed with
heuristics estimates for leaf assertions and regressed backward until the root. The
action corresponding to the minimum is chosen for resolving the current flaw.
A final element for controlling the search may rely on a partial order on the
state variables. Flaws are processed according to this order: no flaw is considered
for the state variable x until all flaws for all state variables that precede x have
been addressed. This scheme works as long as the resolution of flaws on x does
not introduce new flaws for state variables that precede x. It is easy to synthesize
automatically a partial order that guarantees this property for a particular ...