Parsing an expression containing an atom from a String

Question

The method CompUtil.parseOneExpression_fromString gives the following error : The name "Atom$0" cannot be found when the String parsed contains an expression containing the label of an atom directly.

This can be understandable as separate atoms are not defined directly at the module level, but are "generated" during the instance finding process.

BUT! It is possible to evaluate expressions containing atoms directly using the console evaluator coming along with the Alloy Visualizer.

What is then the method in the API used to evaluate in a solution, expressions containing atoms.

Code sample that leads to the previously mentioned error:

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

Answer 1

The parseOneExpression_fromString call in your example fails because you can't really expect to be able to find an atom name in the module object (which represents only your model and knows nothing about any solutions of that model). Once you obtain a solution, you can add all atom and skolem names to the module object, and then you will be able to parse expressions containing atoms names.

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