检查合金中的断言时的奇怪行为

Question

我正在尝试在以下模型中检查 verifyingUndefinedFields 断言：

module Tests
open law6_withStaticSemantic

assert verifyingUndefinedFields {
    some fa:FieldAccess | fa.pExp in newCreator && fa.id_fieldInvoked !in fa.pExp.((id_cf.(*extend)).fields)
}

check verifyingUndefinedFields

所呈现的模型又使用了另一个模型：law6_withStaticSemantic。下面是这个模型的一个非常简化的版本：

module TestWithStaticSemantic    
open javametamodel_withStaticSemantic    
sig Left,Right extends Class{}

one sig ARight, BRight, CRight extends Right{}

one sig ALeft, BLeft, CLeft extends Left{}

pred law6RightToLeft[] {
    twoClassesDeclarationInHierarchy[]
    mirroringOfTwoClassesDeclarationsExceptForTheFieldMoved[]
    law6[]
}

pred twoClassesDeclarationInHierarchy[] {...}    
pred mirroringOfTwoClassesDeclarationsExceptForTheFieldMoved[] {...}
... 
run law6RightToLeft for 10 but 10 Id, exactly 2 FieldAccess, exactly 11 Type, 4 Method, exactly 1 Field, 4 SequentialComposition, 8 Expression, 4 Block, exactly 1 LiteralValue

第二个模型（law6_withStaticSemantic）根据定义的谓词生成实例。但是，当我在第一个模型中运行断言时，生成的反例不遵循第二个模型的谓词中定义的条件。考虑到先前模型的谓词，我如何构建/运行将检查反例的断言？

之前在以下问题中对模型进行了更详细的解释：

How to build recursive predicates/functions in Alloy

Using Alloy functions in a recursive way through transitive closures

Answer 1

只有在您的规范中某处调用了后者时，谓词和断言的属性才会在您生成的实例集中“强制执行”。

在模型 2 中，您执行的命令 (run law6RightToLeft) 包含对您希望应用的谓词的引用。因此，您可以看到生成的实例遵守该谓词的约束。

现在，在第一个模型中，您检查一个独立于 law6RightToLeft 谓词的断言。如果您想将此谓词中描述的属性强制执行到您的生成实例集，则应因此将其转换为，或在事实中引用它。