Model-Based Explorative Testing for Willemt/Raft

This project adopts a model-based testing approach to test willemt/raft. The word explorative means that real code execution is manipulated by the model.

To summarize,

1. We modelled Willemt/raft in TLA+ and found invariant violations.
2. Traces generated by TLC model checker are converted to test cases, and test cases are executed in real code.
3. An invariant violation in TLA+ is reproduced in real code.

Currently the TLA+ specifications are made public. The testing code will be public soon.

Usage

cd tla
make run-not-fixed  # the version has bugs
make run-fixed      # the version fixed bugs
make run            # both run-not-fixed and run-fixed
make clean