Команда "check_fsm" используется в оболочке nuxmv для проверки условий взаимоблокировки в модели, содержащей конечные доменные переменные. Но в случае моделей, содержащих бесконечные доменные переменные, такие как целые числа без диапазона или вещественной переменной, модель нельзя построить с помощью команды "go". Как мы можем проверить тупик с помощью команды go_msat для построения модели и дальнейшего анализа.