CODEWITHSUNDEEP
encodingabstractalloy
qartal
qartal

Reputation: 2064

Encoding abstract keyword semantic in Alloy by constraints

I would like to encode the abstract keyword semantic as a constraint in Alloy (be patient, I need to do this for a reason! :) ). if I have the following code:

abstract sig A {}
sig a1 extends A{}
sig a2 extends A{}

I think its meaning would be as following (I hope I am right!):

sig A {}
sig a1 in A{}
sig a2 in A{}

fact {
   A=a1+a2         //A is nothing other than a1 and a2
   a1 & a2 = none  // a1 and a1 are disjoint
}

so the two above signatures are equal (i.e., would be semantically equal):

I am eager to use the Abstract keyword that Alloy provide to make life easy, But the problem arises when I make A to be a subset of sig O and use abstract keyword:

sig O{}
abstract sig A in O{}
sig a1 extends A{}
sig a2 extends A{}

above syntax returns an error! Alloy complains:"Subset signature cannot be abstract.", so my first question is : Why Alloy does not allow this?

I don't stop and encode abstract keyword semantic (as explained above) , and come to the following code:

sig O{}
sig A in O{}
sig a1 in A{}
sig a2 in A{}

fact {
    A=a1+a2             // A can not be independently instantiated
    a1 & a2 = none      // a1 and a2 are disjoint
}

And this works, and everything is fine :)

Now if I want to add a3 to my Alloy specification, I need to tweak my specification as the following:

sig O{}
sig A in O{}
sig a1 in A{}
sig a2 in A{}
sig a3 in A{}

fact {
    A=a1+a2+3           
    a1 & a2 = none  
    a1 & a3 = none
    a2 & a3 = none
}

But as you see by comparing the two specification above, if I want to continue this, and add a4 in a similar way to my specification, I need to change the fact part even more, and this continues to be hassle! Actually the number of ai & aj =none (for i=1..n) expressions are increasing non-monotonously! i.e., adding a4 force me to add more than one constraint:

fact {
    A=a1+a2+3 +a4           
    a1 & a2 = none  
    a1 & a3 = none
    a1 & a4 = none
    a2 & a3 = none
    a2 & a4 = none
    a3 & a4 = none

}

So my second question: Is there any workaround (or probably simpler way) to do this?

Any comment is appreciated. Thx :)

Upvotes: 0

Views: 133

Answers (1)

C. M. Sperberg-McQueen
C. M. Sperberg-McQueen

Reputation: 25034

On Q1 (why does Alloy not allow extension of subset signatures?): I don't know.

On Q2 (is there a workaround): the simplest workaround is to make a1 ... an be subsignatures (extensions) of A, and find another way to establish the relation of A and O. In the simple examples you have given, O has no subtypes so simply changing A in O to A extends O would work.

If O is already partitioned by other signatures you haven't shown us, then that workaround doesn't work; it's impossible to say what would work without more detail. (Ideally, you want a minimum complete working example to illustrate the difficulty: the examples you give are minimal, and illustrate one difficulty, but they don't illustrate why A cannot be an extension of O.)

[Addendum]

In a comment, you say

The reason [that I used A in O instead of A extends O] is that there is another signature C in O that is not shown here. A and C are not necessarily disjoint, so that is the reason I think I have to use in instead of extend in defining them to be subset of O.

The devil is in the details, but the conclusion doesn't follow from the premises stated. If A and C both extend O, they will be disjoint, but if one uses extend and the other uses in they are not automatically disjoint. So if you want to have A and C each be a subset of O, and A to be partitioned by several other signatures, it is possible to do so (unless there are other constraints not yet mentioned).

sig O {}
abstract sig A extends O {}
sig a1, a2 extends A {}
sig a3, a4 extends A {}
sig C in O {}

Upvotes: 2

Related Questions