"check_fsm" command is used in nuxmv shell for checking deadlock conditions in model containing finite domain variables. But in case of models containing infinite domain variables like integers with no range or real variable the model can't be built with "go" command. How can we check for deadlock with "go_msat" command for building the model and further analysis.
Asked
Active
Viewed 64 times
2
-
Good question. You might want to contact `nuXmv` directly about this issue. – Patrick Trentin Jan 16 '19 at 09:04