Assertion Failure about iimc

[mgudemann]

This seems to be a race condition, I get 0, 1 or the above error as possible results for this model. When using either --thread_limit 1 or only the KLive tactic -t klive I always get 0 as result, both with iimc direct and within valgrind. Is this your expected result?

Btw. I am not an author of iimc nor am I affiliated with the university of Colorado. I simply keep this repository as the original webpage of iimc is currently offline.

[mgudemann]

I investigated a bit further. The above error is not a race condition, but a disagreement of the GSH and KLive tactics. Actually, GSH changes its result if reductions are applied before. To reproduce:

iimc -t pp -t gsh test.aag

returns 1, while

iimc -t gsh test.aag

returns 0, just as the KLive tactic (with or without reduction). When GSH finds a conclusion before KLive, this is reported in the proofattachment and therefore the assert fails once KLive finishes.

My suggestion is to use the KLive tactic, with preprocessing if required. According to verification with nuxmv / check_ltlspec_klive, the property is true.

[progirep]

Hi Matthias, thanks a lot for investigating this. Since the problem instance was actually constructed fuzz testing of a reactive synthesis tool, I can only trust the other tools (you tried nuxmv, I tried only aigbmc) that the property is really satisfied.

I am also aware that you are not actually an author of this tool - but I filed the bug report anyway since it may be helpful for other researchers and practitioners who want to apply iimc, and they are most likely to see it here. Your description of how to circumvent the problem is definitely helpful, so thanks for the workaround!

[mgudemann]

Ok, thanks for the explanation. It seems that I should really have a look at fuzzing - it even finds bugs in software that is not analyzed! What fuzzing tool do you use?

I am also aware that you are not actually an author of this tool - but I filed the bug report anyway since it may be helpful for other researchers and practitioners who want to apply iimc, and they are most likely to see it here.

I had just wanted to make clear that I'll unlikely be able to fix the code. In any case, I will write to Fabio Somenzi about this issue. There are also other problems with this model, the iictl tactic fails with a violated assert and ic3 reports 1. This is probably understandable, but I think it would be better to have an error message with these tactics.