title: Spec Explorer - Abstract specification of behaviour
body: <p>I am currently evaluating Spec Explorer, but I am stuck with a problem concerning abstract specifications of function behaviour.
  I have something like :</p>
  
  <pre><code>[TypeBinding("Implementation.ImplementationElement")]
  public class ModelElement
  { /*... */ }
  public class ModelBehaviour
  {
    [Rule]
    public static void doSomething()
    {
      ModelElement sel = SelectElement(elements);
      // ... do something with sel
    }
    private static Set&lt;ModelElement&gt; elements = new Set&lt;ModelElement&gt;();
  }
  </code></pre>
  
  <p>Now I do not want to define <code>SelectElement(Set&lt;ModelElement&gt; e)</code> explicitly in the model program. I would prefer to specify it with a postcondition like <code>elements.contains(\result);</code>. Is this somehow possible ?</p>
  
  <p>The problem with the explicit definition is that I would enforce a selection strategy.</p>
  
  <p>I tried to avoid the problem in the following way (maybe I am just missing something small and someone could give me a hint to do it correctly):</p>
  
  <ol>
  <li>Add a parameter <code>ModelElement e</code> to <code>doSomething</code></li>
  <li>Add condition <code>Condition.IsTrue(elements.Contains(e))</code> to <code>doSomething</code></li>
  <li>Define an action in the config-script <code>SelectElement</code></li>
  <li><p>Define a machine <code>SelectAndDo</code> in the config-Script as follows:</p>
  
  <pre><code>machine SelectAndDo() : Main
  {
    let ImplementationElement e 
        Where {.Condition.IsTrue(e.Equals(SelectElement()));.} 
        in doSomething(e)
  }
  </code></pre></li>
  <li>Use <code>SelectAndDo</code> instead of <code>doSomething</code></li>
  </ol>
  
  <p>However, this does not work, because the exploration of the corresponding model enters an error state.
  If this does not work at all, is there a good alternative to Spec Explorer on Windows, preferably stable? Can FsCheck be recommended for testing stateful systems? </p>