alloy - eval() 无法正常工作

Question

尝试在 a4solution 中评估谓词时出现以下错误:

Fatal error in /some/path at line 9 column 2: Field "field (A/Attribute <: type)" is not bound to a legal value during translation.

错误源代码如下:

for(ExprVar a : solution.getAllAtoms()){    
    // additional checks are here to assure that a is of an "appropriate type"
     solution.eval(predicate.call(a));
}

在我徒劳地尝试自己解决这个问题时，我从这个来源阅读了http://code.google.com/p/alloy4eclipse/issues/detail?id=86从文件中读取解决方案的方式可能会导致此问题。但消息来源没有提供更多细节。

我已经创建了我的解决方案对象如下:

        XMLNode xml = new XMLNode(new StringReader(source.getFileContent()));
        this.solution = A4SolutionReader.read(new ArrayList<Sig>(), xml); 

感谢您的支持

Answer 1

问题是要评估的表达式 (predicate.call(a)) 是从一个 CompModule 对象(即 predicate > 函数是从那里获取的)，而根据其计算表达式的解决方案对象不是从同一个 CompModule 获得的，而是从文件中读取的。

一般来说，当从 xml 文件中读取解决方案时，为了安全起见，建议从该 xml 文件中重新读取和重构所有内容，例如，

XMLNode xmlNode = new XMLNode(new File("my_solution.xml"));
String alloySourceFilename = xmlNode.iterator().next().getAttribute("filename");
Module module = CompUtil.parseEverything_fromFile(rep, null, alloySourceFilename);
A4Solution ans = A4SolutionReader.read(module.getAllReachableSigs(), xmlNode);

在某些情况下，只需将信号从原始 CompModule 传递到重构的解决方案就足够了:

XMLNode xmlNode = new XMLNode(new File("my_solution.xml"));
A4Solution ans = A4SolutionReader.read(originalModule.getAllReachableSigs(), xmlNode);