Request for Adding Support for NuXMV
BentleyJOakes opened this issue · 2 comments
Hello,
An industry partner on my side is interested in using FASTEN, but has a requirement of using reals and integers instead of ranges in their solutions.
As far as I understand, this is possible if NuXMV is used as the FASTEN backend, instead of NuSMV.
Right now, I believe using NuXMV is done by replacing the NuSMV binary. However, this still allows the user to use NuXMV keywords, which will fail (as in my issue #27). And the real keyword would not be available.
Kindly, could there be a NuXMV option provided within FASTEN? Such that toggling it switches to "NuXMV mode", where a) the nuxmv binary is used, and b) both the integer and real keywords be allowed?
Please let me know if this is not feasible. Thanks.
Hi Bentley,
there is an initial nuxmv integration in the "com.mbeddr.formal.nusmv" project (there is already com.mbeddr.formal.nuxmv, com.mbeddr.formal.nuxmv.source languages and com.mbeddr.formal.nuxmv.pluginSolution solution). They are not packaged yet in the FASTEN RCP distribution, but this could be easily fixed.
Everything specific to NuXMV shall belong to these languages :-) (in the modular spirit of MPS DSLs stacks)
Please feel free to extend the nuxmv language with what you need - and add them to the build.
Dan
This is now available ... please check and re-open if it is not the case.