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

/util/src/main/java/net/automatalib/util/automaton/procedural/CFMPSViewSPA.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.automaton.procedural;

import java.util.ArrayList;
import java.util.Collection;
import java.util.Collections;
import java.util.HashMap;
import java.util.List;
import java.util.Map;
import java.util.Map.Entry;
import java.util.Set;

import net.automatalib.alphabet.ProceduralInputAlphabet;
import net.automatalib.automaton.fsa.DFA;
import net.automatalib.automaton.procedural.SPA;
import net.automatalib.common.util.HashUtil;
import net.automatalib.graph.ContextFreeModalProcessSystem;
import net.automatalib.graph.ProceduralModalProcessGraph;
import net.automatalib.ts.modal.transition.ProceduralModalEdgeProperty;
import net.automatalib.ts.modal.transition.ProceduralModalEdgeProperty.ProceduralType;
import org.checkerframework.checker.nullness.qual.Nullable;

/**
 * This class represents a {@link ContextFreeModalProcessSystem}-based view of the instrumented language for a given
 * {@link SPA}, which allows one to model-check language properties of {@link SPA}s with tools such as M3C.
 *
 * @param <I>
 *         input symbol type
 */
class CFMPSViewSPA<I> implements ContextFreeModalProcessSystem<I, Void> {

    private final SPA<?, I> spa;
    private final Map<I, ProceduralModalProcessGraph<?, I, ?, Void, ?>> pmpgs;

    CFMPSViewSPA(SPA<?, I> spa) {
        this.spa = spa;

        final Map<I, DFA<?, I>> procedures = spa.getProcedures();
        this.pmpgs = new HashMap<>(HashUtil.capacity(procedures.size()));

        for (Entry<I, DFA<?, I>> e : procedures.entrySet()) {
            this.pmpgs.put(e.getKey(), new MPGView<>(spa, e.getKey(), e.getValue()));
        }
    }

    @Override
    public Map<I, ProceduralModalProcessGraph<?, I, ?, Void, ?>> getPMPGs() {
        return this.pmpgs;
    }

    @Override
    public @Nullable I getMainProcess() {
        return this.spa.getInitialProcedure();
    }

    private static final class MPGView<S, I>
            implements ProceduralModalProcessGraph<S, I, PMPGEdge<I, S>, Void, ProceduralModalEdgeProperty> {

        private static final Object INITIAL = new Object();
        private static final Object FINAL = new Object();

        private final ProceduralInputAlphabet<I> alphabet;
        private final Collection<I> proceduralInputs;
        private final I procedure;
        private final DFA<S, I> dfa;
        private final S dfaInit;

        private final S initialNode;
        private final S finalNode;

        // we make sure to handle 'init' and 'end' correctly
        @SuppressWarnings("unchecked")
        MPGView(SPA<?, I> spa, I procedure, DFA<S, I> dfa) {

            final S dfaInit = dfa.getInitialState();

            if (dfaInit == null) {
                throw new IllegalArgumentException("Empty DFAs cannot be mapped to ModalProcessGraphs");
            }

            this.alphabet = spa.getInputAlphabet();
            this.proceduralInputs = spa.getProceduralInputs();
            this.procedure = procedure;
            this.dfa = dfa;
            this.dfaInit = dfaInit;

            this.initialNode = (S) INITIAL;
            this.finalNode = (S) FINAL;
        }

        @Override
        public Collection<PMPGEdge<I, S>> getOutgoingEdges(S node) {
            if (node == initialNode) {
                return Collections.singletonList(new PMPGEdge<>(this.procedure, this.dfaInit, ProceduralType.INTERNAL));
            } else if (node == finalNode) {
                return Collections.emptyList();
            } else {
                final List<PMPGEdge<I, S>> result;

                if (this.dfa.isAccepting(node)) {
                    result = new ArrayList<>(this.proceduralInputs.size() + 1);
                    result.add(new PMPGEdge<>(this.alphabet.getReturnSymbol(),
                                              this.getFinalNode(),
                                              ProceduralType.INTERNAL));
                } else {
                    result = new ArrayList<>(this.proceduralInputs.size());
                }

                for (I i : proceduralInputs) {
                    final S succ = this.dfa.getSuccessor(node, i);
                    if (succ != null) {
                        final ProceduralType type;

                        if (alphabet.isCallSymbol(i)) {
                            type = ProceduralType.PROCESS;
                        } else if (alphabet.isInternalSymbol(i)) {
                            type = ProceduralType.INTERNAL;
                        } else {
                            throw new IllegalStateException("Unexpected symbol type");
                        }

                        result.add(new PMPGEdge<>(i, succ, type));
                    }
                }

                return result;
            }
        }

        @Override
        public S getTarget(PMPGEdge<I, S> edge) {
            return edge.succ;
        }

        @Override
        public Collection<S> getNodes() {
            final List<S> nodes = new ArrayList<>(dfa.size() + 2);
            nodes.add(this.initialNode);
            nodes.add(this.finalNode);
            nodes.addAll(dfa.getStates());
            return nodes;
        }

        @Override
        public Set<Void> getNodeProperty(S node) {
            return Collections.emptySet();
        }

        @Override
        public ProceduralModalEdgeProperty getEdgeProperty(PMPGEdge<I, S> edge) {
            return edge;
        }

        @Override
        public I getEdgeLabel(PMPGEdge<I, S> edge) {
            return edge.input;
        }

        @Override
        public S getFinalNode() {
            return this.finalNode;
        }

        @Override
        public S getInitialNode() {
            return this.initialNode;
        }
    }
}

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.automaton.procedural;
17
18	import java.util.ArrayList;
19	import java.util.Collection;
20	import java.util.Collections;
21	import java.util.HashMap;
22	import java.util.List;
23	import java.util.Map;
24	import java.util.Map.Entry;
25	import java.util.Set;
26
27	import net.automatalib.alphabet.ProceduralInputAlphabet;
28	import net.automatalib.automaton.fsa.DFA;
29	import net.automatalib.automaton.procedural.SPA;
30	import net.automatalib.common.util.HashUtil;
31	import net.automatalib.graph.ContextFreeModalProcessSystem;
32	import net.automatalib.graph.ProceduralModalProcessGraph;
33	import net.automatalib.ts.modal.transition.ProceduralModalEdgeProperty;
34	import net.automatalib.ts.modal.transition.ProceduralModalEdgeProperty.ProceduralType;
35	import org.checkerframework.checker.nullness.qual.Nullable;
36
37	/**
38	* This class represents a {@link ContextFreeModalProcessSystem}-based view of the instrumented language for a given
39	* {@link SPA}, which allows one to model-check language properties of {@link SPA}s with tools such as M3C.
40	*
41	* @param <I>
42	* input symbol type
43	*/
44	class CFMPSViewSPA<I> implements ContextFreeModalProcessSystem<I, Void> {
45
46	private final SPA<?, I> spa;
47	private final Map<I, ProceduralModalProcessGraph<?, I, ?, Void, ?>> pmpgs;
48
49	CFMPSViewSPA(SPA<?, I> spa) {	2✔
50	this.spa = spa;	2✔
51
52	final Map<I, DFA<?, I>> procedures = spa.getProcedures();	2✔
53	this.pmpgs = new HashMap<>(HashUtil.capacity(procedures.size()));	2✔
54
55	for (Entry<I, DFA<?, I>> e : procedures.entrySet()) {	2✔
56	this.pmpgs.put(e.getKey(), new MPGView<>(spa, e.getKey(), e.getValue()));	2✔
57	}	2✔
58	}	2✔
59
60	@Override
61	public Map<I, ProceduralModalProcessGraph<?, I, ?, Void, ?>> getPMPGs() {
62	return this.pmpgs;	2✔
63	}
64
65	@Override
66	public @Nullable I getMainProcess() {
67	return this.spa.getInitialProcedure();	2✔
68	}
69
70	private static final class MPGView<S, I>
71	implements ProceduralModalProcessGraph<S, I, PMPGEdge<I, S>, Void, ProceduralModalEdgeProperty> {
72
73	private static final Object INITIAL = new Object();	2✔
74	private static final Object FINAL = new Object();	2✔
75
76	private final ProceduralInputAlphabet<I> alphabet;
77	private final Collection<I> proceduralInputs;
78	private final I procedure;
79	private final DFA<S, I> dfa;
80	private final S dfaInit;
81
82	private final S initialNode;
83	private final S finalNode;
84
85	// we make sure to handle 'init' and 'end' correctly
86	@SuppressWarnings("unchecked")
87	MPGView(SPA<?, I> spa, I procedure, DFA<S, I> dfa) {	2✔
88
89	final S dfaInit = dfa.getInitialState();	2✔
90
91	if (dfaInit == null) {	2✔
92	throw new IllegalArgumentException("Empty DFAs cannot be mapped to ModalProcessGraphs");	×
93	}
94
95	this.alphabet = spa.getInputAlphabet();	2✔
96	this.proceduralInputs = spa.getProceduralInputs();	2✔
97	this.procedure = procedure;	2✔
98	this.dfa = dfa;	2✔
99	this.dfaInit = dfaInit;	2✔
100
101	this.initialNode = (S) INITIAL;	2✔
102	this.finalNode = (S) FINAL;	2✔
103	}	2✔
104
105	@Override
106	public Collection<PMPGEdge<I, S>> getOutgoingEdges(S node) {
107	if (node == initialNode) {	2✔
108	return Collections.singletonList(new PMPGEdge<>(this.procedure, this.dfaInit, ProceduralType.INTERNAL));	2✔
109	} else if (node == finalNode) {	2✔
110	return Collections.emptyList();	2✔
111	} else {
112	final List<PMPGEdge<I, S>> result;
113
114	if (this.dfa.isAccepting(node)) {	2✔
115	result = new ArrayList<>(this.proceduralInputs.size() + 1);	2✔
116	result.add(new PMPGEdge<>(this.alphabet.getReturnSymbol(),	2✔
117	this.getFinalNode(),	2✔
118	ProceduralType.INTERNAL));
119	} else {
120	result = new ArrayList<>(this.proceduralInputs.size());	2✔
121	}
122
123	for (I i : proceduralInputs) {	2✔
124	final S succ = this.dfa.getSuccessor(node, i);	2✔
125	if (succ != null) {	2✔
126	final ProceduralType type;
127
128	if (alphabet.isCallSymbol(i)) {	2✔
129	type = ProceduralType.PROCESS;	2✔
130	} else if (alphabet.isInternalSymbol(i)) {	2✔
131	type = ProceduralType.INTERNAL;	2✔
132	} else {
133	throw new IllegalStateException("Unexpected symbol type");	×
134	}
135
136	result.add(new PMPGEdge<>(i, succ, type));	2✔
137	}
138	}	2✔
139
140	return result;	2✔
141	}
142	}
143
144	@Override
145	public S getTarget(PMPGEdge<I, S> edge) {
146	return edge.succ;	2✔
147	}
148
149	@Override
150	public Collection<S> getNodes() {
151	final List<S> nodes = new ArrayList<>(dfa.size() + 2);	2✔
152	nodes.add(this.initialNode);	2✔
153	nodes.add(this.finalNode);	2✔
154	nodes.addAll(dfa.getStates());	2✔
155	return nodes;	2✔
156	}
157
158	@Override
159	public Set<Void> getNodeProperty(S node) {
160	return Collections.emptySet();	2✔
161	}
162
163	@Override
164	public ProceduralModalEdgeProperty getEdgeProperty(PMPGEdge<I, S> edge) {
165	return edge;	2✔
166	}
167
168	@Override
169	public I getEdgeLabel(PMPGEdge<I, S> edge) {
170	return edge.input;	2✔
171	}
172
173	@Override
174	public S getFinalNode() {
175	return this.finalNode;	2✔
176	}
177
178	@Override
179	public S getInitialNode() {
180	return this.initialNode;	2✔
181	}
182	}
183	}

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