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

64.0

/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.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.
     * <p>
     * If the formula does not adhere to the expected syntax, this method should throw a {@link
     * IllegalArgumentException}, possibly containing nested causes that further elaborate on why the formula couldn't
     * be verified.
     *
     * @param formula
     *         the formula to verify
     */
    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()) {
                    LOGGER.warn("Could not delete file: " + etf.getAbsolutePath());
                }
                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()) {
                    LOGGER.warn("Could not delete file: " + ltlFile.getAbsolutePath());
                }
                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()) {
                LOGGER.warn("Could not delete file: " + etf.getAbsolutePath());
            }
            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()) {
                    LOGGER.warn("Could not delete file: " + etf.getAbsolutePath());
                }
                if (!ltlFile.delete()) {
                    LOGGER.warn("Could not delete file: " + ltlFile.getAbsolutePath());
                }
                if (!gcf.delete()) {
                    LOGGER.warn("Could not delete file: " + gcf.getAbsolutePath());
                }
            }
        }
    }

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

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.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	* <p>
120	* If the formula does not adhere to the expected syntax, this method should throw a {@link
121	* IllegalArgumentException}, possibly containing nested causes that further elaborate on why the formula couldn't
122	* be verified.
123	*
124	* @param formula
125	* the formula to verify
126	*/
127	protected abstract void verifyFormula(String formula) throws FormatException;
128
129	@Override
130	public boolean isKeepFiles() {
131	return keepFiles;	2✔
132	}
133
134	@Override
135	public Function<String, I> getString2Input() {
136	return string2Input;	2✔
137	}
138
139	/**
140	* Finds a counterexample for the given {@code formula}, and given {@code hypothesis} in FSM format.
141	*
142	* @param hypothesis
143	* the hypothesis to check
144	* @param inputs
145	* the inputs which should be regarded for checking
146	* @param formula
147	* the formula that should be checked
148	*
149	* @return a file containing the FSM representation for the found counterexample, or {@code null} if no such
150	* counterexample could be found.
151	*
152	* @see AbstractLTSmin
153	*/
154	protected final @Nullable File findCounterExampleFSM(A hypothesis, Collection<? extends I> inputs, String formula) {
155
156	try {
157	verifyFormula(formula);	2✔
NEW 158	} catch (FormatException fe) {	×
NEW 159	throw new ModelCheckingException(fe);	×
160	}	2✔
161
162	final File etf;
163
164	try {
165	// create the ETF that will contain the LTS of the hypothesis
166	etf = File.createTempFile("automaton2etf", ".etf");	2✔
167
168	try {
169	// write to the ETF file
170	automaton2ETF(hypothesis, inputs, etf);	2✔
171	} catch (ModelCheckingException mce) {	2✔
172	if (!keepFiles && !etf.delete()) {	2✔
173	LOGGER.warn("Could not delete file: " + etf.getAbsolutePath());	×
174	}
175	throw mce;	2✔
176	}	2✔
177	} catch (IOException ioe) {	×
178	throw new ModelCheckingException(ioe);	×
179	}	2✔
180
181	final File ltlFile;
182
183	try {
184	// write LTL formula to a file because long formulae may cause problems as direct inputs to LTSmin
185	ltlFile = File.createTempFile("formula", ".ltl");	2✔
186
187	try (Writer w = IOUtil.asBufferedUTF8Writer(ltlFile)) {	2✔
188	// write to the file
189	w.write(formula);	2✔
190	} catch (IOException ioe) {	×
191	if (!keepFiles && !ltlFile.delete()) {	×
192	LOGGER.warn("Could not delete file: " + ltlFile.getAbsolutePath());	×
193	}
194	throw ioe;	×
195	}	2✔
196	} catch (IOException ioe) {	×
197	throw new ModelCheckingException(ioe);	×
198	}	2✔
199
200	final File gcf;
201
202	try {
203	// create the GCF that will possibly contain the counterexample
204	gcf = File.createTempFile("etf2gcf", ".gcf");	2✔
205	} catch (IOException ioe) {	×
206	if (!keepFiles && !etf.delete()) {	×
207	LOGGER.warn("Could not delete file: " + etf.getAbsolutePath());	×
208	}
209	throw new ModelCheckingException(ioe);	×
210	}	2✔
211
212	// the command lines for the ProcessBuilder
213	final List<String> ltsminCommandLine = CollectionUtil.list(// add the etf2lts-mc binary	2✔
214	LTSminUtil.ETF2LTS_MC,
215	// add the ETF file that contains the hypothesis
216	etf.getAbsolutePath(),	2✔
217	// add the LTL formula
218	"--ltl=" + ltlFile,
219	// write the trace to this file
220	"--trace=" + gcf.getAbsolutePath(),	2✔
221	// use only one thread (hypotheses are always small)
222	"--threads=1",
223	// use LTSmin LTL semantics
224	"--ltl-semantics=ltsmin",
225	// do not abort on partial LTSs
226	"--allow-undefined-edges");
227
228	if (LTSminUtil.isVerbose()) {	2✔
229	ltsminCommandLine.add("-v");	×
230	}
231
232	ltsminCommandLine.addAll(getExtraCommandLineOptions());	2✔
233
234	try {
235	final int ltsminExitValue = runCommandLine(ltsminCommandLine);	2✔
236
237	if (ltsminExitValue == 0) {	2✔
238	// we have not found a counterexample
239	return null;	2✔
240	} else if (ltsminExitValue == 1) {	2✔
241	// we have found a counterexample
242
243	// create a file for the FSM
244	final File fsm;
245	try {
246	fsm = File.createTempFile("gcf2fsm", ".fsm");	2✔
247	} catch (IOException ioe) {	×
248	throw new ModelCheckingException(ioe);	×
249	}	2✔
250
251	final List<String> convertCommandLine = CollectionUtil.list(// add the ltsmin-convert binary	2✔
252	LTSminUtil.LTSMIN_CONVERT,
253	// use the GCF as input
254	gcf.getAbsolutePath(),	2✔
255	// use the FSM as output
256	fsm.getAbsolutePath(),	2✔
257	// required option
258	"--rdwr");
259
260	if (LTSminUtil.isVerbose()) {	2✔
261	convertCommandLine.add("-v");	×
262	}
263
264	final int convertExitValue = runCommandLine(convertCommandLine);	2✔
265
266	// check the conversion is successful
267	if (convertExitValue != 0) {	2✔
268	throw new ModelCheckingException(	×
269	"Could not convert GCF to FSM. Enable debug logging to see LTSmin's debug information.");
270	}
271
272	return fsm;	2✔
273	} else {
274	throw new ModelCheckingException(	×
275	"Could not model check ETF. Enable debug logging to see LTSmin's debug information.");
276	}
277	} finally {
278	if (!keepFiles) {	2✔
279	if (!etf.delete()) {	2✔
280	LOGGER.warn("Could not delete file: " + etf.getAbsolutePath());	×
281	}
282	if (!ltlFile.delete()) {	2✔
283	LOGGER.warn("Could not delete file: " + ltlFile.getAbsolutePath());	×
284	}
285	if (!gcf.delete()) {	2✔
286	LOGGER.warn("Could not delete file: " + gcf.getAbsolutePath());	×
287	}
288	}
289	}
290	}
291
292	static int runCommandLine(List<String> commandLine) {
293	try {
294	LOGGER.debug("Invoking LTSmin binary as: {}", String.join(" ", commandLine));	2✔
295	return ProcessUtil.invokeProcess(commandLine, LOGGER::debug);	2✔
296	} catch (IOException \| InterruptedException e) {	×
297	throw new ModelCheckingException(e);	×
298	}
299	}
300	}

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