GAVS+ Wiki

(A) Migrate from http://www6.in.tum.de/~chengch/gavs/ to sourceforge

(B) For game solving from textual format (only for compact version, where one needs to add the maximal vertex index as the 4th parameter; type java -jar GAVS+.jar -help for enabling such options), enable efficient encoding for safety, reachability, and Büchi winning condition.

Originally, if one reads a textural format, then the BDD variable ordering is done first by listing all PRE_VARIABLES, followed by all POST_VARIABLES. This makes the solver very slow in larger examples (the correct way should be PRE_1 POST_1 PRE_2 POST_2, i.e., to alternate the bits).

The change was initially done for LaBRI, CNRS to privately test their reachability game solver. The optimized encoding appears in PDDL-based solver, but not for graph-based games.