[m-rev.] for review: allow search mode to be changed in DD

[Julien Fischer]

On Fri, 19 Aug 2005, Ian MacLarty wrote:

> For review by anyone.
>
> Estimated hours taken: 12
> Branches: main
>
> Allow the search mode to be changed from within the declarative debugger.
>
Hooray!

> Make binary search independent of subterm dependency tracking.  The
> user can now perform a binary search along the path between the current
> question and the root of the search space using the command `mode binary'
> (or `m b').
>
> browser/declarative_analyser.m:
> 	Make reask_last_question fail instead of throwing an exception
> 	if there is no last question.  If it fails we
> 	recompute the question.  This happens when the user
> 	resumes with a new search mode.
>
> 	Do not return an analyser response when showing info, since we can
> 	just call reask_last_question.
>
> 	Make set_fallback_search_mode set the last_search_question field to
> 	no.  This will force the question to be recomputed with the new
> 	search strategy when analysis continues.
>
> 	Add change_search_mode which handles the users request to change the
> 	current search mode from within a declarative debugging session.
>
> 	Do not perform a binary search after tracking a subterm unless
> 	instructed to do so by the user.
>
> browser/declarative_debugger.m:
> 	Allow search mode changes to be undone.
> 	Handle the new change_search oracle response.
> 	Handle the fact that reask_last_question is now semidet.
>
> browser/declarative_oracle.m:
> 	Add a change_search oracle response.
> 	Add a predicate to indicate which oracle responses are undoable.
>
> browser/declarative_user.m:
> 	Add a change_search user response.
>
> doc/user_guide.texi:
> 	Rephrase the description of the undo command to take into account that
> 	search mode changes can be undone.
> 	Add a section about the binary search mode.
> 	Rearrange some text and reword some sentences slightly.
>
> tests/debugger/mdb_command_test.inp:
> tests/debugger/declarative/Mmakefile:
> tests/debugger/declarative/binary_search.exp:
> tests/debugger/declarative/binary_search.exp2:
> tests/debugger/declarative/binary_search.inp:
> tests/debugger/declarative/binary_search.inp2:
> tests/debugger/declarative/change_search.exp:
> tests/debugger/declarative/change_search.inp:
> tests/debugger/declarative/change_search.m:
> tests/debugger/declarative/info.exp:
> tests/debugger/declarative/info.inp:
> 	Test the `mode' command and do not expect the declarative debugger to
> 	automatically go into binary search mode once it has tracked a subterm.
>
...

> Index: doc/user_guide.texi
> ===================================================================
> RCS file: /home/mercury1/repository/mercury/doc/user_guide.texi,v
> retrieving revision 1.449
> diff -u -r1.449 user_guide.texi
> --- doc/user_guide.texi	9 Aug 2005 07:14:00 -0000	1.449
> +++ doc/user_guide.texi	18 Aug 2005 09:11:09 -0000
> @@ -4135,9 +4135,13 @@
>  Skip this question and ask a different one if possible.
>  @sp 1
>  @item undo
> -Reset the state of the declarative debugger to what it was before the most
> -recent `yes', `no', `inadmissible', `trust', `skip' or `mark' answer that has
> -not already been undone.
> +Reset the state of the declarative debugger to the state it was in when
> +the question that came before the current question, and that hasn't already
> +been undone, was asked.

That's not an improvement.

> + at sp 1
> + at item mode [ top-down | divide-and-query | binary ]
> +Change the current search mode.  The search modes may be abbreviated to
> + at samp{td}, @samp{dq} and @samp{b} respectively.
>  @sp 1
>  @item browse [--xml] [@var{n}]
>  Start the interactive term browser and browse the @var{n}th argument
> @@ -4279,49 +4283,42 @@
>  @node Search Modes
>  @subsection Search Modes
>
> -Currently the declarative debugger can operate in one of two modes when
> -searching for a bug.  The mode to use can be specified as an option to the
> - at samp{dd} command.  See @ref{Declarative debugging mdb commands} for
> -information on how to do this.
> +The declarative debugger can operate in one of several modes when
> +searching for a bug.  The user can specify which mode to use by giving the

It may be worth mentioning that the mode of the dd affects what
questions are asked.

> + at samp{--search-mode} option to the @samp{dd} command (see
> + at ref{Declarative debugging mdb commands}) or with the @samp{mode} declarative
> +debugger command (see @ref{Declarative debugging commands}).
>
> - at subsubsection Top-down Search
> + at subsubsection Top-down Mode
>
>  Using this mode the declarative debugger will ask about the children of the
> -last atom whose assertion was false.  This makes the search more predictable
> +last question the user answered @samp{no} to.  The child calls will be asked
> +about in the order they were executed.  This makes the search more predictable
>  from the user's point of view as the questions will more or less follow the
>  program execution.  The drawback of top-down search is that it may require a
>  lot of questions to be answered before a bug is found, especially with deeply
> -recursive program runs.
> +recursive programs.
>
>  This search mode is used by default when no other mode is specified.
>
> - at subsubsection Divide and Query Search
> + at subsubsection Divide and Query Mode
>
> -With this search mode the declarative debugger will attempt to halve the size of
> -the search space with each question.  In many cases this will result in the
> +With this search mode the declarative debugger will attempt to halve the size

s/will attempt/attempts/


> +of the search space with each question.  In many cases this will result in the
>  bug being found after O(log(N)) questions where N is the number of events
>  between the event where the @samp{dd} command was given and the corresponding
> - at samp{CALL} event.  This makes the search feasible for deeply recursive runs
> + at samp{CALL} event.  This makes the search feasible for long running programs
>  where top-down search would require an unreasonably large number of questions
>  to be answered.  However, the questions may appear to come from unrelated parts
>  of the program which can make them harder to answer.
>
> - at subsubsection When different search modes are used
> -
> -If a search mode is given when invoking the declarative debugger then that
> -search mode will be used, unless (a) a subterm is marked during the session,
> -in which case the subterm is tracked to its origin, or (b) the user
> -hasn't answered @samp{no} to any questions yet,
> -in which case top-down search is used until @samp{no} is answered to at least
> -one question.
> + at subsubsection Binary Search Mode
>
> -If you do not specify a search mode when giving the @samp{dd} command then the
> -behaviour depends on wether the @samp{--resume} option is present.  If it is
> -then the previous search mode will be used, otherwise top-down search will
> -be used.
> -
> -You can check the search mode used to find a particular question by issuing
> -an @samp{info} command at the question prompt in the declarative debugger.
> +The user may ask the declarative debugger to do a binary search along the
> +path in the call tree between the current question and the question that the
> +user last answered @samp{no} to.  This is useful, for example, when a
> +recursive predicate is producing incorrect output, but the base case is
> +correct.
>
>  @node Improving the search
>  @subsection Improving the search
> @@ -4445,6 +4442,23 @@
>  predicates and functions in the same module as the predicate or function in the
>  current question.  See the @samp{trust} command in
>  @ref{Declarative debugging commands}.
> +
> + at subsubsection When different search modes are used
> +
> +If a search mode is given when invoking the declarative debugger then that
> +search mode will be used, unless (a) a subterm is marked during the session,
> +in which case the subterm is tracked to its origin, or (b) the user
> +hasn't answered @samp{no} to any questions yet,

s/hasn't/has not/

> +in which case top-down search is used until @samp{no} is answered to at least
> +one question.
> +

> +If you do not specify a search mode when giving the @samp{dd} command then the
> +behaviour depends on wether the @samp{--resume} option is present.  If it is

s/wether/whether/

I suggest:

	If no search mode is specified with the @samp{dd} command then
	the search mode depends on if the @samp{--resume} option is
	given.

> +then the previous search mode will be used, otherwise top-down search will
> +be used.
> +
> +You can check the search mode used to find a particular question by issuing
> +an @samp{info} command at the question prompt in the declarative debugger.
>

Other than your change to the user guide section about the undo command,
the rest of that looks fine.

Julien.

--------------------------------------------------------------------------
mercury-reviews mailing list
post:  mercury-reviews at cs.mu.oz.au
administrative address: owner-mercury-reviews at cs.mu.oz.au
unsubscribe: Address: mercury-reviews-request at cs.mu.oz.au Message: unsubscribe
subscribe:   Address: mercury-reviews-request at cs.mu.oz.au Message: subscribe
--------------------------------------------------------------------------