INSTALLATION Kind by default calls a wrapped version fo the yices library "yicesw" in order to help avoid an input buffer overflow error on large problems. To build yicesw, download and install the GMP-statically-compiled version of yices 1.0.9, noting the directory you installed it to, then run: ./build-yicesw where is the base yices installation directory. Copy the resulting binary to the same directory as the Kind executable. Yices 1.0.9 can be found at http://yices.csl.sri.com/, under the "previous versions" sections of the downloads. There is a click-through license you must agree to for yices. Our tests were run using the yices-1.0.9-i686-pc-linux-gnu-static-gmp.tar.gz distribution. (This is known to not compile correctly under RedHat Enterprise Linux 3, however RHEL 4 appears to work properly.) --- Alternately Kind can be called with the yices executable, though it may encounter a buffer overflow error on very large problems (and, unfortunately, this cause is usually not obvious from examining the resulting error messages -- generally they refer to a truncated variable name). Copy the yices binary to the same directory as Kind, and run Kind with the -yices-exec option. --- If you desire Kind to create variable dependency graphs, you must have the "dot" program from the graphviz suite installed and located on your default execition path. --- LUSTRE FILES: Kind currently does not support included files, and there can be no forward references of nodes. There is only very limited support for non- linear arithmetic, records, and the "when" operation. We do not support arrays, recursive calls, or user-defined types at this time. The topmost node to be checked should include the special comment line --%MAIN somewhere in its body. If no node includes this line, then the last node in the source file is taken to be the topmost node. Properties to be checked should appear in special comment lines in the body of the topmost node: --%PROPERTY where is a Lustre Boolean expression, ending with a semicolon. Multiple property lines are conjoined. Example: node sum (x:int) returns (sum:int); let sum = x -> x + pre sum; tel node resetsum (x:int; r:bool) returns (sum:int); let sum = if r then 0 else (x -> x + pre sum); --%MAIN --%PROPERTY if r then sum=0 else sum <> 0; tel ~ ~ --- RUNNING KIND: Usage: kind lustre-file Kind options: -n Stop after n iterations (default 200) -t Stop after n seconds (default max_int) -step_size Only check induction every n steps (default 1) -yices_exec Use Yices executable as solver (default: yices_wrapper) -flags Pass string to solver cammand line (default: n/a) -sal_ind Perform sal-like induction behavior at step n (default false) -debug Include debugging output (default: false) -quiet Only return final answer (default: false) -noscratch Do not log scratchwork to disk (default: log to disk) -bmc Only performs BMC (default: false) -loop Include loopfree constraint formulas + term check (default: false) -compression Include path compression but not term check (default: false) -finite_term Include the finite termination check constraint, but no loopfree constraint (default: false) -static_loop Use a statically calculated loopfree constraint (default: false) -interleave_term_checks Perform term checks prior to an induction step check (default: false) -abs_single Use fine-grained abstraction refinement (default: false) -path Use path-based abstraction refinement (default: false) -dot Prints dot graph of dependencies (default: false) -dotall Outputs all abstraction dependency graphs to graphXXX.dot (default: false) -no_moddiv Do not include div and mod definitions (default: false) -single_solver Uses 1 solver instance for both ground/symbolic formulas (default: false) -buffer_limit Try decreasing this if the program hangs early (default 200000) -only_inputs Only print inputs in counterexamples (default: false) -help Display this list of options --help Display this list of options In more detail: Timeouts: -n x: halts once reaching depth x -t x: halts after x seconds Solver options: -yices_exec: use yices executable instead of wrapper version -flags x: pass the string x to the yices binary The wrapper version of yices only recognizes the flag "-debug" -buffer_limit x: Try decreasing this if program seems to hang early. It determines the maximum length of strings sent to yices; sometimes a too-long string can cause yices to hang. -no_moddiv: may need to include this if a version of yices later than 1.0.9 is used Induction/BMC behavior (default: k-induction, step size 1) -step_size x: (x>0) If x>1 then only perform induction check every x steps -bmc: run in BMC mode only -sal_ind x: run BMC to depth x, then perform an induction step, then stop Abstraction options (default: no abstraction) -abs: use basic abstraction, 1 variable refined per iteration -path: use "path refinement", several related variables refined per iteration Path compression options (default: no path compression) -loop: full path compression + termination check -compression: path compression only -finite_term: termination check only -static_loop: full path compression, but do not take abstraction into account -interleave_term_checks: Only perform termination checks prior to an induction step check (step_size-1) General behavior -single-solver: only use one solver instance for both base and step case -ite: perform ITE eliminations -aggdef: use aggregate definitions (alternate translation) Output -quiet: minimal output -debug: include extra (excessive) debugging information in output -noscratch: normally Kind produces scratch files detailing all calls to yices for inspection or hand-modification (1 for each solver). This option does not populate said extra files. -only_inputs: Counterexamples generally include all (refined) variables. Ths limits them to only display input variable values. These require the dot graphing program to be installed and produce .dot and .gif files: -dot: generate a dot graph of static variable dependencies -dotall: generate dot graphs of variable dependencies as they are refined --- kind-loop.pl This script calls Kind in an iterative deepening mode with restarts; SAL was run with a similar script. Usage: perl kind-loop.pl