model-checking - 使用 nuSMV 进行假设担保的感应

Question

我有一个异步对称环形协议，它有 5 个满足给定属性的进程。我想证明（或获得反例）该属性对于具有 6 个或更多进程的协议是正确的；那是

∀n.φ(n)

我决定使用假设保证，并nuSMV用于模型检查。

我知道以前版本的SMV可以Cadence支持此功能，但是有什么方法可以实现假设保证nuSMV吗？
如果没有，我可以使用其他模型检查器SPIN吗？

谢谢你。