Extension for nuXmv

[haspltom]

Hello,

nice tool and features!

Is it planned to extend the tool to be able to handle xmv-output as well?
Or if not, can you may make suggestions how to tackle this the best way?

Best regards
Thomas

[igor-buzhinsky]

Hi Thomas,

Thanks!

In simple cases, nuXmv output will be accepted due to having the same format as the one of NuSMV. If you need some nuXmv-specific features, the answer depends on these exact features. Adding support of rationals would be relatively easy. Adding support of timed traces would be more troublesome, but I believe that it is possible.

What exactly would you like to be supported? It it is a simple thing, maybe I can add it. If it is less simple, I can advise which pieces of code need to be modfied to implement it.

This tool is no longer actively developed. On the other hand, there is another tool: https://github.com/ShakeAnApple/cxbacktracker, which is. In short, it explains counterexamples not only on the formula, but also on the diagram of modules. nuXmv support is one of the options for future development of this tool.

[haspltom]

Hello.

Thanks for your reply.

We tried to use the tool with a nuXmv output and the error message we got, was that real values are not supported.
So, this would be the first feature we favor.
Appart from that, it is hard to say, what else features would be needed as we do not get over this first error message.
We definitely do not use timed nuXmv currently.

Thanks anyways for your suggestion for the other tool, we are currently trying this as well.

Best regards
Thomas

[igor-buzhinsky]

Hi,

I added support of reals. Files like this should now be supported: https://github.com/igor-buzhinsky/nusmv_counterexample_visualizer/blob/master/example-input-nuxmv-reals.txt
However, I haven't thoroughly tested this feature, I am going to do this on Wednesday. If there are things that I am missing, please let me know.

[igor-buzhinsky]

Hi,

I haven't found any more bugs. Reals should work.

[haspltom]

Very cool, thanks!
Simple nuXmv output with reals works fine now.