Strange behavior when checking assertions in Alloy

Question

I am trying to check for verifyingUndefinedFields assertion in the following model:

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

The model presented in turn uses another one: law6_withStaticSemantic. Below, there is a very simplified version of this model:

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

The second model (law6_withStaticSemantic) generates instances according the predicates defined. However, when i run the assertion in the first model, the counterexamples generated do not follow the conditions defined in the predicates of the second model. How can i build/run an assertion that will check for a counterexample considering the predicates of the previous model?

The models were explained in more detail previously in the following questions:

How to build recursive predicates/functions in Alloy

Using Alloy functions in a recursive way through transitive closures

Answer 1

Properties of predicate and assertion are "enforced" in your set of generated instances only if those latter are called somewhere in your specification.

In model 2, the command you execute (run law6RightToLeft) contains a reference to the predicate you want to see applied. You can thus see that instances generated abide to the constraints of that predicate.

Now, in the first model, you check an assertion which is independent from this law6RightToLeft predicate. If you want to enforce the properties described in this predicate to your set of generated instance, you should thus convert it to, or refer to it in a fact.