Recursive data types in Promela

Question

I am trying to make a B-Tree in Promela so that I can prove stuff about it, however, it seems that Promela does not support recursive data types. This doesn't work:

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

How can I make a B-Tree in Promela, and if I can't, which tool would you suggest? I considered QuickCheck and Prolog. However making a B-Tree in Prolog would be hard too.

Answer 1

You'll represent the children using an index into a statically defined array of nodes. Like this:

#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;

With this, you 'allocate' nodes by incrementing next_node_id and can access a child by referencing into nodes using the child's id.