1. Xinhao Yuan
  2. DrillMC


Drill Model Checker (DMC) is a modelling and testing framework for real distributed systems.

Currently it works with C++ code. Support for other languages is in the plan.

# Build


 - cmake
 - C++ toolchain with C++11 support
 - boost
 - openssl
 - thrift


 - python
 - thriftpy
 - JDK for Java JNI wrapper 

make debug will generate build/Debug for debug build.
make release will generate build/Release for release build.

## MSVC build


 - boost Windows build
   - Prebuilt - https://sourceforge.net/projects/boost/files/boost-binaries/
 - openssl Windows build
   - Prebuilt (unoffical) - https://slproweb.com/products/Win32OpenSSL.html
 - thrift compiler Windows binary
 - thrift cpp library Windows build

First you need to create MSVCConfig.cmake (from MSVCConfig.cmake.default) to fit your environment.

Use MSVCBuild.cmd or ``make msvc'' to generate project files for building Drill. 

### Thrift issues

 - Thrift 0.9.3:
   - the libthrift MSVC project is missing some source files:

	 server\TServerFramework.{h,cpp} - requires NOMINMAX macro to be defined to resolve std::min and std::max symbol conflict.

   - For release build, there seems to be some problems with /GL while linking with Drill DLL. Turning it off resolves the issue.

# License

MIT - See the LICENSE file

# Quick Guide - How to run the builtin examples.

1. Build Drill projects. After projects built, you should find executables/libraies in the output directory named:

  - DMCExplorer
  - DMCCppWrapper
  - WrapperUnitTest

2. Running DMCExplorer without parameters with print help messages for your reference.

3. Suppose the current working directory is the output dir. Running the following command line will run one of the example named "LocalSync" with simple log output:

  ./DMCExplorer -i ../../PresetConf/RandomOnceDebug.conf [ ./WrapperUnitTest LocalSync ]
  Please refer to help messages for the meaning of parameters.
  Changing "LocalSync" to other names will run other examples.
  Running WrapperUnitTest without parameters will print all possible names.