2. checkstat
2.1 NAME
checkstat - checks SPASS behavior on problem files
2.2 SYNOPSIS
checkstat [-cdFiklmopPrstTuvVwx] dir_1/file_1 ... dir_n/file_n
2.3 DESCRIPTION
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):
-
A problem state is declared satisfiable
(unsatisfiable), and SPASS computes unsatisfiable (satisfiable).
-
SPASS returns an invalid proof (only if proof checking is enabled).
-
The SPASS completion and the reference completion differ
(if completion checking is enabled, and a reference file is present).
-
SPASS reports that not all memory has been cleaned up.
-
SPASS memory use reporting is inconsistent: Either SPASS gives memory use information for the current file, but has not given it for the previous files, or vice versa, gives no memory information
for the current file, but has done this for previous files.
-
The problem state could not be extracted from the
problem file.
-
No problem state could be extracted from
the SPASS output, for example due to a segmentation fault.
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:
-
SPASS runs out of time or out of memory.
-
SPASS decides a problem whose state is declared 'unknown'.
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.
2.4 OPTIONS
The following options are supported by checkstat:
- -v
- Verbose mode. Prints information on the currently checked directory, file, and uncritical events. Default is 'off'.
- -V
- 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.
- -c
- Specify time limit for proof checker pcs.
- -l
- 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.
- -u
- Check SPASS proofs for correctness ('u' for 'unsatisfiable').
- -s
- 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).
- -r
- Run. Continue after errors.
- -w
- Print warning if model checking is enabled, a model has been found,
but the reference does not exist.
- -P
- 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.
- -d
- Debug. Lots of output about intermediate results etc.
- -k
- Keep. Keep generated temporary files.
- -o
- Use SPASS instead of OTTER for proof checking.
- -x
- Extension. Process all file parameters, regardless of
extension. Normally, files with unknown extensions are ignored.
- -i
- Interactive. Reads file names from standard input.
- -m
- Mode. Print out command line.
2.5 EXAMPLES
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
2.6 AUTHORS
Thorsten Engel
Christian Theobalt
Contact : Christoph Weidenbach <weidenb@mpi-sb.mpg.de>
2.7 SEE ALSO
filestat(1), pcs(1), pgen(1), rescmp(1), tpform(1), tpget(1), deprose(1), dfg2otter(1), dfg2otterpl(1), SPASS(1)
This document was generated
by Renate Schmidt on March, 10 2003
using texi2html