12650654883

Committed 07 Jan 2025 11:26AM UTC coverage: 91.569%. First build

Build # 12650654883

Build Type

Pull #85

github

Committed by

web-flow

Commit Message

Merge 2499df5ae into d156e0830

Pull Request Pull Request #85: Update dependencies

Run Details

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

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 / 12650654883

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