我们可以在NuSMV中拥有终端状态吗？

Question

是否有可能在NuSMV中有一个没有转换到任何其他状态的状态？例如，在我的代码l3中没有任何转换是有效的吗？当我运行这个NuSMV给我错误“案件条件不详尽”。谢谢！

MODULE main

VAR

location: {l1,l2,l3};


ASSIGN

init(location):=l1;

next(location):= case
             (location = l1): l2;
             (location = l2): l1;
             (location = l2): l3;
             esac;