<commit_before>Kind 2
======

A multi-engine, parallel, SMT-based automatic model checker for safety properties of Lustre programs. 

Kind 2 takes as input a Lustre file annotated with properties to prove invariant (see [Lustre syntax](doc/Lustre.md)), and outputs which of the properties are true for all inputs, as well as an input sequence for those properties that are falsified. To ease processing by front-end tools, Kind 2 can output its results in [XML format](doc/XML.md).

Kind 2 runs a process for bounded model checking (BMC), a process for k-induction, and a process for IC3 in parallel on all properties simultaneously. It incrementally outputs counterexamples to properties as well as properties proved invariant.

The following command-line options control its operation (run ```kind2 --help``` for a full list).

```--enable {BMC|IND|PDR}``` Select model checking engines
   
By default, all three model checking engines are run in parallel. Give any combination of ```--enable BMC```, ```--enable IND``` and ```--enable PDR``` to select which engines to run. The option ``--enable BMC`` alone will not be able to prove properties valid, choosing ``--enable IND`` only will not produce any results. Any other combination is sound (properties claimed to be invariant are indeed invariant) and counterexample-complete (a counterexample will be produced for each property that is not invariant, given enough time and resources).

```--timeout_wall SECS``` Run for SECS seconds of wall clock time

```--timeout_virtual SECS``` Run for SECS of CPU time
 
```--smtsolver {Z3|CVC4|mathsat5} ``` Select SMT solver

The default is ```Z3```, but see options of the ```./build.sh``` script to override at compile time
  
```--z3_bin PROGRAM``` Executable for Z3

```--cvc4_bin PROGRAM``` Executable for CVC4

```--mathsat5_bin PROGRAM``` Executable for MathSat5

```--bmc_max K``` Run bounded model checking for up to ```K``` steps

```-v``` Output informational messages

```-xml``` Output in XML format


Requirements
============

- Linux or Mac OS X
- OCaml 4.01 or later
- A supported SMT solvers
 - [Z3](http://z3.codeplex.com) (presently recommended), 
 - [CVC4](http://cvc4.cs.nyu.edu), (must use ```--pdr_tighten_unsat_core false```) or
 - [MathSat5](http://mathsat.fbk.eu/)

Building and installing
=======================

If you got the sources from the Github repository, you need to run first

    ./autogen.sh

In any case, the commands

    ./build.sh
    make install

will configure and build ZeroMQ, CZMQ, the OCaml bindings and Kind 2 and install the binary `kind2` into `/usr/local/bin` provided that you have write access to that directory. Call `./build.sh --prefix=PATH` to install the Kind 2 binary into `PATH/bin` instead. If you need to pass options to the configure scripts of any of ZeroMQ, CZMQ, the OCaml bindings or Kind 2, add these to the `build.sh` call. Use `./configure --help` after `autogen.sh` to see all available options.

You need a supported SMT solver, at the momemt either Z3, CVC4 or MathSat5 on your path when running `kind2`.<commit_msg>Added Menhir among the requirements<commit_after>Kind 2
======

A multi-engine, parallel, SMT-based automatic model checker for safety properties of Lustre programs. 

Kind 2 takes as input a Lustre file annotated with properties to prove invariant (see [Lustre syntax](doc/Lustre.md)), and outputs which of the properties are true for all inputs, as well as an input sequence for those properties that are falsified. To ease processing by front-end tools, Kind 2 can output its results in [XML format](doc/XML.md).

Kind 2 runs a process for bounded model checking (BMC), a process for k-induction, and a process for IC3 in parallel on all properties simultaneously. It incrementally outputs counterexamples to properties as well as properties proved invariant.

The following command-line options control its operation (run ```kind2 --help``` for a full list).

```--enable {BMC|IND|PDR}``` Select model checking engines
   
By default, all three model checking engines are run in parallel. Give any combination of ```--enable BMC```, ```--enable IND``` and ```--enable PDR``` to select which engines to run. The option ``--enable BMC`` alone will not be able to prove properties valid, choosing ``--enable IND`` only will not produce any results. Any other combination is sound (properties claimed to be invariant are indeed invariant) and counterexample-complete (a counterexample will be produced for each property that is not invariant, given enough time and resources).

```--timeout_wall SECS``` Run for SECS seconds of wall clock time

```--timeout_virtual SECS``` Run for SECS of CPU time
 
```--smtsolver {Z3|CVC4|mathsat5} ``` Select SMT solver

The default is ```Z3```, but see options of the ```./build.sh``` script to override at compile time
  
```--z3_bin PROGRAM``` Executable for Z3

```--cvc4_bin PROGRAM``` Executable for CVC4

```--mathsat5_bin PROGRAM``` Executable for MathSat5

```--bmc_max K``` Run bounded model checking for up to ```K``` steps

```-v``` Output informational messages

```-xml``` Output in XML format


Requirements
============

- Linux or Mac OS X
- OCaml 4.01 or later
- [Menhir](http://gallium.inria.fr/~fpottier/menhir/) parser generator
- A supported SMT solvers
 - [Z3](http://z3.codeplex.com) (presently recommended), 
 - [CVC4](http://cvc4.cs.nyu.edu), (must use ```--pdr_tighten_unsat_core false```) or
 - [MathSat5](http://mathsat.fbk.eu/)

Building and installing
=======================

If you got the sources from the Github repository, you need to run first

    ./autogen.sh

In any case, the commands

    ./build.sh
    make install

will configure and build ZeroMQ, CZMQ, the OCaml bindings and Kind 2 and install the binary `kind2` into `/usr/local/bin` provided that you have write access to that directory. Call `./build.sh --prefix=PATH` to install the Kind 2 binary into `PATH/bin` instead. If you need to pass options to the configure scripts of any of ZeroMQ, CZMQ, the OCaml bindings or Kind 2, add these to the `build.sh` call. Use `./configure --help` after `autogen.sh` to see all available options.

You need a supported SMT solver, at the momemt either Z3, CVC4 or MathSat5 on your path when running `kind2`.
{'fraction_non_alphanumeric': 0.11279273538314481, 'fraction_numerical': 0.010195953480962243, 'mean_word_length': 4.244778613199665, 'pattern_counts': {'":': 0, '<': 3, '<?xml version=': 0, '>': 3, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 2}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '277656', 'n_tokens_mistral': 1847, 'n_tokens_neox': 1749, 'n_words': 866}