"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
Proposed as answer byYiming CaoThursday, May 10, 2012 2:05 AM
Thursday, May 10, 2012 2:03 AM
Microsoft is conducting an online survey to understand your opinion of the Msdn Web site. If you choose to participate, the online survey will be presented to you when you leave the Msdn Web site.