PKIND options

Usage: mpiexec -np [2 or 3] ./pkind [options] input_file

Options:
  • -node : User specified main node (default: the last node that contains a PROPERTY)
  • -n : Stop after n iterations (default 200)
  • -multi : Enables the verification of multiple properties in an incremental fascion. (default: false)
  • -k_incremental : Generate incremental invariants until n iterations (default: k=200)
  • -no_incremental : Generate non incremental invariants. (default: generate incremental invariants)
  • -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_wrapper)
  • -flags : Pass string to solver command 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 Prints the current inductive counterexample (default: false)
  • -scratch : Do not log scratch work to disk (default: Don't log to disk)
  • -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 loop-free 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

KIND options

Usage: kind lustre-file

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)
  • -cvc3 Use CVC3 as solver (default: yices_wrapper)
  • -yices_exec Use Yices executable as solver (default: yices_wrapper)
  • -flags Pass string to solver command 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 scratch-work 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 loop-free constraint (default: false)
  • -static_loop Use a statically calculated loop-free 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

KIND-INV options

Usage: kind-inv [-inv_int and/or -inv_bool][options] lustre-file

Options:
  • -node User specified main node (default: the last node that contains a PROPERTY)
  • -inv_bool Generate boolean implication type invariants
  • -inv_int Generate integer less_or_equal type invariants
  • -rm_trivial_inv Leave trivial invariants there (default: Remove trivial invariants)
  • -yices_exec Use Yices executable as solver (default: yices_wrapper)
  • -debug Include debugging output (default: false)
  • -quiet Only return final answer (default: true)
  • -verbose Return more details (default: false)
  • -version Print version & copyright information
  • -help Display this list of options
  • --help Display this list of options
counter for vBulletin