解析從字符串

Question

方法CompUtil.parseOneExpression_fromString含有的原子的表達提供了以下錯誤：名稱「原子$ 0」無法找到當解析的字符串包含含有一個原子的標籤的表達直。

這可以理解，因爲單獨的原子不是直接在模塊級別定義，而是在實例查找過程中「生成」。

但是！可以使用與Alloy Visualizer一起使用的控制檯評估器直接評估包含原子的表達式。

那麼API中用於評估解決方案的方法是什麼，包含原子的表達式。

代碼示例，導致前面提到的錯誤：

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

Answer 1

，因爲你不能真正期望能夠在module對象找到一個原子名parseOneExpression_fromString呼叫你的榜樣失敗（代表只有你的模型，並且對該模型的任何解決方案一無所知）。一旦獲得解決方案，您可以將所有原子和skolem名稱添加到模塊對象，然後您將能夠解析包含原子名稱的表達式。

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); }