CODEWITHSUNDEEP
scopeassertionuniversalalloyquantifiers
Jesús Galán
Jesús Galán

Reputation: 13

Alloy - Dealing with unbounded universal quantifiers

Good afternoon,

I've been experiencing an issue with Alloy when dealing with unbounded universal quantifiers. As explained in Daniel Jackson's book 'Software Abstractions' (Section 5.3 'Unbounded Universal Quantifiers'), Alloy has a subtle limitation regarding universal quantifiers and assertion checking. Alloy produces spurious counterexamples in some cases, such as the next one to check that sets are closed under union (shown in the aforementioned book):

sig Set {
  elements: set Element
}
sig Element {}

assert Closed {
  all s0, s1: Set | some s2: Set |
    s2.elements = s0.elements + s1.elements
}
check Closed for 3

Producing a counterexample such as:

Set = {(S0),(S1)}
Element = {(E0),(E1)}
s0 = {(S0)}
s1 = {(S1)}
elements = {(S0,E0), (S1,E1)}

where the analyser didn't populate Set with enough values (a missing Set atom, S2, containing the union of S0 and S1).

Two solutions to this general problem are suggested then in the book:

1) Declaring a generator axiom to force Alloy to generate all possible instances. For example:

fact SetGenerator{
  some s: Set | no s.elements
  all s: Set, e: Element |
    some s': Set | s'.elements = s.elements + e
}

This solution, however, produces a scope explosion and may also lead to inconsistencies.

2) Omitting the generator axiom and using the bounded-universal form for constraints. That is, quantified variable's bounding expression doesn't mention the names of generated signatures. However, not every assertion can be expressed in such a form.

My question is: is there any specific rule to choose any of these solutions? It isn't clear to me from the book.

Thanks.

Upvotes: 1

Views: 176

Answers (1)

Daniel Jackson
Daniel Jackson

Reputation: 2768

No, there's no specific rule (or at least none that I've come up with). In practice, this doesn't arise very often, so I would deal with each case as it comes up. Do you have a particular example in mind?

Also, bear in mind that sometimes you can formulate your problem with a higher order quantifier (ie a quantifier over a set or relation) and in that case you can use Alloy*, an extension of Alloy that supports higher order analysis.

Upvotes: 0

Related Questions