Странное поведение при проверке утверждений в сплаве

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. Если вы хотите применить свойства, описанные в этом предикате, к вашему набору сгенерированного экземпляра, вы должны, таким образом, преобразовать его или ссылаться на него в факте.