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.

Wrong branch...

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

Fix typo

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

deleted conjunction

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

Initialize arrayAlternationLevel

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