permutation_t Class Reference

stores a permutation of the states, ordered by block More...

#include <liblts_bisim_dnj.h>

Detailed Description

stores a permutation of the states, ordered by block

This is the central concept of the refinable partition: the permutation of the states, such that states belonging to the same block are adjacent.

Iterating over the states of a block will therefore be done using the permutation_t array.

This is the central concept of the refinable partition: the permutation of the states, such that states belonging to the same block are adjacent, and also that blocks belonging to the same constellation are adjacent.

Iterating over the states of a block or the blocks of a constellation will therefore be done using the permutation_t array.

---

The documentation for this class was generated from the following files:

• lts/include/mcrl2/lts/detail/liblts_bisim_dnj.h
• lts/include/mcrl2/lts/detail/liblts_bisim_gjkw.h