Today I want to talk about model slicing which is one of the more advanced features of Spec Explorer. Slicing is extremely powerful, because it allows you to build your models very generically, and then create many slices of that model with differing purposes.
I’m going to show some very simple examples on how slicing works, and then I will dig up the Binary Search Tree model to illustrate how this would work in practice.
Slicing
For my example on slicing I’m going to construct a very simple model. The state is one integer variable, and I have two rules defined the following way:
[Rule(Action = "A()")]
static void A()
{
value *= -1;
}
[Rule(Action = "B()")]
static void B()
{
value++;
}
Rule “A” flips the sign of the value and “B” increases it by one. The state space of this model is infinite. If you explore it you get something like:
