locked
Limiting state space

    Question

  • Is there a way to stop Spec Explorer from traversing the entire set of object roots while determining state and just limit it to certain fields/properties? Currently it's very difficult not to introduce non-deterministic behaviour unintentionally. For instance, a call to Array.Contains without second parameter specified will split the state in two - the one with System.Collections.Generic.EqualityComparer.defaultComparer = null (during the first exploration of the action) and System.Collections.Generic.EqualityComparer.defaultComparer != null (during the consequtive exploration steps).

    Thank you.

    Friday, January 14, 2011 2:00 PM

Answers

  • Hi Tokaplan,

    Everything in memory is part of the state. The reason is any change to the object model can have consequences on enabled steps. In your particular case, you should use the modeling collections (SetContainer<T>, SequenceContainer<T>, MapContainer<T,S> instead of .Net built-in types) to insure there will be no unintended side effects. This is not limited to parameters, it applies to model state too. You can also declare certain types as native so that Spec Explorer doesn't explore their operations. You can find information about this in the Spec Explorer documentation here.

    Best,

    Nico

    Monday, January 17, 2011 10:40 PM
    Moderator

All replies

  • Hi, tokaplan,

    Can you share your code here?

    I am not sure how you use arrays in SpecExplorer, but SpecExplorer does not allow using arrays as parameters, you can always choose Spec Explorer collection types:

    Set, Sequence, Map : value type, immutable

    SetContainer, SequenceContainer, MapContainer: reference type, mutable

    Thanks,

    Xiang

    Saturday, January 15, 2011 1:19 AM
    Moderator
  • The array I'm referring to is part of the state (a static member field of the model class, not a parameter). Let's concentrate on the essence of the question for a moment: is there a way to define what exactly should constitute a state for Spec Explorer?
    Monday, January 17, 2011 3:12 PM
  • Hi Tokaplan,

    Everything in memory is part of the state. The reason is any change to the object model can have consequences on enabled steps. In your particular case, you should use the modeling collections (SetContainer<T>, SequenceContainer<T>, MapContainer<T,S> instead of .Net built-in types) to insure there will be no unintended side effects. This is not limited to parameters, it applies to model state too. You can also declare certain types as native so that Spec Explorer doesn't explore their operations. You can find information about this in the Spec Explorer documentation here.

    Best,

    Nico

    Monday, January 17, 2011 10:40 PM
    Moderator