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
added translation for Const
oasis: Correctly declare TCSLib dependency for pgsolver
translation only uses subformulas if their negation is not a subformula
added optimized translation
nom2fix and solveNom
translation from nominal to EG AF works for K
added VAR to patternmatching
Translation for K
translation calculates fisher ladner closure correctly
tried to use Fischer-Ladner Closure but not working yet
part 1 and 3 of translation
first part of translations is implemented
Replace String.split_on_char with custom implementation
String.split_on_char was introduced in OCaml 4.04, but we want tosupport 4.02.
Move verifyFormula after simplification
Enforce aconjunctivity globally
In the future, we would need a switch for that
Add script to generate test formulas
- gen.ml: Generates a specific set of formulas, usable for benchmarking cool against pgsolver
Disable debug output
Fix alternation level computation
Disable backjumping for now
Temporarily add some debug output
Fix priority for empty foci
Swap priorities of partial permutations
Since the automaton must be complemented, our priorities have to bejust the other way round.
Include priority of nodes in dot output
Correctly add new formulas if deferral changes
Enable new focus tracking by default
- In the future this should only happen if the formula is not alternation free, but aconjunctive (or via a cli-switch)
Fix a few bugs with the new focus tracker
Actually use depth first tracking
Implement depth-first tracking for deferral sets
was accidentally left uninitialized
First try at depth first tracking
Properly calculate priority for partial permutations
- Compute n based on the size of the Fischer-Ladner-Closure and maximum alternation depth of the input formula- Handle the case where no formula has been removed or is active
Calculate and save alternation depth of input formula
Implement equality and hashing for partial permutations
First implementation of tracking for partial permutation
Expose computed alternation level for other modules
Calculate alternation level for every formula
Actually used polymorphic focus tracking
Modularize reasoner by focus tracking strategy
Set states without children to Sat early
We can set states without children to Sat right after we expand them.
Correctly represent root Core in parity games
In the two games we solve, expandable cores are represented either asthemselves or as the successful node. Unfortunately the root node wasalways represented as itself, leading to wrong results. This is nowfixed.
Change game algorithm from Stratimprlocal2 to Stratimprlocal
As the former is not deterministic
Add a single satisfiable game node to states without children
Only iterate through open states in PG solution
Remove last call to propagateUnsatMu
Keep node mapping to parity game on the fly
Don't set all expandable cores to unsat
namely those that have children
Solve game twice to accommodate for partial games
WIP: First steps towards using pgsolver
Also available in: Atom