1.1 --- a/doc-src/Nitpick/nitpick.tex Wed Mar 10 08:04:50 2010 +0100
1.2 +++ b/doc-src/Nitpick/nitpick.tex Wed Mar 10 14:21:01 2010 +0100
1.3 @@ -4,6 +4,7 @@
1.4 \usepackage{amssymb}
1.5 \usepackage[english,french]{babel}
1.6 \usepackage{color}
1.7 +\usepackage{footmisc}
1.8 \usepackage{graphicx}
1.9 %\usepackage{mathpazo}
1.10 \usepackage{multicol}
1.11 @@ -1019,7 +1020,7 @@
1.12 can be disabled by setting the \textit{bisim\_depth} option to $-1$. The
1.13 bisimilarity check is then performed \textsl{after} the counterexample has been
1.14 found to ensure correctness. If this after-the-fact check fails, the
1.15 -counterexample is tagged as ``likely genuine'' and Nitpick recommends to try
1.16 +counterexample is tagged as ``quasi genuine'' and Nitpick recommends to try
1.17 again with \textit{bisim\_depth} set to a nonnegative integer. Disabling the
1.18 check for the previous example saves approximately 150~milli\-seconds; the speed
1.19 gains can be more significant for larger scopes.
1.20 @@ -1031,7 +1032,7 @@
1.21 \textbf{lemma} ``$\lbrakk xs = \textit{LCons}~a~\textit{xs};\>\, \textit{ys} = \textit{LCons}~a~\textit{ys}\rbrakk
1.22 \,\Longrightarrow\, \textit{xs} = \textit{ys}$'' \\
1.23 \textbf{nitpick} [\textit{bisim\_depth} = $-1$, \textit{show\_datatypes}] \\[2\smallskipamount]
1.24 -\slshape Nitpick found a likely genuine counterexample for $\textit{card}~'a$ = 2: \\[2\smallskipamount]
1.25 +\slshape Nitpick found a quasi genuine counterexample for $\textit{card}~'a$ = 2: \\[2\smallskipamount]
1.26 \hbox{}\qquad Free variables: \nopagebreak \\
1.27 \hbox{}\qquad\qquad $a = a_1$ \\
1.28 \hbox{}\qquad\qquad $\textit{xs} = \textsl{THE}~\omega.\; \omega =
1.29 @@ -1901,7 +1902,7 @@
1.30
1.31 \textbf{Warning:} If the option is set to \textit{true}, Nitpick might
1.32 nonetheless ignore some polymorphic axioms. Counterexamples generated under
1.33 -these conditions are tagged as ``likely genuine.'' The \textit{debug}
1.34 +these conditions are tagged as ``quasi genuine.'' The \textit{debug}
1.35 (\S\ref{output-format}) option can be used to find out which axioms were
1.36 considered.
1.37
1.38 @@ -2002,7 +2003,7 @@
1.39 \begin{enum}
1.40 \item[$\bullet$] \textbf{\textit{true}}: Tentatively treat the (co)in\-duc\-tive
1.41 predicate as if it were well-founded. Since this is generally not sound when the
1.42 -predicate is not well-founded, the counterexamples are tagged as ``likely
1.43 +predicate is not well-founded, the counterexamples are tagged as ``quasi
1.44 genuine.''
1.45
1.46 \item[$\bullet$] \textbf{\textit{false}}: Treat the (co)in\-duc\-tive predicate
1.47 @@ -2050,7 +2051,7 @@
1.48 of $-1$ means that no predicate is generated, in which case Nitpick performs an
1.49 after-the-fact check to see if the known coinductive datatype values are
1.50 bidissimilar. If two values are found to be bisimilar, the counterexample is
1.51 -tagged as ``likely genuine.'' The iteration counts are automatically bounded by
1.52 +tagged as ``quasi genuine.'' The iteration counts are automatically bounded by
1.53 the sum of the cardinalities of the coinductive datatypes occurring in the
1.54 formula to falsify.
1.55
1.56 @@ -2100,7 +2101,7 @@
1.57
1.58 \begin{enum}
1.59 \item[$\bullet$] \textbf{\textit{true}}: Finitize the datatype. Since this is
1.60 -unsound, counterexamples generated under these conditions are tagged as ``likely
1.61 +unsound, counterexamples generated under these conditions are tagged as ``quasi
1.62 genuine.''
1.63 \item[$\bullet$] \textbf{\textit{false}}: Don't attempt to finitize the datatype.
1.64 \item[$\bullet$] \textbf{\textit{smart}}: Perform a monotonicity analysis to
1.65 @@ -2268,7 +2269,7 @@
1.66 {\small See also \textit{max\_potential} (\S\ref{output-format}).}
1.67
1.68 \opfalse{check\_genuine}{trust\_genuine}
1.69 -Specifies whether genuine and likely genuine counterexamples should be given to
1.70 +Specifies whether genuine and quasi genuine counterexamples should be given to
1.71 Isabelle's \textit{auto} tactic to assess their validity. If a ``genuine''
1.72 counterexample is shown to be spurious, the user is kindly asked to send a bug
1.73 report to the author at
1.74 @@ -2282,7 +2283,7 @@
1.75
1.76 \begin{enum}
1.77 \item[$\bullet$] \textbf{\textit{genuine}}: Nitpick found a genuine counterexample.
1.78 -\item[$\bullet$] \textbf{\textit{likely\_genuine}}: Nitpick found a ``likely
1.79 +\item[$\bullet$] \textbf{\textit{quasi\_genuine}}: Nitpick found a ``quasi
1.80 genuine'' counterexample (i.e., a counterexample that is genuine unless
1.81 it contradicts a missing axiom or a dangerous option was used inappropriately).
1.82 \item[$\bullet$] \textbf{\textit{potential}}: Nitpick found a potential counterexample.
1.83 @@ -2313,12 +2314,18 @@
1.84
1.85 The supported solvers are listed below:
1.86
1.87 +\let\foo
1.88 +
1.89 \begin{enum}
1.90
1.91 \item[$\bullet$] \textbf{\textit{MiniSat}}: MiniSat is an efficient solver
1.92 written in \cpp{}. To use MiniSat, set the environment variable
1.93 \texttt{MINISAT\_HOME} to the directory that contains the \texttt{minisat}
1.94 -executable. The \cpp{} sources and executables for MiniSat are available at
1.95 +executable.%
1.96 +\footnote{Important note for Cygwin users: The path must be specified using
1.97 +native Windows syntax. Make sure to escape backslashes properly.%
1.98 +\label{cygwin-paths}}
1.99 +The \cpp{} sources and executables for MiniSat are available at
1.100 \url{http://minisat.se/MiniSat.html}. Nitpick has been tested with versions 1.14
1.101 and 2.0 beta (2007-07-21).
1.102
1.103 @@ -2333,14 +2340,17 @@
1.104 \item[$\bullet$] \textbf{\textit{PicoSAT}}: PicoSAT is an efficient solver
1.105 written in C. You can install a standard version of
1.106 PicoSAT and set the environment variable \texttt{PICOSAT\_HOME} to the directory
1.107 -that contains the \texttt{picosat} executable. The C sources for PicoSAT are
1.108 +that contains the \texttt{picosat} executable.%
1.109 +\footref{cygwin-paths}
1.110 +The C sources for PicoSAT are
1.111 available at \url{http://fmv.jku.at/picosat/} and are also bundled with Kodkodi.
1.112 Nitpick has been tested with version 913.
1.113
1.114 \item[$\bullet$] \textbf{\textit{zChaff}}: zChaff is an efficient solver written
1.115 in \cpp{}. To use zChaff, set the environment variable \texttt{ZCHAFF\_HOME} to
1.116 -the directory that contains the \texttt{zchaff} executable. The \cpp{} sources
1.117 -and executables for zChaff are available at
1.118 +the directory that contains the \texttt{zchaff} executable.%
1.119 +\footref{cygwin-paths}
1.120 +The \cpp{} sources and executables for zChaff are available at
1.121 \url{http://www.princeton.edu/~chaff/zchaff.html}. Nitpick has been tested with
1.122 versions 2004-05-13, 2004-11-15, and 2007-03-12.
1.123
1.124 @@ -2350,26 +2360,32 @@
1.125
1.126 \item[$\bullet$] \textbf{\textit{RSat}}: RSat is an efficient solver written in
1.127 \cpp{}. To use RSat, set the environment variable \texttt{RSAT\_HOME} to the
1.128 -directory that contains the \texttt{rsat} executable. The \cpp{} sources for
1.129 -RSat are available at \url{http://reasoning.cs.ucla.edu/rsat/}. Nitpick has been
1.130 -tested with version 2.01.
1.131 +directory that contains the \texttt{rsat} executable.%
1.132 +\footref{cygwin-paths}
1.133 +The \cpp{} sources for RSat are available at
1.134 +\url{http://reasoning.cs.ucla.edu/rsat/}. Nitpick has been tested with version
1.135 +2.01.
1.136
1.137 \item[$\bullet$] \textbf{\textit{BerkMin}}: BerkMin561 is an efficient solver
1.138 written in C. To use BerkMin, set the environment variable
1.139 \texttt{BERKMIN\_HOME} to the directory that contains the \texttt{BerkMin561}
1.140 -executable. The BerkMin executables are available at
1.141 +executable.\footref{cygwin-paths}
1.142 +The BerkMin executables are available at
1.143 \url{http://eigold.tripod.com/BerkMin.html}.
1.144
1.145 \item[$\bullet$] \textbf{\textit{BerkMin\_Alloy}}: Variant of BerkMin that is
1.146 included with Alloy 4 and calls itself ``sat56'' in its banner text. To use this
1.147 version of BerkMin, set the environment variable
1.148 \texttt{BERKMINALLOY\_HOME} to the directory that contains the \texttt{berkmin}
1.149 -executable.
1.150 +executable.%
1.151 +\footref{cygwin-paths}
1.152
1.153 \item[$\bullet$] \textbf{\textit{Jerusat}}: Jerusat 1.3 is an efficient solver
1.154 written in C. To use Jerusat, set the environment variable
1.155 \texttt{JERUSAT\_HOME} to the directory that contains the \texttt{Jerusat1.3}
1.156 -executable. The C sources for Jerusat are available at
1.157 +executable.%
1.158 +\footref{cygwin-paths}
1.159 +The C sources for Jerusat are available at
1.160 \url{http://www.cs.tau.ac.il/~ale1/Jerusat1.3.tgz}.
1.161
1.162 \item[$\bullet$] \textbf{\textit{SAT4J}}: SAT4J is a reasonably efficient solver
1.163 @@ -2384,7 +2400,9 @@
1.164 \item[$\bullet$] \textbf{\textit{HaifaSat}}: HaifaSat 1.0 beta is an
1.165 experimental solver written in \cpp. To use HaifaSat, set the environment
1.166 variable \texttt{HAIFASAT\_\allowbreak HOME} to the directory that contains the
1.167 -\texttt{HaifaSat} executable. The \cpp{} sources for HaifaSat are available at
1.168 +\texttt{HaifaSat} executable.%
1.169 +\footref{cygwin-paths}
1.170 +The \cpp{} sources for HaifaSat are available at
1.171 \url{http://cs.technion.ac.il/~gershman/HaifaSat.htm}.
1.172
1.173 \item[$\bullet$] \textbf{\textit{smart}}: If \textit{sat\_solver} is set to
1.174 @@ -2668,7 +2686,7 @@
1.175 \postw
1.176
1.177 The return value is a new proof state paired with an outcome string
1.178 -(``genuine'', ``likely\_genuine'', ``potential'', ``none'', or ``unknown''). The
1.179 +(``genuine'', ``quasi\_genuine'', ``potential'', ``none'', or ``unknown''). The
1.180 \textit{params} type is a large record that lets you set Nitpick's options. The
1.181 current default options can be retrieved by calling the following function
1.182 defined in the \textit{Nitpick\_Isar} structure: