Implement partition refinement algorithm

Question

Partition Refinement Algorithm

I have this algorithm from another Stack Exchange question:

Let

S = {x_1,x_2,x_3,x_4,x_5}

be the state space and

R = {
      (x_1,a,x_2),
      (x_1,b,x_3),
      (x_2,a,x_2),
      (x_3,a,x_4),
      (x_3,b,x_5),
      (x_4,a,x_4), // loop
      (x_5,a,x_5), // loop (a-transition)
      (x_5,b,x_5)  // loop (b-transition)
}

be the transition relation

Then we start with the partition

Pi_1 = {{x_1,x_2,x_3,x_4,x_5}}

where all the states are lumped together.

Now, x_2 and x_4 can both always do an a-transition to a state, but no b-transitions, whereas the remaining states can do both a- and b-transitions, so we split the state space as

Pi_2 = {{x_1,x_3,x_5},{x_2,x_4}}.

Next, x_5 can do an a-transition into the class {x_1,x_3,x_5}, but x_1 and x_3 can not, since their a-transitions go into the class {x_2,x_4}. Hence these should again be split, so we get

Pi_3 = {{x_1,x_3},{x_5},{x_2,x_4}}.

Now it should come as no surprise that x_3 can do a b-transition into the class {x_5}, but x_1 can not, so they must also be split, so we get

Pi_4 = {{x_1},{x_3},{x_5},{x_2,x_4}},

and if you do one more step, you will see that Pi_4 = Pi_5, so this is the result.

Implementation

I do not know how to implement this algorithm in JavaScript.

// blocks in initial partition (only consist of 1 block)
const initialPartition = { block1: getStates() };

// new partition
const partition = {};

// loop through each block in the partition
Object.values(initialPartition).forEach(function (block) {

  // now split the block into subgroups based on the relations.
  // loop through each node in block to see to which nodes it has relations
  block.forEach(function (node) {

    // recursively get edges (and their targets) coming out of the node
    const successors = node.successors();

    // ...

  }

});

I guess I should create a function that for each node can say which transitions it can make. If I have such function, I can loop through each node in each block, find the transitions, and create a key using something like

const key = getTransitions(node).sort().join();

and use this key to group the nodes into subblocks, making it possible to do something like

// blocks in initial partition (only consist of 1 block)
const initialPartition = { block1: getStates() };

// new partition
const partition = {};

// keep running until terminating
while (true) {

  // loop through each block in the partition
  Object.values(initialPartition).forEach(function (block) {

    // now split the block into subgroups based on the relations.
    // loop through each node in block to see to which nodes it has relations
    block.forEach(function (node) {

      // get possible transitions
      const key = getTransitions(node).sort().join();

      // group by key
      partition[key].push(node);

    }

  });

}

but I need to remember which nodes were already separated into blocks, so the subblocks keep becoming smaller (i.e. if I have {{x_1,x_3,x_5},{x_2,x_4}}, I should remember that these blocks can only become smaller, and never 'interchange').

Can someone give an idea on how to implement the algorithm? Just in pseudocode or something, so I can implement how to get the nodes' successors, incomers, labels (e.g. a-transition or b-transition), etc. This is a bisimulation algorithm, and the algorithm is implemented in Haskell in the slides here, but I do not understand Haskell.