证明可能性

本文探讨了形式化方法中的可能性属性P(x)，它表示"x在模型中可能发生"，这是安全性和活性属性之外的重要第三类属性。作者讨论了如何用可能性属性验证规范的正确性，并指出虽然主流工具如Alloy和TLA+不原生支持P(x)，但简单的可达性属性可以通过A(!x)的反例来验证。