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