
==============================
About KIND
==============================

KIND is a k-induction based model checker for Lustre programs.  The KIND
included in this distribution can only handle single-node Lustre programs.

This distribution includes the following tools:

 * kind : a sequential k-induction based model checker for Lustre programs (single property)
 * kind-inv : an offline invariants generator for Lustre programs
 * pkind : an incremental and parallel k-induction based model checker for Lustre programs (multiple properties)


=======================================
How to install KIND 
=======================================

See the INSTALL file for a full description of the compilation process of KIND.
For a quick install, issue the following commands:

> ./configure
> make
> make install


==================================================
Lustre files supported by KIND
==================================================

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.

For integer constants, only those with up to nine digits are supported.
For floating-points numbers, only up to nine digits can appear right or
left of the decimal point.  Floating-points number of the form 0.000000E+00
are supported.

Properties to be checked should appear in special comment lines in the body
of the topmost node:

  --%PROPERTY <lustre property>

where <lustre property> is a Lustre Boolean expression, ending with a
semicolon.  Multiple property lines are conjoined.

Moreover KIND allows the verification of multiple properties in an
incremental fashion. More information about this feature can be found
in 'Multi-Property-README' file.


=============
Running KIND
=============

To run PKIND with incremental invariant generation: 

  mpiexec -np 3 pkind <options> [LUSTRE FILE]


To run PKIND with invariant generation and the verification of multiple properties in an incremental fashion:

  mpiexec -np 3 pkind -multi <options> [LUSTRE FILE]


To run PKIND with invariant generation, where the invariant generation is not generated incrementally:

  mpiexec -np 3 pkind -no_incremental <options> [LUSTRE FILE]


To run PKIND without invariant generation:

  mpiexec -np 2 pkind <options> [LUSTRE FILE]


To run sequential KIND:

   kind <options> [LUSTRE FILE]


To run the offline invariant generator:

   kind-inv -inv_int [and/or -inv_bool]  <options> [LUSTRE FILE]



=======
Contact
=======

For more information please contact:
    Temesghen Kahsai (temesghen-kahsaiazene@uiowa.edu) 
or Cesare Tinelli (cesare-tinelli@uiowa.edu).
