7848080436

Committed 09 Feb 2024 06:23PM UTC coverage: 89.895% (+0.05%) from 89.841%

Build # 7848080436

Build Type

push

github

Committed by

web-flow

Commit Message

Unify parsing exceptions and hide implementation details (#74)

* unify parsing exceptions and hide implementation details

* add changelog entry

* add missing throws statements

Run Details

9 of 18 new or added lines in 8 files covered. (50.0%)

3 existing lines in 1 file now uncovered.

15808 of 17585 relevant lines covered (89.89%)

1.66 hits per line

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

80.0

/modelchecking/ltsmin/src/main/java/net/automatalib/modelchecker/ltsmin/ltl/LTSminLTLDFA.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.modelchecker.ltsmin.ltl;

import java.io.File;
import java.io.IOException;
import java.util.Collection;
import java.util.function.Function;

import de.learnlib.tooling.annotation.builder.GenerateBuilder;
import net.automatalib.automaton.fsa.DFA;
import net.automatalib.automaton.fsa.impl.CompactDFA;
import net.automatalib.exception.FormatException;
import net.automatalib.exception.ModelCheckingException;
import net.automatalib.modelchecker.ltsmin.LTSminDFA;
import net.automatalib.modelchecker.ltsmin.LTSminLTLParser;
import net.automatalib.modelchecking.Lasso.DFALasso;
import net.automatalib.modelchecking.ModelCheckerLasso.DFAModelCheckerLasso;
import net.automatalib.modelchecking.impl.DFALassoImpl;
import net.automatalib.serialization.fsm.parser.FSM2DFAParser;
import org.checkerframework.checker.nullness.qual.Nullable;
import org.slf4j.Logger;
import org.slf4j.LoggerFactory;

/**
 * An LTL model checker using LTSmin for DFAs.
 *
 * @param <I>
 *         the input type
 */
public class LTSminLTLDFA<I> extends AbstractLTSminLTL<I, DFA<?, I>, DFALasso<I>>
        implements DFAModelCheckerLasso<I, String>, LTSminDFA<I, DFALasso<I>> {

    private static final Logger LOGGER = LoggerFactory.getLogger(LTSminLTLDFA.class);

    /**
     * The index in the FSM state vector for accept/reject.
     */
    public static final String LABEL_NAME = "label";

    /**
     * The value in the state vector for acceptance.
     */
    public static final String LABEL_VALUE = "accept";

    @GenerateBuilder(defaults = AbstractLTSminLTL.BuilderDefaults.class)
    public LTSminLTLDFA(boolean keepFiles, Function<String, I> string2Input, int minimumUnfolds, double multiplier) {
        super(keepFiles, string2Input, minimumUnfolds, multiplier);
    }

    @Override
    protected void verifyFormula(String formula) throws FormatException {
        LTSminLTLParser.requireValidLetterFormula(formula);
    }

    /**
     * Converts the FSM file to a {@link DFALasso}.
     *
     * @param automaton
     *         the DFA used to compute the number of loop unrolls.
     *
     * @see AbstractLTSminLTL#findCounterExample(Object, Collection, Object)
     */
    @Override
    public @Nullable DFALasso<I> findCounterExample(DFA<?, I> automaton, Collection<? extends I> inputs, String property) {
        final File fsm = findCounterExampleFSM(automaton, inputs, property);

        if (fsm == null) {
            return null;
        }

        try {
            final CompactDFA<I> dfa =
                    FSM2DFAParser.getParser(inputs, getString2Input(), LABEL_NAME, LABEL_VALUE).readModel(fsm);

            return new DFALassoImpl<>(dfa, inputs, computeUnfolds(automaton.size()));
        } catch (IOException | FormatException e) {
            throw new ModelCheckingException(e);
        } finally {
            // check if we must keep the FSM
            if (!isKeepFiles() && !fsm.delete()) {
                LOGGER.warn("Could not delete file: " + fsm.getAbsolutePath());
            }
        }
    }
}

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.modelchecker.ltsmin.ltl;
17
18	import java.io.File;
19	import java.io.IOException;
20	import java.util.Collection;
21	import java.util.function.Function;
22
23	import de.learnlib.tooling.annotation.builder.GenerateBuilder;
24	import net.automatalib.automaton.fsa.DFA;
25	import net.automatalib.automaton.fsa.impl.CompactDFA;
26	import net.automatalib.exception.FormatException;
27	import net.automatalib.exception.ModelCheckingException;
28	import net.automatalib.modelchecker.ltsmin.LTSminDFA;
29	import net.automatalib.modelchecker.ltsmin.LTSminLTLParser;
30	import net.automatalib.modelchecking.Lasso.DFALasso;
31	import net.automatalib.modelchecking.ModelCheckerLasso.DFAModelCheckerLasso;
32	import net.automatalib.modelchecking.impl.DFALassoImpl;
33	import net.automatalib.serialization.fsm.parser.FSM2DFAParser;
34	import org.checkerframework.checker.nullness.qual.Nullable;
35	import org.slf4j.Logger;
36	import org.slf4j.LoggerFactory;
37
38	/**
39	* An LTL model checker using LTSmin for DFAs.
40	*
41	* @param <I>
42	* the input type
43	*/
44	public class LTSminLTLDFA<I> extends AbstractLTSminLTL<I, DFA<?, I>, DFALasso<I>>
45	implements DFAModelCheckerLasso<I, String>, LTSminDFA<I, DFALasso<I>> {
46
47	private static final Logger LOGGER = LoggerFactory.getLogger(LTSminLTLDFA.class);	2✔
48
49	/**
50	* The index in the FSM state vector for accept/reject.
51	*/
52	public static final String LABEL_NAME = "label";
53
54	/**
55	* The value in the state vector for acceptance.
56	*/
57	public static final String LABEL_VALUE = "accept";
58
59	@GenerateBuilder(defaults = AbstractLTSminLTL.BuilderDefaults.class)
60	public LTSminLTLDFA(boolean keepFiles, Function<String, I> string2Input, int minimumUnfolds, double multiplier) {
61	super(keepFiles, string2Input, minimumUnfolds, multiplier);	2✔
62	}	2✔
63
64	@Override
65	protected void verifyFormula(String formula) throws FormatException {
66	LTSminLTLParser.requireValidLetterFormula(formula);	2✔
67	}	2✔
68
69	/**
70	* Converts the FSM file to a {@link DFALasso}.
71	*
72	* @param automaton
73	* the DFA used to compute the number of loop unrolls.
74	*
75	* @see AbstractLTSminLTL#findCounterExample(Object, Collection, Object)
76	*/
77	@Override
78	public @Nullable DFALasso<I> findCounterExample(DFA<?, I> automaton, Collection<? extends I> inputs, String property) {
79	final File fsm = findCounterExampleFSM(automaton, inputs, property);	2✔
80
81	if (fsm == null) {	2✔
82	return null;	2✔
83	}
84
85	try {
86	final CompactDFA<I> dfa =	2✔
87	FSM2DFAParser.getParser(inputs, getString2Input(), LABEL_NAME, LABEL_VALUE).readModel(fsm);	2✔
88
89	return new DFALassoImpl<>(dfa, inputs, computeUnfolds(automaton.size()));	2✔
NEW 90	} catch (IOException \| FormatException e) {	×
91	throw new ModelCheckingException(e);	×
92	} finally {
93	// check if we must keep the FSM
94	if (!isKeepFiles() && !fsm.delete()) {	2✔
95	LOGGER.warn("Could not delete file: " + fsm.getAbsolutePath());	×
96	}
97	}
98	}
99	}

LearnLib / automatalib / 7848080436

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