We can set states without children to Sat right after we expand them.

In the two games we solve, expandable cores are represented either as
themselves or as the successful node. Unfortunately the root node was
always represented as itself, leading to wrong results. This is now
fixed.

As the former is not deterministic

namely those that have children

A parity game solver that will be used to solve games arising from the
full mu-calculus.

- Adds a new submodule under `vendor/` for pgsolver. Linking without
  including it in the source proved difficult at the moment.
- Adds a new library `libpgsolver` to _oasis that contains the files
  from pgsolver that we need in cool.

The user can now choose which fragment of the mu-calculus the reasoner
uses. More specialized fragments can have better performance
characteristics.

Adds a new module CoolUtils.Args that implements a generic command
line argument parser. This makes it easier to add new options to the
main program.

- Read only one formula, we also only generate one graph
- Don't print a prompt or the satisfiability result

This allows to redirect the output graph to a file or directly to dot.

Adds a whole new set of tests that don't just test the whole reasoning
process on a formula, but smaller individual functions.

Right now there are only two tests but more should follow.

Enables 'make test' and 'ocaml setup.ml -test' to run the testsuite.

Adds many new targets including 'test' and 'distclean'

Previously, the algorithm for the aconjunctive fragment would insert
many cores for each child of a modal rule and add those as children of
the rule application to the state.

This was wrong for multiple reasons:

1. Dependency tracking for the backjumping implementation assumes that
   the number of children of a rule application is fixed
2. Propagation with multiple children computes an OR of the children
   instead of AND

Now, for each modal rule application multiple rules are added as
children of the state, each with the cores of the original rule paired
with every possible combination of deferrals.

Makes it easier to find failing formulas for further fine-grained
analysis.

This formula is not aconjunctive and should be wrongly declared as
satisfiable by the algorithm that assumes aconjunctivity.

This doesn't work right now: The new algorithm also answers with
"unsat".

Previously, cool would simply raise an exception if the formula was
not aconjunctive. This was done to ease testing of the new reasoner
algorithm.

Now, the reasoner decides whether the formula is aconjunctive or not
and uses a specific algorithm based on the result.

Hans-Peter Deifel authored 7 years ago and Hans-Peter Deifel committed 7 years ago

This fails currently, because the check for aconjunctivity is
currently hard coded, ruling out all formulas that aren't
aconjunctive.

Hans-Peter Deifel authored 7 years ago and Hans-Peter Deifel committed 7 years ago

For the aconjunctive fragment, we replace the generation of a single
core with all tracked deferrals by the generation of multiple cores,
each annotated with a single deferral from the above set.

0 and 1 are used for Sat and Unsat respectively. But if the child
throws an exception, another exit status is returned which the parent
now recognizes.

As it stands, cool leaks tons of memory with each `isSat` call. Until
this is fixed, the new `--slow` testsuite would need at least 16GB of
memory if all formulas are decided in one process. Thus, we now call
isSat in a new child-process and allow the OS to reclaim memory after
the child exits.

NB: This uses the Unix.fork API, which is not available on Windows.

This imports some of the quickly decidable ctl comparision benchmark
formulas into the test suite.

The testsuite also gained a --slow parameter, that enables slower (but
still fairly fast) formulas.