Project

General

Profile

Statistics
| Branch: | Revision:

cool / src / testsuite @ 1d36cd07

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

c9ed384b 03/22/2017 02:09 PM Hans-Peter Deifel

Merge branch 'remove-gmlmip'

2ed7312f 03/22/2017 02:05 PM Hans-Peter Deifel

Disable all testcases involving PML

a57eb439 03/21/2017 09:12 PM Hans-Peter Deifel

Add vim modeline to all OCaml files

9fdc9f4d 03/16/2017 07:08 PM Hans-Peter Deifel

Get testsuite running again

Fixes the syntax of all tests that use R and B as identifiers, which
are keywords now.

Also disables all tests involving nominals as they are currently all
throwing exceptions.

3c42e3f1 03/16/2017 07:08 PM Hans-Peter Deifel

Fix testsuite for K

R and B are now keywords and were used as identifiers. Now, r and
b (lowercase) is used instead in the testcases. For consistency, all
other identifiers were lowercased, too.

e01c4a03 05/14/2016 05:10 AM Christoph Egger

Merge remote-tracking branch 'origin/master' into flatmu

4c4531ea 02/11/2016 05:19 PM Thorsten Wißmann

CL: more test formulas

c1a08c36 02/11/2016 05:08 PM Thorsten Wißmann

CL: create enough rule 2 applications

The previous optimization in the rule 2 applications of coalition logic
left out some rule applications. Now, do enough but still do not
generate unnecessarily many rule applications.

9944c81b 02/11/2016 04:46 PM Thorsten Wißmann

Add init function to testsuite sections

Allow testcase sections to adjust the global settings before evaluating
the test formulas.

99d301af 02/09/2016 11:40 AM Christoph Egger

Replace A by a and E by e in testsuite

A and E are syntax elements in CTL
"Fixes" the testsuite for K

9609611d 02/05/2016 02:00 PM Thorsten Wißmann

Fix CL for diamond formula sets with all agents

For the case of two (or more) diamond formulas who all mention the full
agent list, no rule was created, because the former CL algorithm only
created rules for proper subsets of the agent list. This adds the...

ea6ba714 07/06/2015 04:35 PM Thorsten Wißmann

Add crucial testcases for K*K

ce35fe09 02/05/2015 04:00 AM Thorsten Wißmann

Implement testcase skipping to avoid PML crashes

72e541b6 07/21/2014 02:42 PM Thorsten Wißmann

Add failing PML+K testcase

aadc6a87 07/21/2014 02:33 PM Thorsten Wißmann

Flush stdout more often in testsuite

c855ba91 07/21/2014 11:34 AM Thorsten Wißmann

Change AtMostProbable to LessProbableThan

The actual box of PML (in GMLMIP) is: less probable than. The Diamond
is: At least Probable than.

So now you have ¬[p] C = <p> C.

eda515b6 07/21/2014 11:05 AM Thorsten Wißmann

Add ocaml part of PML rule application

910d5f05 07/21/2014 10:55 AM Thorsten Wißmann

Remove redundancy from testsuite file

afec59bf 07/17/2014 12:00 PM Thorsten Wißmann

Fix name of testsuite section K*KD

db23edf7 07/16/2014 02:50 PM Thorsten Wißmann

Implement more generic functor parsing/printing

68ba7342 07/16/2014 02:28 PM Thorsten Wißmann

Implement sortTable generation

9a28ed81 07/16/2014 01:53 PM Thorsten Wißmann

Fix testcase for K*KD and add K+KD cases

c41abd35 07/16/2014 12:08 PM Thorsten Wißmann

Add testcases for K×KD (i.e. for fusion)

5043b258 07/16/2014 12:08 PM Thorsten Wißmann

Add more testcases for K

f71032c3 07/11/2014 03:01 AM Thorsten Wißmann

Add smallest DL98 testcases to testsuite

2483bba8 05/16/2014 09:11 PM Thorsten Wißmann

Add CL testcases

dcb82f00 05/16/2014 09:04 PM Thorsten Wißmann

Add statistics to testsuite output

ee45f2fd 05/16/2014 08:49 PM Thorsten Wißmann

Add testcases for nominal

abc6c263 05/16/2014 08:43 PM Thorsten Wißmann

Add testcases for KD

ab2d3adc 05/16/2014 08:18 PM Thorsten Wißmann

Add basic testcase checking

b33c1f3f 05/16/2014 07:22 PM Thorsten Wißmann

Add basic testsuite skeleton