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.88

/modelchecking/m3c/src/main/java/net/automatalib/modelchecker/m3c/transformer/ADDTransformer.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.modelchecker.m3c.transformer;

import java.util.ArrayList;
import java.util.BitSet;
import java.util.List;
import java.util.Objects;
import java.util.Set;

import info.scce.addlib.dd.xdd.XDD;
import info.scce.addlib.dd.xdd.XDDManager;
import info.scce.addlib.dd.xdd.latticedd.example.BooleanVector;
import net.automatalib.modelchecker.m3c.formula.AbstractModalFormulaNode;
import net.automatalib.modelchecker.m3c.formula.BoxNode;
import net.automatalib.modelchecker.m3c.formula.DependencyGraph;
import net.automatalib.modelchecker.m3c.formula.DiamondNode;
import net.automatalib.modelchecker.m3c.formula.EquationalBlock;
import net.automatalib.modelchecker.m3c.formula.FormulaNode;
import net.automatalib.ts.modal.transition.ModalEdgeProperty;
import org.checkerframework.checker.nullness.qual.EnsuresNonNullIf;
import org.checkerframework.checker.nullness.qual.MonotonicNonNull;
import org.checkerframework.checker.nullness.qual.Nullable;

/**
 * An ADDTransformer represents a property transformer for a single ADD (Algebraic Decision Diagram).
 *
 * @param <L>
 *         edge label type
 * @param <AP>
 *         atomic proposition type
 */
public class ADDTransformer<L, AP> extends AbstractPropertyTransformer<ADDTransformer<L, AP>, L, AP> {

    private final XDDManager<BooleanVector> xddManager;
    private final @MonotonicNonNull XDD<BooleanVector> add;

    ADDTransformer(XDDManager<BooleanVector> xddManager, XDD<BooleanVector> add) {
        this.xddManager = xddManager;
        this.add = add;
    }

    ADDTransformer(XDDManager<BooleanVector> xddManager, XDD<BooleanVector> add, boolean isMust) {
        super(isMust);
        this.xddManager = xddManager;
        this.add = add;
    }

    /**
     * Constructor used to initialize the property transformer of a node.
     *
     * @param xddManager
     *         used to create the ADD
     * @param dependGraph
     *         of the formula that is currently being solved
     */
    public ADDTransformer(XDDManager<BooleanVector> xddManager, DependencyGraph<L, AP> dependGraph) {
        this.xddManager = xddManager;
        final boolean[] terminal = new boolean[dependGraph.getNumVariables()];
        for (EquationalBlock<L, AP> block : dependGraph.getBlocks()) {
            if (block.isMaxBlock()) {
                for (FormulaNode<L, AP> node : block.getNodes()) {
                    terminal[node.getVarNumber()] = true;
                }
            }
        }
        add = xddManager.constant(new BooleanVector(terminal));
    }

    /**
     * Creates the identity function. This sets the internal {@link XDD ADD} to {@code null} to avoid the construction
     * of the ADD, which is very expensive. To prevent null-pointer exceptions when using {@link #getAdd()}, it can be
     * checked with {@link #isIdentity()}.
     *
     * @param ddManager
     *         used to create the ADD
     */
    public ADDTransformer(XDDManager<BooleanVector> ddManager) {
        this.xddManager = ddManager;
        this.add = null;
    }

    /**
     * Constructor used to create the property transformer for an edge.
     *
     * @param xddManager
     *         used to create the ADD
     * @param edgeLabel
     *         of the edge
     * @param edgeProperty
     *         of the edge
     * @param dependGraph
     *         of the formula that is currently being solved
     * @param <TP>
     *         edge property type
     */
    public <TP extends ModalEdgeProperty> ADDTransformer(XDDManager<BooleanVector> xddManager,
                                                         L edgeLabel,
                                                         TP edgeProperty,
                                                         DependencyGraph<L, AP> dependGraph) {
        this.xddManager = xddManager;
        final List<XDD<BooleanVector>> list = new ArrayList<>();
        for (FormulaNode<L, AP> node : dependGraph.getFormulaNodes()) {
            final boolean[] terminal = new boolean[dependGraph.getNumVariables()];
            final XDD<BooleanVector> falseDD = xddManager.constant(new BooleanVector(terminal));
            if (node instanceof AbstractModalFormulaNode) {
                final AbstractModalFormulaNode<L, AP> modalNode = (AbstractModalFormulaNode<L, AP>) node;
                final L action = modalNode.getAction();
                if ((action == null || action.equals(edgeLabel)) &&
                    (!(modalNode instanceof DiamondNode) || edgeProperty.isMust())) {
                    int xj = modalNode.getVarNumberChild();
                    final boolean[] thenTerminal = new boolean[dependGraph.getNumVariables()];
                    thenTerminal[modalNode.getVarNumber()] = true;
                    final XDD<BooleanVector> thenDD = xddManager.constant(new BooleanVector(thenTerminal));
                    final XDD<BooleanVector> id = xddManager.ithVar(xj, thenDD, falseDD);
                    list.add(id);
                } else if (modalNode instanceof BoxNode) {
                    terminal[modalNode.getVarNumber()] = true;
                    list.add(xddManager.constant(new BooleanVector(terminal)));
                }
            }
        }

        XDD<BooleanVector> tmpADD;
        if (list.isEmpty()) {
            tmpADD = xddManager.constant(new BooleanVector(new boolean[dependGraph.getNumVariables()]));
        } else {
            tmpADD = list.get(0);
            for (int i = 1; i < list.size(); i++) {
                tmpADD = tmpADD.apply(BooleanVector::or, list.get(i));
            }
        }

        this.add = tmpADD;
    }

    @Override
    public BitSet evaluate(boolean[] input) {
        final boolean[] leafData = this.add == null ? input : this.add.eval(input).v().data();
        final BitSet satisfiedVars = new BitSet();
        for (int i = 0; i < leafData.length; i++) {
            if (leafData[i]) {
                satisfiedVars.set(i);
            }
        }
        return satisfiedVars;
    }

    @Override
    // false-positive, see https://github.com/typetools/checker-framework/issues/4872
    @SuppressWarnings("dereference.of.nullable")
    public ADDTransformer<L, AP> compose(ADDTransformer<L, AP> other) {
        final XDD<BooleanVector> compAdd;

        if (this.isIdentity() && other.isIdentity()) {
            throw new IllegalStateException("Two identity functions should never be composed");
        } else if (this.isIdentity()) {
            compAdd = new XDD<>(other.add.ptr(), xddManager);
        } else if (other.isIdentity()) {
            compAdd = new XDD<>(this.add.ptr(), xddManager);
        } else {
            compAdd = other.add.monadicApply(arg -> {
                boolean[] terminal = arg.data().clone();
                return this.add.eval(terminal).v();
            });
        }

        return new ADDTransformer<>(xddManager, compAdd, this.isMust());
    }

    @Override
    public ADDTransformer<L, AP> createUpdate(Set<AP> atomicPropositions,
                                              List<ADDTransformer<L, AP>> compositions,
                                              EquationalBlock<L, AP> currentBlock) {
        XDD<BooleanVector> updatedADD;
        final DiamondOperation<AP> diamondOp = new DiamondOperation<>(atomicPropositions, currentBlock);
        if (compositions.isEmpty()) {
            assert this.add != null : "The identity function should never be updated";
            updatedADD = this.add.monadicApply(new DiamondOperationDeadlock<>(atomicPropositions, currentBlock));
        } else {
            final XDD<BooleanVector> firstAdd = compositions.get(0).add;
            assert firstAdd != null : "The identity function should never be updated";
            updatedADD = preserveUpdatedTransformer(firstAdd, currentBlock);

            for (ADDTransformer<L, AP> composition : compositions) {
                assert composition.add != null : "The identity function should never be updated";
                updatedADD = updatedADD.apply(diamondOp, composition.add);
            }
        }

        return new ADDTransformer<>(xddManager, updatedADD);
    }

    private XDD<BooleanVector> preserveUpdatedTransformer(XDD<BooleanVector> rightDD,
                                                          EquationalBlock<L, AP> currentBlock) {
        assert this.add != null : "The identity function should never be updated";
        /* We create a new XDD where the information of this.add (the add before the update) is 'injected'
        into rightDD, the first composition DD, such that the bits corresponding to subformulas outside the current
        block are preserved */
        return this.add.apply((booleanVectorBeforeUpdate, booleanVectorRight) -> {
            boolean[] result = booleanVectorBeforeUpdate.data().clone();
            for (FormulaNode<?, AP> node : currentBlock.getNodes()) {
                result[node.getVarNumber()] = booleanVectorRight.data()[node.getVarNumber()];
            }
            return new BooleanVector(result);
        }, rightDD);
    }

    /**
     * Returns the ADD which represents the property transformer.
     *
     * @return the ADD which represents the property transformer or {@code null} if the property transformer is the
     * identity function
     */
    public @Nullable XDD<BooleanVector> getAdd() {
        return this.add;
    }

    /**
     * Returns whether the property transformer is the identity function.
     *
     * @return {@code true} if the property transformer is the identity function, {@code false} otherwise
     */
    @EnsuresNonNullIf(result = false, expression = {"add", "getAdd()"})
    @SuppressWarnings("contracts.conditional.postcondition") // getAdd() is pure
    public boolean isIdentity() {
        return this.add == null;
    }

    @Override
    public int hashCode() {
        return Objects.hashCode(add);
    }

    @Override
    public boolean equals(@Nullable Object o) {
        if (this == o) {
            return true;
        }
        if (o == null || getClass() != o.getClass()) {
            return false;
        }

        final ADDTransformer<?, ?> that = (ADDTransformer<?, ?>) o;

        return Objects.equals(this.add, that.add);
    }
}

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.modelchecker.m3c.transformer;
17
18	import java.util.ArrayList;
19	import java.util.BitSet;
20	import java.util.List;
21	import java.util.Objects;
22	import java.util.Set;
23
24	import info.scce.addlib.dd.xdd.XDD;
25	import info.scce.addlib.dd.xdd.XDDManager;
26	import info.scce.addlib.dd.xdd.latticedd.example.BooleanVector;
27	import net.automatalib.modelchecker.m3c.formula.AbstractModalFormulaNode;
28	import net.automatalib.modelchecker.m3c.formula.BoxNode;
29	import net.automatalib.modelchecker.m3c.formula.DependencyGraph;
30	import net.automatalib.modelchecker.m3c.formula.DiamondNode;
31	import net.automatalib.modelchecker.m3c.formula.EquationalBlock;
32	import net.automatalib.modelchecker.m3c.formula.FormulaNode;
33	import net.automatalib.ts.modal.transition.ModalEdgeProperty;
34	import org.checkerframework.checker.nullness.qual.EnsuresNonNullIf;
35	import org.checkerframework.checker.nullness.qual.MonotonicNonNull;
36	import org.checkerframework.checker.nullness.qual.Nullable;
37
38	/**
39	* An ADDTransformer represents a property transformer for a single ADD (Algebraic Decision Diagram).
40	*
41	* @param <L>
42	* edge label type
43	* @param <AP>
44	* atomic proposition type
45	*/
46	public class ADDTransformer<L, AP> extends AbstractPropertyTransformer<ADDTransformer<L, AP>, L, AP> {	2✔
47
48	private final XDDManager<BooleanVector> xddManager;
49	private final @MonotonicNonNull XDD<BooleanVector> add;
50
51	ADDTransformer(XDDManager<BooleanVector> xddManager, XDD<BooleanVector> add) {	2✔
52	this.xddManager = xddManager;	2✔
53	this.add = add;	2✔
54	}	2✔
55
56	ADDTransformer(XDDManager<BooleanVector> xddManager, XDD<BooleanVector> add, boolean isMust) {
57	super(isMust);	2✔
58	this.xddManager = xddManager;	2✔
59	this.add = add;	2✔
60	}	2✔
61
62	/**
63	* Constructor used to initialize the property transformer of a node.
64	*
65	* @param xddManager
66	* used to create the ADD
67	* @param dependGraph
68	* of the formula that is currently being solved
69	*/
70	public ADDTransformer(XDDManager<BooleanVector> xddManager, DependencyGraph<L, AP> dependGraph) {	2✔
71	this.xddManager = xddManager;	2✔
72	final boolean[] terminal = new boolean[dependGraph.getNumVariables()];	2✔
73	for (EquationalBlock<L, AP> block : dependGraph.getBlocks()) {	2✔
74	if (block.isMaxBlock()) {	2✔
75	for (FormulaNode<L, AP> node : block.getNodes()) {	2✔
76	terminal[node.getVarNumber()] = true;	2✔
77	}	2✔
78	}
79	}	2✔
80	add = xddManager.constant(new BooleanVector(terminal));	2✔
81	}	2✔
82
83	/**
84	* Creates the identity function. This sets the internal {@link XDD ADD} to {@code null} to avoid the construction
85	* of the ADD, which is very expensive. To prevent null-pointer exceptions when using {@link #getAdd()}, it can be
86	* checked with {@link #isIdentity()}.
87	*
88	* @param ddManager
89	* used to create the ADD
90	*/
91	public ADDTransformer(XDDManager<BooleanVector> ddManager) {	2✔
92	this.xddManager = ddManager;	2✔
93	this.add = null;	2✔
94	}	2✔
95
96	/**
97	* Constructor used to create the property transformer for an edge.
98	*
99	* @param xddManager
100	* used to create the ADD
101	* @param edgeLabel
102	* of the edge
103	* @param edgeProperty
104	* of the edge
105	* @param dependGraph
106	* of the formula that is currently being solved
107	* @param <TP>
108	* edge property type
109	*/
110	public <TP extends ModalEdgeProperty> ADDTransformer(XDDManager<BooleanVector> xddManager,
111	L edgeLabel,
112	TP edgeProperty,
113	DependencyGraph<L, AP> dependGraph) {	2✔
114	this.xddManager = xddManager;	2✔
115	final List<XDD<BooleanVector>> list = new ArrayList<>();	2✔
116	for (FormulaNode<L, AP> node : dependGraph.getFormulaNodes()) {	2✔
117	final boolean[] terminal = new boolean[dependGraph.getNumVariables()];	2✔
118	final XDD<BooleanVector> falseDD = xddManager.constant(new BooleanVector(terminal));	2✔
119	if (node instanceof AbstractModalFormulaNode) {	2✔
120	final AbstractModalFormulaNode<L, AP> modalNode = (AbstractModalFormulaNode<L, AP>) node;	2✔
121	final L action = modalNode.getAction();	2✔
122	if ((action == null \|\| action.equals(edgeLabel)) &&	2✔
123	(!(modalNode instanceof DiamondNode) \|\| edgeProperty.isMust())) {	2✔
124	int xj = modalNode.getVarNumberChild();	2✔
125	final boolean[] thenTerminal = new boolean[dependGraph.getNumVariables()];	2✔
126	thenTerminal[modalNode.getVarNumber()] = true;	2✔
127	final XDD<BooleanVector> thenDD = xddManager.constant(new BooleanVector(thenTerminal));	2✔
128	final XDD<BooleanVector> id = xddManager.ithVar(xj, thenDD, falseDD);	2✔
129	list.add(id);	2✔
130	} else if (modalNode instanceof BoxNode) {	2✔
131	terminal[modalNode.getVarNumber()] = true;	2✔
132	list.add(xddManager.constant(new BooleanVector(terminal)));	2✔
133	}
134	}
135	}	2✔
136
137	XDD<BooleanVector> tmpADD;
138	if (list.isEmpty()) {	2✔
139	tmpADD = xddManager.constant(new BooleanVector(new boolean[dependGraph.getNumVariables()]));	2✔
140	} else {
141	tmpADD = list.get(0);	2✔
142	for (int i = 1; i < list.size(); i++) {	2✔
143	tmpADD = tmpADD.apply(BooleanVector::or, list.get(i));	2✔
144	}
145	}
146
147	this.add = tmpADD;	2✔
148	}	2✔
149
150	@Override
151	public BitSet evaluate(boolean[] input) {
152	final boolean[] leafData = this.add == null ? input : this.add.eval(input).v().data();	2✔
153	final BitSet satisfiedVars = new BitSet();	2✔
154	for (int i = 0; i < leafData.length; i++) {	2✔
155	if (leafData[i]) {	2✔
156	satisfiedVars.set(i);	2✔
157	}
158	}
159	return satisfiedVars;	2✔
160	}
161
162	@Override
163	// false-positive, see https://github.com/typetools/checker-framework/issues/4872
164	@SuppressWarnings("dereference.of.nullable")
165	public ADDTransformer<L, AP> compose(ADDTransformer<L, AP> other) {
166	final XDD<BooleanVector> compAdd;
167
168	if (this.isIdentity() && other.isIdentity()) {	2✔
169	throw new IllegalStateException("Two identity functions should never be composed");	2✔
170	} else if (this.isIdentity()) {	2✔
171	compAdd = new XDD<>(other.add.ptr(), xddManager);	2✔
172	} else if (other.isIdentity()) {	2✔
173	compAdd = new XDD<>(this.add.ptr(), xddManager);	2✔
174	} else {
175	compAdd = other.add.monadicApply(arg -> {	2✔
176	boolean[] terminal = arg.data().clone();	2✔
177	return this.add.eval(terminal).v();	2✔
178	});
179	}
180
181	return new ADDTransformer<>(xddManager, compAdd, this.isMust());	2✔
182	}
183
184	@Override
185	public ADDTransformer<L, AP> createUpdate(Set<AP> atomicPropositions,
186	List<ADDTransformer<L, AP>> compositions,
187	EquationalBlock<L, AP> currentBlock) {
188	XDD<BooleanVector> updatedADD;
189	final DiamondOperation<AP> diamondOp = new DiamondOperation<>(atomicPropositions, currentBlock);	2✔
190	if (compositions.isEmpty()) {	2✔
191	assert this.add != null : "The identity function should never be updated";	2✔
192	updatedADD = this.add.monadicApply(new DiamondOperationDeadlock<>(atomicPropositions, currentBlock));	2✔
193	} else {
194	final XDD<BooleanVector> firstAdd = compositions.get(0).add;	2✔
195	assert firstAdd != null : "The identity function should never be updated";	2✔
196	updatedADD = preserveUpdatedTransformer(firstAdd, currentBlock);	2✔
197
198	for (ADDTransformer<L, AP> composition : compositions) {	2✔
199	assert composition.add != null : "The identity function should never be updated";	2✔
200	updatedADD = updatedADD.apply(diamondOp, composition.add);	2✔
201	}	2✔
202	}
203
204	return new ADDTransformer<>(xddManager, updatedADD);	2✔
205	}
206
207	private XDD<BooleanVector> preserveUpdatedTransformer(XDD<BooleanVector> rightDD,
208	EquationalBlock<L, AP> currentBlock) {
209	assert this.add != null : "The identity function should never be updated";	2✔
210	/* We create a new XDD where the information of this.add (the add before the update) is 'injected'
211	into rightDD, the first composition DD, such that the bits corresponding to subformulas outside the current
212	block are preserved */
213	return this.add.apply((booleanVectorBeforeUpdate, booleanVectorRight) -> {	2✔
214	boolean[] result = booleanVectorBeforeUpdate.data().clone();	2✔
215	for (FormulaNode<?, AP> node : currentBlock.getNodes()) {	2✔
216	result[node.getVarNumber()] = booleanVectorRight.data()[node.getVarNumber()];	2✔
217	}	2✔
218	return new BooleanVector(result);	2✔
219	}, rightDD);
220	}
221
222	/**
223	* Returns the ADD which represents the property transformer.
224	*
225	* @return the ADD which represents the property transformer or {@code null} if the property transformer is the
226	* identity function
227	*/
228	public @Nullable XDD<BooleanVector> getAdd() {
229	return this.add;	2✔
230	}
231
232	/**
233	* Returns whether the property transformer is the identity function.
234	*
235	* @return {@code true} if the property transformer is the identity function, {@code false} otherwise
236	*/
237	@EnsuresNonNullIf(result = false, expression = {"add", "getAdd()"})
238	@SuppressWarnings("contracts.conditional.postcondition") // getAdd() is pure
239	public boolean isIdentity() {
240	return this.add == null;	2✔
241	}
242
243	@Override
244	public int hashCode() {
245	return Objects.hashCode(add);	×
246	}
247
248	@Override
249	public boolean equals(@Nullable Object o) {
250	if (this == o) {	2✔
251	return true;	×
252	}
253	if (o == null \|\| getClass() != o.getClass()) {	2✔
254	return false;	×
255	}
256
257	final ADDTransformer<?, ?> that = (ADDTransformer<?, ?>) o;	2✔
258
259	return Objects.equals(this.add, that.add);	2✔
260	}
261	}

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