How to evaluate in a given solution a predicate declared in a different model than the one used to generate the aforementionned solution

Question

Suppose we have two modules A and B, (A is opened in B)

You generate a solution from A, and have some parametrized predicates in B that only reasons about elements of A BUT for some reasons you can't put those predicates in the module A.

How to evaluate the predicates declared in B in the solution generated from A ?

Here are the following steps I follow to try reaching this goal (unsuccessfully)

1. Generate a solution from A
2. Read this solution using all the reachable signatures of B
3. Parse an expression to give as argument based on A
4. Retrieve the predicate declared in B
5. Evaluate the predicate retrieved in step 4 in the solution read in step 2 using the argument defined in step 3.

IF the predicates body do not contain any reference to elements of module A then, the evaluation is successful. ELSE it produces a fatal error of the kind:

Field "field (Sig <: field)" is not bound to a legal value during translation.

Answer 1

I managed to evaluate a predicate declared in a module different than the one used to generate the solution, but only through a dirty workaround by working at the String level.

Here are the steps I followed:

1. Extract the body of all the predicates and mapped them to their name (by parsing the file myself)

2. Extract the names of the argument taken by those predicates using the Alloy API (more convenient, but one could also retrieve those by parsing the content of the module directly)

3. Replace in each body (recovered in step 1) the occurrence of the argument names (recovered in step 2) by the desired expression. (the value you want to associate to your arguments, be it a sig, an atom , or any other alloy expressions)

4. Parse the body obtained in 3 as an Alloy Expression (using CompUtil.parseOneExpression_fromString) and evaluate it in the solution.

Dirty... but working ... ;-)

Answer 2

You generate a solution from A, and have some parametrized predicates in B that only reasons about elements of A BUT for some reasons you can't put those predicates in the module A.

No you can't do that. When you obtain a solution for module A, the solution will not know anything about the module B (since A doesn't include/open B), so you can't fetch a predicate from B and evaluate it against the solution for A.

I understand your point, and why you think that conceptually you should be able to do this. It seems reasonable that you can store some extra predicates in a separate file, then later read and parse them into expressions, and since in general you should be able to evaluate any expression against any solution, you might expect your original scenario to work. In practice, however, what happens is that when you parse a predicate from B that talks about some sig or field from A, the object representing that sig/field is physically different from the object for the same sig/field when it was parsed from module A. Consequently, you get errors saying "sig/field is not bound to a legal value", simply because there exist a bound for the "other" sig/field, but not the one you're passing.