title: Link between Alloy vars. and primary vars. and Alloy relational variables
body: <p>I can't seem to understand the meaning of the <code>vars.</code> and <code>primary vars.</code> numbers that are displayed when solving is done. The Alloy book in section 5.2.1 explains that Alloy relational variables are mapped to boolean variables associated to the tuples of each relation. but I don't understand the correspondence between this definition of variables and the variable counts displayed in the gui. For example when this code is run (I am using the Alloy Analyzer 4.2 build date: 2012-09-25 15:54 EDT.):</p>
  
  <pre><code>sig A {}
  
  pred show {}
  run show for 2
  </code></pre>
  
  <p>it displays </p>
  
  <pre><code>0 vars. 0 primary vars. 0 clauses.
  </code></pre>
  
  <p>although there there exists one relation. And when this code is run :</p>
  
  <pre><code>sig A {}
  fact {no A }
  pred show {}
  run show for 2
  </code></pre>
  
  <p>the variables count is like this :</p>
  
  <pre><code>6 vars. 2 primary vars. 5 clauses.
  </code></pre>
  
  <p>I can understand that maybe the 2 primary vars correspond to the max 2 elements of set A but I don't understand what are the 4 more variables that are enumerated.</p>