- Apr 20, 2017
-
-
- Apr 14, 2017
-
-
Hans-Peter Deifel authored
We can set states without children to Sat right after we expand them.
-
Hans-Peter Deifel authored
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.
-
- Apr 13, 2017
-
-
Hans-Peter Deifel authored
As the former is not deterministic
-
Hans-Peter Deifel authored
-
- Apr 12, 2017
-
-
Hans-Peter Deifel authored
-
Hans-Peter Deifel authored
-
Hans-Peter Deifel authored
-
- Apr 11, 2017
-
-
Hans-Peter Deifel authored
namely those that have children
-
Hans-Peter Deifel authored
-
- Apr 10, 2017
-
-
Hans-Peter Deifel authored
-
Hans-Peter Deifel authored
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.
-
- Apr 06, 2017
-
-
Hans-Peter Deifel authored
-
Hans-Peter Deifel authored
The user can now choose which fragment of the mu-calculus the reasoner uses. More specialized fragments can have better performance characteristics.
-
-
Hans-Peter Deifel authored
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.
-
Hans-Peter Deifel authored
- 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.
-
Hans-Peter Deifel authored
-
Hans-Peter Deifel authored
-
Hans-Peter Deifel authored
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.
-
Hans-Peter Deifel authored
Enables 'make test' and 'ocaml setup.ml -test' to run the testsuite.
-
Hans-Peter Deifel authored
Adds many new targets including 'test' and 'distclean'
-
Hans-Peter Deifel authored
-
Hans-Peter Deifel authored
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.
-
Hans-Peter Deifel authored
-
Hans-Peter Deifel authored
-
Hans-Peter Deifel authored
Makes it easier to find failing formulas for further fine-grained analysis.
-
Hans-Peter Deifel authored
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".
-
Hans-Peter Deifel authored
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.
-
This fails currently, because the check for aconjunctivity is currently hard coded, ruling out all formulas that aren't aconjunctive.
-
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.
-
Hans-Peter Deifel authored
-
- Mar 31, 2017
-
-
Kristin Braun authored
-
- Mar 27, 2017
-
-
Kristin Braun authored
-
Kristin Braun authored
-
Hans-Peter Deifel authored
-
Hans-Peter Deifel authored
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.
-
- Mar 26, 2017
-
-
Hans-Peter Deifel authored
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.
-
Hans-Peter Deifel authored
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.
-
- Mar 23, 2017
-
-
Kristin Braun authored
-