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

[Lee Naish]

Mark Anthony BROWN <dougl at cs.mu.OZ.AU> writes:

>The oracle now tries to remember previous answers and uses
>them if available, and only asks the user if there is no other
>information.

Great.

>	- Allow the user to answer "don't know".

Also good, though I suggest a better algorithm for handling it below.

>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.

Related to this, I think it would be worthwhile having additional
information associated with each bit of knowledge in the oracle
indicating where it came from (eg lee at cs.mu.oz.au said so at
Wed Aug 18 15:30:00 EST 1999, or its an assertion in file foo.m, or
pred was declared correct by lee at cs.mu.oz.au at Wed Aug 18 15:30:01 etc).
We should (ultimately) be able to get a proof/explanation of any
conclusion of the oracle so we can identify incorrect assertions,
confusion over intended interpretations, etc.


> analyse_children([Child | Children], Bug0, Bug, Oracle0, Oracle) -->
> 	{ edt_root(Child, ChildNode) },
>-	query_oracle(ChildNode, Valid, Oracle0, Oracle1),
>+	query_oracle(ChildNode, Answer, Oracle0, Oracle1),
> 	(
>-		{ Valid = yes },
>+		%
>+		% XXX we currently don't record the assumption used.
>+		% See comment above.
>+		%
>+		{ Answer = known(yes, _) },
> 		analyse_children(Children, Bug0, Bug, Oracle1, Oracle)
> 	;
>-		{ Valid = no },
>+		{ Answer = known(no, _) },
> 		analyse_edt_2(Child, Bug, Oracle1, Oracle)
>+	;
>+		{ Answer = not_known },
>+		{ append(Children, [Child], NewChildren) },
>+		analyse_children(NewChildren, Bug0, Bug, Oracle1, Oracle)
> 	).

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.  This requires analyse_children etc to
have an extra output arg which is a list of "don't know" nodes and a top
level pred which keeps trying to get the user to answer these questions
(or eventually gives up).  The current code is a step in the right
direction at least.  Its not entirely clear what the best algorithm is
but the one suggested above seems reasonable (you can also alert the
user when you are going to repeat questions).

>+	% 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...

>+:- 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).

>+:- type oracle_kb
>+	---> oracle_kb(
>+		%
>+		% For ground atoms, the knowledge is represented directly
>+		% with a map.  This is used, for example, in the common
>+		% case that the user supplies a truth value for a
>+		% "wrong answer" node.
>+		%
>+		map(edt_node, edt_truth)

Might be best to distinguish edt_node and the type for formulas in the
oracle (eventually at least - probably ok for now since things will
expand anyway).  Also, a map may not be flexible enough eventually due
to the kinds of matching required (unification/subsumption, not just
identity) - it getts pretty messy!

>+:- 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)?

>+:- type debugger_command
>+	--->	yes			% The node is valid.
>+	;	no			% The node is invalid.
>+	;	do_not_know		% The user has no answer.
>+	;	browse			% Browse the data before answering.
>+	;	tree			% Browse the EDT.
>+	;	help			% Request help before answering.
>+	;	illegal_command.	% None of the above.
>+
>+
>+:- pred query_user(edt_node, maybe(edt_truth), io__state, io__state).


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}
Should add inadmissible above, at least in a comment or with a "Sorry,
not implemented.\n".

Another thing relating to this is the tree command (and other similar
ones in the future no doubt).  From the users perspective, when they are
asked a question it makes sense that they should be able to ask about
the tree, do various debugger navigation commands, etc.  However, the
questions are asked by the oracle and the oracle (ideally?) should not
know anything about the tree, navigation etc (it just knows the truth
value of certain formulas).  The logical module structure somehow
conflicts with the requirements of the interaction.  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).

You might evan want to add debugger_command to the known case
eventually.  debugger_command needs to have a "default" case for when
the user just says "don't know".

Another possibility would be more the OO style where there is an object
which handles the direct user interaction and passes messages to the
oracle and debugger, but this could be a bit hard with Mercury wrt how
the io__state is passed around.

	lee
--------------------------------------------------------------------------
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
--------------------------------------------------------------------------