假设我们有两个模块A和B，（A在B中打开）
您从 A 生成一个解决方案，并在 B 中有一些参数化谓词，这些谓词仅对 A 的元素进行推理，但由于某些原因，您不能将这些谓词放入模块 A 中。
如何在 A 生成的解决方案中评估 B 中声明的谓词？
以下是我尝试实现此目标所遵循的以下步骤（未成功）
- 从 A 生成解决方案
- 使用 B 的所有可达签名读取此解决方案
- 解析一个表达式作为基于 A 的参数
- 检索 B 中声明的谓词
- 使用步骤 3 中定义的参数评估在步骤 2 中读取的解决方案中在步骤 4 中检索到的谓词。
IF谓词主体不包含对模块 A 元素的任何引用，则评估成功。ELSE它会产生这样的致命错误：
字段“field (Sig <: field>
我设法评估了在与用于生成解决方案的模块不同的模块中声明的谓词，但只能通过在字符串级别工作的肮脏解决方法。
以下是我遵循的步骤：
提取所有谓词的主体并将它们映射到它们的名称（通过我自己解析文件）
使用 Alloy API 提取这些谓词所采用的参数的名称（更方便，但也可以通过直接解析模块的内容来检索这些参数）
将每个主体（在步骤 1 中恢复）中出现的参数名称（在步骤 2 中恢复）替换为所需的表达式。 （您想要与参数关联的值，可以是 sig、atom 或任何其他合金表达式）
将 3 中获得的主体解析为合金表达式（使用 CompUtil.parseOneExpression_fromString）并在解决方案中对其进行评估。
肮脏...但工作...;-)
本文内容由网友自发贡献，版权归原作者所有，本站不承担相应法律责任。如您发现有涉嫌抄袭侵权的内容，请联系:hwhale#tublm.com(使用前将#替换为@)
