Re: [Toss-devel] Toss deciding MSO

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

Dear Lukasz,

thanks for your quick reply and the fix!

On 19.01.2015 06:06, Lukasz Kaiser wrote:
> Dear Dmitriy,
>
> first of all, thanks for your email! Before we get to your question,
> let me give you a little background on the code you're asking about.
> It is a bit of a side-project of Toss and it was written together with
> an MSO-checking paper (you probably know that, as it seems you're
> doing a PhD in logic as well).
Yes, I've learned about your interesting CSL'10 paper recently. 
Unfortunately much later than I should have.

> I still hope the code is correct, but
> it has not been touched in a few years. Moreover, we are all working
> in the industry now. So - while I'll try to do my best and help you
> with everything - please take into account that we are not working on
> anything related any more and forgive me if it takes a few days to
> answer.
I understand. Thanks all the more for looking into it, given the situation.

>> 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: [...]
>>
>> Have I got the syntax wrong or is this a bug in the Solver?
> You are definitively right - it was a bug in the solver. But it seems
> to me to be a quite trivial one - the whole solving procedure operates
> under the assumption that variables are properly named. I added a
> check in a most recent commit. It solves the problem above, but - as I
> said - there might be some problems left. Hopefully not too many!
>
> Please, grab the latest commit and check again. I hope this old code
> can still be of any use for anything - let us know if we can help :).
Thanks, I will come back if I find more :-)

Best wishes,
Dmitriy