SPOCK - Finding errors by means of logic

Abstract

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.

Installation

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

Download SPOCK from SourceForge.

Requirements:

• Java SE 5.0

• DLV (http://www.dlvsystem.com) *

• lparse (http://www.tcs.hut.fi/Software/smodels) *

• smodels (http://www.tcs.hut.fi/Software/smodels) *

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

Description

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:

• labelled program rules are accepted

• resulting answer sets appear alphabetically sorted

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

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:

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

References:

e-mail Jörg Pührer, [email protected]