[m-dev.] for review: debugging oracle

[Mark Anthony BROWN]

Hi,

This is for Lee to review.  (Comments welcome from anyone, of course).

Cheers,
Mark.


Estimated hours taken: 50

This change adds a more sophisticated oracle to the declarative
debugger.  The oracle now tries to remember previous answers and uses
them if available, and only asks the user if there is no other
information.  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).

browser/declarative_oracle.m:
	- Add the abstract type "oracle_assumption", which identifies
	  an internal assumption of the oracle.
	- Add the type "oracle_answer", which the oracle returns to the
	  caller.  This holds both the truth value and the assumption
	  used.
	- Implement a knowledge base to store the previous answers.
	  This data structure is designed to be able to store arbitrary
	  assertions, although at this stage only one kind of assertion
	  is used.
	- Where possible, use the KB to answer questions, instead of
	  asking the user.
	- Allow the user to answer "don't know".
	- Update comments.

browser/declarative_debugger.m:
	Use the new interface to the oracle.  Handle "don't know"
	answers in a simple way: either save the question and ask it
	later or return without finding any bug.

tests/debugger/declarative/Mmakefile:
tests/debugger/declarative/oracle_db.{m,inp,exp}
	Add a test case for the new feature.

Index: browser/declarative_debugger.m
===================================================================
RCS file: /home/mercury1/repository/mercury/browser/declarative_debugger.m,v
retrieving revision 1.4
diff -u -r1.4 declarative_debugger.m
--- declarative_debugger.m	1999/04/30 03:59:49	1.4
+++ declarative_debugger.m	1999/08/11 07:43:39
@@ -67,8 +67,8 @@
 	mode edt_children(in, out) is det
 ].
 
-:- pred analyse_edt(T, io__input_stream, io__output_stream, oracle_data,
-		oracle_data, io__state, io__state) <= evaluation_tree(T).
+:- pred analyse_edt(T, io__input_stream, io__output_stream, oracle_state,
+		oracle_state, io__state, io__state) <= evaluation_tree(T).
 :- mode analyse_edt(in, in, in, in, out, di, uo) is det.
 
 %-----------------------------------------------------------------------------%
@@ -239,7 +239,7 @@
 		% persistent.  It really should be saved between
 		% calls to this predicate.
 		%
-	{ oracle_data_init(Oracle0) },
+	{ oracle_state_init(Oracle0) },
 	analyse_edt(EDT, MdbIn, MdbOut, Oracle0, _).
 
 
@@ -247,14 +247,22 @@
 	io__set_input_stream(MdbIn, OldIn),
 	io__set_output_stream(MdbOut, OldOut),
 	{ edt_root(EDT, RootNode) },
-	query_oracle(RootNode, Valid, Oracle0, Oracle1),
+	query_oracle(RootNode, Answer, Oracle0, Oracle1),
 	(
-		{ Valid = yes },
+		%
+		% XXX We don't record the assumption used.  It is not
+		% used by the back end anyway.
+		%
+		{ Answer = known(yes, _) },
 		{ Bug = not_found },
 		{ Oracle = Oracle1 }
 	;
-		{ Valid = no },
+		{ Answer = known(no, _) },
 		analyse_edt_2(EDT, Bug, Oracle1, Oracle)
+	;
+		{ Answer = not_known },
+		{ Bug = not_found },
+		{ Oracle = Oracle1 }
 	),
 	report_bug(Bug),
 	io__set_input_stream(OldIn, _),
@@ -264,7 +272,7 @@
 	%
 	% Assumes the root note is not valid.
 	%
-:- pred analyse_edt_2(T, declarative_bug(T), oracle_data, oracle_data,
+:- pred analyse_edt_2(T, declarative_bug(T), oracle_state, oracle_state,
 		io__state, io__state) <= evaluation_tree(T).
 :- mode analyse_edt_2(in, out, in, out, di, uo) is det.
 
@@ -274,7 +282,7 @@
 
 
 :- pred analyse_children(list(T), declarative_bug(T), declarative_bug(T),
-		oracle_data, oracle_data, io__state, io__state)
+		oracle_state, oracle_state, io__state, io__state)
 				<= evaluation_tree(T).
 :- mode analyse_children(in, in, out, in, out, di, uo) is det.
 
@@ -282,13 +290,21 @@
 	[].
 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)
 	).
 
 
Index: browser/declarative_oracle.m
===================================================================
RCS file: /home/mercury1/repository/mercury/browser/declarative_oracle.m,v
retrieving revision 1.3
diff -u -r1.3 declarative_oracle.m
--- declarative_oracle.m	1999/05/30 03:54:31	1.3
+++ declarative_oracle.m	1999/08/11 07:58:12
@@ -9,101 +9,243 @@
 %	This module implements the oracle for a Mercury declarative debugger.
 % It is called by the front end of the declarative debugger to provide 
 % information about the intended interpretation of the program being
-% debugged.  The current implementation simply asks the user directly.
+% debugged.
 %
+% The module has two sub-components, the knowledge base and the user
+% interface.  The knowledge base is a cache for all the assumptions
+% that the oracle is currently making.  When the oracle is queried,
+% it first checks the KB to see if an answer is available there.
+%
+% The user interface is the means by which a query can be forwarded
+% to the user.  If no answer is available in the KB, then the oracle
+% uses the UI to get the required answer from the user.  Before
+% returning the answer, the new knowledge is added to the KB so the
+% user will not be asked the same question twice.
+%
 
 :- module declarative_oracle.
 :- interface.
 :- import_module io.
 :- import_module declarative_debugger.
 
+	%
+	% The oracle state.  This is threaded around the declarative
+	% debugger.
+	%
+:- type oracle_state.
+
+	%
+	% The identifier of an assumption used by the oracle.
+	%
+:- type oracle_assumption.
+
 	%
-	% The oracle database.  This is threaded around the declarative
-	% debugger, but currently stores no information.
+	% A response that the oracle gives to the caller.  If the
+	% answer is known, the assumption used is also returned.
 	%
-:- type oracle_data.
+:- type oracle_answer
+	--->	known(edt_truth, oracle_assumption)
+	;	not_known.
 
 	%
 	% Query the oracle about the program being debugged.  The first
 	% argument is a node in the evaluation tree, the second argument
-	% is its validity in the intended interpretation.
+	% is the oracle response.  The oracle state is threaded through
+	% so its contents can be updated after user responses.
 	%
-:- pred query_oracle(edt_node, edt_truth, oracle_data, oracle_data,
+:- pred query_oracle(edt_node, oracle_answer, oracle_state, oracle_state,
 		io__state, io__state).
 :- mode query_oracle(in, out, in, out, di, uo) is det.
 
 	%
 	% Produce a new oracle state.
 	%
-:- pred oracle_data_init(oracle_data).
-:- mode oracle_data_init(out) is det.
+:- pred oracle_state_init(oracle_state).
+:- mode oracle_state_init(out) is det.
 
 %-----------------------------------------------------------------------------%
 
 :- implementation.
-:- import_module bool, list, char, require, std_util, string.
-:- import_module util.
+:- import_module bool, list, char, require, std_util, string, map.
+:- import_module util, browse.
 
-:- type oracle_data == unit.
+:- type oracle_state
+	--->	oracle(
+%			browser_state,		% XXX not used yet
+			oracle_kb
+		).
 
-:- type debugger_command
-	--->	yes
-	;	no
-	;	browse
-	;	tree
-	;	help
-	;	illegal_command.
+oracle_state_init(oracle(KB)) :-
+	oracle_kb_init(KB).
+
 
+:- pred get_oracle_kb(oracle_state, oracle_kb).
+:- mode get_oracle_kb(in, out) is det.
 
-oracle_data_init(unit).
+get_oracle_kb(oracle(KB), KB).
 
+:- pred set_oracle_kb(oracle_state, oracle_kb, oracle_state).
+:- mode set_oracle_kb(in, in, out) is det.
 
-query_oracle(Node, Valid, Oracle0, Oracle) -->
-	query_user(Node, Answer),
+set_oracle_kb(oracle(_), KB, oracle(KB)).
+
+query_oracle(Node, Answer, Oracle0, Oracle) -->
 	(
-		{ Answer = yes },
-		{ Valid = yes },
+		{ query_oracle_kb(Node, Oracle0, KBTruth, KBAssumption) }
+	->
+		{ Answer = known(KBTruth, KBAssumption) },
 		{ Oracle = Oracle0 }
 	;
-		{ Answer = no },
-		{ Valid = no },
-		{ Oracle = Oracle0 }
+		query_user(Node, MaybeTruth),
+		{
+			MaybeTruth = yes(Truth),
+			%
+			% We don't need to check the consistency of this
+			% assertion because we only get here if the KB
+			% didn't know the answer already.
+			%
+			add_oracle_assumption(Node, Truth, Assumption,
+					Oracle0, Oracle),
+			Answer = known(Truth, Assumption)
+		;
+			MaybeTruth = no,
+			Answer = not_known,
+			Oracle = Oracle0
+		}
+	).
+
+
+%-----------------------------------------------------------------------------%
+
+	%
+	% This section implements the oracle knowledge base, which
+	% stores anything that the debugger knows about the intended
+	% interpretation.  This can be used to check the correctness
+	% of an EDT node.  The KB stores items of knowledge, called
+	% oracle assumptions, and these can be referred to from outside
+	% this module by the use of an identifier.
+	%
+
+	%
+	% The type of the knowledge base.  Other fields may be added in
+	% the future, such as for assertions made on-the-fly by the user,
+	% or assertions in the program text.
+	%
+:- 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)
+	).
+
+
+	%
+	% The type of identifiers for the oracle assumptions.
+	%
+:- type oracle_assumption
+			%
+			% Truth value came from a table of ground atoms.
+			%
+	--->	ground(edt_node).
+
+
+:- pred query_oracle_kb(edt_node, oracle_state, edt_truth, oracle_assumption).
+:- mode query_oracle_kb(in, in, out, out) is semidet.
+
+query_oracle_kb(Node, Oracle, Truth, Assumption) :-
+	get_oracle_kb(Oracle, oracle_kb(NodeMap)),
+	map__search(NodeMap, Node, Truth),
+	Assumption = ground(Node).
+
+
+:- pred add_oracle_assumption(edt_node, edt_truth, oracle_assumption,
+		oracle_state, oracle_state).
+:- mode add_oracle_assumption(in, in, out, in, out) is det.
+
+add_oracle_assumption(Node, Truth, Assumption, Oracle0, Oracle) :-
+	get_oracle_kb(Oracle0, oracle_kb(NodeMap0)),
+	map__set(NodeMap0, Node, Truth, NodeMap),
+	set_oracle_kb(Oracle0, oracle_kb(NodeMap), Oracle),
+	Assumption = ground(Node).
+
+
+:- pred oracle_kb_init(oracle_kb).
+:- mode oracle_kb_init(out) is det.
+
+oracle_kb_init(oracle_kb(NodeMap)) :-
+	map__init(NodeMap).
+
+
+%-----------------------------------------------------------------------------%
+
+	%
+	% This section handles the interactive part of the declarative
+	% debugging process.  The user is presented with an EDT node,
+	% and is asked to respond about the truth of the node in the
+	% intended interpretation.
+	%
+
+	%
+	% These are the responses the user can give.
+	%
+:- 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).
+:- mode query_user(in, out, di, uo) is det.
+
+query_user(Node, MaybeTruth) -->
+	write_node(Node),
+	io__nl,
+	get_command("Valid? ", Command),
+	(
+		{ Command = yes },
+		{ MaybeTruth = yes(yes) }
 	;
-		{ Answer = browse },
+		{ Command = no },
+		{ MaybeTruth = yes(no) }
+	;
+		{ Command = do_not_know },
+		{ MaybeTruth = no }
+	;
+		{ Command = browse },
 		io__write_string("Sorry, not implemented.\n"),
-		query_oracle(Node, Valid, Oracle0, Oracle)
+		query_user(Node, MaybeTruth)
 	;
-		{ Answer = tree },
+		{ Command = tree },
 		io__write_string("Sorry, not implemented.\n"),
-		query_oracle(Node, Valid, Oracle0, Oracle)
+		query_user(Node, MaybeTruth)
 	;
-		{ Answer = help },
+		{ Command = help },
 		io__write_strings([
 			"According to the intended interpretation",
 			" of the program, answer one of:\n",
 			"\ty\tyes\n",
 			"\tn\tno\n",
+			"\td\tdon't know\n",
 %			"\tb\tbrowse the atom arguments (not yet)\n",
 %			"\tt\tprint the evaluation tree (not yet)\n",
 			"\th, ?\tthis help message\n"
 		]),
-		query_oracle(Node, Valid, Oracle0, Oracle)
+		query_user(Node, MaybeTruth)
 	;
-		{ Answer = illegal_command },
+		{ Command = illegal_command },
 		io__write_string("Unknown command, 'h' for help.\n"),
-		query_oracle(Node, Valid, Oracle0, Oracle)
+		query_user(Node, MaybeTruth)
 	).
 
 
-:- pred query_user(edt_node, debugger_command, io__state, io__state).
-:- mode query_user(in, out, di, uo) is det.
-
-query_user(Node, Answer) -->
-	write_node(Node),
-	io__nl,
-	get_command("Valid? ", Answer).
-
-
 :- pred get_command(string, debugger_command, io__state, io__state).
 :- mode get_command(in, out, di, uo) is det.
 
@@ -134,6 +276,7 @@
 
 command_chars(['y' | _], yes).
 command_chars(['n' | _], no).
+command_chars(['d' | _], do_not_know).
 command_chars(['b' | _], browse).
 command_chars(['t' | _], tree).
 command_chars(['h' | _], help).
Index: tests/debugger/declarative/Mmakefile
===================================================================
RCS file: /home/mercury1/repository/tests/debugger/declarative/Mmakefile,v
retrieving revision 1.4
diff -u -r1.4 Mmakefile
--- Mmakefile	1999/07/23 16:31:43	1.4
+++ Mmakefile	1999/08/08 04:49:51
@@ -27,6 +27,7 @@
 SMALL_DECLARATIVE_PROGS= 	\
 	gcf			\
 	if_then_else		\
+	oracle_db		\
 	propositional
 
 MCFLAGS = --trace deep --trace-decl
@@ -72,6 +73,9 @@
 
 if_then_else.out: if_then_else if_then_else.inp
 	$(MDB) ./if_then_else < if_then_else.inp > if_then_else.out 2>&1
+
+oracle_db.out: oracle_db oracle_db.inp
+	$(MDB) ./oracle_db < oracle_db.inp > oracle_db.out 2>&1
 
 queens.out: queens queens.inp
 	$(MDB) ./queens < queens.inp > queens.out 2>&1


New File: tests/debugger/declarative/oracle_db.m

:- module oracle_db.
:- interface.
:- import_module io.
:- pred main(io__state::di, io__state::uo) is det.
:- implementation.

main -->
	(
		{ a(99, 99, 99) }
	->
		io__write_string("yes.\n")
	;
		io__write_string("no.\n")
	).

:- pred a(int, int, int).
:- mode a(in, in, in) is semidet.

a(X, Y, Z) :-
	b(X),
	b(Y),
	b(Z).

:- pred b(int).
:- mode b(in) is semidet.

b(99).


New File: tests/debugger/declarative/oracle_db.inp

echo on
goto 9
dd_wrong
n
y
continue -a


New File: tests/debugger/declarative/oracle_db.exp

       1:      1  1 CALL pred oracle_db:main/2-0 (det) 
mdb> echo on
Command echo enabled.
mdb> goto 9
       9:      2  2 EXIT pred oracle_db:a/3-0 (semidet) 
mdb> dd_wrong
a(99, 99, 99)
Valid? n
b(99)
Valid? y
Incorrect instance found:

a(99, 99, 99) :-
	b(99),
	b(99),
	b(99).

       9:      2  2 EXIT pred oracle_db:a/3-0 (semidet) 
mdb> continue -a
      10:      1  1 THEN pred oracle_db:main/2-0 (det) t;
yes.
      11:      1  1 EXIT pred oracle_db:main/2-0 (det) 

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