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: Add dividing example for aconjunctive fragment
tests: Don't use exit status 0 if tests failed
tests: Print summary for failed tests at the end
Makes it easier to find failing formulas for further fine-grainedanalysis.
tests: Add example where new Algorithm should fail
This formula is not aconjunctive and should be wrongly declared assatisfiable by the algorithm that assumes aconjunctivity.
This doesn't work right now: The new algorithm also answers with"unsat".
Add test cases for aconjunctive fragment
This fails currently, because the check for aconjunctivity iscurrently hard coded, ruling out all formulas that aren'taconjunctive.
Add vim modelines to more files
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 lots of test cases for CTL.
This imports some of the quickly decidable ctl comparision benchmarkformulas into the test suite.
The testsuite also gained a --slow parameter, that enables slower (butstill fairly fast) formulas.
Merge branch 'remove-gmlmip'
Disable all testcases involving PML
Add vim modeline to all OCaml files
Get testsuite running again
Fixes the syntax of all tests that use R and B as identifiers, whichare keywords now.
Also disables all tests involving nominals as they are currently allthrowing exceptions.
Fix testsuite for K
R and B are now keywords and were used as identifiers. Now, r andb (lowercase) is used instead in the testcases. For consistency, allother identifiers were lowercased, too.
Merge remote-tracking branch 'origin/master' into flatmu
CL: more test formulas
CL: create enough rule 2 applications
The previous optimization in the rule 2 applications of coalition logicleft out some rule applications. Now, do enough but still do notgenerate unnecessarily many rule applications.
Add init function to testsuite sections
Allow testcase sections to adjust the global settings before evaluatingthe test formulas.
Replace A by a and E by e in testsuite
A and E are syntax elements in CTL"Fixes" the testsuite for K
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...
Add crucial testcases for K*K
Implement testcase skipping to avoid PML crashes
Add failing PML+K testcase
Flush stdout more often in testsuite
Change AtMostProbable to LessProbableThan
The actual box of PML (in GMLMIP) is: less probable than. The Diamondis: At least Probable than.
So now you have ¬[p] C = <p> C.
Add ocaml part of PML rule application
Remove redundancy from testsuite file
Fix name of testsuite section K*KD
Implement more generic functor parsing/printing
Implement sortTable generation
Fix testcase for K*KD and add K+KD cases
Add testcases for K×KD (i.e. for fusion)
Add more testcases for K
Add smallest DL98 testcases to testsuite
Add CL testcases
Add statistics to testsuite output
Add testcases for nominal
Add testcases for KD
Add basic testcase checking
Add basic testsuite skeleton