Promela中的递归数据类型

Question

我正在尝试用Promela创建一个B-Tree，这样我就可以证明一些关于它的东西，然而，Promela似乎不支持递归数据类型。这不起作用：

#define n 2
typedef BTreeNode
{
    int keys[2*n-1];
    BTreeNode children[2*n];
    int c;
};

我如何在Promela中创建B-Tree，如果我不能，你会推荐哪个工具？我考虑过QuickCheck和Prolog。然而，用Prolog制作B-Tree也很难。

Answer 1

您将使用一个静态定义的节点数组中的索引来表示子节点。如下所示：

#define n 2

#define BTreeNodeId   byte
typedef BTreeNode {
  BTreeNodeId my_id;
  int keys[2*n-1];
  BTreeNodeId children[2*n];
  int c;
};

BTreeNode nodes [10];
byte next_node_id = 0;

这样，您就可以通过递增next_node_id来“分配”节点，并且可以通过使用子节点的id引用nodes来访问子节点。