12304577693

Committed 12 Dec 2024 08:51PM UTC coverage: 91.182% (+0.4%) from 90.804%

Build # 12304577693

Build Type

push

github

Committed by

web-flow

Commit Message

Overhaul minimization code (#83)

* add valmaris algorithm

* initial PT refactoring

* implement bisimulation via valmari

* add documentation

* cleanups

* add invasive hopcroft methods

* some more universal tests

* performance tweaks

* move OneSEVPAMinimizer

* improve documentation

* cleanup

* wording

* fix javadoc errors

Run Details

564 of 581 new or added lines in 25 files covered. (97.07%)

1 existing line in 1 file now uncovered.

16535 of 18134 relevant lines covered (91.18%)

1.69 hits per line

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

90.85

/util/src/main/java/net/automatalib/util/partitionrefinement/Hopcroft.java

/* Copyright (C) 2013-2024 TU Dortmund University
 * This file is part of AutomataLib, http://www.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.partitionrefinement;

import java.util.Arrays;
import java.util.Iterator;
import java.util.PrimitiveIterator;
import java.util.Spliterator;
import java.util.Spliterators;

import org.checkerframework.checker.nullness.qual.Nullable;

/**
 * An implementation of Hopcroft's algorithm for computing the functional coarsest partition.
 * <p>
 * To ensure maximal performance, this class is designed in a very low-level fashion, exposing most of its internal
 * fields directly. It should only ever be used directly, and its use should be hidden behind a facade such that neither
 * this class nor any of its methods/referenced objects are exposed at an API level.
 * <p>
 * This class stores most of its internal data in several, or possibly even a single, (mostly {@code int}) array(s), to
 * achieve maximal cache efficiency. The layout of these arrays is described in the documentation of the respective
 * public fields:
 * <ul>
 *     <li>{@link #blockData}</li>
 *     <li>{@link #predOfsData}</li>
 *     <li>{@link #predData}</li>
 *     <li>{@link #blockForState}</li>
 * </ul>
 * The {@link HopcroftInitializers} provides methods for initializing this data structure for
 * common cases (e.g., DFA minimization). Similarly, the {@link HopcroftExtractors} class provides methods for
 * transforming the resulting data structure.
 */
public class Hopcroft {

    /**
     * The number of input symbols.
     */
    public int numInputs;
    /**
     * The number of states.
     */
    public int numStates;
    /**
     * The array storing the raw block data, i.e., the states contained in a certain block. It is assumed that the
     * positions {@link Block#low} and {@link Block#high} refer to this array.
     */
    public int[] blockData;
    /**
     * The array storing the position data, i.e., for each state, its index in the {@link #blockData} array.
     * <p>
     * The layout of this array is assumed to be the following: for the state {@code i}, where <code>0 &lt;= i &lt;
     * {@link #numStates}</code>, the index of {@code i} in {@link #blockData} is <code>{@link #posData}[{@link
     * #posDataLow} + i]</code>.
     */
    public int[] posData;
    /**
     * The lowest index storing position data in the {@link #posData} array.
     */
    public int posDataLow;
    /**
     * The array storing the predecessor offset data, i.e., for each state and input symbol, the delimiting offsets of
     * the respective predecessor list. The offsets are assumed to refer to the {@link #predData} array.
     * <p>
     * The layout of this array is assumed to be the following: for state {@code i} and input symbol {@code j}, where
     * <code>0 &lt;= i &lt; {@link #numStates}</code> and <code>0 &lt;= j &lt; {@link #numInputs}</code>, the offset
     * (in the {@link #predData} array) of the first {@code j}-predecessor of {@code i} is
     * <code>{@link #predOfsData}[{@link
     * #predOfsDataLow} + j*{@link #numStates} + i]</code>, and the last {@code j}-predecessor of {@code i} is
     * <code>{@link #predOfsData}[{@link #predOfsDataLow} + j*{@link #numStates} + i + 1] - 1</code>. Note that this
     * requires the index <code>{@link #predOfsDataLow} + {@link #numInputs} * {@link #numStates}</code> to be valid,
     * and the contents of the {@link #predOfsData} array at this index must be the highest offset of any predecessor
     * plus one.
     */
    public int[] predOfsData;
    /**
     * The lowest index storing predecessor offset data in the {@link #predOfsData} array.
     */
    public int predOfsDataLow;
    /**
     * The array storing the predecessor data, i.e., for each state and input symbol, a list of the respective
     * predecessors.
     * <p>
     * The layout of this array is assumed to be the following: for state {@code i} and input symbol {@code j}, where
     * <code>0 &lt;= i &lt; {@link #numStates}</code> and <code>0 &lt;= j &lt; {@link #numInputs}</code>, the {@code
     * j}-predecessors of {@code i} are the elements of {@link #predData} from index <code>{@link #predOfsData}[{@link
     * #predOfsDataLow} + j*{@link #numStates} + i]</code>, inclusive, to index <code>{@link #predOfsData}[{@link
     * #predOfsDataLow} + j*{@link #numStates} + i + 1]</code>, exclusive.
     */
    public int[] predData;
    /**
     * The array mapping states (in the range between {@code 0} and {@link #numStates}) to their containing block.
     */
    public Block[] blockForState;
    // the head of the block linked list
    private @Nullable Block blocklistHead;
    // the block count
    private int numBlocks;
    // the head of the worklist linked list
    private @Nullable Block worklistHead;
    // the tail of the worklist linked list
    private @Nullable Block worklistTail;
    // the head of the 'touched' list
    private @Nullable Block touchedHead;

    public void setSize(int numStates, int numInputs) {
        this.numStates = numStates;
        this.numInputs = numInputs;
    }

    public void setBlockForState(Block[] blockForState) {
        this.blockForState = blockForState;
    }

    public void setBlockData(int[] blockData) {
        this.blockData = blockData;
    }

    public void setPosData(int[] posData, int posDataLow) {
        this.posData = posData;
        this.posDataLow = posDataLow;
    }

    public void setPredOfsData(int[] predOfsData, int predOfsDataLow) {
        this.predOfsData = predOfsData;
        this.predOfsDataLow = predOfsDataLow;
    }

    public void setPredData(int[] predData) {
        this.predData = predData;
    }

    /**
     * Removes all blocks which are empty from the block list. The {@link Block#id IDs} of the blocks are adjusted to
     * remain contiguous.
     * <p>
     * Note that this method does not modify the worklist, i.e., it should only be called when the worklist is empty.
     */
    public void removeEmptyBlocks() {
        Block curr = blocklistHead;
        Block prev = null;
        int effId = 0;
        while (curr != null) {
            if (!curr.isEmpty()) {
                curr.id = effId++;
                if (prev != null) {
                    prev.nextBlock = curr;
                } else {
                    blocklistHead = curr;
                }
                prev = curr;
            }
            curr = curr.nextBlock;
        }
        if (prev != null) {
            prev.nextBlock = null;
        } else {
            blocklistHead = null;
        }
        numBlocks = effId;
    }

    /**
     * Automatically creates a {@link #blockForState} mapping, and sets it as the current one.
     *
     * @see #createBlockForStateMap()
     * @see #setBlockForState(Block[])
     */
    public void initBlockForStateMap() {
        this.blockForState = createBlockForStateMap();
    }

    /**
     * Creates the {@link #blockForState} mapping from the blocks in the block list, and the contents of the {@link
     * #blockData} array.
     *
     * @return a {@link #blockForState} mapping consistent with the {@link #blockData}
     */
    public Block[] createBlockForStateMap() {
        Block[] map = new Block[numStates];
        for (Block b = blocklistHead; b != null; b = b.nextBlock) {
            int low = b.low, high = b.high;
            for (int i = low; i < high; i++) {
                int state = blockData[i];
                map[state] = b;
            }
        }
        return map;
    }

    private void initWorklist() {
        Block largest = blocklistHead;
        if (largest == null) {
            return;
        }
        int largestSize = largest.size();
        for (Block b = largest.nextBlock; b != null; b = b.nextBlock) {
            int size = b.size();
            if (size > largestSize) {
                addToWorklist(largest);
                largest = b;
                largestSize = size;
            } else {
                addToWorklist(b);
            }
        }
    }

    private void addToWorklist(Block b) {
        if (worklistHead == null) {
            worklistHead = b;
        } else {
            assert worklistTail != null;
            worklistTail.nextInWorklist = b;
        }
        worklistTail = b;
    }

    /**
     * Refines the partition until it stabilizes.
     */
    public void computeCoarsestStablePartition() {
        initWorklist();
        Block curr;
        while ((curr = poll()) != null) {
            int blockRange = curr.high - curr.low;
            // copy blockData, because #moveLeft() may change its data while we iterate over it
            // TODO maybe find an implementation that does not need to workaround this concurrent modification
            int[] blockCopy = new int[blockRange];
            System.arraycopy(blockData, curr.low, blockCopy, 0, blockRange);
            int predOfsBase = predOfsDataLow;
            for (int i = 0; i < numInputs; i++) {
                for (int j = 0; j < blockRange; j++) {
                    int state = blockCopy[j];
                    int predOfsIdx = predOfsBase + state;
                    int predLow = predOfsData[predOfsIdx], predHigh = predOfsData[predOfsIdx + 1];
                    for (int k = predLow; k < predHigh; k++) {
                        int pred = predData[k];
                        moveLeft(pred);
                    }
                }
                predOfsBase += numStates;
                processTouched();
            }
        }
    }

    private @Nullable Block poll() {
        if (worklistHead == null) {
            return null;
        }
        Block b = worklistHead;
        worklistHead = b.nextInWorklist;
        b.nextInWorklist = null;
        if (worklistHead == null) {
            worklistTail = null;
        }

        return b;
    }

    /**
     * Move the state to the left of its Block ptr, and advance the ptr. This allows for the grouping of states with
     * similar behavior.
     *
     * @param state
     *         state to be moved left within its Block.
     */
    private void moveLeft(int state) {
        Block b = blockForState[state];

        // singletons need no splitting
        if (b.size() == 1) {
            return;
        }

        int posIdx = posDataLow + state;
        int inBlockIdx = posData[posIdx];
        int ptr = b.ptr;

        if (ptr == -1) {
            // This block has not been touched yet. Queue it up, and initialize its ptr.
            b.nextTouched = touchedHead;
            touchedHead = b;
            ptr = b.low;
            b.ptr = ptr;
        }

        if (ptr <= inBlockIdx) {
            if (ptr < inBlockIdx) {
                // inBlockIdx is to the right of ptr. Swap the block positions.
                int other = blockData[ptr];
                blockData[ptr] = blockData[inBlockIdx];
                blockData[inBlockIdx] = other;

                posData[posIdx] = ptr;
                posData[posDataLow + other] = inBlockIdx;
            }
            b.ptr = ptr + 1;
        }
    }

    private void processTouched() {
        Block b = touchedHead;
        while (b != null) {
            Block next = b.nextTouched;
            b.nextTouched = null;
            Block splt = split(b);
            if (splt != null) {
                addToWorklist(splt);
            }
            b = next;
        }

        touchedHead = null;
    }

    /**
     * Invoke Block's split, and if it is successful, update PaigeTarjan fields to reflect the new block.
     *
     * @param b
     *         block to split
     *
     * @return smaller split block, or null if split is not successful
     */
    private @Nullable Block split(Block b) {
        Block splt = b.split(numBlocks);
        if (splt == null) {
            return null;
        }
        numBlocks++;
        int spltLow = splt.low, spltHigh = splt.high;
        for (int i = spltLow; i < spltHigh; i++) {
            int state = blockData[i];
            blockForState[state] = splt;
        }
        return splt;
    }

    /**
     * Creates a new block. The {@link Block#low} and {@link Block#high} fields will be initialized to {@code -1}.
     *
     * @return a newly created block.
     */
    public Block createBlock() {
        Block b = new Block(-1, -1, numBlocks++, blocklistHead);
        blocklistHead = b;
        return b;
    }

    /**
     * Iterates over the current {@link #blockList() block list} and sets every block's {@link Block#low low} and
     * {@link Block#high high} pointer to the accumulated sum of its own high pointer and its preceding blocks' high
     * pointers, effectively reducing each block to a single representative padded by its previous range.
     */
    public void canonizeBlocks() {
        int curr = 0;
        for (Block b : blockList()) {
            curr += b.high;
            b.high = curr;
            b.low = curr;
        }
    }

    /**
     * Retrieves the corresponding block for a given state (ID).
     *
     * @param id
     *         the state ID
     *
     * @return the block containing the specified state
     */
    public Block getBlockForState(int id) {
        return blockForState[id];
    }

    /**
     * Retrieves a representative state from the given block. This method behaves deterministically.
     *
     * @param b
     *         the block
     *
     * @return a representative state in the specified block
     */
    public int getRepresentative(Block b) {
        return blockData[b.low];
    }

    /**
     * Retrieves an iterator for the contents of the given block.
     *
     * @param b
     *         the block
     *
     * @return an iterator for the contents of the specified block
     */
    public PrimitiveIterator.OfInt statesInBlockIterator(Block b) {
        return Spliterators.iterator(statesInBlockSpliterator(b));
    }

    /**
     * Retrieves a spliterator for the contents of the given block.
     *
     * @param b
     *         the block
     *
     * @return a spliterator for the contents of the specified block
     */
    public Spliterator.OfInt statesInBlockSpliterator(Block b) {
        return Arrays.spliterator(blockData, b.low, b.high);
    }

    /**
     * Retrieves an iterator for iterating over all blocks in the block list.
     *
     * @return an iterator for iterating over all blocks
     */
    public Iterator<Block> blockListIterator() {
        return Block.blockListIterator(blocklistHead);
    }

    /**
     * Retrieves an {@link Iterable} that provides the iterator returned by {@link #blockListIterator()}.
     *
     * @return an {@link Iterable} for iterating over all blocks
     */
    public Iterable<Block> blockList() {
        return this::blockListIterator;
    }

    /**
     * Retrieves the total number of blocks in the block list.
     *
     * @return the total number of blocks
     */
    public int getNumBlocks() {
        return numBlocks;
    }
}

1	/* Copyright (C) 2013-2024 TU Dortmund University
2	* This file is part of AutomataLib, http://www.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.partitionrefinement;
17
18	import java.util.Arrays;
19	import java.util.Iterator;
20	import java.util.PrimitiveIterator;
21	import java.util.Spliterator;
22	import java.util.Spliterators;
23
24	import org.checkerframework.checker.nullness.qual.Nullable;
25
26	/**
27	* An implementation of Hopcroft's algorithm for computing the functional coarsest partition.
28	* <p>
29	* To ensure maximal performance, this class is designed in a very low-level fashion, exposing most of its internal
30	* fields directly. It should only ever be used directly, and its use should be hidden behind a facade such that neither
31	* this class nor any of its methods/referenced objects are exposed at an API level.
32	* <p>
33	* This class stores most of its internal data in several, or possibly even a single, (mostly {@code int}) array(s), to
34	* achieve maximal cache efficiency. The layout of these arrays is described in the documentation of the respective
35	* public fields:
36	* <ul>
37	* <li>{@link #blockData}</li>
38	* <li>{@link #predOfsData}</li>
39	* <li>{@link #predData}</li>
40	* <li>{@link #blockForState}</li>
41	* </ul>
42	* The {@link HopcroftInitializers} provides methods for initializing this data structure for
43	* common cases (e.g., DFA minimization). Similarly, the {@link HopcroftExtractors} class provides methods for
44	* transforming the resulting data structure.
45	*/
46	public class Hopcroft {	2✔
47
48	/**
49	* The number of input symbols.
50	*/
51	public int numInputs;
52	/**
53	* The number of states.
54	*/
55	public int numStates;
56	/**
57	* The array storing the raw block data, i.e., the states contained in a certain block. It is assumed that the
58	* positions {@link Block#low} and {@link Block#high} refer to this array.
59	*/
60	public int[] blockData;
61	/**
62	* The array storing the position data, i.e., for each state, its index in the {@link #blockData} array.
63	* <p>
64	* The layout of this array is assumed to be the following: for the state {@code i}, where <code>0 <= i <
65	* {@link #numStates}</code>, the index of {@code i} in {@link #blockData} is <code>{@link #posData}[{@link
66	* #posDataLow} + i]</code>.
67	*/
68	public int[] posData;
69	/**
70	* The lowest index storing position data in the {@link #posData} array.
71	*/
72	public int posDataLow;
73	/**
74	* The array storing the predecessor offset data, i.e., for each state and input symbol, the delimiting offsets of
75	* the respective predecessor list. The offsets are assumed to refer to the {@link #predData} array.
76	* <p>
77	* The layout of this array is assumed to be the following: for state {@code i} and input symbol {@code j}, where
78	* <code>0 <= i < {@link #numStates}</code> and <code>0 <= j < {@link #numInputs}</code>, the offset
79	* (in the {@link #predData} array) of the first {@code j}-predecessor of {@code i} is
80	* <code>{@link #predOfsData}[{@link
81	* #predOfsDataLow} + j*{@link #numStates} + i]</code>, and the last {@code j}-predecessor of {@code i} is
82	* <code>{@link #predOfsData}[{@link #predOfsDataLow} + j*{@link #numStates} + i + 1] - 1</code>. Note that this
83	* requires the index <code>{@link #predOfsDataLow} + {@link #numInputs} * {@link #numStates}</code> to be valid,
84	* and the contents of the {@link #predOfsData} array at this index must be the highest offset of any predecessor
85	* plus one.
86	*/
87	public int[] predOfsData;
88	/**
89	* The lowest index storing predecessor offset data in the {@link #predOfsData} array.
90	*/
91	public int predOfsDataLow;
92	/**
93	* The array storing the predecessor data, i.e., for each state and input symbol, a list of the respective
94	* predecessors.
95	* <p>
96	* The layout of this array is assumed to be the following: for state {@code i} and input symbol {@code j}, where
97	* <code>0 <= i < {@link #numStates}</code> and <code>0 <= j < {@link #numInputs}</code>, the {@code
98	* j}-predecessors of {@code i} are the elements of {@link #predData} from index <code>{@link #predOfsData}[{@link
99	* #predOfsDataLow} + j*{@link #numStates} + i]</code>, inclusive, to index <code>{@link #predOfsData}[{@link
100	* #predOfsDataLow} + j*{@link #numStates} + i + 1]</code>, exclusive.
101	*/
102	public int[] predData;
103	/**
104	* The array mapping states (in the range between {@code 0} and {@link #numStates}) to their containing block.
105	*/
106	public Block[] blockForState;
107	// the head of the block linked list
108	private @Nullable Block blocklistHead;
109	// the block count
110	private int numBlocks;
111	// the head of the worklist linked list
112	private @Nullable Block worklistHead;
113	// the tail of the worklist linked list
114	private @Nullable Block worklistTail;
115	// the head of the 'touched' list
116	private @Nullable Block touchedHead;
117
118	public void setSize(int numStates, int numInputs) {
119	this.numStates = numStates;	2✔
120	this.numInputs = numInputs;	2✔
121	}	2✔
122
123	public void setBlockForState(Block[] blockForState) {
124	this.blockForState = blockForState;	2✔
125	}	2✔
126
127	public void setBlockData(int[] blockData) {
128	this.blockData = blockData;	2✔
129	}	2✔
130
131	public void setPosData(int[] posData, int posDataLow) {
132	this.posData = posData;	2✔
133	this.posDataLow = posDataLow;	2✔
134	}	2✔
135
136	public void setPredOfsData(int[] predOfsData, int predOfsDataLow) {
137	this.predOfsData = predOfsData;	2✔
138	this.predOfsDataLow = predOfsDataLow;	2✔
139	}	2✔
140
141	public void setPredData(int[] predData) {
142	this.predData = predData;	2✔
143	}	2✔
144
145	/**
146	* Removes all blocks which are empty from the block list. The {@link Block#id IDs} of the blocks are adjusted to
147	* remain contiguous.
148	* <p>
149	* Note that this method does not modify the worklist, i.e., it should only be called when the worklist is empty.
150	*/
151	public void removeEmptyBlocks() {
152	Block curr = blocklistHead;	2✔
153	Block prev = null;	2✔
154	int effId = 0;	2✔
155	while (curr != null) {	2✔
156	if (!curr.isEmpty()) {	2✔
157	curr.id = effId++;	2✔
158	if (prev != null) {	2✔
159	prev.nextBlock = curr;	2✔
160	} else {
161	blocklistHead = curr;	2✔
162	}
163	prev = curr;	2✔
164	}
165	curr = curr.nextBlock;	2✔
166	}
167	if (prev != null) {	2✔
168	prev.nextBlock = null;	2✔
169	} else {
170	blocklistHead = null;	×
171	}
172	numBlocks = effId;	2✔
173	}	2✔
174
175	/**
176	* Automatically creates a {@link #blockForState} mapping, and sets it as the current one.
177	*
178	* @see #createBlockForStateMap()
179	* @see #setBlockForState(Block[])
180	*/
181	public void initBlockForStateMap() {
182	this.blockForState = createBlockForStateMap();	×
183	}	×
184
185	/**
186	* Creates the {@link #blockForState} mapping from the blocks in the block list, and the contents of the {@link
187	* #blockData} array.
188	*
189	* @return a {@link #blockForState} mapping consistent with the {@link #blockData}
190	*/
191	public Block[] createBlockForStateMap() {
192	Block[] map = new Block[numStates];	×
193	for (Block b = blocklistHead; b != null; b = b.nextBlock) {	×
194	int low = b.low, high = b.high;	×
195	for (int i = low; i < high; i++) {	×
196	int state = blockData[i];	×
197	map[state] = b;	×
198	}
199	}
200	return map;	×
201	}
202
203	private void initWorklist() {
204	Block largest = blocklistHead;	2✔
205	if (largest == null) {	2✔
NEW 206	return;	×
207	}
208	int largestSize = largest.size();	2✔
209	for (Block b = largest.nextBlock; b != null; b = b.nextBlock) {	2✔
210	int size = b.size();	2✔
211	if (size > largestSize) {	2✔
212	addToWorklist(largest);	2✔
213	largest = b;	2✔
214	largestSize = size;	2✔
215	} else {
216	addToWorklist(b);	2✔
217	}
218	}
219	}	2✔
220
221	private void addToWorklist(Block b) {
222	if (worklistHead == null) {	2✔
223	worklistHead = b;	2✔
224	} else {
225	assert worklistTail != null;	2✔
226	worklistTail.nextInWorklist = b;	2✔
227	}
228	worklistTail = b;	2✔
229	}	2✔
230
231	/**
232	* Refines the partition until it stabilizes.
233	*/
234	public void computeCoarsestStablePartition() {
235	initWorklist();	2✔
236	Block curr;
237	while ((curr = poll()) != null) {	2✔
238	int blockRange = curr.high - curr.low;	2✔
239	// copy blockData, because #moveLeft() may change its data while we iterate over it
240	// TODO maybe find an implementation that does not need to workaround this concurrent modification
241	int[] blockCopy = new int[blockRange];	2✔
242	System.arraycopy(blockData, curr.low, blockCopy, 0, blockRange);	2✔
243	int predOfsBase = predOfsDataLow;	2✔
244	for (int i = 0; i < numInputs; i++) {	2✔
245	for (int j = 0; j < blockRange; j++) {	2✔
246	int state = blockCopy[j];	2✔
247	int predOfsIdx = predOfsBase + state;	2✔
248	int predLow = predOfsData[predOfsIdx], predHigh = predOfsData[predOfsIdx + 1];	2✔
249	for (int k = predLow; k < predHigh; k++) {	2✔
250	int pred = predData[k];	2✔
251	moveLeft(pred);	2✔
252	}
253	}
254	predOfsBase += numStates;	2✔
255	processTouched();	2✔
256	}
257	}	2✔
258	}	2✔
259
260	private @Nullable Block poll() {
261	if (worklistHead == null) {	2✔
262	return null;	2✔
263	}
264	Block b = worklistHead;	2✔
265	worklistHead = b.nextInWorklist;	2✔
266	b.nextInWorklist = null;	2✔
267	if (worklistHead == null) {	2✔
268	worklistTail = null;	2✔
269	}
270
271	return b;	2✔
272	}
273
274	/**
275	* Move the state to the left of its Block ptr, and advance the ptr. This allows for the grouping of states with
276	* similar behavior.
277	*
278	* @param state
279	* state to be moved left within its Block.
280	*/
281	private void moveLeft(int state) {
282	Block b = blockForState[state];	2✔
283
284	// singletons need no splitting
285	if (b.size() == 1) {	2✔
286	return;	2✔
287	}
288
289	int posIdx = posDataLow + state;	2✔
290	int inBlockIdx = posData[posIdx];	2✔
291	int ptr = b.ptr;	2✔
292
293	if (ptr == -1) {	2✔
294	// This block has not been touched yet. Queue it up, and initialize its ptr.
295	b.nextTouched = touchedHead;	2✔
296	touchedHead = b;	2✔
297	ptr = b.low;	2✔
298	b.ptr = ptr;	2✔
299	}
300
301	if (ptr <= inBlockIdx) {	2✔
302	if (ptr < inBlockIdx) {	2✔
303	// inBlockIdx is to the right of ptr. Swap the block positions.
304	int other = blockData[ptr];	2✔
305	blockData[ptr] = blockData[inBlockIdx];	2✔
306	blockData[inBlockIdx] = other;	2✔
307
308	posData[posIdx] = ptr;	2✔
309	posData[posDataLow + other] = inBlockIdx;	2✔
310	}
311	b.ptr = ptr + 1;	2✔
312	}
313	}	2✔
314
315	private void processTouched() {
316	Block b = touchedHead;	2✔
317	while (b != null) {	2✔
318	Block next = b.nextTouched;	2✔
319	b.nextTouched = null;	2✔
320	Block splt = split(b);	2✔
321	if (splt != null) {	2✔
322	addToWorklist(splt);	2✔
323	}
324	b = next;	2✔
325	}	2✔
326
327	touchedHead = null;	2✔
328	}	2✔
329
330	/**
331	* Invoke Block's split, and if it is successful, update PaigeTarjan fields to reflect the new block.
332	*
333	* @param b
334	* block to split
335	*
336	* @return smaller split block, or null if split is not successful
337	*/
338	private @Nullable Block split(Block b) {
339	Block splt = b.split(numBlocks);	2✔
340	if (splt == null) {	2✔
341	return null;	2✔
342	}
343	numBlocks++;	2✔
344	int spltLow = splt.low, spltHigh = splt.high;	2✔
345	for (int i = spltLow; i < spltHigh; i++) {	2✔
346	int state = blockData[i];	2✔
347	blockForState[state] = splt;	2✔
348	}
349	return splt;	2✔
350	}
351
352	/**
353	* Creates a new block. The {@link Block#low} and {@link Block#high} fields will be initialized to {@code -1}.
354	*
355	* @return a newly created block.
356	*/
357	public Block createBlock() {
358	Block b = new Block(-1, -1, numBlocks++, blocklistHead);	2✔
359	blocklistHead = b;	2✔
360	return b;	2✔
361	}
362
363	/**
364	* Iterates over the current {@link #blockList() block list} and sets every block's {@link Block#low low} and
365	* {@link Block#high high} pointer to the accumulated sum of its own high pointer and its preceding blocks' high
366	* pointers, effectively reducing each block to a single representative padded by its previous range.
367	*/
368	public void canonizeBlocks() {
369	int curr = 0;	2✔
370	for (Block b : blockList()) {	2✔
371	curr += b.high;	2✔
372	b.high = curr;	2✔
373	b.low = curr;	2✔
374	}	2✔
375	}	2✔
376
377	/**
378	* Retrieves the corresponding block for a given state (ID).
379	*
380	* @param id
381	* the state ID
382	*
383	* @return the block containing the specified state
384	*/
385	public Block getBlockForState(int id) {
386	return blockForState[id];	2✔
387	}
388
389	/**
390	* Retrieves a representative state from the given block. This method behaves deterministically.
391	*
392	* @param b
393	* the block
394	*
395	* @return a representative state in the specified block
396	*/
397	public int getRepresentative(Block b) {
398	return blockData[b.low];	2✔
399	}
400
401	/**
402	* Retrieves an iterator for the contents of the given block.
403	*
404	* @param b
405	* the block
406	*
407	* @return an iterator for the contents of the specified block
408	*/
409	public PrimitiveIterator.OfInt statesInBlockIterator(Block b) {
410	return Spliterators.iterator(statesInBlockSpliterator(b));	×
411	}
412
413	/**
414	* Retrieves a spliterator for the contents of the given block.
415	*
416	* @param b
417	* the block
418	*
419	* @return a spliterator for the contents of the specified block
420	*/
421	public Spliterator.OfInt statesInBlockSpliterator(Block b) {
422	return Arrays.spliterator(blockData, b.low, b.high);	×
423	}
424
425	/**
426	* Retrieves an iterator for iterating over all blocks in the block list.
427	*
428	* @return an iterator for iterating over all blocks
429	*/
430	public Iterator<Block> blockListIterator() {
431	return Block.blockListIterator(blocklistHead);	2✔
432	}
433
434	/**
435	* Retrieves an {@link Iterable} that provides the iterator returned by {@link #blockListIterator()}.
436	*
437	* @return an {@link Iterable} for iterating over all blocks
438	*/
439	public Iterable<Block> blockList() {
440	return this::blockListIterator;	2✔
441	}
442
443	/**
444	* Retrieves the total number of blocks in the block list.
445	*
446	* @return the total number of blocks
447	*/
448	public int getNumBlocks() {
449	return numBlocks;	2✔
450	}
451	}

LearnLib / automatalib / 12304577693

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