[Toss-devel] Toss deciding MSO

[Dmitriy T. <tr...@in...>]

Dear Toss-developers,

referring to SVN r1932.

I am experimenting with Toss as a decision procedure for MSO on finite 
words.

Currently, to check formulas I hijack your unit test infrastructure. In 
particular,
I enter my formulas in Solver/ClassTest.ml using the predefined 
structure omega.
The is surely a more high-level way to do this (but I haven't had the 
time to find it;
please point me there if it is easy).

Now I have added a following test:

test_check "all a0, |A0, |A1 ( ( ex a1 ( a1 = a0 and |A0(a1) ) ) <-> 
|A0(a0) )" "omega" omega true;

It fails with:
> OUnit: Check  (argument: all a0, |A0, |A1
>  ((not ex a1 (a1 = a0 and |A0(a1)) and not |A0(a0)) or
>   (ex a1 (a1 = a0 and |A0(a1)) and |A0(a0))) on omega)
> expected:
> true
>  but  got:
> false

The formula should however be true, if I interpret the input syntax 
correctly. Below I give the example in MONA's syntax (and indeed MONA 
says "valid" here).

var1 a0;
var2 A0, A1;
(ex1 a1: a1 = a0 & a1 in A0) <=> a0 in A0;

Have I got the syntax wrong or is this a bug in the Solver?

Thanks & best wishes,
Dmitriy