1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
|
<!DOCTYPE html PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html401/loose.dtd">
<html>
<!-- Created on February, 23 2010 by texi2html 1.78 -->
<!--
Written by: Lionel Cons <Lionel.Cons@cern.ch> (original author)
Karl Berry <karl@freefriends.org>
Olaf Bachmann <obachman@mathematik.uni-kl.de>
and many others.
Maintained by: Many creative people.
Send bugs and suggestions to <texi2html-bug@nongnu.org>
-->
<head>
<title>frequently asked questions about SPASS: 2. checkstat</title>
<meta name="description" content="frequently asked questions about SPASS: 2. checkstat">
<meta name="keywords" content="frequently asked questions about SPASS: 2. checkstat">
<meta name="resource-type" content="document">
<meta name="distribution" content="global">
<meta name="Generator" content="texi2html 1.78">
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
<style type="text/css">
<!--
a.summary-letter {text-decoration: none}
pre.display {font-family: serif}
pre.format {font-family: serif}
pre.menu-comment {font-family: serif}
pre.menu-preformatted {font-family: serif}
pre.smalldisplay {font-family: serif; font-size: smaller}
pre.smallexample {font-size: smaller}
pre.smallformat {font-family: serif; font-size: smaller}
pre.smalllisp {font-size: smaller}
span.roman {font-family:serif; font-weight:normal;}
span.sansserif {font-family:sans-serif; font-weight:normal;}
ul.toc {list-style: none}
-->
</style>
</head>
<body lang="en" bgcolor="#FFFFFF" text="#000000" link="#0000FF" vlink="#800080" alink="#FF0000">
<table cellpadding="1" cellspacing="1" border="0">
<tr><td valign="middle" align="left">[<a href="script_1.html#SEC1" title="Beginning of this chapter or previous chapter"> << </a>]</td>
<td valign="middle" align="left">[<a href="script_3.html#SEC18" title="Next chapter"> >> </a>]</td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left">[<a href="script.html#Top" title="Cover (top) of document">Top</a>]</td>
<td valign="middle" align="left">[Contents]</td>
<td valign="middle" align="left">[Index]</td>
<td valign="middle" align="left">[<a href="script_abt.html#SEC_About" title="About (help)"> ? </a>]</td>
</tr></table>
<hr size="2">
<a name="checkstat"></a>
<a name="SEC10"></a>
<h1 class="chapter"> 2. checkstat </h1>
<hr size="6">
<a name="SEC11"></a>
<h2 class="section"> 2.1 NAME </h2>
<p>checkstat - checks SPASS behavior on problem files
</p>
<hr size="6">
<a name="SEC12"></a>
<h2 class="section"> 2.2 SYNOPSIS </h2>
<p><strong>checkstat</strong> [‘<samp>-cdFiklmopPrstTuvVwx</samp>’] <var>dir_1/file_1</var> … <var>dir_n/file_n</var>
</p>
<hr size="6">
<a name="SEC13"></a>
<h2 class="section"> 2.3 DESCRIPTION </h2>
<p>The <strong>checkstat</strong> script is intended for automatically checking the declared
state of a theorem proving problem, specified in <strong>DFG</strong> syntax, against
the state computed by the <strong>SPASS</strong> theorem prover. The script is written
in <strong>Perl</strong>.
</p>
<p>For using the proof and model checking facilities, the <strong>pcs</strong> and
<strong>rescmp</strong> programs must exist in the same directory as <strong>checkstat</strong>, or the
corresponding environment variables <strong>PCS</strong> and <strong>RESCMP</strong> must be set
to their paths.
</p>
<p><strong>checkstat</strong> 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. <strong>checkstat</strong> evokes <strong>SPASS</strong> on each file and compares its
result with the problem state specified in the 'status' field of the
<strong>DFG</strong> problem description. Optionally (see below), <strong>SPASS</strong> proofs can be
verified by a proof checker, and <strong>SPASS</strong> completions can be checked
against reference completions. If <strong>SPASS</strong> outputs memory check
information in the format produced by the 'CHECK' compile time
variable, then <strong>checkstat</strong> verifies that all memory has been cleaned up at
the end of the <strong>SPASS</strong> run.
</p>
<p><strong>checkstat</strong> continues as long as no <i>critical</i> events
occur, which are (besides standard system errors, e.g. in file
access):
</p>
<ul>
<li>
A problem state is declared satisfiable
(unsatisfiable), and <strong>SPASS</strong> computes unsatisfiable (satisfiable).
</li><li>
<strong>SPASS</strong> returns an invalid proof (only if proof checking is enabled).
</li><li>
The <strong>SPASS</strong> completion and the reference completion differ
(if completion checking is enabled, and a reference file is present).
</li><li>
<strong>SPASS</strong> reports that not all memory has been cleaned up.
</li><li>
<strong>SPASS</strong> memory use reporting is inconsistent: Either <strong>SPASS</strong> 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.
</li><li>
The problem state could not be extracted from the
problem file.
</li><li>
No problem state could be extracted from
the <strong>SPASS</strong> output, for example due to a segmentation fault.
</li></ul>
<p>These errors are reported, and <strong>checkstat</strong> stops. All other possible events
are classified as <i>uncritical</i>. They are fully reported in the
moment of their occurrence only if the <strong>-v</strong> option has been
activated. Their occurrence is always mentioned in a final event
statistic, but not with the associated problem files. Uncritical
events are:
</p><ul>
<li>
<strong>SPASS</strong> runs out of time or out of memory.
</li><li>
<strong>SPASS</strong> decides a problem whose state is declared 'unknown'.
</li></ul>
<p>If a file '<i>filename</i>.dfg' is in the set of specified files, and
there exists corresponding corresponding '.cnf' file '<i>filename</i>.cnf' in the same directory,
then this file is passed to <strong>SPASS</strong>, even if it is not a parameter to
<strong>checkstat</strong>. I.e.,
</p><dl compact="compact">
<dd><p><strong>checkstat</strong> test.dfg
</p></dd>
</dl>
<p>passes the file 'test.cnf' to <strong>SPASS</strong> if it exists in the current
working directory.
</p>
<hr size="6">
<a name="SEC14"></a>
<h2 class="section"> 2.4 OPTIONS </h2>
<p>The following options are supported by <strong>checkstat</strong>:
</p>
<dl compact="compact">
<dt> <kbd>-v</kbd></dt>
<dd><p>Verbose mode. Prints information on the currently checked directory, file, and uncritical events. Default is 'off'.
</p></dd>
<dt> <kbd>-V</kbd></dt>
<dd><p>Very verbose mode. Enables verbose mode, and prints output of proof checker <strong>pcs</strong>.
</p></dd>
<dt> <kbd>-p <i>prover</i></kbd></dt>
<dd><p>Specify prover. Can be used for setting <strong>SPASS</strong> options, see examples below. Default is value of the environment variable 'SPASS'.
</p></dd>
<dt> <kbd>-t <i>limit</i></kbd></dt>
<dd><p>Specify a time limit for <strong>SPASS</strong> (in seconds). Default is 10 seconds.
</p></dd>
<dt> <kbd>-c</kbd></dt>
<dd><p>Specify time limit for proof checker <strong>pcs</strong>.
</p></dd>
<dt> <kbd>-l</kbd></dt>
<dd><p>Log <strong>SPASS</strong> result for each file '<i>filename</i>.cnf' in '<i>filename</i>.log'.
Default is 'off'. This option is to be used with care, as a <strong>Perl</strong>
variable with the same size as the <strong>SPASS</strong> output is created in the memory.
</p></dd>
<dt> <kbd>-u</kbd></dt>
<dd><p>Check <strong>SPASS</strong> proofs for correctness ('u' for 'unsatisfiable').
</p></dd>
<dt> <kbd>-s</kbd> </dt>
<dd><p>Check <strong>SPASS</strong> completions against reference completions.
The reference completion corresponding to a problem file <i>filename</i>
.<i>ext</i>', where <i>ext</i> is some <strong>DFG</strong> file
extension, is '<i>filename</i>.<i>mod</i>' and must be located in the same directory
as the problem file. ('s' is for 'satisfiable).
</p></dd>
<dt> <kbd>-r</kbd></dt>
<dd><p>Run. Continue after errors.
</p></dd>
<dt> <kbd>-w</kbd></dt>
<dd><p>Print warning if model checking is enabled, a model has been found,
but the reference does not exist.
</p></dd>
<dt> <kbd>-P</kbd></dt>
<dd><p>Specify <strong>SPASS</strong> options. Enclose in single quotes to protect from shell please.
</p></dd>
<dt> <kbd>-T <i>limit</i></kbd></dt>
<dd><p>Enable timing by shell. Stops in time even if <strong>SPASS</strong> timing does
not work.
</p></dd>
<dt> <kbd>-c <i>limit</i></kbd></dt>
<dd><p>Specify time limit in seconds for proof checker. This is the time
available for verifying one proof step in a proof.
</p></dd>
<dt> <kbd>-d</kbd></dt>
<dd><p>Debug. Lots of output about intermediate results etc.
</p></dd>
<dt> <kbd>-k</kbd></dt>
<dd><p>Keep. Keep generated temporary files.
</p></dd>
<dt> <kbd>-o</kbd></dt>
<dd><p>Use <strong>SPASS</strong> instead of <small>OTTER</small> for proof checking.
</p></dd>
<dt> <kbd>-x</kbd></dt>
<dd><p>Extension. Process all file parameters, regardless of
extension. Normally, files with unknown extensions are ignored.
</p></dd>
<dt> <kbd>-i</kbd></dt>
<dd><p>Interactive. Reads file names from standard input.
</p></dd>
<dt> <kbd>-m</kbd></dt>
<dd><p>Mode. Print out command line.
</p></dd>
</dl>
<hr size="6">
<a name="SEC15"></a>
<h2 class="section"> 2.5 EXAMPLES </h2>
<p>To check a single file with some extra <strong>SPASS</strong> options:
</p><dl compact="compact">
<dd><p><strong>checkstat</strong> -p 'SPASS <i>options</i>' <i>filename</i>
</p></dd>
</dl>
<p>To check all files with '.cnf' suffix in directory 'Test':
</p><dl compact="compact">
<dd><p><strong>checkstat</strong> Test/*.cnf
</p></dd>
</dl>
<hr size="6">
<a name="SEC16"></a>
<h2 class="section"> 2.6 AUTHORS </h2>
<p>Thorsten Engel and Christian Theobalt
</p>
<p>Contact : spass@mpi-inf.mpg.de
</p>
<hr size="6">
<a name="SEC17"></a>
<h2 class="section"> 2.7 SEE ALSO </h2>
<p>filestat(1), pcs(1), pgen(1), rescmp(1), tpform(1), tpget(1), deprose(1), dfg2otter(1), dfg2otterpl(1), SPASS(1)
</p>
<hr size="6">
<table cellpadding="1" cellspacing="1" border="0">
<tr><td valign="middle" align="left">[<a href="#SEC10" title="Beginning of this chapter or previous chapter"> << </a>]</td>
<td valign="middle" align="left">[<a href="script_3.html#SEC18" title="Next chapter"> >> </a>]</td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left"> </td>
<td valign="middle" align="left">[<a href="script.html#Top" title="Cover (top) of document">Top</a>]</td>
<td valign="middle" align="left">[Contents]</td>
<td valign="middle" align="left">[Index]</td>
<td valign="middle" align="left">[<a href="script_abt.html#SEC_About" title="About (help)"> ? </a>]</td>
</tr></table>
<p>
<font size="-1">
This document was generated by <em>Christoph Weidenbach</em> on <em>February, 23 2010</em> using <a href="http://www.nongnu.org/texi2html/"><em>texi2html 1.78</em></a>.
</font>
<br>
</p>
</body>
</html>
|
