Рекурсивные типы данных в Promela

Question

Я пытаюсь создать B-Tree в Promela, чтобы я мог доказать что-то об этом, однако кажется, что Promela не поддерживает рекурсивные типы данных. Это не работает:

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

Как я могу сделать B-Tree в Promela, и если я не могу, какой инструмент вы бы предложили? Я рассмотрел QuickCheck и Пролог. Однако сделать 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, и можете обращаться к дочернему элементу, ссылаясь на nodes используя идентификатор ребенка.