Question about the MBT/SpecExplorer concepts.

Question

What is Path as PathDepthBound  is concerned?

What is Step as StepBound is concerned?

What is State as StateBound is concerned?

What does '0', '2', '4' mean in S0, S2, S4, and how are they numbered?

I find the MSDN document did a poor job to explain this concepts. Hope someone could shed some light on this.

It would be great if some online reference about such concepts behind SpecExplorer/MBT can be offered.

---

sam witwiki

Answer 1

Hi Sam,

"Bounds" in Spec Explorer are for configuring resources allowed for exploration. I agree with you that the document content should be more elaborated. Just quick explanation here:

    PathDepthBound controls the maximum depth of path to explore. The depth is the number of steps taken from the initial state (S0) to a given state.

    StepBound controls the overall maximum steps to explore.

    StateBound controls the overall maximum states to explore.

The '0', '2', '4' you saw are just sequential numbering of states. Each time Spec Explorer identifies a new state, it labels it with an incremental number. The reason why you see even number only is that, by default the graph viewer collapses call/return atomic steps for you. E.g., in the exploration of the template model project, a transition:

    (S0) - Add(1) -> (S2)

is actually the collapsed version of:

    (S0) - call Add(1) -> <S1> - return Add -> (S2).

You can suppress the collapsing by toggling the "ViewCollapseSteps" switch in a view definition.

---

Thanks, Yiming