是否有一个简单的模型检查器工具。我计划实现一个模型检查器工具,该工具将分析一些预定义属性的代码。
最佳答案
一个重要的工具是 SPIN , 使用 Promela 语言。如果你使用 LaTeX,还有 TLA+ .
这些不会分析您的代码,但会让您表达您的假设和状态转换的模型,然后分析无效状态。换句话说,它们会检测模型中的问题,而不是模型的实现。
我看过Goanna的演示,但我不知道它是否可用(商业或其他);这具有实际分析您的源代码的优势。
看看你的问题,再看看你问题中的评论,听起来你真的应该先阅读一些文献。也许,The Spin Model Checker , 或 Specifying Systems (可从 Leslie Lamport's website 下载)。您需要重新构建问题,这样您就不会尝试解决停机问题。
关于c++ - 简单模型检查器工具,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/218951/