检查 Alloy 中的断言时的奇怪行为

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）根据定义的谓词生成实例。但是，当 i 运行第一个模型中的断言时，生成的反例不遵循第二个模型中谓词中定义的条件。考虑到先前模型的谓词，我如何 build/run 一个将检查反例的断言？

之前在以下问题中更详细地解释了这些模型：

Using Alloy functions in a recursive way through transitive closures

Answer 1

谓词和断言的属性 "enforced" 在您生成的实例集中，仅当后者在您的规范中某处被调用时。

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

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

检查 Alloy 中的断言时的奇怪行为

Strange behavior when checking assertions in Alloy

assertions

alloy

predicates