model-checking - 如何识别包含无限域变量的模型中的死锁条件？

Question

“check_fsm”命令在 nuxmv shell 中用于检查包含有限域变量的模型中的死锁条件。但是如果模型包含无限域变量，例如没有范围的整数或实变量，则无法使用“go”命令构建模型。我们如何使用“go_msat”命令检查死锁以构建模型和进一步分析。