Wrong results for simple formulas

[dtraytel]

Dear Lukáš, Ondřej, and Tomáš^2,

recently, I came across your very interesting TACAS'15 paper: Nested Antichains for WS1S. While I'm not yet through with its technical sections, I gave your tool a try. Unfortunately, I am experiencing problems with the simplest formulas.

The following says UNSATISFIABLE:

ex.mona:
ws1s;
var1 a;
var2 A;
a in A <=> a in A;

./dWiNA ex.mona
./dWiNA --use-mona-dfa ex.mona
./dWiNA --no-expnf ex.mona

The following corner case just segfaults:

true.mona:
true;

./dWiNA --use-mona-dfa true.mona
./dWiNA --no-expnf true.mona

MONA says, of course, valid for both examples.

Or have I got the syntax somehow wrong?

I refer to commit 4bc4895.

Best wishes,
Dmitriy

[tfiedor]

Dear Dmitriy,

thank you for your interest in our approach. The tool is still prototype and during october we implemented the new version, which needs lots of optimizations and is not fully tested, so there may be some bugs. I don't see problem in the syntax, but during the evaluation we didn't work with formulae without variables and with free variables.

I will look more deeply into this formulae in few weeks, as I am currently occupied with different research.

Best regards,
Tomas Fiedor.

[dtraytel]

Dear Tomas,

thanks for the quick reply!

Just for the record, ground formulas with superfluous quantifier, e.g.

all1 a0, a1: a0 = a0;

also currently give unexpected results.

If you wonder why and how I get those funny formulas: I was performing random testing on my own inefficient and tiny implementation (https://github.com/dtraytel/WS1S), and simultaneously trying different tools as well.

Best wishes,
Dmitriy