关于MBT / SpecExplorer概念的问题。 [英] Question about the MBT/SpecExplorer concepts.

问题描述

什么是路径 PathDepthBound  是关注？

What is Path as PathDepthBound  is concerned?

步骤 StepBound  是什么？

What is Step as StepBound is concerned?

什么是州 StateBound 有关吗？

在S0，S2，S4中'0'，'2'，'4'是什么意思，它们是如何编号的？

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

我发现MSDN文档在解释这个概念方面做得不好。希望有人可以对此有所了解。

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

如果可以提供有关SpecExplorer / MBT背后的此类概念的在线参考，那就太棒了。

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

sam witwiki

sam witwiki

推荐答案

嗨Sam，

" Bounds"在Spec Explorer中用于配置允许浏览的资源。我同意你的意见，文件内容应该更加详细。这里只需快速解释：

"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控制要探索的最大路径深度。深度是从初始状态（S0）到给定状态所采取的步数。

    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控制要探索的总体最大步骤。

    StepBound controls the overall maximum steps to explore.

    StateBound控制要探索的总体最大状态。

    StateBound controls the overall maximum states to explore.

您看到的'0'，'2'，'4'只是状态的顺序编号。每次Spec Explorer识别新状态时，它都会使用增量编号对其进行标记。您只看到偶数的原因是，默认情况下，图形查看器会为您调用call / return
原子步骤。例如，在模板模型项目的探索中，过渡：

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） - 添加（1） - > （S2）

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

实际上是折叠后的版本：

is actually the collapsed version of:

    （S0） - 调用Add（1） - > < S1> - 返回添加 - > （S2）。

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

您可以通过切换" ViewCollapseSteps "来抑制折叠。切换到
查看定义。

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

这篇关于关于MBT / SpecExplorer概念的问题。的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！