How to build recursive predicates/functions in All

Question

I am trying to generate in Alloy two sets of classes, for instance, classes before a refactoring application and classes after a refactoring application. Suppose in the first set we have the following classes:

ALeft -> BLeft -> CLeft    
                  Class1
                  Class2 -> Class3
                         -> Class4

meaning that ALeft is the parent of BLeft which in turn is the parent of CLeft, Class1 and Class2, which in turn is the parent of Class3 and Class4.

On the other hand, following the same reasoning, we have in the second set the following group of classes:

ARight -> BRight -> CRight
                    Class1'
                    Class2' -> Class3'
                            -> Class4'

Since each set represent the same classes but in different chronological order (different states), it is necessary to guarantee the corresponding equivalences, such as Class1 and Class1' are equivalent meaning that they have the same fields, methods, and so on (consider that the refactoring occurs only in B and C classes) . For the same reasoning, Class2 and Class2', Class3 and Class3', Class4 and Class4' are also equivalent. In addition, we should have an equivalence among the methods in Left and Right classes. For instance, if we have a Left class method like:

public int leftClassMethod(){
    new ALeft().other();
}

Then, there must be a corresponding Right class method like:

public int rightClassMethod(){
    new ARight().other();
}

As suggested by Loic (in this discussion list), the equivalence of these classes started to be guaranteed but we have to complement the predicate classesAreTheSame below, in order to also guarantee the equivalence of their methods. Consider the model below:

abstract sig Id {}

sig ClassId, MethodId,FieldId extends Id {}

one sig public, private_, protected extends Accessibility {}

abstract sig Type {}

abstract sig PrimitiveType extends Type {}

one sig Long_, Int_ extends PrimitiveType {}

sig Class extends Type {
    id: one ClassId,
    extend: lone Class,
    methods: set Method,
    fields: set Field,
}

sig Method {
    id : one MethodId,
    param: lone Type,
    return: one Type,
    acc: lone Accessibility,
    b: one Block
}

sig Block {
    statements: one SequentialComposition
}

sig SequentialComposition {
    first: one StatementExpression,
    rest: lone SequentialComposition
}

abstract sig Expression {}
abstract sig StatementExpression extends Expression {}

sig MethodInvocation extends StatementExpression{
    pExp: lone PrimaryExpression, 
    id_methodInvoked: one Method
}

sig AssignmentExpression extends StatementExpression {
    pExpressionLeft: one FieldAccess,
    pExpressionRight: one {Expression - newCreator - VoidMethodInvocation - PrimaryExpression - AssignmentExpression }
}

abstract sig PrimaryExpression extends Expression {}

sig this_, super_ extends PrimaryExpression {}

sig newCreator extends PrimaryExpression {
    id_cf : one Class
}

sig FieldAccess {
    pExp: one PrimaryExpression,
    id_fieldInvoked: one Field
}

sig Left,Right extends Class{}

one sig ARight, BRight, CRight extends Right{}

one sig ALeft, BLeft, CLeft extends Left{}

pred law6RightToLeft[] {
    twoClassesDeclarationInHierarchy[]
}

pred twoClassesDeclarationInHierarchy[] {
     no disj x,y:Right | x.id=y.id
     Right.*extend & Left.*extend=none
     one r: Right | r.extend= none
     one l:Left| l.extend=none

     ARight.extend=none
     ALeft.extend=none
     BRight in CRight.extend
     BLeft in CLeft.extend
     ARight in BRight.extend
     ALeft in BLeft.extend
     #(extend.BRight) > 2
     #(extend.BLeft) > 2
     #(extend.ARight) = 1
     #(extend.ALeft) = 1
     CLeft.id=CRight.id

     all m:Method | m in ((*extend).ALeft).methods => m !in ((*extend).ARight).methods
     all m:Method | m in ((*extend).ARight).methods => m !in ((*extend).ALeft).methods
     some Method
     all r:Right | all l:Left|  (r.extend= none and l.extend=none) implies classesAreTheSameAndSoAreTheirCorrespondingSons[r,l]
}

pred classesAreTheSameAndSoAreTheirCorrespondingSons[right,left: Class]{
    classesAreTheSame[right,left]
    all r: right.^~extend | one l :left.^~extend | classesAreTheSame[r,l] and classesAreTheSame[r.extend ,l.extend]
    all l:left.^~extend | one r :right.^~extend | classesAreTheSame[r,l] and  classesAreTheSame[r.extend ,l.extend]
}

pred classesAreTheSame[r,l: Class]{
    r.id=l.id
    r.fields=l.fields

    #r.methods = #l.methods
    all mr: r.methods | one ml: l.methods | mr.id = ml.id && mr.b != ml.b 
    all mr: l.methods | one ml: r.methods | mr.id = ml.id && mr.b != ml.b 

    all r1: r.methods, r2: l.methods | r1.id = r2.id => 
        equalsSeqComposition[r1.b.statements, r2.b.statements]
}

pred equalsSeqComposition[sc1, sc2: SequentialComposition]{
    equalsStatementExpression[sc1.first, sc2.first] 
    //#sc1.(*rest) = #sc2.(*rest)
}

pred equalsStatementExpression [s1, s2: StatementExpression]{
    s1 in AssignmentExpression => (s2 in AssignmentExpression && equalsAssignment[s1, s2])
    s1 in MethodInvocation => (s2 in MethodInvocation && equalsMethodInvocation[s1, s2])
    s1 in VoidMethodInvocation => (s2 in VoidMethodInvocation && equalsVoidMethodInvocation[s1, s2])
}

pred equalsAssignment [ae, ae2:AssignmentExpression]{
    equalsPrimaryExpression[(ae.pExpressionLeft).pExp, (ae2.pExpressionLeft).pExp]
    equalsPExpressionRight[ae.pExpressionRight, ae2.pExpressionRight]
}

pred equalsPrimaryExpression[p1, p2:PrimaryExpression]{
    p1 in newCreator  => p2 in newCreator && equalsClassesId [p1.id_cf, p2.id_cf]
    p1 in this_ => p2 in this_ 
    p1 in super_ => p2 in super_
}

pred equalsPExpressionRight[e1, e2:Expression]{
    e1 in LiteralValue => e2 in LiteralValue 
    e1 in MethodInvocation => e2 in MethodInvocation && equalsMethodInvocation[e1, e2]
}

pred equalsMethodInvocation[m1, m2:MethodInvocation]{
    equalsPrimaryExpression[m1.pExp, m2.pExp]
    m1.id_methodInvoked.id = m2.id_methodInvoked.id 
    m1.param = m2.param
}

pred equalsVoidMethodInvocation[m1, m2:VoidMethodInvocation]{
    equalsPrimaryExpression[m1.pExp, m2.pExp]
    m1.id_voidMethodInvoked.id = m2.id_voidMethodInvoked.id
    m1.param = m2.param
}

run law6RightToLeft for 10 but 17 Id, 17 Type, 17 Class

My idea was identifying the corresponding methods (leftClassMethod() and rightClassMethod()) through their ids (which is guaranteed to be the same, according to the model). However, the predicate equalsSeqComposition is not working and the situation gets worse when i try to include the rest relation of the signature SequentialComposition in comparison (commented above in the predicate equalsSeqComposition). This last comparison is even more difficult since Alloy do not allow recursion and the same levels of inheritence as ordering is lost when you use transitive closure. Any idea how can i represent this in Alloy?

Answer 1

It is possible to call functions and predicate recursively in Alloy only if the recursion depth does not exeed 3 see : Programming recursive functions in alloy

For your problem, You can emulate the recursion you are trying to specify using the transitive closure operator.

I would rewrite your predicate classesAreTheSameAndSoAreTheirCorrespondingSons as follows :

pred classesAreTheSameAndSoAreTheirCorrespondingSons[right,left: Class]{
    classesAreTheSame[right,left]
    all r: right.^~extend | one l :left.^~extend | classesAreTheSame[r,l] and classesAreTheSame[r.extend ,l.extend]
    all l:left.^~extend | one r :right.^~extend | classesAreTheSame[r,l] and  classesAreTheSame[r.extend ,l.extend]
}

This predicate enforces that the two classes right and left given are the same, and that any classes r/l inheriting (directly or indirectly) right/left has one counter part in the classes l/r inheriting (directly or indirectly) left/right , respectively.

The checkclassesAreTheSame[r.extend ,l.extend] is meant to check that r and l are in the same levels of inheritence as ordering is lost when you use transitive closure.

Here is the small model I designed to play with your problem :

abstract sig Class {
    id: Int,
    extend: lone Class
}{
   this not in this.^@extend
}

sig Left,Right extends Class{}

fact{
     no disj x,y:Right | x.id=y.id
     Right.*extend & Left.*extend=none 
     one r: Right | r.extend= none 
     one l:Left| l.extend=none
     all r:Right | all l:Left|  (r.extend= none and l.extend=none) implies classesAreTheSameAndSoAreTheirCorrespondingSons[r,l]    
}

pred classesAreTheSameAndSoAreTheirCorrespondingSons[right,left: Class]{
    classesAreTheSame[right,left]
    all r: right.^~extend | one l :left.^~extend | classesAreTheSame[r,l] and classesAreTheSame[r.extend ,l.extend]
    all l:left.^~extend | one r :right.^~extend | classesAreTheSame[r,l] and  classesAreTheSame[r.extend ,l.extend]
}

pred classesAreTheSame[r,l: Class]{
    r.id=l.id
}
run {} for exactly 10 Class

Good luck for the rest ;)