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