Skip to content

Add lexer for NuSMV/nuXmv model checker language#2135

Open
deme3 wants to merge 1 commit intorouge-ruby:masterfrom
deme3:feature.add_nuxmv_lang
Open

Add lexer for NuSMV/nuXmv model checker language#2135
deme3 wants to merge 1 commit intorouge-ruby:masterfrom
deme3:feature.add_nuxmv_lang

Conversation

@deme3
Copy link

@deme3 deme3 commented Jun 11, 2025

This MR adds support for the nuXmv/NuSMV/SMV model checkers input language.

nuXmv is a superset and an enhancement over the NuSMV model checker, both of which developed by Fondazione Bruno Kessler, a research institute in Trento (IT). In turn, NuSMV originated by Carnegie Mellon University's "SMV", a symbolic model checker supporting CTL.

Not sure if relevant to the scope of reviewing the merge request, but fyi: Language reference is in User Manuals for both programs, which are listed here: https://nuxmv.fbk.eu/documentation.html.

Adding this language, it being a superset of the two previous languages mentioned, will virtually add support for all of them. (Note the aliases provided by the lexer are in fact: nuxmv, nusmv, and smv)

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant