Add command line flag for fragment
The user can now choose which fragment of the mu-calculus the reasoneruses. More specialized fragments can have better performancecharacteristics.
tests: Print summary for failed tests at the end
Makes it easier to find failing formulas for further fine-grainedanalysis.
tests: Throw error if child doesn't return 0 or 1
0 and 1 are used for Sat and Unsat respectively. But if the childthrows an exception, another exit status is returned which the parentnow recognizes.
tests: Run reasoner in new process for each formula
As it stands, cool leaks tons of memory with each `isSat` call. Untilthis is fixed, the new `--slow` testsuite would need at least 16GB ofmemory if all formulas are decided in one process. Thus, we now call...
Add vim modeline to all OCaml files
Fix CL for diamond formula sets with all agents
For the case of two (or more) diamond formulas who all mention the fullagent list, no rule was created, because the former CL algorithm onlycreated rules for proper subsets of the agent list. This adds the...
Flush stdout more often in testsuite
Add more testcases for K
Add smallest DL98 testcases to testsuite
Add statistics to testsuite output
Add testcases for KD
Add basic testcase checking
Add basic testsuite skeleton