2

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

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

如何在 Alloy 中构建递归谓词/函数

通过传递闭包以递归方式使用 Alloy 函数

4

1 回答 1

2

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

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

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

于 2015-11-13T08:54:11.313 回答