# BMCTool

This tool aims to combine NuSMV with SAT solvers (namely Painless)
in order to perform Bounded Model Checking (BMC) on SMV programs.

# Dependecies
```
# NuSMV
To build NuSMV, CUDD, MiniSat and/or ZChaff as them are distributed,
you will need:

  * An ANSI C compiler (gcc will do, as will several versions of cc)
  * An ANSI C++ compiler (g++ will do)
  * GNU Flex version 2.5 or greater
  * GNU Bison version 1.22 or greater
  * cmake utility version 2.8 or greater
  * GNU make utility version 3.74 or greater
  * GNU patch utility
  * GNU tar and gzip utilities
  * Library libxml2
  * A fully working 'latex' environment for generation of documentation
  * Program 'doxygen' for generation of the programmer's documentation
  * Library 'readline' for a shell usability improvement.

For more information see NuSMV-2.6.0/NuSMV/README.txt

# painless/periplo
You will need:

  * autoconf
  * libtool
  * bison
  * flex

For more information about PeRIPLO installation : https://code.google.com/archive/p/periplo/wikis/BuildPeRIPLOFromSources.wiki


You also need :
  
  * gmp library
  * math library

```

# Compile Project

Type the following instructions:
```
# Just after cloning the repository, do not forget to clone submodules.
git submodule update --init
cd painless && git checkout ak/bmc && cd ..

# Build NuSMV
make build-nusmv

# Build PeRIPLO
cd painless/periplo &&  libtoolize && autoreconf --install --force && cd ../..

# Build painless
make build-painless

# Build bmctool
make build

#If dynamic NuSMV libraries could not be found, you have to setup LD_LIBRARY_PATH variable
export LD_LIBRARY_PATH=<PATH_TO_DYN_LIB>/NuSMV-2.6.0/NuSMV/lib:$LD_LIBRARY_PATH

```

Optionnaly if you want to live at HEAD from remote painless branch 
```
# update your submodule
git submodule update --remote
```