PKIND -- Incremental and Parallel k-induction model checker for multiple properties of Lustre programs.
 
Usage: mpiexec -np [2 or 3] ./pkind  [options] input_file

  -node  :User specified main node (default: the last node that contains a PROPERTY)

  -n 	:Stop after n iterations (default 200)

  -no_multi 	: Disables the verification of multiple properties in an incremental fascion. (default: false)

  -k_incremental 	:Generate incremental invariants until k iterations (default: k=200)
 
  -no_incremental 	:Generate non incremental invariants. (default: generate incremental invariants)
 
  -range          :Maximum range for which to generate candidates for mode variables (default: max range = 10)

  -mpi_abort 	:It will abort the mpi environment. Useful when the solver returns with an answer but the environment is not terminated yet. (default false)
 
  -cvc3 	:Use CVC3 as solver (default: yicesw)
 
  -yices_exec 	:Use Yices executable as solver (default: yices)

  -solver_path 	:Specify the path to the solver. Used for KIND GUI. (default: specified by ./configure)
   
  -flags 	:Pass string to solver cammand line (default: n/a)

  -debug 	:Include debugging output (default: false)

  -quiet 	:Only return final answer (default: true)

  -verbose 	:Return more details (default: false)

  -induct_cex 	:Print the current inductive counterexample (default: false)

  -scratch 	:Log scratchwork to disk (default: Don't log to disk)

  -xml 	        :Generate KIND result in XML format (default: false)

  -only_inputs 	:Only print inputs in counterexamples (default: false)

  -dot 	: Prints dot graph of dependencies (default: false)

  -dotall 	:Outputs all abstraction dependency graphs to graphXXX.dot (default: false)

  -loop 	:Include loopfree constraint formulas + term check (default: false)

  -compression 	:Include path compression but not term check (default: false)

  -version :Print version & copyright information

  -help  :Display this list of options

  --help  :Display this list of options
