PKIND -- Incremental and Parallel k-induction model checker for verification of multiple properties of Lustre programs.
 
Usage: pkind  [options] input_file

  -with-inv-gen :Activate invariant generation  based on a predefined template. It will generate invariants of type BOOL and INT.

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

  -n 	:Stop after n iterations (default 200)

  -timeout      :Setting a timeout (default: 100.00)

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

  -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)
 
  -yices_exec 	:Use Yices executable as solver (default: yices)

  -flags 	:Pass string to solver cammand line (default: n/a)

  -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)

  -debug 	:Include debugging output (default: false)

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

  -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
