Module net.automatalib.util

Package net.automatalib.util.partitionrefinement

Class Valmari

java.lang.Object

net.automatalib.util.partitionrefinement.Valmari

public class Valmari
extends Object

Valmari's algorithm for computing the relational coarsest partition as presented in Simple Bisimilarity Minimization in O(m log n) Time by Antti Valmari.

To ensure maximal performance, this class is designed in a very low-level fashion, exposing most of its internal fields directly. For a more convenient access to its functionality, resort to the utility functions in ValmariInitializers and ValmariExtractors, respectively.

Nested Class Summary

Nested Classes

Modifier and Type	Class	Description
static class	Valmari.RefinablePartition	A refinable partition data structure.

Field Summary

Fields

Modifier and Type	Field	Description
Valmari.RefinablePartition	blocks
Valmari.RefinablePartition	clusters

Constructor Summary

Constructors

Constructor	Description
Valmari(int[] blocks, int[] tail, int[] label, int[] head)	Default constructor.

Method Summary

Modifier and Type	Method	Description
void	computeCoarsestStablePartition()

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Detail

blocks

public final Valmari.RefinablePartition blocks

clusters

public final Valmari.RefinablePartition clusters

Constructor Detail

Valmari

public Valmari(int[] blocks,
               int[] tail,
               int[] label,
               int[] head)

Default constructor. Note that the transitions are expected to be sorted first by their label and second by their source states. This can be typically achieved by initializing the arrays in a nested loop similar to

 
 for (int in : inputs) {
     for (int src : states) {
         for (int tgt : successors(src, in)) {
             tail[m] = src;
             label[m] = in;
             head[m] = tgt;
             m++;
         }
     }
 }
 

Further constraints are documented in the respective parameter descriptions.

Note that the contents of the arrays may be modified during the computation of the relational coarsest partition.

Parameters:

blocks - The initial classification of states. That is, blocks[i] denotes that class of state i. The classes need to be numbered continuously from 0 to k - 1, where k denotes the number of initial partition classes. Thus, the length of blocks implies the number of states.

tail - The source states of transitions. That is, tail[i] denotes the source state of transition i. Each value must be smaller than blocks.length.

label - The labels of transitions. That is, label[i] denotes the label of transition i. The labels need to be numbered continuously from 0 to l - 1, where l denotes the number of labels.

head - The target states of transitions. That is, tail[i] denotes the target state of transition i. Each value must be smaller than blocks.length.

Method Detail

computeCoarsestStablePartition

public void computeCoarsestStablePartition()