v4.3
Jun 3 2017 Oliver Friedmann
- Use OASIS and OPAM instead of submodules and make
Aug 5 2016 Oliver Friedmann
- Change Makefile to use Ocamlbuild instead
Jul 1 2016 Oliver Friedmann
Jun 27 2016 Oliver Friedmann
- Added support for generating MDP-like valuations
May 8 2014 Oliver Friedmann
- Added tool for analyzing winning strategies
Sep 11 2013 Martin Lange
- Added Fixpoint Iteration Algorithm
Aug 07 2013 Oliver Friedmann
- Fixed a bug in the verification algorithm (thanks to Maks Verver for finding it!)
Jun 24 2013 Michael Falk
- Added a new solver based on a reduction to mu-calculus model checking
Jun 6 2013 Martin Lange
- Added a functor Build in src/paritygame/paritygame.ml which turns a datatype for paritygame nodes into a function that creates a parity game from some initial node given functions that create the successors etc. of a node.
- Added a new benchmark "langincl" formalising an inclusion problem between an NBA and a DBA as a solitaire game of index 3. See this for the use of the functor Build.
Apr 26 2013 Oliver Friedmann
- Added a parity game to abstract unique sink / grid unique sink orientations called "auso"
Oct 16 2012 Oliver Friedmann
- You can now compile PGSolver with ocamlc; just create copies of all three (./, ./satsolvers, ./tcslib) "Config.default" and name them "Config"; set "COMPILE_WITH_OPT=NO"
May 17 2012 Oliver Friedmann
- Added visualization scripts for strategy iteration
- Changed the strategy iteration lower bound generators into one big generating tool
Apr 30 2012 Oliver Friedmann
- Updated Generators
- Added LP'fication tool
- Added Improvement Arena tool
Feb 24 2012 Oliver Friedmann
- Changed inclusion of config files
- Renamed "Libversion" to "Libpgsolver"
May 08 2011 Oliver Friedmann
- Added round-robin lower bound generator
Apr 28 2011 Martin Lange
Jan 23 2011 Oliver Friedmann
- Added lower bound generator for Fearnley's non-oblivious rule
Jan 05 2011 Oliver Friedmann
- Solvers are now parameterized via the command line
- All strategy improvement solvers are now seen as one solver
Dec 02 2010 Martin Lange
Nov 28 2010 Oliver Friedmann
- Changed definition of partial solvers
- Fixed minor bug in stratimprlocal
Feb 02 2010 Oliver Friedmann
- Removed Recursive Preservation Algorithm (it was just experimental and didn't prove to be a real improvement...)
- Removed Force Reach Algorithm (that was an experimental incomplete algorithm and it wasn't good either)
Jan 17 2010 Oliver Friedmann
- New Generator Towers Of Hanoi
- New Solver Strategy Iteration by Reduction to DPG
- New Solver Vorobyov's Randomized Approach #1
- New Solver Vorobyov's Randomized Approach #2
- New Genuine Solver Local Strategy Improvement
- Improved Solver Implementation Model Checker by Stevens / Stirling
- Outsourced almost all utility functions and modules to TCSLib
- Enabled Local Solving in PGSolver and Benchmark
- Library Version of PGSolver
Mar 28 2009 Oliver Friedmann
- Added GeneratorList containing a list of all generators; Makefile now automatically compiles these generators.
- Added new generator expstratvoege which is a simplified version of expstratimpr enforcing exponential behaviour w.r.t. Voege and Puri.
Mar 27 2009 Martin Lange
- Added .depend compilation
- Added new elevator verification generator
- Jurdzinski Generator is currently broken.
Mar 23 2009 Oliver Friedmann
- Removed external solver for linear inequality systems. Created a very slow but exact solution for dpgs. Megiddo's algorithm for solving inequality systems should be implemented. Note: Exponential Strategy Improvement Examples also work with Puri's Algorithm.
Mar 22 2009 Oliver Friedmann
- Added experimental solver using the standard reduction to DPG (experimental). It requires GLPK as well as OCAMLGLPK to be compiled into PGSolver. Unfortunately, floating point precision only suffices for very very very small games. Therefore, this algorithm is practically unusable in this context. One should implement another version relying on exact rational numbers; since GLPK is not able to exact parameters other than float, one has to implement a native linear inequality solver. Megiddo's algorithm should suffice.
Mar 20 2009 Oliver Friedmann
- Improved Small Progress Measures Implementation: It now computes the SPM for both players simultaneously and checks after a number of steps if there is already a stable dominion and if so, the respective spms of the other player are marked as top.
Mar 17 2009 Oliver Friedmann
- Enriched Arg2-Module s.t. sub-parsing is supported
- Added support for generators in PGSolver; use LINKGENERATORS=YES in Config file to enable linking of generators into PGSolver
Mar 10 2009 Oliver Friedmann
- Added SATSolversForOcaml/SatSolverMods which should be included in Makefiles using Sat Solvers
- Added PGSolver/SolverList which should be included in Makefiles using Parity Game Solvers
Mar 08 2009 Oliver Friedmann
- Renamed expstratimpr --> superpolystratimpr
- Added new expstratimpr with linear number of edges
Mar 02 2009 Oliver Friedmann
- Removed Benchmarks, Preciousgames, demos and satsolvers subdirectory
- Outsourced satsolvers as separate package
- Outsourced mlsolver as separate package
- Added printing of parsable solution and strategy
- Added parsing of parsable solution and strategy
Feb 26 2009 Oliver Friedmann
- Moved global fixed point algorithm to temporary folder
Feb 25 2009 Oliver Friedmann
- Added global fixed point algorithm; generated strategy is NOT correct ATM
- Fixed Makefiles s.t. it really compiles without gcc
Feb 12 2009 Oliver Friedmann
- Updated configuration files s.t. SATSolvers have to be configured only in the respective config file
- Updated documentation as well
Feb 11 2009 Martin Lange
- Added min-party / max-parity coversion
- Node: jurdzinskigame generates min-parity games!
Jan 28 2009 Oliver Friedmann
- Added strategy improvement SAT reduction
Jan 26 2009 Oliver Friedmann
- Added install.txt
- Updated documentation w.r.t. parser
- Updated tools w.r.t. parser
- Added Parserhelper.parse_from_channel: in_channel -> bool -> Paritygame.paritygame The second parameter enables / disables sanity checking
- Parser: Removed parser routines from Paritygame.ml (and moved them to parser.mly)
- Model Checker: Now it returns an underapproximation instead of a solution to the whole scc. Major speed up.
Jan 25 2009 Oliver Friedmann
- Updated documentation: Model Checker Generator, Obfuscator
- Added Model Checker worst-case generator
- Obfuscator: Fixed edge obfuscation, New command line parameters.
- Model Checker: A bit more output
Jan 24 2009 Oliver Friedmann
- Documentation Update: Benchmarks, Developer's Guide
Jan 22 2009 Oliver Friedmann
- Documentation Update: Combine Tool, Transformer, Benchmark Tool
- Added Combine Tool
- Added Transformations.combine_games: paritygame list -> paritygame
- Tested compiling and integrating SAT solvers on a clean machine and it worked. It's a miracle!
- Documentation Update: Installation, Compilation, Supported Sat Solvers, Parameters of PGSolver, Invocation Output, Specification, Compressor, Obfuscator
Jan 21 2009 Oliver Friedmann
- Enhanced Clustered Random Generator
- Renamed GameBased Algorithm to LocalModelChecker
- Improved Attractor Computation
Jan 21 2009 Martin Lange
Jan 20 2009 Oliver Friedmann
- Documentation Update: Updated intro, algorithms, License
- Added version info (src/pgsolver/info.ml)
- Updated tool and generator output
Jan 19 2009 Oliver Friedmann
Jan 16 2009 Martin Lange
- Altered random generation: See src/tools/randomutils.ml val get_pairwise_different_from_range : int -> int -> int -> int list
- Altered parser: Parity games now need to start with the line "parity n;" where n is supposed to be the heighest occurring node number. Increases parser performance.