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.