13138848026

Committed 04 Feb 2025 02:53PM UTC coverage: 92.108% (+2.2%) from 89.877%

Build # 13138848026

Build Type

push

github

Committed by

mtf90

Commit Message

[maven-release-plugin] prepare release automatalib-0.12.0

Run Details

16609 of 18032 relevant lines covered (92.11%)

1.7 hits per line

Source File
Press 'n' to go to next uncovered line, 'b' for previous

98.45

/util/src/main/java/net/automatalib/util/minimizer/Minimizer.java

/* Copyright (C) 2013-2025 TU Dortmund University
 * This file is part of AutomataLib <https://automatalib.net>.
 *
 * Licensed under the Apache License, Version 2.0 (the "License");
 * you may not use this file except in compliance with the License.
 * You may obtain a copy of the License at
 *
 *     http://www.apache.org/licenses/LICENSE-2.0
 *
 * Unless required by applicable law or agreed to in writing, software
 * distributed under the License is distributed on an "AS IS" BASIS,
 * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
 * See the License for the specific language governing permissions and
 * limitations under the License.
 */
package net.automatalib.util.minimizer;

import java.util.Collection;
import java.util.Collections;
import java.util.HashMap;
import java.util.Iterator;
import java.util.List;
import java.util.Map;

import net.automatalib.common.smartcollection.DefaultLinkedList;
import net.automatalib.common.smartcollection.ElementReference;
import net.automatalib.common.smartcollection.IntrusiveLinkedList;
import net.automatalib.common.smartcollection.UnorderedCollection;
import net.automatalib.common.util.mapping.MutableMapping;
import net.automatalib.graph.UniversalGraph;
import net.automatalib.util.graph.traversal.GraphTraversal;
import org.checkerframework.checker.nullness.qual.Nullable;
import org.checkerframework.checker.nullness.qual.RequiresNonNull;

/**
 * Automaton minimizer. The automata are accessed via the {@link UniversalGraph} interface, and may be partially
 * defined. Note that undefined transitions are preserved, thus, they have no semantics that could be modeled otherwise
 * wrt. this algorithm.
 * <p>
 * The implemented algorithm is described in the paper <a href="https://doi.org/10.1109/ISIT.2007.4557131">Minimizing
 * incomplete automata</a> by Marie-Pierre Beal and Maxime Crochemore.
 *
 * @param <S>
 *         state class.
 * @param <L>
 *         transition label class.
 */
public final class Minimizer<S, L> {

    // The following attributes may be reused. Most of them are used
    // as local variables in the split() method, but storing them
    // as attributes helps to avoid costly re-allocations.
    private final DefaultLinkedList<Block<S, L>> splitters = new DefaultLinkedList<>();
    private final IntrusiveLinkedList<TransitionLabel<S, L>> letterList = new IntrusiveLinkedList<>();
    private final IntrusiveLinkedList<State<S, L>> stateList = new IntrusiveLinkedList<>();
    private final IntrusiveLinkedList<Block<S, L>> splitBlocks = new IntrusiveLinkedList<>();
    private final IntrusiveLinkedList<Block<S, L>> newBlocks = new IntrusiveLinkedList<>();
    private final IntrusiveLinkedList<State<S, L>> finalList = new IntrusiveLinkedList<>();
    // These attributes belong to a specific minimization process.
    private @Nullable MutableMapping<S, State<S, L>> stateStorage;
    private @Nullable UnorderedCollection<Block<S, L>> partition;
    private int numBlocks;

    /**
     * Minimizes an automaton. The automaton is not minimized directly, instead, a {@link MinimizationResult} structure
     * is returned. The automaton is interfaced using an adapter implementing the {@link UniversalGraph} interface.
     *
     * @param <S>
     *         state class.
     * @param <L>
     *         transition label class.
     * @param graph
     *         the automaton interface.
     *
     * @return the result structure.
     */
    public static <S, L> MinimizationResult<S, L> minimize(UniversalGraph<S, ?, ?, L> graph) {
        return minimize(graph, graph.getNodes());
    }

    public static <S, L> MinimizationResult<S, L> minimize(UniversalGraph<S, ?, ?, L> graph,
                                                           Collection<? extends S> start) {
        return new Minimizer<S, L>().performMinimization(graph, start);
    }

    /**
     * Performs the minimization of an automaton.
     * <p>
     * The automaton is accessed via a {@link UniversalGraph}. The result of the minimization process is effectively a
     * partition on the set of states, each element (block) in this partition contains equivalent states that can be
     * merged in a minimized automaton.
     *
     * @param <E>
     *         edge identifier class.
     * @param graph
     *         the automaton interface.
     * @param initialNodes
     *         the initial nodes from which reachable nodes should be determined
     *
     * @return a {@link MinimizationResult} structure, containing the state partition.
     */
    public <E> MinimizationResult<S, L> performMinimization(UniversalGraph<S, E, ?, L> graph,
                                                            Collection<? extends S> initialNodes) {
        // Initialize the data structures (esp. state records) and build
        // the initial partition.
        Collection<Block<S, L>> initialBlocks = initialize(graph, initialNodes);

        // Add all blocks from the initial partition as an element
        // of the partition, and as a potential splitter.
        partition = new UnorderedCollection<>(initialBlocks.size());
        ///splitters.hintNextCapacity(initialBlocks.size());

        for (Block<S, L> block : initialBlocks) {
            if (block.isEmpty()) {
                continue;
            }
            addToPartition(block);
            addToSplitterQueue(block);
            numBlocks++;
        }

        // Split the blocks of the partition, until no splitters
        // remain
        while (!splitters.isEmpty()) {
            Block<S, L> block = splitters.choose();
            removeFromSplitterQueue(block);

            split(block);
            updateBlocks();
        }

        // Return the result.
        MinimizationResult<S, L> result = new MinimizationResult<>(stateStorage, partition);

        // Ensure the garbage collection isn't hampered
        stateStorage = null;
        partition = null;
        numBlocks = 0;

        return result;
    }

    public MinimizationResult<S, L> performMinimization(UniversalGraph<S, ?, ?, L> graph) {
        return performMinimization(graph, graph.getNodes());
    }

    /**
     * Builds the initial data structures and performs the initial partitioning.
     */
    private <E> Collection<Block<S, L>> initialize(UniversalGraph<S, E, ?, L> graph,
                                                   Collection<? extends S> initialNodes) {
        if (initialNodes.isEmpty()) {
            return Collections.emptyList();
        }

        Iterable<? extends S> origStates = GraphTraversal.depthFirstOrder(graph, initialNodes);

        Map<L, TransitionLabel<S, L>> transitionMap = new HashMap<>();

        final MutableMapping<S, State<S, L>> mapping = graph.createStaticNodeMapping();

        int numStates = 0;
        for (S origState : origStates) {
            State<S, L> state = new State<>(numStates++, origState);
            mapping.put(origState, state);
            stateList.add(state);
        }

        InitialPartitioning<S, L> initPartitioning = new HashMapInitialPartitioning<>(graph);

        for (State<S, L> state : stateList) {
            S origState = state.getOriginalState();

            Block<S, L> block = initPartitioning.getBlock(origState);
            block.addState(state);

            for (E edge : graph.getOutgoingEdges(origState)) {
                S origTarget = graph.getTarget(edge);
                State<S, L> target = mapping.get(origTarget);
                L label = graph.getEdgeProperty(edge);
                TransitionLabel<S, L> transition = transitionMap.computeIfAbsent(label, TransitionLabel::new);
                Edge<S, L> edgeObj = new Edge<>(state, target, transition);
                state.addOutgoingEdge(edgeObj);
                target.addIncomingEdge(edgeObj);
            }
        }
        stateList.quickClear();
        stateStorage = mapping;

        return initPartitioning.getInitialBlocks();
    }

    /**
     * Adds a block to the partition.
     */
    @RequiresNonNull("partition")
    private void addToPartition(Block<S, L> block) {
        ElementReference ref = partition.referencedAdd(block);
        block.setPartitionReference(ref);
    }

    /**
     * Adds a block as a potential splitter.
     */
    private void addToSplitterQueue(Block<S, L> block) {
        ElementReference ref = splitters.referencedAdd(block);
        block.setSplitterQueueReference(ref);
    }

    /**
     * Removes a block from the splitter queue. This is done when it is split completely and thus no longer existant.
     */
    private boolean removeFromSplitterQueue(Block<S, L> block) {
        ElementReference ref = block.getSplitterQueueReference();
        if (ref == null) {
            return false;
        }

        splitters.remove(ref);
        block.setSplitterQueueReference(null);

        return true;
    }

    /**
     * This method realizes the core of the actual minimization, the "split" procedure.
     * <p>
     * A split separates in each block the states, if any, which have different transition characteristics wrt. a
     * specified block, the splitter.
     * <p>
     * This method does not perform actual splits, but instead it modifies the splitBlocks attribute to containing the
     * blocks that could potentially be split. The information on the subsets into which a block is split is contained
     * in the sub-blocks of the blocks in the result list.
     * <p>
     * The actual splitting is performed by the method updateBlocks().
     */
    private void split(Block<S, L> splitter) {
        // STEP 1: Collect the states that have outgoing edges
        // pointing to states inside the currently considered blocks.
        // Also, a list of transition labels occuring on these
        // edges is created.
        for (State<S, L> state : splitter.getStates()) {
            for (Edge<S, L> edge : state.getIncoming()) {
                TransitionLabel<S, L> transition = edge.getTransitionLabel();
                State<S, L> newState = edge.getSource();
                // Blocks that only contain a single state cannot
                // be split any further, and thus are of no
                // interest.
                if (newState.isSingletonBlock()) {
                    continue; //continue;
                }
                if (transition.addToSet(newState)) {
                    letterList.add(transition);
                }
            }
        }

        // STEP 2: Build the signatures. A signature of a state
        // is a sequence of the transition labels of its outgoing
        // edge that point into the considered split block.
        // The iteration over the label list in the outer loop
        // guarantees a consistent ordering of the transition labels.
        for (TransitionLabel<S, L> letter : letterList) {
            for (State<S, L> state : letter.getSet()) {
                if (state.addToSignature(letter)) {
                    stateList.add(state);
                    state.setSplitPoint(false);
                }
            }
            letter.clearSet();
        }
        letterList.clear();

        // STEP 3: Discriminate the states. This is done by weak
        // sorting the states. At the end of the weak sort, the finalList
        // will contain the states in such an order that only states belonging
        // to the same block having the same signature will be contiguous.

        // First, initialize the buckets of each block. This is done
        // for grouping the states by their corresponding block.
        for (State<S, L> state : stateList) {
            Block<S, L> block = state.getBlock();
            if (block.addToBucket(state)) {
                splitBlocks.add(block);
            }
        }
        stateList.clear();

        for (Block<S, L> block : splitBlocks) {
            stateList.concat(block.getBucket());
        }

        // Now, the states are ordered according to their signatures
        int i = 0;

        while (!stateList.isEmpty()) {
            for (State<S, L> state : stateList) {
                TransitionLabel<S, L> letter = state.getSignatureLetter(i);
                if (letter == null) {
                    finalList.pushBack(state);
                } else if (letter.addToBucket(state)) {
                    letterList.add(letter);
                }

                // If this state was the first to be added to the respective
                // bucket, or it differs from the previous entry in the previous
                // letter, it is a split point.
                final State<S, L> prev = state.getPrev();
                if (prev == null) {
                    state.setSplitPoint(true);
                } else if (i > 0 && prev.getSignatureLetter(i - 1) != state.getSignatureLetter(i - 1)) {
                    state.setSplitPoint(true);
                }
            }
            stateList.clear();

            for (TransitionLabel<S, L> letter : letterList) {
                stateList.concat(letter.getBucket());
            }
            letterList.clear();

            i++;
        }

        Block<S, L> prevBlock = null;

        State<S, L> prev = null;
        for (State<S, L> state : finalList) {
            Block<S, L> currBlock = state.getBlock();
            if (currBlock != prevBlock) {
                currBlock.createSubBlock();
                prevBlock = currBlock;
            } else if (state.isSplitPoint()) {
                currBlock.createSubBlock();
            }
            currBlock.addToSubBlock(state);
            if (prev != null) {
                prev.reset();
            }
            prev = state;
        }
        if (prev != null) {
            prev.reset();
        }
        finalList.clear();

        // Step 4 of the algorithm is done in the method
        // updateBlocks()
    }

    /**
     * This method performs the actual splitting of blocks, using the sub block information stored in each block
     * object.
     */
    @RequiresNonNull("partition")
    private void updateBlocks() {
        for (Block<S, L> block : splitBlocks) {
            // Ignore blocks that have no elements in their sub blocks.
            int inSubBlocks = block.getElementsInSubBlocks();
            if (inSubBlocks == 0) {
                continue;
            }

            boolean blockRemains = inSubBlocks < block.size();

            boolean reuseBlock = !blockRemains;

            List<UnorderedCollection<State<S, L>>> subBlocks = block.getSubBlocks();
            // If there is only one sub block which contains all elements of
            // the block, then no split needs to be performed.
            if (!blockRemains && subBlocks.size() == 1) {
                block.clearSubBlocks();
                continue;
            }

            Iterator<UnorderedCollection<State<S, L>>> subBlockIt = subBlocks.iterator();

            if (reuseBlock) {
                UnorderedCollection<State<S, L>> first = subBlockIt.next();
                block.getStates().swap(first);
                updateBlockReferences(block);
            }

            while (subBlockIt.hasNext()) {
                UnorderedCollection<State<S, L>> subBlockStates = subBlockIt.next();

                if (blockRemains) {
                    for (State<S, L> state : subBlockStates) {
                        block.removeState(state.getBlockReference());
                    }
                }

                Block<S, L> subBlock = new Block<>(numBlocks++, subBlockStates);
                updateBlockReferences(subBlock);
                newBlocks.add(subBlock);
                addToPartition(subBlock);
            }

            newBlocks.add(block);
            block.clearSubBlocks();

            // If the split block previously was in the queue, add all newly
            // created blocks to the queue. Otherwise, it's enough to add
            // all but the largest
            if (removeFromSplitterQueue(block)) {
                addAllToSplitterQueue(newBlocks);
            } else {
                addAllButLargest(newBlocks);
            }
            newBlocks.clear();
        }

        splitBlocks.clear();
    }

    /**
     * Sets the blockReference-attribute of each state in the collection to the corresponding ElementReference of the
     * collection.
     */
    private static <S, L> void updateBlockReferences(Block<S, L> block) {
        UnorderedCollection<State<S, L>> states = block.getStates();
        for (ElementReference ref : states.references()) {
            State<S, L> state = states.get(ref);
            state.setBlockReference(ref);
            state.setBlock(block);
        }
    }

    /**
     * Adds all but the largest block of a given collection to the splitter queue.
     */
    private void addAllToSplitterQueue(Collection<Block<S, L>> blocks) {
        for (Block<S, L> block : blocks) {
            addToSplitterQueue(block);
        }
    }

    private void addAllButLargest(Collection<Block<S, L>> blocks) {
        Block<S, L> largest = null;

        for (Block<S, L> block : blocks) {
            if (largest == null) {
                largest = block;
            } else if (block.size() > largest.size()) {
                addToSplitterQueue(largest);
                largest = block;
            } else {
                addToSplitterQueue(block);
            }
        }
    }

}

1	/* Copyright (C) 2013-2025 TU Dortmund University
2	* This file is part of AutomataLib <https://automatalib.net>.
3	*
4	* Licensed under the Apache License, Version 2.0 (the "License");
5	* you may not use this file except in compliance with the License.
6	* You may obtain a copy of the License at
7	*
8	* http://www.apache.org/licenses/LICENSE-2.0
9	*
10	* Unless required by applicable law or agreed to in writing, software
11	* distributed under the License is distributed on an "AS IS" BASIS,
12	* WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
13	* See the License for the specific language governing permissions and
14	* limitations under the License.
15	*/
16	package net.automatalib.util.minimizer;
17
18	import java.util.Collection;
19	import java.util.Collections;
20	import java.util.HashMap;
21	import java.util.Iterator;
22	import java.util.List;
23	import java.util.Map;
24
25	import net.automatalib.common.smartcollection.DefaultLinkedList;
26	import net.automatalib.common.smartcollection.ElementReference;
27	import net.automatalib.common.smartcollection.IntrusiveLinkedList;
28	import net.automatalib.common.smartcollection.UnorderedCollection;
29	import net.automatalib.common.util.mapping.MutableMapping;
30	import net.automatalib.graph.UniversalGraph;
31	import net.automatalib.util.graph.traversal.GraphTraversal;
32	import org.checkerframework.checker.nullness.qual.Nullable;
33	import org.checkerframework.checker.nullness.qual.RequiresNonNull;
34
35	/**
36	* Automaton minimizer. The automata are accessed via the {@link UniversalGraph} interface, and may be partially
37	* defined. Note that undefined transitions are preserved, thus, they have no semantics that could be modeled otherwise
38	* wrt. this algorithm.
39	* <p>
40	* The implemented algorithm is described in the paper <a href="https://doi.org/10.1109/ISIT.2007.4557131">Minimizing
41	* incomplete automata</a> by Marie-Pierre Beal and Maxime Crochemore.
42	*
43	* @param <S>
44	* state class.
45	* @param <L>
46	* transition label class.
47	*/
48	public final class Minimizer<S, L> {	2✔
49
50	// The following attributes may be reused. Most of them are used
51	// as local variables in the split() method, but storing them
52	// as attributes helps to avoid costly re-allocations.
53	private final DefaultLinkedList<Block<S, L>> splitters = new DefaultLinkedList<>();	2✔
54	private final IntrusiveLinkedList<TransitionLabel<S, L>> letterList = new IntrusiveLinkedList<>();	2✔
55	private final IntrusiveLinkedList<State<S, L>> stateList = new IntrusiveLinkedList<>();	2✔
56	private final IntrusiveLinkedList<Block<S, L>> splitBlocks = new IntrusiveLinkedList<>();	2✔
57	private final IntrusiveLinkedList<Block<S, L>> newBlocks = new IntrusiveLinkedList<>();	2✔
58	private final IntrusiveLinkedList<State<S, L>> finalList = new IntrusiveLinkedList<>();	2✔
59	// These attributes belong to a specific minimization process.
60	private @Nullable MutableMapping<S, State<S, L>> stateStorage;
61	private @Nullable UnorderedCollection<Block<S, L>> partition;
62	private int numBlocks;
63
64	/**
65	* Minimizes an automaton. The automaton is not minimized directly, instead, a {@link MinimizationResult} structure
66	* is returned. The automaton is interfaced using an adapter implementing the {@link UniversalGraph} interface.
67	*
68	* @param <S>
69	* state class.
70	* @param <L>
71	* transition label class.
72	* @param graph
73	* the automaton interface.
74	*
75	* @return the result structure.
76	*/
77	public static <S, L> MinimizationResult<S, L> minimize(UniversalGraph<S, ?, ?, L> graph) {
78	return minimize(graph, graph.getNodes());	2✔
79	}
80
81	public static <S, L> MinimizationResult<S, L> minimize(UniversalGraph<S, ?, ?, L> graph,
82	Collection<? extends S> start) {
83	return new Minimizer<S, L>().performMinimization(graph, start);	2✔
84	}
85
86	/**
87	* Performs the minimization of an automaton.
88	* <p>
89	* The automaton is accessed via a {@link UniversalGraph}. The result of the minimization process is effectively a
90	* partition on the set of states, each element (block) in this partition contains equivalent states that can be
91	* merged in a minimized automaton.
92	*
93	* @param <E>
94	* edge identifier class.
95	* @param graph
96	* the automaton interface.
97	* @param initialNodes
98	* the initial nodes from which reachable nodes should be determined
99	*
100	* @return a {@link MinimizationResult} structure, containing the state partition.
101	*/
102	public <E> MinimizationResult<S, L> performMinimization(UniversalGraph<S, E, ?, L> graph,
103	Collection<? extends S> initialNodes) {
104	// Initialize the data structures (esp. state records) and build
105	// the initial partition.
106	Collection<Block<S, L>> initialBlocks = initialize(graph, initialNodes);	2✔
107
108	// Add all blocks from the initial partition as an element
109	// of the partition, and as a potential splitter.
110	partition = new UnorderedCollection<>(initialBlocks.size());	2✔
111	///splitters.hintNextCapacity(initialBlocks.size());
112
113	for (Block<S, L> block : initialBlocks) {	2✔
114	if (block.isEmpty()) {	2✔
115	continue;	×
116	}
117	addToPartition(block);	2✔
118	addToSplitterQueue(block);	2✔
119	numBlocks++;	2✔
120	}	2✔
121
122	// Split the blocks of the partition, until no splitters
123	// remain
124	while (!splitters.isEmpty()) {	2✔
125	Block<S, L> block = splitters.choose();	2✔
126	removeFromSplitterQueue(block);	2✔
127
128	split(block);	2✔
129	updateBlocks();	2✔
130	}	2✔
131
132	// Return the result.
133	MinimizationResult<S, L> result = new MinimizationResult<>(stateStorage, partition);	2✔
134
135	// Ensure the garbage collection isn't hampered
136	stateStorage = null;	2✔
137	partition = null;	2✔
138	numBlocks = 0;	2✔
139
140	return result;	2✔
141	}
142
143	public MinimizationResult<S, L> performMinimization(UniversalGraph<S, ?, ?, L> graph) {
144	return performMinimization(graph, graph.getNodes());	2✔
145	}
146
147	/**
148	* Builds the initial data structures and performs the initial partitioning.
149	*/
150	private <E> Collection<Block<S, L>> initialize(UniversalGraph<S, E, ?, L> graph,
151	Collection<? extends S> initialNodes) {
152	if (initialNodes.isEmpty()) {	2✔
153	return Collections.emptyList();	×
154	}
155
156	Iterable<? extends S> origStates = GraphTraversal.depthFirstOrder(graph, initialNodes);	2✔
157
158	Map<L, TransitionLabel<S, L>> transitionMap = new HashMap<>();	2✔
159
160	final MutableMapping<S, State<S, L>> mapping = graph.createStaticNodeMapping();	2✔
161
162	int numStates = 0;	2✔
163	for (S origState : origStates) {	2✔
164	State<S, L> state = new State<>(numStates++, origState);	2✔
165	mapping.put(origState, state);	2✔
166	stateList.add(state);	2✔
167	}	2✔
168
169	InitialPartitioning<S, L> initPartitioning = new HashMapInitialPartitioning<>(graph);	2✔
170
171	for (State<S, L> state : stateList) {	2✔
172	S origState = state.getOriginalState();	2✔
173
174	Block<S, L> block = initPartitioning.getBlock(origState);	2✔
175	block.addState(state);	2✔
176
177	for (E edge : graph.getOutgoingEdges(origState)) {	2✔
178	S origTarget = graph.getTarget(edge);	2✔
179	State<S, L> target = mapping.get(origTarget);	2✔
180	L label = graph.getEdgeProperty(edge);	2✔
181	TransitionLabel<S, L> transition = transitionMap.computeIfAbsent(label, TransitionLabel::new);	2✔
182	Edge<S, L> edgeObj = new Edge<>(state, target, transition);	2✔
183	state.addOutgoingEdge(edgeObj);	2✔
184	target.addIncomingEdge(edgeObj);	2✔
185	}	2✔
186	}	2✔
187	stateList.quickClear();	2✔
188	stateStorage = mapping;	2✔
189
190	return initPartitioning.getInitialBlocks();	2✔
191	}
192
193	/**
194	* Adds a block to the partition.
195	*/
196	@RequiresNonNull("partition")
197	private void addToPartition(Block<S, L> block) {
198	ElementReference ref = partition.referencedAdd(block);	2✔
199	block.setPartitionReference(ref);	2✔
200	}	2✔
201
202	/**
203	* Adds a block as a potential splitter.
204	*/
205	private void addToSplitterQueue(Block<S, L> block) {
206	ElementReference ref = splitters.referencedAdd(block);	2✔
207	block.setSplitterQueueReference(ref);	2✔
208	}	2✔
209
210	/**
211	* Removes a block from the splitter queue. This is done when it is split completely and thus no longer existant.
212	*/
213	private boolean removeFromSplitterQueue(Block<S, L> block) {
214	ElementReference ref = block.getSplitterQueueReference();	2✔
215	if (ref == null) {	2✔
216	return false;	2✔
217	}
218
219	splitters.remove(ref);	2✔
220	block.setSplitterQueueReference(null);	2✔
221
222	return true;	2✔
223	}
224
225	/**
226	* This method realizes the core of the actual minimization, the "split" procedure.
227	* <p>
228	* A split separates in each block the states, if any, which have different transition characteristics wrt. a
229	* specified block, the splitter.
230	* <p>
231	* This method does not perform actual splits, but instead it modifies the splitBlocks attribute to containing the
232	* blocks that could potentially be split. The information on the subsets into which a block is split is contained
233	* in the sub-blocks of the blocks in the result list.
234	* <p>
235	* The actual splitting is performed by the method updateBlocks().
236	*/
237	private void split(Block<S, L> splitter) {
238	// STEP 1: Collect the states that have outgoing edges
239	// pointing to states inside the currently considered blocks.
240	// Also, a list of transition labels occuring on these
241	// edges is created.
242	for (State<S, L> state : splitter.getStates()) {	2✔
243	for (Edge<S, L> edge : state.getIncoming()) {	2✔
244	TransitionLabel<S, L> transition = edge.getTransitionLabel();	2✔
245	State<S, L> newState = edge.getSource();	2✔
246	// Blocks that only contain a single state cannot
247	// be split any further, and thus are of no
248	// interest.
249	if (newState.isSingletonBlock()) {	2✔
250	continue; //continue;	2✔
251	}
252	if (transition.addToSet(newState)) {	2✔
253	letterList.add(transition);	2✔
254	}
255	}	2✔
256	}	2✔
257
258	// STEP 2: Build the signatures. A signature of a state
259	// is a sequence of the transition labels of its outgoing
260	// edge that point into the considered split block.
261	// The iteration over the label list in the outer loop
262	// guarantees a consistent ordering of the transition labels.
263	for (TransitionLabel<S, L> letter : letterList) {	2✔
264	for (State<S, L> state : letter.getSet()) {	2✔
265	if (state.addToSignature(letter)) {	2✔
266	stateList.add(state);	2✔
267	state.setSplitPoint(false);	2✔
268	}
269	}	2✔
270	letter.clearSet();	2✔
271	}	2✔
272	letterList.clear();	2✔
273
274	// STEP 3: Discriminate the states. This is done by weak
275	// sorting the states. At the end of the weak sort, the finalList
276	// will contain the states in such an order that only states belonging
277	// to the same block having the same signature will be contiguous.
278
279	// First, initialize the buckets of each block. This is done
280	// for grouping the states by their corresponding block.
281	for (State<S, L> state : stateList) {	2✔
282	Block<S, L> block = state.getBlock();	2✔
283	if (block.addToBucket(state)) {	2✔
284	splitBlocks.add(block);	2✔
285	}
286	}	2✔
287	stateList.clear();	2✔
288
289	for (Block<S, L> block : splitBlocks) {	2✔
290	stateList.concat(block.getBucket());	2✔
291	}	2✔
292
293	// Now, the states are ordered according to their signatures
294	int i = 0;	2✔
295
296	while (!stateList.isEmpty()) {	2✔
297	for (State<S, L> state : stateList) {	2✔
298	TransitionLabel<S, L> letter = state.getSignatureLetter(i);	2✔
299	if (letter == null) {	2✔
300	finalList.pushBack(state);	2✔
301	} else if (letter.addToBucket(state)) {	2✔
302	letterList.add(letter);	2✔
303	}
304
305	// If this state was the first to be added to the respective
306	// bucket, or it differs from the previous entry in the previous
307	// letter, it is a split point.
308	final State<S, L> prev = state.getPrev();	2✔
309	if (prev == null) {	2✔
310	state.setSplitPoint(true);	2✔
311	} else if (i > 0 && prev.getSignatureLetter(i - 1) != state.getSignatureLetter(i - 1)) {	2✔
312	state.setSplitPoint(true);	2✔
313	}
314	}	2✔
315	stateList.clear();	2✔
316
317	for (TransitionLabel<S, L> letter : letterList) {	2✔
318	stateList.concat(letter.getBucket());	2✔
319	}	2✔
320	letterList.clear();	2✔
321
322	i++;	2✔
323	}
324
325	Block<S, L> prevBlock = null;	2✔
326
327	State<S, L> prev = null;	2✔
328	for (State<S, L> state : finalList) {	2✔
329	Block<S, L> currBlock = state.getBlock();	2✔
330	if (currBlock != prevBlock) {	2✔
331	currBlock.createSubBlock();	2✔
332	prevBlock = currBlock;	2✔
333	} else if (state.isSplitPoint()) {	2✔
334	currBlock.createSubBlock();	2✔
335	}
336	currBlock.addToSubBlock(state);	2✔
337	if (prev != null) {	2✔
338	prev.reset();	2✔
339	}
340	prev = state;	2✔
341	}	2✔
342	if (prev != null) {	2✔
343	prev.reset();	2✔
344	}
345	finalList.clear();	2✔
346
347	// Step 4 of the algorithm is done in the method
348	// updateBlocks()
349	}	2✔
350
351	/**
352	* This method performs the actual splitting of blocks, using the sub block information stored in each block
353	* object.
354	*/
355	@RequiresNonNull("partition")
356	private void updateBlocks() {
357	for (Block<S, L> block : splitBlocks) {	2✔
358	// Ignore blocks that have no elements in their sub blocks.
359	int inSubBlocks = block.getElementsInSubBlocks();	2✔
360	if (inSubBlocks == 0) {	2✔
361	continue;	×
362	}
363
364	boolean blockRemains = inSubBlocks < block.size();	2✔
365
366	boolean reuseBlock = !blockRemains;	2✔
367
368	List<UnorderedCollection<State<S, L>>> subBlocks = block.getSubBlocks();	2✔
369	// If there is only one sub block which contains all elements of
370	// the block, then no split needs to be performed.
371	if (!blockRemains && subBlocks.size() == 1) {	2✔
372	block.clearSubBlocks();	2✔
373	continue;	2✔
374	}
375
376	Iterator<UnorderedCollection<State<S, L>>> subBlockIt = subBlocks.iterator();	2✔
377
378	if (reuseBlock) {	2✔
379	UnorderedCollection<State<S, L>> first = subBlockIt.next();	2✔
380	block.getStates().swap(first);	2✔
381	updateBlockReferences(block);	2✔
382	}
383
384	while (subBlockIt.hasNext()) {	2✔
385	UnorderedCollection<State<S, L>> subBlockStates = subBlockIt.next();	2✔
386
387	if (blockRemains) {	2✔
388	for (State<S, L> state : subBlockStates) {	2✔
389	block.removeState(state.getBlockReference());	2✔
390	}	2✔
391	}
392
393	Block<S, L> subBlock = new Block<>(numBlocks++, subBlockStates);	2✔
394	updateBlockReferences(subBlock);	2✔
395	newBlocks.add(subBlock);	2✔
396	addToPartition(subBlock);	2✔
397	}	2✔
398
399	newBlocks.add(block);	2✔
400	block.clearSubBlocks();	2✔
401
402	// If the split block previously was in the queue, add all newly
403	// created blocks to the queue. Otherwise, it's enough to add
404	// all but the largest
405	if (removeFromSplitterQueue(block)) {	2✔
406	addAllToSplitterQueue(newBlocks);	2✔
407	} else {
408	addAllButLargest(newBlocks);	2✔
409	}
410	newBlocks.clear();	2✔
411	}	2✔
412
413	splitBlocks.clear();	2✔
414	}	2✔
415
416	/**
417	* Sets the blockReference-attribute of each state in the collection to the corresponding ElementReference of the
418	* collection.
419	*/
420	private static <S, L> void updateBlockReferences(Block<S, L> block) {
421	UnorderedCollection<State<S, L>> states = block.getStates();	2✔
422	for (ElementReference ref : states.references()) {	2✔
423	State<S, L> state = states.get(ref);	2✔
424	state.setBlockReference(ref);	2✔
425	state.setBlock(block);	2✔
426	}	2✔
427	}	2✔
428
429	/**
430	* Adds all but the largest block of a given collection to the splitter queue.
431	*/
432	private void addAllToSplitterQueue(Collection<Block<S, L>> blocks) {
433	for (Block<S, L> block : blocks) {	2✔
434	addToSplitterQueue(block);	2✔
435	}	2✔
436	}	2✔
437
438	private void addAllButLargest(Collection<Block<S, L>> blocks) {
439	Block<S, L> largest = null;	2✔
440
441	for (Block<S, L> block : blocks) {	2✔
442	if (largest == null) {	2✔
443	largest = block;	2✔
444	} else if (block.size() > largest.size()) {	2✔
445	addToSplitterQueue(largest);	2✔
446	largest = block;	2✔
447	} else {
448	addToSplitterQueue(block);	2✔
449	}
450	}	2✔
451	}	2✔
452
453	}

LearnLib / automatalib / 13138848026

Source File Press 'n' to go to next uncovered line, 'b' for previous

Source File
Press 'n' to go to next uncovered line, 'b' for previous