实用地将合金实例导出到文件答案

【问题标题】：Pragmatically export Alloy Instances to a file实用地将合金实例导出到文件
【发布时间】：2017-09-20 13:30:12
【问题描述】：

我有一个合金模型。该模型是我编写的软件中的一些决策逻辑。在该模型中，我有一些创建示例的谓词。谓词创建预期行为和超出预期行为的实例。我很乐意将这些示例作为我的代码单元测试的输入。

有没有人有一些软件的例子，它与 Alloy 交互以将生成的许多例子转储到一个文件中？我很想运行一个程序，获取一个包含许多实例的文件，然后将该文件用作我的测试程序的输入。

这让我很感兴趣，因为创建的示例和反例通常不是我在手写测试输入时想要做的。

想法？

【问题讨论】：

标签： alloy

【解决方案1】：

您可以在“文件/导出到”菜单中导出实例。

如果您可以使用 Java 工作，那么知道我们正在 github 上建立一个开源 repo 可能会很有趣：https://github.com/AlloyTools/

我认为将您的代码与此代码链接并生成您的测试用例或从适当的文件中提供它们非常容易。

我对 Alloy 的这种应用非常感兴趣，所以请随时关注我们https://groups.google.com/forum/#!forum/alloytools

【讨论】：

我更喜欢 Java，这是一个好兆头！我应该查看 repo 的哪一部分？
我对 Alloy 代码很陌生，但我创建了 repo。我们将快照发布到oss.sonatype.org/content/repositories/snapshots repo 中的 org.alloytools:org.alloytools.alloy.dist:5.0.0-SNAPSHOT。如果你把它放在你的类路径中，你就会拥有所有的合金代码，包括本机 SAT 求解器。我会看看github.com/AlloyTools/org.alloytools.alloy/blob/…。 A4Solution 包含一组具有当前解决方案的元组。