CODEWITHSUNDEEP
alloy
Attila Karoly
Attila Karoly

Reputation: 1021

Unexpected results in playing with relations

/*
sig a {
}

sig b {
}
*/

pred rel_test(r : univ -> univ) {
    # r = 1
}

run {
    some r : univ -> univ {
        rel_test [r]
    }
} for 2

Running this small test, $r contains one element in every generated instance. When sig a and sig b are uncommented, however, the first instance is this:

enter image description here

In my explanation, $r has 9 tuples here and still, the predicate which asks for a one tuple relation succeeds. Where am I wrong?

An auxiliary question: are these two declarations equivalent?

pred rel_test(r : univ -> univ)
pred rel_test(r : set univ -> univ)

Upvotes: 1

Views: 95

Answers (2)

Alcino Cunha
Alcino Cunha

Reputation: 186

The problem is that with the Forbid Overflow option set to No the integer semantics in Alloy is wrap around, and with the default scope of 3 (bits), then indeed 9=1, as you can confirm in the evaluator.

With the signatures a and b commented the biggest relation that can be generated with scope 2 has 4 tuples (since the max size of univ is 2), so the problem does not occur.

It also does not occur in the latest build because I believe it comes with the Forbid Overflow option set to Yes by default, and with that option the semantics of integers rules out instances where overflows occur, precisely the case when you compute the size of the relation with 9 tuples. More details about this alternative integer semantics can be found in the paper "Preventing arithmetic overflows in Alloy" by Aleksandar Milicevic and Daniel Jackson.

Upvotes: 2

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

Reputation: 25034

On the main question: what version of Alloy are you using? I'm unable to replicate the behavior you describe (using Alloy 4.2 of 22 Feb 2015 on OS X 10.6.8).

On the auxiliary question: it appears so. (The language reference is not quite as explicit as one might wish, but it begins one part of its discussion of multiplicities with "If the right-hand expression denotes a unary relation ..." and (in what I take to be the context so defined) "the default multiplicity is one"; the conditional would make no sense if the default multiplicity were always one.

On the other hand, the same interpretive logic would lead to the conclusion that the language reference believes that unary multiplicity keywords are only allowed before expressions denoting unary relations (which would appear to make r: set univ -> univ ungrammatical). But Alloy accepts the expression and parses it as set (univ -> univ). (The alternative parse, (set univ) -> univ, would be very hard to assign a meaning to.)

Upvotes: 1

Related Questions