Alloy – 从.als生成.xml实例

我需要在程序中从.als生成随机的.xml实例。 我设法通过在后台运行合金（不可见的JFrame）并调用doOpen，doExecuteLatest和doShowLatest函数来做到这一点。 但每次运行我的代码时都要等合金开始是一件痛苦的事。 我认为如果我只使用合成代码部分执行此程序（我想这将是kodkod）会更有效率。 有谁知道这是怎么做到的吗？ 我发现合金的代码非常令人困惑……

Answer 1

您可以使用Alloy API。 生成实例并将其编写为XML文件可以按照以下步骤轻松完成：

1. 从源文件中读取合金模型。

   model = CompUtil.parseEverything_fromFile（null，null，“yourmodel.als”）;

2. 获取执行命令。 例如 ：

   命令cmd = model.getAllCommands（）。get（0）;

3. 使用步骤2中获取的命令执行模型

   A4Solution解决方案= TranslateAlloyToKodkod.execute_command（null，model.getAllReachableSigs（），cmd，new A4Options（））;

4. 写下在步骤3中生成的解决方案

solution.writeXML（ “路径/到/ your.xml”）;

示例可以在Alloy jar文件的edu.mit.csail.sdg.alloy4whole包中找到