Project

General

Profile

Statistics
| Branch: | Revision:

cool / src / testsuite @ master

Name Size
  ctl
CTLFormulas.ml 1.33 MB
CTLFormulas.mli 149 Bytes
CTLTestCases.ml 488 Bytes
CTLTestCases.mli 113 Bytes
DL98TestCases.ml 13.8 KB
DL98TestCases.mli 125 Bytes
Testsuite.ml 2.6 KB
Testsuite.mli 560 Bytes
cool-testsuite.ml 8.11 KB

Latest revisions

# Date Author Comment
f24367c4 04/06/2017 05:57 PM Hans-Peter Deifel

Add command line flag for fragment

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

c4503f4f 04/06/2017 05:57 PM Hans-Peter Deifel

tests: Add dividing example for aconjunctive fragment

3d2f5068 04/06/2017 05:57 PM Hans-Peter Deifel

tests: Don't use exit status 0 if tests failed

4a20854e 04/06/2017 05:57 PM Hans-Peter Deifel

tests: Print summary for failed tests at the end

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

0d6818bb 04/06/2017 05:57 PM Hans-Peter Deifel

tests: Add example where new Algorithm should fail

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".

bc706b79 04/06/2017 05:56 PM Hans-Peter Deifel

Add test cases for aconjunctive fragment

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

8d9a2669 03/27/2017 08:48 AM Hans-Peter Deifel

Add vim modelines to more files

8c810657 03/27/2017 08:36 AM Hans-Peter Deifel

tests: Throw error if child doesn't return 0 or 1

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.

ad0b75b1 03/26/2017 09:29 AM Hans-Peter Deifel

tests: Run reasoner in new process for each formula

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...

b002efa8 03/26/2017 09:29 AM Hans-Peter Deifel

Add lots of test cases for CTL.

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.

View revisions

Also available in: Atom