12459117572

Committed 22 Dec 2024 05:57PM UTC coverage: 91.532% (+0.3%) from 91.183%

Build # 12459117572

Build Type

push

github

Committed by

mtf90

Commit Message

cleanups

as reported by IntelliJ's analysis

Run Details

4 of 17 new or added lines in 10 files covered. (23.53%)

9 existing lines in 3 files now uncovered.

16581 of 18115 relevant lines covered (91.53%)

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);

    /**
     * @see #isKeepFiles()
     */
    private final boolean keepFiles;

    /**
     * @see #getString2Input()
     */
    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
     */
    protected AbstractLTSmin(boolean keepFiles, Function<String, I> string2Input) {
        this.keepFiles = keepFiles;
        this.string2Input = string2Input;

        if (!LTSminUtil.supports(getMinimumRequiredVersion())) {
            throw new ModelCheckingException("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 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	/**
71	* @see #isKeepFiles()
72	*/
73	private final boolean keepFiles;
74
75	/**
76	* @see #getString2Input()
77	*/
78	private final Function<String, I> string2Input;
79
80	/**
81	* Constructs a new AbstractLTSmin.
82	*
83	* @param keepFiles
84	* whether to keep intermediate files, (e.g. etfs, gcfs etc.).
85	* @param string2Input
86	* a function that transforms edges in FSM files to actual input.
87	*
88	* @throws ModelCheckingException
89	* when the LTSmin binaries can not be run successfully.
90	*
91	* @see AbstractLTSmin
92	*/
93	protected AbstractLTSmin(boolean keepFiles, Function<String, I> string2Input) {	2✔
94	this.keepFiles = keepFiles;	2✔
95	this.string2Input = string2Input;	2✔
96
97	if (!LTSminUtil.supports(getMinimumRequiredVersion())) {	2✔
98	throw new ModelCheckingException("LTSmin binary could not be detected in the correct version");	×
99	}
100	}	2✔
101
102	/**
103	* Returns the minimum required version of LTSmin.
104	*
105	* @return the major version.
106	*/
107	protected abstract LTSminVersion getMinimumRequiredVersion(@UnknownInitialization(AbstractLTSmin.class) AbstractLTSmin<I, A, R> this);
108
109	/**
110	* Returns the extra command line options that should be given to the etf2lts-mc binary.
111	*
112	* @return the extra command line options.
113	*/
114	protected abstract List<String> getExtraCommandLineOptions();
115
116	/**
117	* This method must verify that the given formula adheres to the expected syntax of the chosen serialization format
118	* for hypotheses of {@code this} model-checker.
119	*
120	* @param formula
121	* the formula to verify
122	*
123	* @throws FormatException
124	* if the formula does not adhere to the expected syntax
125	*/
126	protected abstract void verifyFormula(String formula) throws FormatException;
127
128	@Override
129	public boolean isKeepFiles() {
130	return keepFiles;	2✔
131	}
132
133	@Override
134	public Function<String, I> getString2Input() {
135	return string2Input;	2✔
136	}
137
138	/**
139	* Finds a counterexample for the given {@code formula}, and given {@code hypothesis} in FSM format.
140	*
141	* @param hypothesis
142	* the hypothesis to check
143	* @param inputs
144	* the inputs which should be regarded for checking
145	* @param formula
146	* the formula that should be checked
147	*
148	* @return a file containing the FSM representation for the found counterexample, or {@code null} if no such
149	* counterexample could be found.
150	*
151	* @see AbstractLTSmin
152	*/
153	protected final @Nullable File findCounterExampleFSM(A hypothesis, Collection<? extends I> inputs, String formula) {
154
155	try {
156	verifyFormula(formula);	2✔
157	} catch (FormatException fe) {	×
158	throw new ModelCheckingException(fe);	×
159	}	2✔
160
161	final File etf;
162
163	try {
164	// create the ETF that will contain the LTS of the hypothesis
165	etf = File.createTempFile("automaton2etf", ".etf");	2✔
166
167	try {
168	// write to the ETF file
169	automaton2ETF(hypothesis, inputs, etf);	2✔
170	} catch (ModelCheckingException mce) {	2✔
171	if (!keepFiles && !etf.delete()) {	2✔
NEW 172	logFileWarning(etf);	×
173	}
174	throw mce;	2✔
175	}	2✔
176	} catch (IOException ioe) {	×
177	throw new ModelCheckingException(ioe);	×
178	}	2✔
179
180	final File ltlFile;
181
182	try {
183	// write LTL formula to a file because long formulae may cause problems as direct inputs to LTSmin
184	ltlFile = File.createTempFile("formula", ".ltl");	2✔
185
186	try (Writer w = IOUtil.asBufferedUTF8Writer(ltlFile)) {	2✔
187	// write to the file
188	w.write(formula);	2✔
189	} catch (IOException ioe) {	×
190	if (!keepFiles && !ltlFile.delete()) {	×
NEW 191	logFileWarning(ltlFile);	×
192	}
193	throw ioe;	×
194	}	2✔
195	} catch (IOException ioe) {	×
196	throw new ModelCheckingException(ioe);	×
197	}	2✔
198
199	final File gcf;
200
201	try {
202	// create the GCF that will possibly contain the counterexample
203	gcf = File.createTempFile("etf2gcf", ".gcf");	2✔
204	} catch (IOException ioe) {	×
205	if (!keepFiles && !etf.delete()) {	×
NEW 206	logFileWarning(etf);	×
207	}
208	throw new ModelCheckingException(ioe);	×
209	}	2✔
210
211	// the command lines for the ProcessBuilder
212	final List<String> ltsminCommandLine = CollectionUtil.list(// add the etf2lts-mc binary	2✔
213	LTSminUtil.ETF2LTS_MC,
214	// add the ETF file that contains the hypothesis
215	etf.getAbsolutePath(),	2✔
216	// add the LTL formula
217	"--ltl=" + ltlFile,
218	// write the trace to this file
219	"--trace=" + gcf.getAbsolutePath(),	2✔
220	// use only one thread (hypotheses are always small)
221	"--threads=1",
222	// use LTSmin LTL semantics
223	"--ltl-semantics=ltsmin",
224	// do not abort on partial LTSs
225	"--allow-undefined-edges");
226
227	if (LTSminUtil.isVerbose()) {	2✔
228	ltsminCommandLine.add("-v");	×
229	}
230
231	ltsminCommandLine.addAll(getExtraCommandLineOptions());	2✔
232
233	try {
234	final int ltsminExitValue = runCommandLine(ltsminCommandLine);	2✔
235
236	if (ltsminExitValue == 0) {	2✔
237	// we have not found a counterexample
238	return null;	2✔
239	} else if (ltsminExitValue == 1) {	2✔
240	// we have found a counterexample
241
242	// create a file for the FSM
243	final File fsm;
244	try {
245	fsm = File.createTempFile("gcf2fsm", ".fsm");	2✔
246	} catch (IOException ioe) {	×
247	throw new ModelCheckingException(ioe);	×
248	}	2✔
249
250	final List<String> convertCommandLine = CollectionUtil.list(// add the ltsmin-convert binary	2✔
251	LTSminUtil.LTSMIN_CONVERT,
252	// use the GCF as input
253	gcf.getAbsolutePath(),	2✔
254	// use the FSM as output
255	fsm.getAbsolutePath(),	2✔
256	// required option
257	"--rdwr");
258
259	if (LTSminUtil.isVerbose()) {	2✔
260	convertCommandLine.add("-v");	×
261	}
262
263	final int convertExitValue = runCommandLine(convertCommandLine);	2✔
264
265	// check the conversion is successful
266	if (convertExitValue != 0) {	2✔
267	throw new ModelCheckingException(	×
268	"Could not convert GCF to FSM. Enable debug logging to see LTSmin's debug information.");
269	}
270
271	return fsm;	2✔
272	} else {
273	throw new ModelCheckingException(	×
274	"Could not model check ETF. Enable debug logging to see LTSmin's debug information.");
275	}
276	} finally {
277	if (!keepFiles) {	2✔
278	if (!etf.delete()) {	2✔
NEW 279	logFileWarning(etf);	×
280	}
281	if (!ltlFile.delete()) {	2✔
NEW 282	logFileWarning(ltlFile);	×
283	}
284	if (!gcf.delete()) {	2✔
NEW 285	logFileWarning(gcf);	×
286	}
287	}
288	}
289	}
290
291	private static int runCommandLine(List<String> commandLine) {
292	try {
293	LOGGER.debug("Invoking LTSmin binary as: {}", String.join(" ", commandLine));	2✔
294	return ProcessUtil.invokeProcess(commandLine, LOGGER::debug);	2✔
295	} catch (IOException \| InterruptedException e) {	×
296	throw new ModelCheckingException(e);	×
297	}
298	}
299
300	private static void logFileWarning(File file) {
NEW 301	LOGGER.warn("Could not delete file: '{}'", file.getAbsolutePath());	×
NEW 302	}	×
303	}

LearnLib / automatalib / 12459117572

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