假設一個聲明，我們有兩個模塊A和B，（A在B打開）如何在給定的解決方案評估不同的模型不是用來生成aforementionned解決方案
您生成一個解決方案的謂詞來自A，並且在B中有一些參數化謂詞，只有關於A BUT的元素的原因，因爲某些原因，您不能將這些謂詞放在模塊A中。
如何評估在從B生成的解決方案中聲明的謂詞一個 ？
這裏有以下步驟我跟着來嘗試實現這一目標（失敗）
IF謂詞體不包含到模塊A的元件的任何參考然後，評價是成功的。 ELSE它產生的那種致命的錯誤：
字段「字段（SIG <：場）」翻譯過程中沒有被綁定到一個法律價值。
我設法評估在模塊中聲明的謂詞，它與用於生成解決方案的模塊不同，但只能通過在字符串級別工作來解決骯髒的解決方法。
下面是我遵循的步驟：
提取所有謂詞的身體和他們映射到他們的名字（通過解析文件自己）
抽提液所需要的參數的名稱通過使用Alloy API的謂詞（更方便，但也可以通過直接解析模塊的內容來檢索）
在每個主體（在步驟1中恢復）中替換參數n通過期望的表達方式（在步驟2中恢復）。 （你希望與你的論點相關聯的值，無論是sig，原子還是任何其他合金表達式）
解析3中獲得的合金表達式（使用CompUtil.parseOneExpression_fromString）並在其中評估解決方案。
髒兮兮，但工作... ;-)
您生成來自A的解決方案，並有B中的一些參數化的謂詞，大約只有A的元素，但因爲某些原因考慮，您不能把那些謂詞的模塊A.
不，你不能那樣做。當您獲得模塊A的解決方案時，解決方案將不知道有關模塊B的任何內容（因爲A不包含/打開B），所以您無法從B獲取謂詞，並根據A的解決方案對其進行評估。
我明白你的觀點，爲什麼你在概念上認爲你應該能夠做到這一點。看起來合理的是，你可以在一個單獨的文件中存儲一些額外的謂詞，然後再讀取它們並將它們解析成表達式，因爲一般情況下，你應該能夠針對任何解決方案評估任何表達式，你可能期望你的原始場景能夠工作。然而，實際上，當你解析來自B的談論關於A的一些sig或字段的謂詞時，表示該sig /字段的對象與從同一個sig /字段解析時的對象在物理上是不同的模塊A。因此，你會得到一個錯誤，說「sig/field沒有綁定到合法的值」，只是因爲「other」sig/field存在一個綁定，而不是你傳遞的綁定。