Alloy - 从.als生成.xml实例

Question

我需要在程序中从.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包中找到