title: Alloy - Dealing with unbounded universal quantifiers
body: <p>Good afternoon,</p>
  
  <p>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):</p>
  
  <pre><code>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
  </code></pre>
  
  <p>Producing a counterexample such as:</p>
  
  <pre><code>Set = {(S0),(S1)}
  Element = {(E0),(E1)}
  s0 = {(S0)}
  s1 = {(S1)}
  elements = {(S0,E0), (S1,E1)}
  </code></pre>
  
  <p>where the analyser didn't populate Set with enough values (a missing Set atom, S2, containing the union of S0 and S1).</p>
  
  <p>Two solutions to this general problem are suggested then in the book:</p>
  
  <p>1) Declaring a generator axiom to force Alloy to generate all possible instances. 
  For example:</p>
  
  <pre><code>fact SetGenerator{
    some s: Set | no s.elements
    all s: Set, e: Element |
      some s': Set | s'.elements = s.elements + e
  }
  </code></pre>
  
  <p>This solution, however, produces a scope explosion and may also lead to inconsistencies.</p>
  
  <p>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.</p>
  
  <p>My question is: is there any specific rule to choose any of these solutions? It isn't clear to me from the book.</p>
  
  <p>Thanks.</p>