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 8 years ago and Hans-Peter Deifel committed 7 years ago

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

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.

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.

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.

Hans-Peter Deifel authored 8 years ago and Hans-Peter Deifel committed 8 years ago

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.

Hans-Peter Deifel authored 8 years ago and Hans-Peter Deifel committed 8 years ago

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.

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.

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

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

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
missing rule and lets cool correctly answer the following query:

    $ ./coalg.native sat CL --agents '1' <<< '(~[{1}] p) & ~[{1}] ~p'
    unsatisfiable

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.