Spec Explorer - Abstract specification of behaviour

Question

I am currently evaluating Spec Explorer, but I am stuck with a problem concerning abstract specifications of function behaviour. I have something like :

[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<ModelElement> elements = new Set<ModelElement>();
}

Now I do not want to define SelectElement(Set<ModelElement> e) explicitly in the model program. I would prefer to specify it with a postcondition like elements.contains(\result);. Is this somehow possible ?

The problem with the explicit definition is that I would enforce a selection strategy.

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):

1. Add a parameter ModelElement e to doSomething
2. Add condition Condition.IsTrue(elements.Contains(e)) to doSomething
3. Define an action in the config-script SelectElement

4. Define a machine SelectAndDo in the config-Script as follows:

   machine SelectAndDo() : Main
   {
     let ImplementationElement e 
         Where {.Condition.IsTrue(e.Equals(SelectElement()));.} 
         in doSomething(e)
   }
   

5. Use SelectAndDo instead of doSomething

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?

Answer 1

I figured out what the problem was. The solution sketched above worked actually, but I returned null from SelectElement() if elements was empty, so the condition in the where-clause could not be fulfilled. So instead of returning null, I decided to return an "illegal" element, similar to a Null Object. So my whole solutions looks something like this:

The machine:

machine Full() : Main
{
  Init(); CreateElement();CreateOtherElement();CreateIllegal(); SelectAndDo* || ModelProgram
}

The CreateIllegal() is afaik needed, such that the Condition in SelectAndDo can be fulfilled.

Beside that, I added checks for this illegal value in the model program.

EDIT:

There is actually a nicer, straight-forward way using Choice.Some<T>, which I did not know.