The game (after transformed into a max-parity game)

parity 8; 0 2 0 1,4 "v0"; 1 3 1 0,2 "v1"; 2 1 0 3,6 "v2"; 3 0 1 1,3 "v3"; 4 4 1 5,6 "v4"; 5 1 1 4,6 "v5"; 6 4 0 5,7 "v6"; 7 2 0 4 "v7";

induces an index-out-of-bounds-exception:

`eigheach [~/ownCloud/projects/pgsolver] bin/transformer -mm test.gm | bin/pgsolver -global recursive -v 3
PGSolver Collection Ver. 4.0: Parity Game Solver
Authors: Oliver Friedmann (University of Munich) and Martin Lange (University of Kassel), 2008-2017
http://tcsprojects.org

Reading game from ..................... STDIN
Parsing ............................... 0.00 sec
Chosen solver `recursive' .............
[MAIN: 1.57 msec] Starting Universal Solving Process
[MAIN: 0.04 msec] Considering game...
[MAIN: 0.01 msec] Nodes = 8
[MAIN: 0.01 msec] Edges = 15
[MAIN: 0.01 msec] Index = 5
[GLOBAL: 0.03 msec] Entering global preprocessing phase...
[GLOBAL: 0.01 msec] Removing useless self cycles... 1 transition(s) removed!
[GLOBAL: 0.04 msec] Created sinks: 0!
[GLOBAL: 0.03 msec] Searching for useful self cycles... 0 node(s) found!
[DECOMP: 0.21 msec] Entering decomposition phase at recursion level 0
[DECOMP: 0.04 msec] Considering game of size 8
[DECOMP: 0.06 msec] Decomposed game into 2 SCCs, size of largest SCC is 4
[DECOMP: 0.03 msec] Entering SCC #1 of size 4
[LOCAL: 0.04 msec] Reducing index 4 down to... 2!
[BACKEND: 0.05 msec] Calling backend for this SCC...
[RECURSIVE: 0.02 msec] Solving the game: [0:0,1,{1,2};1:1,1,{0,2};2:0,0,{1,3};3:0,0,{0}]
[RECURSIVE: 0.03 msec] Highest priority 1 belongs to player 1
[RECURSIVE: 0.01 msec] The following nodes have priority 1: P = {1}
[RECURSIVE: 0.02 msec] The attractor of P for player 1 is: {0,1,2,3}
[RECURSIVE: 0.01 msec] First recursive descent to subgame ...

[MAIN: 0.02 msec]  Starting Universal Solving Process
[MAIN: 0.01 msec]  Considering game...
[MAIN: 0.01 msec]    Nodes = 0
[MAIN: 0.01 msec]    Edges = 0

Fatal error: exception Invalid_argument("index out of bounds")
`

This problem is possibly caused by changes in OCaml but currently make will fail on Windows (not sure if this is the case for everyone but it is for me on a fresh install).
It spews out a couple of link errors: undefined reference to 'flexdll_dlopen' etc.

The problem is related to this: http://caml.inria.fr/mantis/print_bug_page.php?bug_id=4784

As suggested I removed the compiler flag (line 52 in the Makefile from CPPCOMPILER=-cc $(OCAMLOPTCPP) to CPPCOMPILER=) and this completely solves the problem.

I don't know if this breaks the makefile on other platforms so I though I just let it know.

Thanks for your time.

Hi, I have got the following issue using OCaml 4.13.1

File "src/solvers/satsolve.ml", line 29, characters 6-12: 29 | solver#add_helper_exactlyone 0 (Array.length delta - 1) [||] (fun j -> Po (Strategy (i, delta.(j))))) game; ^^^^^^ Error: This expression has type Timing.timetable option -> 'weak2 Satwrapper.satWrapper It has no method add_helper_exactlyone Command exited with code 2.

Any fixes for this issue? Thanks!

As far as I understand it, message_depth_tagged updates the last_time variable every time it is called. Is there any reason why last_time is updated even if the actual message is not being output?

This affects the runtime heavily - even if the logs are not displayed, the lines
let now = Sys.time () in
and
last_time := now
are always being called. If this is not done on purpose, a suggested fix would be to just put both of the lines mentioned above in the inline function, resulting in something like

let message_depth_tagged u depth tag s =
  message_depth u depth (fun x -> 
    let now = Sys.time() in
    let last_time_ = !last_time in
    last_time := now;
    "[" ^ String.capitalize_ascii (tag x) ^ ": " ^ Printf.sprintf "%.2f msec" (1000.0 *. (Sys.time() -. last_time_)) ^ "]  " ^ s x)

To use things like ocamlbuild and ocamlfind. The Makefiles are a big mess and I'm mostly to blame for this.

The solution verification algorithm implemented in PGSolver is incomplete; it fails to verify that winning sets are traps for the opposing players (a necessary condition for a correct solution) and consequently it will erroneously accept incorrect solutions.

For example, for this parity game:

parity 2;
0 2 0 0;
1 3 1 1;
2 4 1 0,1;

PGSolver accepts this solution:

paritysol 2;
0 0 0;
1 1 1;
2 0;

... which is wrong, because vertex 2 is really won by Odd (by moving to vertex 1).

The problem is with this line in `verification.ml':

pg_remove_nodes game' !badnodes;

... which removes vertices outside the current winning set, even though they might still be reachable by the opponent. In the example above this leads to the conclusion that vertex 2 is lost by Odd because Odd is forced to move the token to 0.

A good way to solve the problem is to verify that winning sets are traps as an additional "sanity check". An alternative solution is not to remove any vertices when fixing strategies (just restrict edges to create a single-player game) and check that the universal solver yields the expected winning regions, but that is probably less efficient (especially in the common case where the solution is actually valid).

Commit 72a2265 fails to compile for me (running OS X). The relevant snippet of the output is the following:

ocamlopt -I src -I obj -I /usr/local/lib/ocaml -I ./satsolversforocaml/obj -I ./tcslib/obj -I   /usr/local/lib/z3/ocaml -c -o obj/switch_zadeh.cmx src/solvers/stratimpralgs/switch_zadeh.ml
File "src/solvers/stratimpralgs/switch_zadeh.ml", line 17, characters 55-66:
Error: Unbound module Bits
make: *** [obj/switch_zadeh.cmx] Error 2

It seems that Bits is not included anywhere, but it is used in the Zadeh approach to strategy improvement. As a workaround, commenting the line $(PGSOLVERSOBJ)/switch_zadeh.$(COMPILEEXT) \ in the file SolverList disables this particular solver, but allows you to compile and run the tools with the other solvers enabled.

The types of the functions in files src/solvers/stratimpr*ml[i] are still full of "int". A lot of them should be "node".

As it stands, pgsolver has no open source license. Technically, this very heavily limits what can be done with this code. As Github's own guidance says:

"You're under no obligation to choose a license. However, without a license, the default copyright laws apply, meaning that you retain all rights to your source code and no one may reproduce, distribute, or create derivative works from your work. If you're creating an open source project, we strongly encourage you to include an open source license. The Open Source Guide provides additional guidance on choosing the correct license for your project."

Please could an open source license be added to pgsolver?

I cannot find any information on how to properly cite pgsolver when using it for a publication in the repository. Also, there does not appear to be any release of pgsolver on zenodo, which would assign it a citable DOI.

It would be great if you could indicate a preferred citation for pgsolver either in the README.md or using a CITATION.cff file in the root of the repository. Otherwise, I would greatly appreciate any information on how to properly cite this software.

To use OPAM instead of Submodules.

Are there any plans to support OCaml 5?

Currently, too many algorithms depend on the specific structure of the parity game definition.

I'm strugling to compile the newest version of pgsolver..
Any idea what's wrong here?
I've followed the install notes from the readme, and additionally did a opam install extlib as well..

make                                                              ✭develop 
rm -f ./temp/generatedsat.ml
mkdir -p ./temp
echo "" > ./temp/generatedsat.ml
ocamlbuild    -libs nums,str -package extlib -package TCSLib main.native
ocamlfind: Package `extlib' not found
Cannot run Ocamlfind.
Makefile:19: recipe for target 'pgsolver' failed
make: *** [pgsolver] Error 2