DWASP

A modified version of the ASP solver WASP that enables debugging of ASP programs. DWASP takes an faulty logic program together with an test case as input, and asks the user questions about an expected answer set of the program. It then points the user to a set of faulty rules.

Table of contents

• Building
• Usage

Building

In order to compile DWASP boost (http://www.boost.org/) and g++-4.6 (or more recent) are required.

If all libraries have been installed, use

make

to build DWASP.

Other compiling options are also available:

• make BUILD=stats enables the usage of statistics.
• make BUILD=trace enables the possibility to trace the internal behavior of WASP.
• make BUILD=debug compiles WASP for debugging.

Usage

In order to debug a faulty ASP program with DWASP, a test case is required. Such a test case consists of facts, i.e. the input of the ASP program, as well as assertions that specify the expected (partial) answer set. Each assertion is a constraint

:- not a.

if a is expected to be inside the answer set, or a constraint

:- a.

if a is not expected to occur inside the answer set.

In order to start a debugging session, the program and the test case first need to be grounded using the debugging grounder gringo-wrapper:

gringo-wrapper program.lp testcase.in > grounded.dbg

After grounding the program, start DWASP with the the --debug option and specify the debug file generated by gringo-wrapper:

wasp --debug=grounded.dbg

Example debugging session

Consider the following program graph-coloring.lp to color a graph with the three colors blue, red, and yellow:

% Compute nodes from arcs
node(X) :- arc(X, _).
node(X) :- arc(_, X).
% Assign a color to each node
col(X, blue) | col(X, red) | col(X, yellow) :- node(X).
% Different colors for adjacent nodes
:- col(X, C1), col(Y, C2), arc(X, Y).

We create the test-case graph-coloring.in, that specifies a simple graph as input for our program:

% (1) -- (2) -- (3)
arc(1, 2).
arc(2, 3).

If we ground our program together with the test case and start DWASP without the --debug option

gringo graph-coloring.lp graph-coloring.in | wasp

the solver tells us the program is incoherent. In order to find the faulty rule(s), we start DWASP in the debugging mode:

gringo graph-coloring.lp graph-coloring.in > graph-coloring.dbg
wasp --debug=graph-coloring.dbg

DWASP informs us that it is computing the set of rules that cause the incoherence (called unsatisfiable core) and then prompts us to enter a command.

WASP debbuging mode
Computing the unsatisfiable core
WDB>

To view the current unsatisfiable core (i.e. the rules causing the conflict), we use the show core nonground command:

WDB> show core nonground
:- col(X, C1), col(Y, C2), arc(X, Y).
    { C1/red, C2/red, X/1, Y/2 }
    { C1/yellow, C2/red, X/1, Y/2 }
    { C1/blue, C2/red, X/1, Y/2 }
    { C1/red, C2/yellow, X/1, Y/2 }
    { C1/yellow, C2/yellow, X/1, Y/2 }
    { C1/blue, C2/yellow, X/1, Y/2 }
    { C1/red, C2/blue, X/1, Y/2 }
    { C1/yellow, C2/blue, X/1, Y/2 }
    { C1/blue, C2/blue, X/1, Y/2 }
col(X, blue) | col(X, red) | col(X, yellow) :- node(X).
    { X/1 }
    { X/2 }
node(X) :- arc(X, _).
    { X/1 }
    { X/2 }

There are many ground rules inside the core. In order to narrow down the rules causing the conflict, we use the ask command to instruct DWASP to compute a query for us:

WDB> ask
Computing the query
Should 'col(2,blue)' be in the model? (y/n/u):

Since node 2 can be colored with blue, we answer the query with y. We type ask once more and DWASP prompts us the following query:

WDB> ask
Computing the query
Should 'col(1,red)' be in the model? (y/n/u):

Since node 1 can be colored with blue, we again answer the query with y and print the current unsatisfiable core:

WDB> show core nonground
:- col(X, C1), col(Y, C2), arc(X, Y).
    { C1/red, C2/blue, X/1, Y/2 }

The diagnosis now consists of only one rule that is faulty because the check C1 = C2 is missing.