recursion - Promela 中的递归数据类型

Question

我正在尝试在 Promela 中创建一个 B 树，以便我可以证明有关它的内容，但是，Promela 似乎不支持递归数据类型。这不起作用:

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

我如何在 Promela 中制作 B 树，如果不能，您会推荐哪个工具？我考虑过 QuickCheck 和 Prolog。然而，在 Prolog 中制作 B 树也很困难。

Answer 1

您将使用静态定义的节点数组中的索引来表示 child 。像这样:

#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 来访问子节点。