spin - SPIN 现在是否支持 CTL 来表达约束？

Question

我用谷歌搜索了一段时间，发现一些论文提出了 CTL 或 CTL* 模型检查 SPIN。但是，根据 Promela 手册页，没有办法在 Promela 模型中表达 CTL。现在只是提案级别吗？

Answer 1

我几个月前才用过它，但回来确认一下。在浏览了他们最近的发行说明之后，我不得不说不。它仍然只支持检查 LTL 属性，除非您可以访问某些研究项目。

Answer 2

是的，提议/承诺。尽管如此，您也许可以通过将其编译为 NuSVM https://code.google.com/archive/p/s2n/来验证 Promela 上的 CTL