Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Type Name Latest commit message Commit time
Failed to load latest commit information.
checker
external
lib
tests
.clang-format
.configure-custom.sh
.gitignore
.travis.yml
CMakeLists.txt
LICENSE.md
README.md
TODO.md
clang-format.sh
configure
leviathan.sublime-project

README.md

Leviathan

Build Status Build status

About

Leviathan is an implementation of a tableau method for LTL satisfiability checking based on the paper "A new rule for a traditional tree-style LTL tableau" by Mark Reynolds.

This work has been accepted for publication at IJCAI-16 and a preprint can be found here.

Usage

Just call the tool passing the path to a file which contains the formulas to check. The parser is very flexible and supports every common LTL syntax used in other tools. Every line of the file is treated as an independent formula, so more than one formula at a time can be checked.

Moreover several command line options are present:

  • -l or --ltl let the user specify the formula directly on the command line
  • -m or --model generates and prints a model of the formula, if any
  • -p or --parsable generates machine-parsable output
  • --maximum-depth specifies the maximum depth of the tableau (and therefore the maximum size of the model)
  • -v <0-5> or --verbose <0-5> specifies the verbosity of the output
  • --version prints the current version of the tool
  • -h or --help displays the usage message

Usage example

The following sample:

./checker.exe --ltl "G (req => X grant) & req" --model

Outputs the following answer:

The formula is satisfiable!
The following model was found:
State 0:
req
State 1:
grant, !req
State 2:
!req
Loops to state 2

While with the addition of the parsable flag the output is the following:

SAT;{req} -> {grant,!req} -> {!req} -> #2

Compatibility

Leviathan has been written since the beginning with the portability in mind. The only prerequisite is a fairly recent C++11 compiler. It is known to work on Windows, Mac OS X and Linux and compiles correctly under MSVC 2015, GCC 4.8+ and Clang 3.5+.

Future Work

  • Refactor the code to enhance redability and simplify new features addition
  • Remove the dependency on Boost by reimplementing a custom stack and allocator
  • Rewrite the parser to remove the need of Flec++/Bisonc++ which are not easily available
  • Let the user choose the order of application of the tableau rules
  • Investigate the use of caching to quickly prune identical subtrees

See the TODO file for a more complete recap of the work in progress!

License

It is licensed under the very permissive MIT License. For the complete license see the provided LICENSE file in the root directory.

Thanks

Several open-source third-party libraries are currently used in this project:

  • Boost for the dynamic bitset and pool allocator
  • Optional std::optional implementation for C++11
  • cppformat to format the output
  • tclap to parse the command line arguments
  • flexc++ and bisonc++ as the parser generators