Tool to collect structural information from parity games.
Compiling pginfo requires the following:
- A recent C++ compiler, supporting C++11 features, e.g. GCC 4.8 or newer, or Clang 3.5 or newer.
- Boost (especially graph, algorith, shared_ptr, type_traits)
- YAML-CPP
- CMake (2.8 or newer)
For compilation, assume that the source code has been checked out in /path/to/src. We will build the tool in /path/to/build, assuming that the build directory already exists.
First the build is configured using the following command:
cd /path/to/build
cmake /path/to/src -DCMAKE_INSTALL_PREFIX=<prefix>
make
make install
where you should substitute the prefix where you want to install the tool for <prefix>.
If you installed YAML-CPP in a non-standard path, it may not be detected by the CMake script, in that case you can append -DYAMLCPP_DIR=/path/to/yaml to the CMake command.
The tool uses a command line library and a logging library internally. By default, the CMake script tries to look for a pre-installed version of those libaries, and automatically falls back to a version which is included in the sourcetree if no such version can be found. Should you want to use your pre-installed version nevertheless, you can add -DCPPCLI_DIR=/path/to/cppcli or -DCPPLOGGING_DIR=/path/to/cpplogging, respectively, to the CMake line in the instructions above.
pginfo [OPTIONS]... [INFILE [OUTFILE]]
where INFILE contains the parity game from which information needs to be collected in PGSolver format, and OUTFILE is the name of a file to which the structural information will be written in YAML format. OPTIONS is a sequence options, containing for example the measures that need to be computed (multiple measures can be computed in one call to the executable).
The time it takes to compute the measures can be recorded and written to a file in YAML format:
--timings[=FILE]append timing measurements toFILE. Measurements are written to standard error if noFILEis provided
The measures that can be computed are controlled by the following options:
--allcompute all statistics about the graph. Overrules all other options--adcompute alternation-depth using a sorting of priorities--ad-ckscompute alternation-depth using the algorithm from [CKS93]--bfscompute information from BFS on the graph--dfscompute information from DFS on the graph--diametercompute the diameter of the graph--diamondscompute the number of diamonds in the graph--girthcompute the girth of the graph--graphcompute general information about the graph--kellywidth-ubcompute upperbound on Kelly-width--sccscompute strongly connected components--treewidth-lbcompute lowerbound on treewidth--treewidth-ubcompute upperbound on treewidth
Some of the structural information is hard to compute (quadratic complexity or worse). The following options are provided to skip expensive computations for large inputs:
--max-for-expensive=NUMfor BFS and DFS do not records queue or stack sizes if the number of vertices exceedsNUM--neighbourhoods=NUMcompute the sizes of the neighbourhoods up to and includingNUM