Generation of apparently inconsistent alloy instances

Question

I am doing a metamodel in alloy for a subset of Java.

Below we have some signatures:

abstract sig Id {}
sig Package{}
sig ClassId, MethodId,FieldId extends Id {}
abstract sig Accessibility {}
one sig public, private_, protected extends Accessibility {}
abstract sig Type {}
abstract sig PrimitiveType extends Type {}
one sig Int_, Long_ extends PrimitiveType {}

sig Class extends Type {
    package: one Package,
    id: one ClassId,
    extend: lone Class,
    methods: set Method,
    fields: set Field
}
sig Field {
    id : one FieldId,
    type: one Type,
    acc : lone Accessibility
}
sig Method {
    id : one MethodId,
    param: lone Type,
    acc: lone Accessibility,
    return: one Type,
    b: one Body
}
abstract sig Body {}
sig LiteralValue extends Body {} // returns a random value
abstract sig Qualifier {}
one sig this_, super_ extends Qualifier {}
sig MethodInvocation extends Body {
    id_methodInvoked : one Method, 
    q: lone Qualifier
}
//        return new A().k();
sig ConstructorMethodInvocation extends Body {
    id_Class : one Class, 
    cmethodInvoked: one Method
}{
    (this.@cmethodInvoked in (this.@id_Class).methods) || (this.@cmethodInvoked in ((this.@id_Class).^extend).methods && (this.@cmethodInvoked).acc != private_)
}
//        return x;
//        return this.x;
//        return super.x;
sig FieldInvocation extends Body {
    id_fieldInvoked : one Field, 
    qField: lone Qualifier
}
//        return new A().x;
sig ConstructorFieldInvocation extends Body {
    id_cf : one Class, 
    cfieldInvoked: one Field
}{
    (this.@cfieldInvoked in (this.@id_cf).fields) || ( this.@cfieldInvoked in ((this.@id_cf).^extend).fields && (this.@cfieldInvoked).acc != private_)
}

In Java language, we can only invoke a method inside a class (through the instantiation of this class) if this method is not a private method. I tried to represent this restriction in my alloy model through the following signature:

sig ConstructorMethodInvocation extends Body {

    id_Class : one Class, 
    cmethodInvoked: one Method
}{
    (this.@cmethodInvoked in (this.@id_Class).methods || this.@cmethodInvoked in ((this.@id_Class).^extend).methods && (this.@cmethodInvoked).acc != private_)

Thus, a ConstructorMethodInvocation signature in alloy tries to represent a construction in java like new A().x(). In addition, method x() can only be invoked if it is not a private method of class A. So, i put the following restriction (inside ConstructorMethodInvocation signature) in order to avoid calling of private methods of class id_Class:

(this.@cmethodInvoked in (this.@id_Class).methods || this.@cmethodInvoked in ((this.@id_Class).^extend).methods && (this.@cmethodInvoked).acc != private_)

However, despite this restriction, the solver insists on generating instances (for ConstructorMethodInvocation) where cmethodInvoked is a private method of id_Class. The same happens likewise with ConstructorFieldInvocation .

Does anybody see what I am doing wrong?

Answer 1

It's because you misplaced parentheses in the appended facts of the ConstructorMethodInvocation sig: the way it is now, you have a top-level disjunction which allows instances where either (cmethodInvoked is in id_Class.methods) OR (it's in id_Class.^extend.methods and not private). If you change that appended facts block to

{
   this.@cmethodInvoked in this.@id_Class.*extend.methods 
   this.@cmethodInvoked.acc != private_
}

you'll get the intended behavior (the star operator (*) is the reflective transitive closure and it basically means the same as the original disjunction you intended to write; you could still use your old constraint and just fix the parentheses).

To check that there can't exist any ConstructorMethodInvocation instances where the method is private, I executed

check {
  no c: ConstructorMethodInvocation {
    c.cmethodInvoked.acc = private_
  }
}

which found no counterexample.