Answer Set Programming is a well-known declarative programming paradigm proposed in the area of logic programming and non-monotonic reasoning. Although ASP features a simple syntax and an intuitive semantics, errors are common during the development of ASP programs. In this paper we propose a novel debugging approach based on paracoherent reasoning, which allows a user to identify bugs when they are related to wrong constraints. The approach has been implemented in a tool called paradebug, that is made freely available.
Answer Set Programming (ASP) [
Albeit the basic syntax and the semantics of ASP are in general clear also
for novice programmers, during the development of ASP encodings, the
identication of (trivial) errors can be time consuming. For this reason, during the
recent years, several techniques and tools, called debuggers, emerged to help the
programmer to deal with faults in ASP programs [
In this paper we provide a practical contribution in the aforementioned
context by considering an important question related to debug, i.e. why an
interpretation is not an answer set of a program under consideration. In particular,
we report on a preliminary debugging technique based on paracoherent
reasoning [
Answer set programming Syntax. An ASP program P is a nite set of rules of the form h1 _ : : : _ hn `1; : : : ; `m where n; m 0, n + m 6= 0, h1; : : : ; hn are atoms and represent the head of the rule, while `1; : : : ; `m are literals and represent the body of the rule. In particular, an atom is an expression of the form p(t1; : : : ; tk), where p is a predicate of ariety k and t1; : : : ; tk are terms. Terms are alphanumeric strings, and are distinguished in variables and constants. According to the Prolog's convention, only variables start with an uppercase letter. A literal is an atom a or its negation not a, where not denotes the negation as failure. For an atom p, p = not p, for a negated atom not p, not p = p. A rule is called a constraint if n = 0, and a fact if n = 1 and m = 0. An object (atom, rule, etc.) is called ground or propositional, if it contains no variables. Given a program P, let the Herbrand Universe UP be the set of all constants appearing in P and the Herbrand Base BP be the set of all possible ground atoms which can be constructed from the predicate symbols appearing in P with the constants of UP . Given a rule r, Ground (r) denotes the set of rules obtained by applying all possible substitutions from the variables in r to elements of UP . Similarly, given a program P, its ground instantiation is the set Sr2P Ground (r). Given a ground program , let Rules( ), Constr ( ), and At ( ) denote the set of ground rules, ground constraints and ground atoms occurring in .
Semantics. Given a program P, its stable models are de ned using its ground instantiation . Any set I At( ) is an interpretation for a program . A ground atom p is true w.r.t. I if p 2 I; p is false w.r.t. I if p 62 I. A ground literal not p is true w.r.t. I if p 62 I; not p is false w.r.t. I if p 2 I. An interpretation I is a model for if, for every r 2 , at least one atom in the head of r is true w.r.t. I whenever all literals in the body of r are true w.r.t. I. The reduct of a ground program w.r.t. a model I is the program I , obtained from by (i) deleting all rules r 2 whose negative body is false w.r.t. I and (ii) deleting the negative body from the remaining rules. An interpretation I is an answer set (stable model ) of a program if I is a model of , and there is no J I such that J is a model of I . Let AS ( ) denote the set of all answer sets of . A program is coherent if AS ( ) 6= ;, incoherent otherwise.
Example 1. Consider the following program P: node(X) edge(X; Y ) node(X) edge(Y; X) col(X; blue) _ col(X; red) _ col(X; green) node(X)
col(X; C1); col(Y; C2); edge(X; Y ); C1 6= C2 and the set of facts F : the ground instantiation of P [ F is the program the following set of rules Rules( ): comprising and A = fedge(1; 2); edge(2; 3); node(1); node(2); node(3)g. where n 1; m k 0, and a1; : : : ; an; b1; : : : ; bm are ground atoms. Note that does not include constraints (since n 1).
Externally supported program. The externally supported program is a ground program s obtained as follows. For each rule r 2 of the form (1), s contains the rule: and for each atom p 2 At ( ), s contains the rules Kp _nKp and gap(Kp) Kp; not p, where Kp, nKp and gap(Kp) are atoms not appearing in . Intuitively, an atom Kp can be read as p is believed to hold.
Externally extended supported program. The externally extended supported program of is the program es formed by s and by rule:
Ka1 _ _ Kan _ Kbk+1 _ _ Kbm
Kb1 ; not a1; ; not an; not bk+1;
; Kbk ;
Paracoherent answer sets. For a set of atoms S, let GS denote fgap(p) j gap(p) 2 Sg. For a program , I 2 AS ( es ) is an externally supported model (resp. externally extended supported model ) of if there is no M 2 AS ( s ) (resp. M 2 AS ( es )) such that GM GI . In the following, we refer to externally supported models and externally extended supported models as paracoherent answer sets. 3
In this section, we present our approach to the localization of faults in ground ASP programs. In general, one can di erentiate between syntactic and semantic faults. In the rst case, syntactic errors are automatically detected by parser of ASP systems, whereas semantic faults can be detected by a user by analyzing the output of the ASP system.
In the latter case, users usually verify the correctness of programs by checking (simple) test instances, as it is common for software development. In particular, the debugging process is carried out by comparing a number of answer sets computed by an ASP system with solutions determined by hand. Therefore, in order to detect a bug, a user must know at least one answer set of the program for the analyzed instance.
De nition 1 (Buggy program). Let c be a ground intended (correct) program that a user is going to formulate and AS( c) be a set of its known answer sets. Then, a ground program is said to be buggy with respect to a program c if there exists an answer set A 2 AS( c) such that A 62 AS( ). Note that by this de nition our approach deals only with situations in which some answer set of the correct program is missing. The opposite problem { there is an answer set A 2 AS( ) such that A 62 AS( c) { is not the focus of this paper.
Example 2 (Buggy program). Consider the program P of Example 1, representing a (buggy) encoding for the graph coloring problem. During the development of the encoding the user might create a simple graph, e.g. considering the sample instance of the two facts in F . For this instance the user expects the assignment of the blue color to the nodes 1 and 3 as well as of the red color to the node 2 to be among the solutions. However, the corresponding answer set encoding this solution is missing due to a bug in the encoding. In particular, note that the condition C1 6= C2 should be replaced by C1 = C2. C
The situation in which some solution is missing can be detected by means of testing, which is a common approach in software engineering aiming at identi cation and localization of faults in programs.
De nition 2 (Test case). Let c be a ground intended program, and be a ground program. A set of atoms T At ( ) is a test case for i there exists an answer set A 2 AS( c) such that T A.
De nition 3 (Test case failure). Given a ground program and a test case T , let T = f l j l 2 T g, we say that T fails if [ T is incoherent.
Assertions of a test case are modeled by constraints that force the asserted atoms to be in all answer sets. As a result, checking whether a test case T of a program passes or not is reduced to checking whether [ T is coherent, as illustrated in Example 3.
Example 3 (Failing Test Case). Consider the program the test case from Example 1 and
T = fcol(1; blue); col(2; red); col(3; blue)g:
not col(1; blue) not col(2; red) not col(3; blue):
[
Whenever a test case fails, i.e. the given program is buggy, the goal of a debugger is to nd an explanation for this observation.
In the following, we assume that given a ground program and a test case T , the set Rules( ) [ T is coherent and correct, and the buggy rule is located in Constr ( ). Indeed, the goal of our debugger is to nd a set of constraints that are causing the incoherence.
De nition 4 (Diagnosis). Given a ground program and a failing test case T , a diagnosis D of the fault is a minimal set of constraints C Constr ( ) such that ( [ T ) n C is coherent.
Example 4 (Diagnosis). Consider again the program from Example 1 and the program T of Example 3. A diagnosis of the fault D is the set of constraints f col(2; red); col(1; blue); col(3; blue); col(2; red)g. Indeed, ( [ T ) n D is coherent and no subset of D is a diagnosis. C C
In our approach, fault identi cation is done by taking advantages of paracoherent semantics to nd buggy constraints. The key idea is as follows. Given a ground program and the set of constraints Constr ( ), each constraint c 2 Constr ( ) of the form l1; : : : ; lm is normalized, i.e. it is rewritten as the following rule: auxc
not auxc; l1; : : : ; lm where auxc is a fresh symbol not appearing elsewhere in the program. De nition 5 (Normalization). Given a ground program = Rule( ) [ Constr ( ), then the normalized program of , denoted Norm( ), is composed by fauxc not auxc; `1; : : : ; `m j `1; : : : ; `m 2 Constr ( )g.
Example 5 (Normalization). Let be the ground program of Example 1. Then, Norm( ) comprises the following set of rules: aux c1 aux c2 aux c3 aux c4 aux c5 aux c6 aux c7 aux c8 aux c9 aux c10 aux c11 aux c12 not aux c1 ; col(2; red); col(1; green) not aux c2 ; col(2; red); col(1; blue) not aux c3 ; col(2; green); col(1; red) not aux c4 ; col(2; green); col(1; blue) not aux c5 ; col(2; blue); col(1; red) not aux c6 ; col(2; blue); col(1; green) not aux c7 ; col(3; red); col(2; green) not aux c8 ; col(3; red); col(2; blue) not aux c9 ; col(3; green); col(2; red) not aux c10 ; col(3; green); col(2; blue) not aux c11 ; col(3; blue); col(2; red) not aux c12 ; col(3; blue); col(2; green) Note that the number of symbols added in Norm( ) is bounded by the number of constraints in . C
Then, paracoherent rewriting techniques described in Section 2.2 are applied to the rules introduced in the normalization step.
De nition 6 (Debugging program). Let = Rules( ) [ Constr ( ) be a ground program and a test case T . The debugging program D is the program T [ Rules( ) [ Norm( ) , where 2 fs; esg.
Given a debugging program D, its paracoherent answer sets can be used
to build a diagnosis of the fault. Indeed, atoms of the form auxc are included in
a paracoherent answer set, say A, if and only if the corresponding constraint c
cannot be satis ed by any answer set. Therefore, all the constraints associated
to atoms of the form auxc that are true w.r.t. A are part of the diagnosis. Note
that, as shown in [
In this section, we describe a practical implementation of the debugging technique for the computation of a diagnosis described in Section 3. The resulting tool, namely paradebug, is freely available here: https://www.mat.unical. it/~dodaro/paradebug. Moreover, we also present a usage example of paradebug to debug a program.
paradebug is implemented in Python and it takes advantage of the ASP
system dlv2 [
paradebug takes as input a ground program and a test case T . Then, is normalized and the debugging program D is built starting from and T . Subsequently, D is provided as input to the internal solver wasp, which returns as output a paracoherent answer set of D, say M . M is then processed by paradebug and the set of constraints representing the diagnosis are returned. Usage example. Consider the following buggy ASP program representing an encoding of the Graph Coloring problem: node(X) :- edge(X,_). node(X) :- edge(_,X). col(X,blue) | col(X,red) | col(X,green) :- node(X). :- col(X1,C1), col(X2,C2), edge(X1,X2), C1 != C2. edge(1,2).
edge(2,3).
Note that it represents the program P of Example 1. In this case, the buggy rule is
:- col(X1,C1), col(X2,C2), edge(X1,X2), C1 != C2. since the condition C1 != C2 should be C1 = C2.
Test cases can be speci ed according to the directives assertTrue, that speci es atoms that must be in an answer set, and assertFalse, that speci es atoms that must not be in an answer set. In particular, a test case can be the following: assertTrue: col(1,blue). assertTrue: col(2,red).
assertTrue: col(3,blue). which basically represent a scenario where the atoms col(1,blue), col(2,red), and col(3,blue) are all true. However, this answer set cannot be obtained due to the buggy rule. paradebug can thus be used to nd what is the buggy rule by using the following command:
dlv2 --mode=idlv test.asp | ./paradebug.py testcase The output of paradebug is the set of buggy constraints as follows: Set of constraints causing the incoherence: :- col(1,blue), col(2,red).
:- col(2,red), col(3,blue). which indeed represents a correct diagnosis as shown in Example 4. 5
There are multiple approaches to ASP debugging suggested in the literature
including algorithmic [
Concerning meta-programming debuggers, they are usually based on a
general ASP encoding modeling all possible reasons of why some interpretation
of the faulty program is not an answer set. Among the tool based on
metaprogramming, two tools emerged, namely spock [
Our approach is also related to the one implemented in the debugging tool dwasp, that is also built on top of the ASP solver wasp. The approach of dwasp relies on iterative calls to the wasp and on the computation of the socalled unsatis able cores. Our approach is instead based on only one call to the underlying ASP system. Moreover, dwasp features a query-based approach to help the user to identify the buggy rules. Such a feature is not yet implemented in paradebug, but it can be integrated as well. 6
In this paper we presented a debugging approach for ASP programs based on
paracoherent reasoning. This technique has been implemented in a tool called
paradebug, based on the ASP system dlv2. As future work, we plan to extend
the technique presented in this paper to normal and disjunctive rules that are
not supported at the moment. Moreover, we plan to implement the query-based
approach presented in [