12651580329

Committed 07 Jan 2025 12:29PM UTC coverage: 91.569% (+0.03%) from 91.542%

Build # 12651580329

Build Type

push

github

Committed by

web-flow

Commit Message

Update dependencies (#85)

* bump basic dependency versions

* bump checkstyle + cleanups

* bump spotbugs + cleanups

* bump pmd + cleanups

* bump checkerframework + cleanups

* some more cleanups

* ExceptionUtil: support nulls

* improve comments

* cleanup naming + formatting

* formatting

* formatting

* do not fail on javadoc warnings

completness of documentation is now checked by checkstyle and we would have to disable failing anyways when moving on to JDK 17

Run Details

192 of 217 new or added lines in 63 files covered. (88.48%)

4 existing lines in 4 files now uncovered.

16573 of 18099 relevant lines covered (91.57%)

1.69 hits per line

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

62.34

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

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

import net.automatalib.common.setting.AutomataLibSettings;
import net.automatalib.common.util.IOUtil;
import net.automatalib.common.util.collection.CollectionUtil;
import net.automatalib.common.util.process.ProcessUtil;
import net.automatalib.exception.FormatException;
import net.automatalib.exception.ModelCheckingException;
import net.automatalib.modelchecking.ModelChecker;
import net.automatalib.serialization.etf.writer.AbstractETFWriter;
import net.automatalib.serialization.fsm.parser.AbstractFSMParser;
import org.checkerframework.checker.initialization.qual.UnknownInitialization;
import org.checkerframework.checker.nullness.qual.Nullable;
import org.slf4j.Logger;
import org.slf4j.LoggerFactory;

/**
 * An LTL model checker using LTSmin.
 * <p>
 * The user must install LTSmin in order for {@link AbstractLTSmin} to run without exceptions. Once LTSmin is
 * installed the user may specify the path to the installed LTSmin binaries with the property
 * <b>automatalib.ltsmin.path</b>. If this property is not set the binaries will be run as usual (e.g. simply
 * by invoking etf2lts-mc, and ltsmin-convert), which means the user can also specify the location of the binaries in
 * the PATH environment variable.
 * <p>
 * This model checker is implemented as follows. The hypothesis automaton is first written to an LTS in ETF {@link
 * AbstractETFWriter} file, which serves as input for the etf2lts-mc binary. Then the etf2lts-mc binary is run, which
 * will write an LTS in GCF format. This LTS will be a subset of the language of the given hypothesis. Next, the GCF is
 * converted to FSM using the ltsmin-convert binary. Lastly, the FSM is read back into an automaton using an {@link
 * AbstractFSMParser}.
 *
 * @param <I>
 *         the input type.
 * @param <A>
 *         the automaton type.
 * @param <R>
 *         the type of counterexample
 *
 * @see <a href="http://ltsmin.utwente.nl">http://ltsmin.utwente.nl</a>
 * @see AbstractFSMParser
 * @see AbstractETFWriter
 * @see AutomataLibSettings
 */
public abstract class AbstractLTSmin<I, A, R> implements ModelChecker<I, A, String, R>, LTSmin<I, A, R> {

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

    private final boolean keepFiles;
    private final Function<String, I> string2Input;

    /**
     * Constructs a new AbstractLTSmin.
     *
     * @param keepFiles
     *         whether to keep intermediate files, (e.g. etfs, gcfs etc.).
     * @param string2Input
     *         a function that transforms edges in FSM files to actual input.
     *
     * @throws ModelCheckingException
     *         when the LTSmin binaries can not be run successfully.
     *
     * @see AbstractLTSmin
     */
    @SuppressWarnings("PMD.ConstructorCallsOverridableMethod") // it has no semantic impact
    protected AbstractLTSmin(boolean keepFiles, Function<String, I> string2Input) {
        this.keepFiles = keepFiles;
        this.string2Input = string2Input;

        if (!LTSminUtil.supports(getMinimumRequiredVersion())) {
            LOGGER.warn("LTSmin binary could not be detected in the correct version");
        }
    }

    /**
     * Returns the minimum required version of LTSmin.
     *
     * @return the major version.
     */
    protected abstract LTSminVersion getMinimumRequiredVersion(@UnknownInitialization(AbstractLTSmin.class) AbstractLTSmin<I, A, R> this);

    /**
     * Returns the extra command line options that should be given to the etf2lts-mc binary.
     *
     * @return the extra command line options.
     */
    protected abstract List<String> getExtraCommandLineOptions();

    /**
     * This method must verify that the given formula adheres to the expected syntax of the chosen serialization format
     * for hypotheses of {@code this} model-checker.
     *
     * @param formula
     *         the formula to verify
     *
     * @throws FormatException
     *         if the formula does not adhere to the expected syntax
     */
    protected abstract void verifyFormula(String formula) throws FormatException;

    @Override
    public boolean isKeepFiles() {
        return keepFiles;
    }

    @Override
    public Function<String, I> getString2Input() {
        return string2Input;
    }

    /**
     * Finds a counterexample for the given {@code formula}, and given {@code hypothesis} in FSM format.
     *
     * @param hypothesis
     *         the hypothesis to check
     * @param inputs
     *         the inputs which should be regarded for checking
     * @param formula
     *         the formula that should be checked
     *
     * @return a file containing the FSM representation for the found counterexample, or {@code null} if no such
     * counterexample could be found.
     *
     * @see AbstractLTSmin
     */
    protected final @Nullable File findCounterExampleFSM(A hypothesis, Collection<? extends I> inputs, String formula) {

        try {
            verifyFormula(formula);
        } catch (FormatException fe) {
            throw new ModelCheckingException(fe);
        }

        final File etf;

        try {
            // create the ETF that will contain the LTS of the hypothesis
            etf = File.createTempFile("automaton2etf", ".etf");

            try {
                // write to the ETF file
                automaton2ETF(hypothesis, inputs, etf);
            } catch (ModelCheckingException mce) {
                if (!keepFiles && !etf.delete()) {
                    logFileWarning(etf);
                }
                throw mce;
            }
        } catch (IOException ioe) {
            throw new ModelCheckingException(ioe);
        }

        final File ltlFile;

        try {
            // write LTL formula to a file because long formulae may cause problems as direct inputs to LTSmin
            ltlFile = File.createTempFile("formula", ".ltl");

            try (Writer w = IOUtil.asBufferedUTF8Writer(ltlFile)) {
                // write to the file
                w.write(formula);
            } catch (IOException ioe) {
                if (!keepFiles && !ltlFile.delete()) {
                    logFileWarning(ltlFile);
                }
                throw new ModelCheckingException(ioe);
            }
        } catch (IOException ioe) {
            throw new ModelCheckingException(ioe);
        }

        final File gcf;

        try {
            // create the GCF that will possibly contain the counterexample
            gcf = File.createTempFile("etf2gcf", ".gcf");
        } catch (IOException ioe) {
            if (!keepFiles && !etf.delete()) {
                logFileWarning(etf);
            }
            throw new ModelCheckingException(ioe);
        }

        // the command lines for the ProcessBuilder
        final List<String> ltsminCommandLine = CollectionUtil.list(// add the etf2lts-mc binary
                                                                   LTSminUtil.ETF2LTS_MC,
                                                                   // add the ETF file that contains the hypothesis
                                                                   etf.getAbsolutePath(),
                                                                   // add the LTL formula
                                                                   "--ltl=" + ltlFile,
                                                                   // write the trace to this file
                                                                   "--trace=" + gcf.getAbsolutePath(),
                                                                   // use only one thread (hypotheses are always small)
                                                                   "--threads=1",
                                                                   // use LTSmin LTL semantics
                                                                   "--ltl-semantics=ltsmin",
                                                                   // do not abort on partial LTSs
                                                                   "--allow-undefined-edges");

        if (LTSminUtil.isVerbose()) {
            ltsminCommandLine.add("-v");
        }

        ltsminCommandLine.addAll(getExtraCommandLineOptions());

        try {
            final int ltsminExitValue = runCommandLine(ltsminCommandLine);

            if (ltsminExitValue == 0) {
                // we have not found a counterexample
                return null;
            } else if (ltsminExitValue == 1) {
                // we have found a counterexample

                // create a file for the FSM
                final File fsm;
                try {
                    fsm = File.createTempFile("gcf2fsm", ".fsm");
                } catch (IOException ioe) {
                    throw new ModelCheckingException(ioe);
                }

                final List<String> convertCommandLine = CollectionUtil.list(// add the ltsmin-convert binary
                                                                            LTSminUtil.LTSMIN_CONVERT,
                                                                            // use the GCF as input
                                                                            gcf.getAbsolutePath(),
                                                                            // use the FSM as output
                                                                            fsm.getAbsolutePath(),
                                                                            // required option
                                                                            "--rdwr");

                if (LTSminUtil.isVerbose()) {
                    convertCommandLine.add("-v");
                }

                final int convertExitValue = runCommandLine(convertCommandLine);

                // check the conversion is successful
                if (convertExitValue != 0) {
                    throw new ModelCheckingException(
                            "Could not convert GCF to FSM. Enable debug logging to see LTSmin's debug information.");
                }

                return fsm;
            } else {
                throw new ModelCheckingException(
                        "Could not model check ETF. Enable debug logging to see LTSmin's debug information.");
            }
        } finally {
            if (!keepFiles) {
                if (!etf.delete()) {
                    logFileWarning(etf);
                }
                if (!ltlFile.delete()) {
                    logFileWarning(ltlFile);
                }
                if (!gcf.delete()) {
                    logFileWarning(gcf);
                }
            }
        }
    }

    private static int runCommandLine(List<String> commandLine) {
        try {
            LOGGER.debug("Invoking LTSmin binary as: {}", String.join(" ", commandLine));
            return ProcessUtil.invokeProcess(commandLine, LOGGER::debug);
        } catch (IOException | InterruptedException e) {
            throw new ModelCheckingException(e);
        }
    }

    private static void logFileWarning(File file) {
        LOGGER.warn("Could not delete file: '{}'", file.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;
17
18	import java.io.File;
19	import java.io.IOException;
20	import java.io.Writer;
21	import java.util.Collection;
22	import java.util.List;
23	import java.util.function.Function;
24
25	import net.automatalib.common.setting.AutomataLibSettings;
26	import net.automatalib.common.util.IOUtil;
27	import net.automatalib.common.util.collection.CollectionUtil;
28	import net.automatalib.common.util.process.ProcessUtil;
29	import net.automatalib.exception.FormatException;
30	import net.automatalib.exception.ModelCheckingException;
31	import net.automatalib.modelchecking.ModelChecker;
32	import net.automatalib.serialization.etf.writer.AbstractETFWriter;
33	import net.automatalib.serialization.fsm.parser.AbstractFSMParser;
34	import org.checkerframework.checker.initialization.qual.UnknownInitialization;
35	import org.checkerframework.checker.nullness.qual.Nullable;
36	import org.slf4j.Logger;
37	import org.slf4j.LoggerFactory;
38
39	/**
40	* An LTL model checker using LTSmin.
41	* <p>
42	* The user must install LTSmin in order for {@link AbstractLTSmin} to run without exceptions. Once LTSmin is
43	* installed the user may specify the path to the installed LTSmin binaries with the property
44	* <b>automatalib.ltsmin.path</b>. If this property is not set the binaries will be run as usual (e.g. simply
45	* by invoking etf2lts-mc, and ltsmin-convert), which means the user can also specify the location of the binaries in
46	* the PATH environment variable.
47	* <p>
48	* This model checker is implemented as follows. The hypothesis automaton is first written to an LTS in ETF {@link
49	* AbstractETFWriter} file, which serves as input for the etf2lts-mc binary. Then the etf2lts-mc binary is run, which
50	* will write an LTS in GCF format. This LTS will be a subset of the language of the given hypothesis. Next, the GCF is
51	* converted to FSM using the ltsmin-convert binary. Lastly, the FSM is read back into an automaton using an {@link
52	* AbstractFSMParser}.
53	*
54	* @param <I>
55	* the input type.
56	* @param <A>
57	* the automaton type.
58	* @param <R>
59	* the type of counterexample
60	*
61	* @see <a href="http://ltsmin.utwente.nl">http://ltsmin.utwente.nl</a>
62	* @see AbstractFSMParser
63	* @see AbstractETFWriter
64	* @see AutomataLibSettings
65	*/
66	public abstract class AbstractLTSmin<I, A, R> implements ModelChecker<I, A, String, R>, LTSmin<I, A, R> {
67
68	private static final Logger LOGGER = LoggerFactory.getLogger(AbstractLTSmin.class);	2✔
69
70	private final boolean keepFiles;
71	private final Function<String, I> string2Input;
72
73	/**
74	* Constructs a new AbstractLTSmin.
75	*
76	* @param keepFiles
77	* whether to keep intermediate files, (e.g. etfs, gcfs etc.).
78	* @param string2Input
79	* a function that transforms edges in FSM files to actual input.
80	*
81	* @throws ModelCheckingException
82	* when the LTSmin binaries can not be run successfully.
83	*
84	* @see AbstractLTSmin
85	*/
86	@SuppressWarnings("PMD.ConstructorCallsOverridableMethod") // it has no semantic impact
87	protected AbstractLTSmin(boolean keepFiles, Function<String, I> string2Input) {	2✔
88	this.keepFiles = keepFiles;	2✔
89	this.string2Input = string2Input;	2✔
90
91	if (!LTSminUtil.supports(getMinimumRequiredVersion())) {	2✔
NEW 92	LOGGER.warn("LTSmin binary could not be detected in the correct version");	×
93	}
94	}	2✔
95
96	/**
97	* Returns the minimum required version of LTSmin.
98	*
99	* @return the major version.
100	*/
101	protected abstract LTSminVersion getMinimumRequiredVersion(@UnknownInitialization(AbstractLTSmin.class) AbstractLTSmin<I, A, R> this);
102
103	/**
104	* Returns the extra command line options that should be given to the etf2lts-mc binary.
105	*
106	* @return the extra command line options.
107	*/
108	protected abstract List<String> getExtraCommandLineOptions();
109
110	/**
111	* This method must verify that the given formula adheres to the expected syntax of the chosen serialization format
112	* for hypotheses of {@code this} model-checker.
113	*
114	* @param formula
115	* the formula to verify
116	*
117	* @throws FormatException
118	* if the formula does not adhere to the expected syntax
119	*/
120	protected abstract void verifyFormula(String formula) throws FormatException;
121
122	@Override
123	public boolean isKeepFiles() {
124	return keepFiles;	2✔
125	}
126
127	@Override
128	public Function<String, I> getString2Input() {
129	return string2Input;	2✔
130	}
131
132	/**
133	* Finds a counterexample for the given {@code formula}, and given {@code hypothesis} in FSM format.
134	*
135	* @param hypothesis
136	* the hypothesis to check
137	* @param inputs
138	* the inputs which should be regarded for checking
139	* @param formula
140	* the formula that should be checked
141	*
142	* @return a file containing the FSM representation for the found counterexample, or {@code null} if no such
143	* counterexample could be found.
144	*
145	* @see AbstractLTSmin
146	*/
147	protected final @Nullable File findCounterExampleFSM(A hypothesis, Collection<? extends I> inputs, String formula) {
148
149	try {
150	verifyFormula(formula);	2✔
151	} catch (FormatException fe) {	×
152	throw new ModelCheckingException(fe);	×
153	}	2✔
154
155	final File etf;
156
157	try {
158	// create the ETF that will contain the LTS of the hypothesis
159	etf = File.createTempFile("automaton2etf", ".etf");	2✔
160
161	try {
162	// write to the ETF file
163	automaton2ETF(hypothesis, inputs, etf);	2✔
164	} catch (ModelCheckingException mce) {	2✔
165	if (!keepFiles && !etf.delete()) {	2✔
166	logFileWarning(etf);	×
167	}
168	throw mce;	2✔
169	}	2✔
170	} catch (IOException ioe) {	×
171	throw new ModelCheckingException(ioe);	×
172	}	2✔
173
174	final File ltlFile;
175
176	try {
177	// write LTL formula to a file because long formulae may cause problems as direct inputs to LTSmin
178	ltlFile = File.createTempFile("formula", ".ltl");	2✔
179
180	try (Writer w = IOUtil.asBufferedUTF8Writer(ltlFile)) {	2✔
181	// write to the file
182	w.write(formula);	2✔
183	} catch (IOException ioe) {	×
184	if (!keepFiles && !ltlFile.delete()) {	×
185	logFileWarning(ltlFile);	×
186	}
NEW 187	throw new ModelCheckingException(ioe);	×
188	}	2✔
189	} catch (IOException ioe) {	×
190	throw new ModelCheckingException(ioe);	×
191	}	2✔
192
193	final File gcf;
194
195	try {
196	// create the GCF that will possibly contain the counterexample
197	gcf = File.createTempFile("etf2gcf", ".gcf");	2✔
198	} catch (IOException ioe) {	×
199	if (!keepFiles && !etf.delete()) {	×
200	logFileWarning(etf);	×
201	}
202	throw new ModelCheckingException(ioe);	×
203	}	2✔
204
205	// the command lines for the ProcessBuilder
206	final List<String> ltsminCommandLine = CollectionUtil.list(// add the etf2lts-mc binary	2✔
207	LTSminUtil.ETF2LTS_MC,
208	// add the ETF file that contains the hypothesis
209	etf.getAbsolutePath(),	2✔
210	// add the LTL formula
211	"--ltl=" + ltlFile,
212	// write the trace to this file
213	"--trace=" + gcf.getAbsolutePath(),	2✔
214	// use only one thread (hypotheses are always small)
215	"--threads=1",
216	// use LTSmin LTL semantics
217	"--ltl-semantics=ltsmin",
218	// do not abort on partial LTSs
219	"--allow-undefined-edges");
220
221	if (LTSminUtil.isVerbose()) {	2✔
222	ltsminCommandLine.add("-v");	×
223	}
224
225	ltsminCommandLine.addAll(getExtraCommandLineOptions());	2✔
226
227	try {
228	final int ltsminExitValue = runCommandLine(ltsminCommandLine);	2✔
229
230	if (ltsminExitValue == 0) {	2✔
231	// we have not found a counterexample
232	return null;	2✔
233	} else if (ltsminExitValue == 1) {	2✔
234	// we have found a counterexample
235
236	// create a file for the FSM
237	final File fsm;
238	try {
239	fsm = File.createTempFile("gcf2fsm", ".fsm");	2✔
240	} catch (IOException ioe) {	×
241	throw new ModelCheckingException(ioe);	×
242	}	2✔
243
244	final List<String> convertCommandLine = CollectionUtil.list(// add the ltsmin-convert binary	2✔
245	LTSminUtil.LTSMIN_CONVERT,
246	// use the GCF as input
247	gcf.getAbsolutePath(),	2✔
248	// use the FSM as output
249	fsm.getAbsolutePath(),	2✔
250	// required option
251	"--rdwr");
252
253	if (LTSminUtil.isVerbose()) {	2✔
254	convertCommandLine.add("-v");	×
255	}
256
257	final int convertExitValue = runCommandLine(convertCommandLine);	2✔
258
259	// check the conversion is successful
260	if (convertExitValue != 0) {	2✔
261	throw new ModelCheckingException(	×
262	"Could not convert GCF to FSM. Enable debug logging to see LTSmin's debug information.");
263	}
264
265	return fsm;	2✔
266	} else {
267	throw new ModelCheckingException(	×
268	"Could not model check ETF. Enable debug logging to see LTSmin's debug information.");
269	}
270	} finally {
271	if (!keepFiles) {	2✔
272	if (!etf.delete()) {	2✔
273	logFileWarning(etf);	×
274	}
275	if (!ltlFile.delete()) {	2✔
276	logFileWarning(ltlFile);	×
277	}
278	if (!gcf.delete()) {	2✔
279	logFileWarning(gcf);	×
280	}
281	}
282	}
283	}
284
285	private static int runCommandLine(List<String> commandLine) {
286	try {
287	LOGGER.debug("Invoking LTSmin binary as: {}", String.join(" ", commandLine));	2✔
288	return ProcessUtil.invokeProcess(commandLine, LOGGER::debug);	2✔
289	} catch (IOException \| InterruptedException e) {	×
290	throw new ModelCheckingException(e);	×
291	}
292	}
293
294	private static void logFileWarning(File file) {
295	LOGGER.warn("Could not delete file: '{}'", file.getAbsolutePath());	×
296	}	×
297	}

LearnLib / automatalib / 12651580329

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