合金：执行不同运行命令范围的紧凑Java程序

Question

假设我想创建一个Java程序来执行多个Alloy运行，为每个循环更改它们的作用域值（整数从0到9），以检查哪个将花费更少的时间解决方案。

请注意，该命令实际上是相同的，我的意思是，只有范围的值（以及保留字“完全”的存在/不存在）会有所不同。

下面是一个数字例子：

1st run → command: run MyPred for 3 but 5 Int, exactly 1 Sig_Scope1, 1 Sig_Scope2, exactly 1 Sig_Scope3 
2nd run → command: run MyPred for 4 but 5 Int, 2 Sig_Scope1, exactly 2 Sig_Scope2, exactly 2 Sig_Scope3 
3rd run → command: run MyPred for 4 but 5 Int, 2 Sig_Scope1, exactly 1 Sig_Scope2, 1 Sig_Scope3 

依此类推，直到迭代（假设10）的最大数量已经达到。

10th run → command: run MyPred for 4 but 5 Int, 0 Sig_Scope1, exactly 2 Sig_Scope2, 0 Sig_Scope3 

程序的输出将是这样的：

1st run. Found solution: Yes. Spent time: 17 seconds 
2nd run. Found solution: No. Spent time: [it may take a time until the Alloy analyzer is going to return no solution] 
3nd run. Found solution: No. Spent time: [it may take a time until the Alloy analyzer is going to return no solution] 
... 
9th run. Found solution: Yes. Spent time: 21 seconds 
10th run. Found solution: Yes. Spent time: 10 seconds 

在这里，我想经过一个伪代码，但也有不少作品（文字题）我不知道怎么的实施它或我怎样才能找到更多的学习材料：

... 
A4Reporter rep = new A4Reporter() {...} 
... 
Module world = CompUtil.parseEverything_fromFile(rep, null, filename); //reading Alloy filename. 
... 
A4Options options = new A4Options(); //Analyzer’s options. 
... 
Command command: world.getAllCommands(); //I’am looking for Alloy’s ‘run’ commands, for instance, the first run command would be: run MyPred for 3 but 3 Int, exactly 1 Sig_Scope1, 1 Sig_Scope2, exactly 1 Sig_Scope3 
... 
Int max_number_of_runs = 10; 
for(i = 0; i < max_number_of_runs; i++) { 
    A4Solution ans = TranslateAlloyToKodkod.execute_command(rep, world.getAllReachableSigs(), command, options); //get all Signatures, fine :) 
    System.out.println(ans); //printing the whole command. 
    if (ans.satisfiable()) { 
     //How can I get the amount of time (in seconds) to found a solution as an integer or String? 
     //Getting the label of the Sigs. I have got this way, however I do not know if it is the right one. 
     SafeList<Sig> sigs = ans.getAllReachableSigs(); 
      for (Sig sig : sigs) { 
       System.out.println(sig.shortLabel()); 
      } 
     //For each Sig how can I get their values? 
     //How can I build a new command (Command new_built_command) for the next run? The values of scope Sig will come from a list or they will be generated through Java Random class (I mean a know how to generate random integers). 
     command = new_built_command; 
    } else { 
     //A message that the current command did not find a solution as a String! 
    } 
} 

请问你能帮我解答一下吗？

Answer 1

如何建立一个新的命令

你可以看到ExampleUsingTheAPI使用合金API构建合金模型的例子。使用该API，您可以编程构建一个Command以运行。或者，您可以从文本形式的Alloy模型开始，使用CompUtil.parseEverything_fromString对其进行解析，然后在原始Alloy模型上执行字符串查找替换来更新命令，然后重新开始。

对于每个Sig，我如何得到它们的值？

见ExampleCompilingFromSource，线路44基本上，一旦你得到一个A4Solution对象，你可以调用eval方法它来评估对找到的解决方案的任何表达式（如果你传递一个Sig对象，你会得到它的在解决方案中的价值）。

如何，我可以得到（单位：秒），以找到一个解决方案为整数或字符串的时间是多少？

我不确定A4Solution包含任何关于解决时间的信息，所以在这种情况下，你必须自己测量时间。