benchmarks: Rename gen.ml to aconjunctive_mu_generator.ml
Also disables the build of the corresponding executable bydefault (can be reenabled with the flat 'benchmarks').
makestatic.sh: Add 'gen' binary for acmu benchmarks
makestatic.sh: Include benchmarks for aconjunctive mu
benchmarks: Add README
Link ncurses bindings against libtinfo and libgpm
This is needed to produce static binaries.
Revert "Update INSTALL file to reflect current state"
This reverts commit 5de20a335bdf0e0c5e7b940fe69952963720b1cd.
Update INSTALL file to reflect current state
Since pgsolver is now a dependency and is not available in commonLinux distributions, we advise people to install all ocamldependencies with opam instead.
benchmarks: Correctly parse output with REPEATS=1
In this case, no stddev is generated
benchmarks: Fix early_caching_ac formula
benchmarks: Add early_ac formulae to generator
benchmarks: Ignore temporary files when collecting statistics
benchmarks: Set final TIMEOUT and REPEATS parameters
benchmarks: Run mlsolver with -pgs stratimprloc2
benchmarks: Fork a subshell for mlsolver
Otherwise, 'perf stat' returns a zero exit code if mlsolver is killedby a signal (e.g in case of an OOM situation)
benchmarks: Distribute results over different directories
Allows benchmarks of two formula series to be performed in parallelwithout interfering with each other.
benchmarks: Add visual progress feedback
benchmarks: Add script to run 'bench_one_formula' on all formulas
benchmarks: Output numbers with leading zeros
Some csv tools can only sort lexicographically
benchmarks: Save full 'perf stat' output
who knows if we might need it
benchmarks: Set locale to C
This ensures that decimal separators are consistent.
benchmarks: Allow to have multiple directories with benchmark results
benchmarks: Add script to collect results into CSV format
benchmarks: Save output of programs
Allows to collect other results than just the time. For example howmany states the game has and what the result was (sat/unsat).
benchmarks: Add cool with pgsolver support to matrix
benchmarks: Add cool without propagation
benchmarks: Add mlsolver with optimizations to tested programs
benchmarks: Switch mlsolver to 'recursive' strategy
Make propagation rate configurable with command line flag
Adds the parameter --propagationRate
Cache maximum priority of all nodes in graph
So it doesn't have to be recomputed for each propagation.
Unfortunately this optimization doesn't seem to make a difference forthe formulas I tested, but it doesn't hurt either.
Add argument checking to benchmark script
Add benchmark script to compare cool and mlsolver
Remove pgsolver dependency
Implement own parity game solver
Instead of relying on pgsolver for this task.
Use pgsolver from opam instead of bundling it
Simplifies the installation process and allows to compare performancewith other tools that use the same pgsolver version.
Move aconjunctive formula generator to benchmarks/
Add more formula families to gen.ml
generator: Rename formula families to something descriptive
Fix printing of modality of the identity functor
phi generator: Use identity modality for phi
As this speeds things up quite a bit.
phi generator: Add another formula family
CoAlgMisc: Store fixpoint variable name for every deferral
This is only useful for debugging and currently not used anywhere inthe code.
phi generator: Generalize command line syntax
Allows for more variations of the formula and also is a little bitmore self-documenting.
Remove unused code
Fix apply for the partial permutation tracker
- Apply all indices in the map, not only the currently tracked ones.- Apply Stars in the same way as regular formulas
Add negation to generator for phi
Fix formula generator for positive phi
Fix bug in detClosure
gen.ml: Change quantification order
Tried to optimize translation with fixpoint approximation; added depthFormula function in CoAlgFormula
Also available in: Atom