[ < ] [ > ]   [ << ] [ Up ] [ >> ]         [Top] [Contents] [Index] [ ? ]

2. checkstat

[ < ] [ > ]   [ << ] [ Up ] [ >> ]         [Top] [Contents] [Index] [ ? ]

2.1 NAME

checkstat - checks SPASS behavior on problem files

[ < ] [ > ]   [ << ] [ Up ] [ >> ]         [Top] [Contents] [Index] [ ? ]


checkstat [-cdFiklmopPrstTuvVwx] dir_1/file_1 ... dir_n/file_n
[ < ] [ > ]   [ << ] [ Up ] [ >> ]         [Top] [Contents] [Index] [ ? ]


The checkstat script is intended for automatically checking the declared state of a theorem proving problem, specified in DFG syntax, against the state computed by the SPASS theorem prover. The script is written in Perl.

For using the proof and model checking facilities, the pcs and rescmp programs must exist in the same directory as checkstat, or the corresponding environment variables PCS and RESCMP must be set to their paths.

checkstat examines the set of files that is given by all specified files and all files in the specified directories that have a '.cnf', '.frm', or '.dfg' extension. checkstat evokes SPASS on each file and compares its result with the problem state specified in the 'status' field of the DFG problem description. Optionally (see below), SPASS proofs can be verified by a proof checker, and SPASS completions can be checked against reference completions. If SPASS outputs memory check information in the format produced by the 'CHECK' compile time variable, then checkstat verifies that all memory has been cleaned up at the end of the SPASS run.

checkstat continues as long as no critical events occur, which are (besides standard system errors, e.g. in file access):

These errors are reported, and checkstat stops. All other possible events are classified as uncritical. They are fully reported in the moment of their occurrence only if the -v option has been activated. Their occurrence is always mentioned in a final event statistic, but not with the associated problem files. Uncritical events are:

If a file 'filename.dfg' is in the set of specified files, and there exists corresponding corresponding '.cnf' file 'filename.cnf' in the same directory, then this file is passed to SPASS, even if it is not a parameter to checkstat. I.e.,
checkstat test.dfg
passes the file 'test.cnf' to SPASS if it exists in the current working directory.

[ < ] [ > ]   [ << ] [ Up ] [ >> ]         [Top] [Contents] [Index] [ ? ]


The following options are supported by checkstat:

Verbose mode. Prints information on the currently checked directory, file, and uncritical events. Default is 'off'.
Very verbose mode. Enables verbose mode, and prints output of proof checker pcs.
-p prover
Specify prover. Can be used for setting SPASS options, see examples below. Default is value of the environment variable 'SPASS'.
-t limit
Specify a time limit for SPASS (in seconds). Default is 10 seconds.
Specify time limit for proof checker pcs.
Log SPASS result for each file 'filename.cnf' in 'filename.log'. Default is 'off'. This option is to be used with care, as a Perl variable with the same size as the SPASS output is created in the memory.
Check SPASS proofs for correctness ('u' for 'unsatisfiable').
Check SPASS completions against reference completions. The reference completion corresponding to a problem file filename .ext', where ext is some DFG file extension, is 'filename.mod' and must be located in the same directory as the problem file. ('s' is for 'satisfiable).
Run. Continue after errors.
Print warning if model checking is enabled, a model has been found, but the reference does not exist.
Specify SPASS options. Enclose in single quotes to protect from shell please.
-T limit
Enable timing by shell. Stops in time even if SPASS timing does not work.
-c limit
Specify time limit in seconds for proof checker. This is the time available for verifying one proof step in a proof.
Debug. Lots of output about intermediate results etc.
Keep. Keep generated temporary files.
Use SPASS instead of OTTER for proof checking.
Extension. Process all file parameters, regardless of extension. Normally, files with unknown extensions are ignored.
Interactive. Reads file names from standard input.
Mode. Print out command line.

[ < ] [ > ]   [ << ] [ Up ] [ >> ]         [Top] [Contents] [Index] [ ? ]


To check a single file with some extra SPASS options:
checkstat -p 'SPASS options' filename
To check all files with '.cnf' suffix in directory 'Test':
checkstat Test/*.cnf

[ < ] [ > ]   [ << ] [ Up ] [ >> ]         [Top] [Contents] [Index] [ ? ]


Thorsten Engel
Christian Theobalt
Contact : Christoph Weidenbach <weidenb@mpi-sb.mpg.de>

[ < ] [ > ]   [ << ] [ Up ] [ >> ]         [Top] [Contents] [Index] [ ? ]


filestat(1), pcs(1), pgen(1), rescmp(1), tpform(1), tpget(1), deprose(1), dfg2otter(1), dfg2otterpl(1), SPASS(1)

[ << ] [ >> ]           [Top] [Contents] [Index] [ ? ]

This document was generated by Renate Schmidt on March, 10 2003 using texi2html