title: specifying properties of relations in alloy
body: <p>I am trying to express certain mathematical properties of relations in Alloy, but I am not sure if I have the right approach yet, as I am just a beginner. Would appreciate any insights from the community of experts out there!</p>
  
  <p><strong>Specifying the fact that domain of a relation as singleton</strong>. e.g. Is the following a reasonable and correct way to do that?</p>
  
  <pre><code>pred SingletonDomain(r: univ-&gt;univ) {
   one ~r
  }
  
  sig S2 {}
  sig S1 {
   child: set S2
  }
  
  fact {
    SingletonDomain [child]
  }
  </code></pre>
  
  <p>or should it be something like the following</p>
  
  <pre><code>pred SingletonDomain (r: univ-&gt;univ) {
    #S2.~r = 1
  }
  </code></pre>
  
  <p>This is not very modular since the use of S2 is very specific to the particular signature.</p>
  
  <p><strong>Specifying the fact that a relation is a total order.</strong> At the moment I am using the following, basically I am simulating xor </p>
  
  <pre><code>pred total[r: univ-&gt;univ] {
    all disj e, e': Event | (e.r = e' and e'.r != e) or (e.r != e' and e'.r = e)
  }
  </code></pre>
  
  <p>Thanks</p>