|A GPU-based MPG solver|
OverviewThe GPUMPG package contains a GPU-based implementations of several algorithms for solving mean-payoff games.
To use the tool, you need the corresponding OpenCL drivers for your device:
The tool can be invoked by executing
mpgsolver FILE, with FILE being a mean-payoff game. Several options can be specified, list them by executing
The benchmark results can be re-evaluated by running the Bash script
bench/run_benchmarks.sh, with the options in
bench/config adjusted to your system.
Source code, benchmarks and results
- Source code (71 KB, md5sum: 22c9f5c506987654759347ee02844832).
- Precompiled Win64 executable (801 KB, md5sum: a83a7a4c80ba255e6bc8ef62619ff7d7).
- Games from the synthesis of controllers for hybrid systems (563 MB, md5sum: 22867970323da441f42e5d7765dace84).
- Games converted from parity games for equivalence checking problems (6.2 GB, md5sum: ac81d06d4cc684e414d57e1aa33041f7) (from here).
- Games converted from parity games for model checking problems (2.2 GB, md5sum: a509bf2e01bc6c6b12ec0fe83fe42f8e) (from here).
- Compiled results for the above benchmarks (6.2 KB, md5sum: 695ac092c8fe86c237e949ad53aa5327).
- Solutions from our solver for the above benchmarks (739 MB, md5sum: 1cde21047683970d95fe4fb06babfcac).
You need, in addition to one of the OpenCL toolkits given above:
- A C++ compiler. Compilation was tested with g++ 6.1 and the Visual Studio 2015 compiler (msvc-14.0)
Boost in the version 1.61 or higher.
Extract boost to some location and set the environment variable
BOOST_ROOTto that location. You also need to build the static boost libraries with the following commands in the boost folder (adjust toolset if you use another compiler):
- .\b2 -j8 variant=release toolset=msvc-14.0 address-model=64 link=static threading=multi
Then the build script
build_windows.bat builds the project on Windows using Visual Studio 2015 in a 64-bit build. Other builds can be specified by editing the file or invoking CMake by hand.