Visualising Larger State Spaces in Pro B
Visualising Larger State Spaces in Pro B
复制标题
在 Pro B 中可视化更大的状态空间
DOI：
10.1007/11415787_2
复制
发表时间：
2005
期刊：
影响因子：
--
通讯作者：
E. Turner
中科院分区：
文献类型：
--
作者：
M. Leuschel;E. Turner
ProB是B方法的动画和模型检查器。它还允许以图形方式可视化B机的状态空间。这通常非常有用，允许用户快速发现机器是否按预期运行。然而，对于较大的状态空间，可视化很快变得难以被用户掌握（并且图形布局的计算需要相当长的时间）。在本文中，我们提出了两个相对简单的算法，往往大大降低了图的复杂性，同时仍然保持相关信息。这使得可视化更大的状态空间成为可能，并为用户提供有关机器整体行为的即时反馈。该算法已实现theProBtoolset内，我们强调其潜力的几个例子。在47台B机上进行了实验，并对实验结果进行了分析。
ProBis an animator and model checker for the B method. It also allows to visualise the state space of a B machine in graphical way. This is often very useful and allows users to quickly spot whether the machine behaves as expected. However, for larger state spaces the visualisation quickly becomes difficult to grasp by users (and the computation of the graph layout takes considerable time). In this paper we present two relatively simple algorithms to often considerably reduce the complexity of the graphs, while still keeping relevant information. This makes it possible to visualise much larger state spaces and gives the user immediate feedback about the overall behaviour of a machine. The algorithms have been implemented within theProBtoolset and we highlight their potential on several examples. We also conduct a thorough experimentation of the algorithm on 47 B machines and analyse the results.