SPOCK - Finding errors by means of logic


SPOCK is a tool implementing a collection of methods for debugging answer set programs. In particular it features a series of program transformations of normal logic programs as described in [1] and [2]. Additionally a set of handy functions are provided, including the extraction of predicate names, and the usage of dlv, lparse and smodels as external programs.


Note: The tool is written in Java 5.0 and published under the GNU General Public License (GPL).

Download SPOCK from SourceForge.


* ... required as external program for some features of SPOCK

When using one of the external programs, make sure that the PATH variable of your command shell includes the location of the respective application.


The input of SPOCK is a logic program read from the system standard input and/or from (multiple) files. The output varies according to the selected function which is determined by the options set.

The syntax of accepted logic programs allows some special elements from the core languages of the two ASP-solvers dlv and smodels such as disjunctive rules, choice rules and nested expressions of form not not a. The most important syntax-extension of logic programs however is the labelling of rules, allowing debugging mechanisms to explicitly refer to rules. For that the respective rule string is preceeded by its label and a colon.

e.g. a rule labelled by r1 is denoted by:

r1: h :- pb, not nb.

Generally SPOCK is invoked by the following command scheme:

java -jar spock.jar [OPTION]* [FILENAME]*

A list of available option flags can be obtained by the following call:

java -jar spock.jar -help

Invoking ASP-solvers

SPOCK may be used to invoke external ASP solvers (dlv and smodels). This can be useful for mainly two reasons:

The following command runs dlv on the logic program in file FILENAME and outputs its answer sets (dlv has to be in PATH):

java -jar spock.jar -x -o FILENAME

The same result can be achieved using smodels (lparse and smodels have to be in PATH):

java -jar spock.jar -xsm -o FILENAME

Using flag -as instead of -o, Answer sets can be displayed in a graphical dialog providing a good overview for their analysis:

java -jar spock.jar -xsm -as FILENAME


Solver specific limitations will not be compensated in general. Thus disjunctive rules will only be accepted using dlv and programs must be sufficiently domain restricted for use with smodels. Choice rules will be simulated by disjunction with additional auxilary head atoms when used with dlv.

Transformation in [1]

The meta-program D of disjunctive program P is computed by the following call of SPOCK:

java -jar spock.jar -mtr -mpr FILENAME

where FILENAME is the name of a textfile containing P.
The option
-mtr initialises the transformation of P to the input part of D, consisting of meta-atoms
that express which atoms occur in the head, the positive, and the negative body of a rule in P,
whereas option
-mpr outputs the residual meta-program.

Transformations in [2]

The kernel translation T of normal program P can be obtained using the command:

java -jar spock.jar -k FILENAME

The same effect can be achieved using standard input:

java -jar spock.jar -k < FILENAME

For extrapolation of non-existing answer sets, SPOCK provides the following flags for program translations:

-expo :
-exco :
-exlo :
-ex :

-exrules:r1,r2,r3,... :

-sm :

program-oriented extrapolation tagging
completion-oriented extrapolation tagging
loop-oriented extrapolation tagging
all extrapolation tagging (like -expo -exco -exlo)

restrict extrapolation tagging generation to rules with labels r1, r2, r3,...

use smodels-Syntax - needed since the extrapolation approach uses choice rules

Example calls:

The following call returns the kernel-tagging of file test3 and extrapolation tagging (program-,completion-,loop-oriented) for rules r1 and r2:

java -jar spock.jar -k -ex -exrules:r1,r2 -sm test3

The following call returns the kernel-tagging of file
test2 and program- and completion-oriented extrapolation tagging for rule 1:

java -jar spock.jar -k -expo -exco -exrules:1 -sm test2

Using pipes answer sets of the resulting program can be calculated by calling an external ASP-solver:

java -jar spock.jar -k -expo -exco -exrules:1 -sm test2 | java -jar spock.jar -o -xsm



A Meta-Programming Technique for Debugging Answer-Set Programs. Martin Gebser, Jörg Pührer, Torsten Schaub, and Hans Tompits. To appear in Proc. AAAI'08.ps | .pdf ]


Debugging ASP Programs by Means of ASP. Martin Brain, Martin Gebser, Jörg Pührer, Torsten Schaub, Hans Tompits, and Stefan Woltran. In Chitta Baral, Gerhard Brewka, and John Schlipf, editors, Proceedings of the 9th International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR'07), Tempe, AZ, USA, volume 4483 of Lecture Notes in Artificial Intelligence, pages 31–43. Springer, 2007. [ bib | .ps | .pdf ]


That is Illogical Captain!” – The Debugging Support Tool spock for Answer-Set Programs: System Description. Martin Brain, Martin Gebser, Jörg Pührer, Torsten Schaub, Hans Tompits, and Stefan Woltran. In Marina De Vos and Torsten Schaub, editors, Proceedings of the 1st International Workshop on Software Engineering for Answer-Set Programming (SEA'07), Tempe, AZ, USA, pages 71–85, 2007. [ bib | .ps | .pdf ]


spock: A Debugging Support Tool for Logic Programs under the Answer-Set Semantics. Martin Gebser, Jörg Pührer, Torsten Schaub, Hans Tompits, and Stefan Woltran. In Dietmar Seipel, Michael Hanus, Armin Wolf, and Joachim Baumeister, editors, Proceedings of the 21st Workshop on (Constraint) Logic Programming, (WLP'07), Würzburg, Germany, pages 258–261. Technical Report 434, Bayerische Julius-Maximilians-Universität Würzburg, Institut für Informatik, 2007. [ bib | .ps | .pdf ]


e-mail Jörg Pührer, puehrer@kr.tuwien.ac.at