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

96.97

/util/src/main/java/net/automatalib/util/partitionrefinement/Block.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.partitionrefinement;

import java.util.Iterator;
import java.util.NoSuchElementException;

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

/**
 * A block (i.e., partition class) that is maintained during the Paige/Tarjan partition refinement algorithm (see
 * {@link Hopcroft}).
 * <p>
 * Like {@link Hopcroft}, this is a very low-level class that exposes a lot (almost all) of its fields directly. Care
 * should be taken that instances of this class are not returned (in any form) to the API user, but are hidden behind a
 * facade.
 */
public class Block {

    /**
     * The index of the first element in this block in the {@link Hopcroft#blockData} array.
     */
    public int low;
    /**
     * The current pointer, i.e., the delimiter between elements of this block which were found to belong to a potential
     * subclass of this block, and those that do not or have not been checked.
     * <p>
     * This variable will be maintained such that either {@code ptr == -1}, or <code>{@link #low} &lt;= ptr &lt;=
     * {@link #high}</code>.
     */
    public int ptr = -1;
    /**
     * The index of the last element in this block in the {@link Hopcroft#blockData} array, plus one.
     */
    public int high;
    public @Nullable Block nextBlock;
    public int id;
    protected @Nullable Block nextInWorklist;
    protected @Nullable Block nextTouched;

    /**
     * Constructor. Creates a new block with the specified parameters.
     *
     * @param low
     *         the low index of this block's data in the {@link Hopcroft#blockData} array
     * @param high
     *         the high index of this block's data in the {@link Hopcroft#blockData} array
     * @param id
     *         the ID of this block
     * @param next
     *         the next block in the block list
     */
    public Block(int low, int high, int id, @Nullable Block next) {
        this.low = low;
        this.high = high;
        this.id = id;
        this.nextBlock = next;
    }

    static Iterator<Block> blockListIterator(@Nullable Block start) {
        return new BlockListIterator(start);
    }

    /**
     * Retrieves the size of this block.
     *
     * @return the size of this block
     */
    public int size() {
        return high - low;
    }

    /**
     * Checks whether this block is empty.
     *
     * @return {@code true} if this block is empty, {@code false} otherwise
     */
    public boolean isEmpty() {
        return low >= high;
    }

    /**
     * Splits this block, if applicable. If this block cannot be split, {@code null} is returned.
     * <p>
     * A new block (the split result) is created if both <code>{@link #ptr} &gt; {@link #low}</code> and
     * <code>{@link #ptr} &lt; {@link #high}</code>. This new block will contain either the elements between
     * {@link #low} (inclusive) and {@link #ptr} (exclusive), or between {@link #ptr} (inclusive) and {@link #high}
     * (exclusive), depending on whichever range is smaller. This block will be updated to contain the remaining
     * elements.
     * <p>
     * When this method returns (regardless of whether a new block is created), the {@link #ptr} field will have been
     * reset to {@code -1}.
     * <p>
     * Preconditions: this.ptr != -1. Post-conditions: this.ptr = -1.
     *
     * @param newId
     *         the ID of the newly created block, if applicable
     *
     * @return a block
     */
    public @Nullable Block split(int newId) {
        int ptr = this.ptr;
        this.ptr = -1;
        int high = this.high;
        int ptrHighDiff = high - ptr;
        if (ptrHighDiff == 0) {
            return null;
        }
        int low = this.low;
        Block splt;
        if (ptrHighDiff > ptr - low) {
            splt = new Block(low, ptr, newId, nextBlock);
            this.low = ptr;
        } else {
            splt = new Block(ptr, high, newId, nextBlock);
            this.high = ptr;
        }
        this.nextBlock = splt;
        return splt;
    }

    private static final class BlockListIterator implements Iterator<Block> {

        private @Nullable Block curr;

        BlockListIterator(@Nullable Block start) {
            this.curr = start;
        }

        @Override
        public boolean hasNext() {
            return curr != null;
        }

        @Override
        public Block next() {
            Block result = curr;
            if (result == null) {
                throw new NoSuchElementException();
            }
            curr = result.nextBlock;
            return result;
        }
    }
}

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.partitionrefinement;
17
18	import java.util.Iterator;
19	import java.util.NoSuchElementException;
20
21	import org.checkerframework.checker.nullness.qual.Nullable;
22
23	/**
24	* A block (i.e., partition class) that is maintained during the Paige/Tarjan partition refinement algorithm (see
25	* {@link Hopcroft}).
26	* <p>
27	* Like {@link Hopcroft}, this is a very low-level class that exposes a lot (almost all) of its fields directly. Care
28	* should be taken that instances of this class are not returned (in any form) to the API user, but are hidden behind a
29	* facade.
30	*/
31	public class Block {
32
33	/**
34	* The index of the first element in this block in the {@link Hopcroft#blockData} array.
35	*/
36	public int low;
37	/**
38	* The current pointer, i.e., the delimiter between elements of this block which were found to belong to a potential
39	* subclass of this block, and those that do not or have not been checked.
40	* <p>
41	* This variable will be maintained such that either {@code ptr == -1}, or <code>{@link #low} <= ptr <=
42	* {@link #high}</code>.
43	*/
44	public int ptr = -1;	2✔
45	/**
46	* The index of the last element in this block in the {@link Hopcroft#blockData} array, plus one.
47	*/
48	public int high;
49	public @Nullable Block nextBlock;
50	public int id;
51	protected @Nullable Block nextInWorklist;
52	protected @Nullable Block nextTouched;
53
54	/**
55	* Constructor. Creates a new block with the specified parameters.
56	*
57	* @param low
58	* the low index of this block's data in the {@link Hopcroft#blockData} array
59	* @param high
60	* the high index of this block's data in the {@link Hopcroft#blockData} array
61	* @param id
62	* the ID of this block
63	* @param next
64	* the next block in the block list
65	*/
66	public Block(int low, int high, int id, @Nullable Block next) {	2✔
67	this.low = low;	2✔
68	this.high = high;	2✔
69	this.id = id;	2✔
70	this.nextBlock = next;	2✔
71	}	2✔
72
73	static Iterator<Block> blockListIterator(@Nullable Block start) {
74	return new BlockListIterator(start);	2✔
75	}
76
77	/**
78	* Retrieves the size of this block.
79	*
80	* @return the size of this block
81	*/
82	public int size() {
83	return high - low;	2✔
84	}
85
86	/**
87	* Checks whether this block is empty.
88	*
89	* @return {@code true} if this block is empty, {@code false} otherwise
90	*/
91	public boolean isEmpty() {
92	return low >= high;	2✔
93	}
94
95	/**
96	* Splits this block, if applicable. If this block cannot be split, {@code null} is returned.
97	* <p>
98	* A new block (the split result) is created if both <code>{@link #ptr} > {@link #low}</code> and
99	* <code>{@link #ptr} < {@link #high}</code>. This new block will contain either the elements between
100	* {@link #low} (inclusive) and {@link #ptr} (exclusive), or between {@link #ptr} (inclusive) and {@link #high}
101	* (exclusive), depending on whichever range is smaller. This block will be updated to contain the remaining
102	* elements.
103	* <p>
104	* When this method returns (regardless of whether a new block is created), the {@link #ptr} field will have been
105	* reset to {@code -1}.
106	* <p>
107	* Preconditions: this.ptr != -1. Post-conditions: this.ptr = -1.
108	*
109	* @param newId
110	* the ID of the newly created block, if applicable
111	*
112	* @return a block
113	*/
114	public @Nullable Block split(int newId) {
115	int ptr = this.ptr;	2✔
116	this.ptr = -1;	2✔
117	int high = this.high;	2✔
118	int ptrHighDiff = high - ptr;	2✔
119	if (ptrHighDiff == 0) {	2✔
120	return null;	2✔
121	}
122	int low = this.low;	2✔
123	Block splt;
124	if (ptrHighDiff > ptr - low) {	2✔
125	splt = new Block(low, ptr, newId, nextBlock);	2✔
126	this.low = ptr;	2✔
127	} else {
128	splt = new Block(ptr, high, newId, nextBlock);	2✔
129	this.high = ptr;	2✔
130	}
131	this.nextBlock = splt;	2✔
132	return splt;	2✔
133	}
134
135	private static final class BlockListIterator implements Iterator<Block> {
136
137	private @Nullable Block curr;
138
139	BlockListIterator(@Nullable Block start) {	2✔
140	this.curr = start;	2✔
141	}	2✔
142
143	@Override
144	public boolean hasNext() {
145	return curr != null;	2✔
146	}
147
148	@Override
149	public Block next() {
150	Block result = curr;	2✔
151	if (result == null) {	2✔
152	throw new NoSuchElementException();	×
153	}
154	curr = result.nextBlock;	2✔
155	return result;	2✔
156	}
157	}
158	}

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