我想用 Python 编写一个可扩展的程序，该程序将根据用户输入创建合金模型。特别是，我希望用户输入一个图形并使用 Alloy 告诉用户该图形是否具有欧拉路径。我已经在 Alloy 中为特定的图形实例准备好了模型。但是，我正在考虑通过 Python 代码生成 .als 文件，然后通过 Python 启动 Alloy 来评估模型。是否有我可以使用的 Alloy API 或任何命令行参数可以帮助我确定某个谓词是否一致？
谢谢
【问题讨论】：
标签： python model logic alloy formal-methods
没有适用于 Python 的 Alloy API。 official API is in Java;可以在here（以及 StackOverflow 上的此处）找到 API 使用示例。还有一个embedding of Alloy in Ruby，它仍处于 alpha 阶段。
【讨论】：
几天前我的一位同事问了我同样的问题。
我开发了一个基于 Alloy API 的小型 Java 程序，该程序将给定 Alloy 模块的路径作为输入，分析输入模块（考虑遇到的第一个命令），并在分析器找到时显示（作为输出）给定模块和命令的可满足实例。
这里是这个非常简单的程序的链接。 https://www.dropbox.com/s/9ekwegj0ltfs8lq/alloy_text-based.jar?dl=0
希望对你有帮助
【讨论】：