
* Content

./src -- contains all the ".ml" source files.
./doc -- contains a dir for the technical report.
Makefile  -- a makefile that uses ocamlbuild.

* Installation
Compilation:
 autoconf
 ./configure
 make
 make install
 make clean  -- to clean


* Use

Offline invariants generator for single node Lustre program.
Usage: kind-ai [options] input_file
  -yices_exec 	SOLVER: Use Yices executable as solver (default: yices)
  -debug 	OUTPUT: Include debugging output (default: false)
  -quiet 	OUTPUT: Only return final answer (default: true)
  -packs 	Specify which packs should be used
  -full-packs 	Activate the biggest packs possible (COSTLY)
  -print-vars 	Print variables (to help building packs)
  -no-thresholds 	Enforce direct widening without thresholds (faster but less precise)
  -online 	Online mode: dump predicate in yices compliant format on stdout
  -lustre-output 	Lustre output mode: dump predicate as lustre assertions on stdout
  -scc 	Compute SCC and extract candidates for mode variables
  -seq 	Performs a sequence of analyses in an iterative fashion
  -no-analysis 	When used with -scc, only rely on subrange in the lustre file to compute scc representants
  -restart 	Restart with the lowest k after each exhibited model
  -verbose 	OUTPUT: Return more details (default: false)
  -verbose-level 	OUTPUT: Return more details (default: 1)
  -version Print version & copyright information
  -help  Display this list of options
  --help  Display this list of options

* Packs

The syntax for specify the packs is the following:
kind-ai -packs "packs_description" file

packs_description: a space separate list of packs, ie. "pack1 pack2 pack3"
pack: either a global basic_pack bp or a context_pack cp

basic_pack: (pack_type: var1, var2, var3) or (var1, var2, var3) for the default pack_type, varX should be of numerical type
pack_type: oct | poly_loose | poly_strict | poly_eq | ppl_loose | ppl_strict | ppl_grid, default is ppl_loose

context_pack: { expressions: ()} for non relational information under predicate
           or { expressions: basic_pack1 basic_pack2 }

expressions: expr | expr1, expr2
expr: var | ( base_expr )
base_expr: an abitrary /simple/ expression over integer arithmetic (+,-,*,/,div,mod) and boolean (not, and, or , >=, <=, >, <, =)
BE CAREFUL: when var or base_expr is of type integer, it should range over a /small/ finite number of values. Otherwise the analyis is not guarantied to terminate.


