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

【问题标题】：Does SPIN support CTL for expressing constraints now?SPIN 现在是否支持 CTL 来表达约束？
【发布时间】：2016-03-11 18:38:01
【问题描述】：

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

【问题讨论】：

【解决方案1】：

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

【讨论】：

【解决方案2】：

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

【讨论】：