我正在尝试检查以下模型中的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）根据定义的谓词生成实例。但是，当我在第一个模型中运行断言时，生成的反例未遵循第二个模型的谓词中定义的条件。我如何构建/运行一个断言，该断言将考虑先前模型的谓词来检查反例？
先前在以下问题中更详细地解释了模型：
谓词和断言的属性只有在规范中的某个地方被调用时，才会在您生成的实例集中“强制执行”。
在模型2中，您执行的命令（run law6RightToLeft）包含对要查看的谓词的引用。因此，您可以看到生成的实例遵守该谓词的约束。
现在，在第一个模型中，您检查一个独立于该law6RightToLeft谓词的断言。如果要将该谓词中描述的属性强制应用于所生成的实例集，则应将其转换为事实，或在事实中对其进行引用。
本文收集自互联网，转载请注明来源。
如有侵权，请联系[email protected] 删除。
我来说两句