alloy - 从字符串中解析包含原子的表达式

Question

CompUtil.parseOneExpression_fromString 方法给出以下错误:无法找到名称“Atom$0” 当解析的字符串包含表达式时直接包含原子的标签。

这是可以理解的，因为单独的原子不是直接在模块级别定义的，而是在实例查找过程中“生成”的。

但是!可以使用 Alloy Visualizer 附带的控制台计算器直接计算包含原子的表达式。

那么 API 中用于在包含原子的表达式中求值的方法是什么。

导致前面提到的错误的代码示例:

Expr e=CompUtil.parseOneExpression_fromString(module, "Atom$0.field"); 
solution.eval(e); 

Answer 1

您的示例中的 parseOneExpression_fromString 调用失败，因为您不能真正期望能够在 module 对象(仅代表您的模型和对该模型的任何解决方案一无所知)。一旦你得到一个解决方案，你就可以将所有的原子和骨架名称添加到模块对象中，然后你就可以解析包含原子名称的表达式。

module = CompUtil.parseEverything_fromFile(...);
solution = A4SolutionReader.read(module.getAllReachableSigs(), ...);
for(ExprVar a:solution.getAllAtoms())   { module.addGlobal(a.label, a); }
for(ExprVar a:solution.getAllSkolems()) { module.addGlobal(a.label, a); }