[m-dev.] Re: for review: debugging oracle

[Mark Anthony BROWN]

Lee Naish writes:
> Mark Anthony BROWN <dougl at cs.mu.OZ.AU> writes:
> 
> >In addition, the oracle returns an identifier of what
> >assumption was used to give the answer.  This way, when a bug is
> >diagnosed the user will be able to check what assumptions were made
> >(note that at this stage the identifiers are not actually used).
> 
> I agree with the desirability of the (future) functionality but I'm not
> sure about this design.  I think that explaining the diagnisis should be
> independent of the oracle in the first instance.  The debugger should
> keep track of the correctness of the various edt nodes and if an
> explanation is called for the erroneous node + correct/inadm. children can
> be dislayed in some way.  If the user thinks the truth value of a node is
> wrong we can call a new oracle predicate with the formula in the node.

Ok, I understand.

> This (I think) will cycle through the "don't know" questions for the
> children of a single node.  A better algorithm is to have a queue of
> unknown nodes for the whole tree, so you cycle through "don't know"
> questions for the whole tree.

Yes, the current implementation is not particularly clever.  I'll
keep your suggestion in mind, but I won't make it part of this change
since this change is meant to be about the oracle.

> 
> >+	% The identifier of an assumption used by the oracle.
> >+	%
> >+:- type oracle_assumption.
> 
> I don't like this terminology.  I think its best to think of the oracle
> "knowing" things (even if they are occasionally false).  Assertion is
> tempting but probably has too many other uses.  Fact perhaps?  Its a
> unit of knowledge, a formula + associated truth value...

"Fact" would be ambiguous too, IMHO.  I agree that it is best to think
of the oracle as knowing, but I can't think of a word which expresses
this well.  Being an oracle, maybe the word should be "prophecy"?  :-)
I'm not (yet?) convinced that "assumption" isn't the best choice.

> 
> >+:- type oracle_answer
> >+	--->	known(edt_truth, oracle_assumption)
> >+      ;       not_known.
> 
> I would skip the oracle_assumption (see discussion above).
> And enhance not_known (see discussion below).

I'll make both of these changes.

> 
> >+:- type oracle_assumption
> >+                      %
> >+                      % Truth value came from a table of ground atoms.
> >+                      %
> >+      --->    ground(edt_node).
> 
> Add arg to say where/when it became known (see above)?

Good idea.  I think I will leave the details for a later change, though,
since I have a few things on my plate at the moment.

> 
> Best fix up the terminology here (or it will confuse when missing
> answers are handled):
> Nodes are corect/incorrect{/inadmissible}.
> Formulas/atoms/... are valid/not valid (possibly satisfiable){/inadmissible}

Oops.  Yes, of course.

> 
> I think the best
> approach it probably for the oracle to pass back more info to the tree
> search part of the debugger.  Instead of returning a maybe(edt_truth) we
> need to return something like 
> 
> :- type oracle_answer
> 	--->	known(edt_truth)
>       ;       not_known(debugger_command).
> 

I agree.

A relative diff is coming soon.

Cheers,
Mark
-- 
Mark Brown, PhD student            )O+  |  "Another of Fortran's breakthroughs
(m.brown at cs.mu.oz.au)                   |  was the GOTO statement, which was...
Dept. of Computer Science and Software  |  uniquely simple and understandable"
Engineering, University of Melbourne    |              -- IEEE, 1994
--------------------------------------------------------------------------
mercury-developers mailing list
Post messages to:       mercury-developers at cs.mu.oz.au
Administrative Queries: owner-mercury-developers at cs.mu.oz.au
Subscriptions:          mercury-developers-request at cs.mu.oz.au
--------------------------------------------------------------------------