6763327895

Committed 05 Nov 2023 07:29PM UTC coverage: 89.726% (-0.1%) from 89.868%

Build # 6763327895

Build Type

push

github

Committed by

mtf90

Commit Message

fix typo

Run Details

4 of 4 new or added lines in 4 files covered. (100.0%)

99 existing lines in 18 files now uncovered.

15677 of 17472 relevant lines covered (89.73%)

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-2023 TU Dortmund
 * 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 com.google.common.collect.Lists;
import net.automatalib.AutomataLibSettings;
import net.automatalib.common.util.IOUtil;
import net.automatalib.common.util.process.ProcessUtil;
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);

    @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 (IllegalArgumentException iae) {
            throw new ModelCheckingException(iae);
        }

        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 = Lists.newArrayList(// 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 = Lists.newArrayList(// 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-2023 TU Dortmund
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 com.google.common.collect.Lists;
26	import net.automatalib.AutomataLibSettings;
27	import net.automatalib.common.util.IOUtil;
28	import net.automatalib.common.util.process.ProcessUtil;
29	import net.automatalib.exception.ModelCheckingException;
30	import net.automatalib.modelchecking.ModelChecker;
31	import net.automatalib.serialization.etf.writer.AbstractETFWriter;
32	import net.automatalib.serialization.fsm.parser.AbstractFSMParser;
33	import org.checkerframework.checker.initialization.qual.UnknownInitialization;
34	import org.checkerframework.checker.nullness.qual.Nullable;
35	import org.slf4j.Logger;
36	import org.slf4j.LoggerFactory;
37
38	/**
39	* An LTL model checker using LTSmin.
40	* <p>
41	* The user must install LTSmin in order for {@link AbstractLTSmin} to run without exceptions. Once LTSmin is
42	* installed the user may specify the path to the installed LTSmin binaries with the property
43	* <b>automatalib.ltsmin.path</b>. If this property is not set the binaries will be run as usual (e.g. simply
44	* by invoking etf2lts-mc, and ltsmin-convert), which means the user can also specify the location of the binaries in
45	* the PATH environment variable.
46	* <p>
47	* This model checker is implemented as follows. The hypothesis automaton is first written to an LTS in ETF {@link
48	* AbstractETFWriter} file, which serves as input for the etf2lts-mc binary. Then the etf2lts-mc binary is run, which
49	* will write an LTS in GCF format. This LTS will be a subset of the language of the given hypothesis. Next, the GCF is
50	* converted to FSM using the ltsmin-convert binary. Lastly, the FSM is read back into an automaton using an {@link
51	* AbstractFSMParser}.
52	*
53	* @param <I>
54	* the input type.
55	* @param <A>
56	* the automaton type.
57	* @param <R>
58	* the type of counterexample
59	*
60	* @see <a href="http://ltsmin.utwente.nl">http://ltsmin.utwente.nl</a>
61	* @see AbstractFSMParser
62	* @see AbstractETFWriter
63	* @see AutomataLibSettings
64	*/
65	public abstract class AbstractLTSmin<I, A, R> implements ModelChecker<I, A, String, R>, LTSmin<I, A, R> {
66
67	private static final Logger LOGGER = LoggerFactory.getLogger(AbstractLTSmin.class);	2✔
68
69	/**
70	* @see #isKeepFiles()
71	*/
72	private final boolean keepFiles;
73
74	/**
75	* @see #getString2Input()
76	*/
77	private final Function<String, I> string2Input;
78
79	/**
80	* Constructs a new AbstractLTSmin.
81	*
82	* @param keepFiles
83	* whether to keep intermediate files, (e.g. etfs, gcfs etc.).
84	* @param string2Input
85	* a function that transforms edges in FSM files to actual input.
86	*
87	* @throws ModelCheckingException
88	* when the LTSmin binaries can not be run successfully.
89	*
90	* @see AbstractLTSmin
91	*/
92	protected AbstractLTSmin(boolean keepFiles, Function<String, I> string2Input) {	2✔
93	this.keepFiles = keepFiles;	2✔
94	this.string2Input = string2Input;	2✔
95
96	if (!LTSminUtil.supports(getMinimumRequiredVersion())) {	2✔
UNCOV 97	throw new ModelCheckingException("LTSmin binary could not be detected in the correct version");	×
98	}
99	}	2✔
100
101	/**
102	* Returns the minimum required version of LTSmin.
103	*
104	* @return the major version.
105	*/
106	protected abstract LTSminVersion getMinimumRequiredVersion(@UnknownInitialization(AbstractLTSmin.class) AbstractLTSmin<I, A, R> this);
107
108	/**
109	* Returns the extra command line options that should be given to the etf2lts-mc binary.
110	*
111	* @return the extra command line options.
112	*/
113	protected abstract List<String> getExtraCommandLineOptions();
114
115	/**
116	* This method must verify that the given formula adheres to the expected syntax of the chosen serialization format
117	* for hypotheses of {@code this} model-checker.
118	* <p>
119	* If the formula does not adhere to the expected syntax, this method should throw a {@link
120	* IllegalArgumentException}, possibly containing nested causes that further elaborate on why the formula couldn't
121	* be verified.
122	*
123	* @param formula
124	* the formula to verify
125	*/
126	protected abstract void verifyFormula(String formula);
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✔
UNCOV 157	} catch (IllegalArgumentException iae) {	×
158	throw new ModelCheckingException(iae);	×
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✔
UNCOV 172	LOGGER.warn("Could not delete file: " + etf.getAbsolutePath());	×
173	}
174	throw mce;	2✔
175	}	2✔
UNCOV 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✔
UNCOV 189	} catch (IOException ioe) {	×
190	if (!keepFiles && !ltlFile.delete()) {	×
191	LOGGER.warn("Could not delete file: " + ltlFile.getAbsolutePath());	×
192	}
UNCOV 193	throw ioe;	×
194	}	2✔
UNCOV 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✔
UNCOV 204	} catch (IOException ioe) {	×
205	if (!keepFiles && !etf.delete()) {	×
206	LOGGER.warn("Could not delete file: " + etf.getAbsolutePath());	×
207	}
UNCOV 208	throw new ModelCheckingException(ioe);	×
209	}	2✔
210
211	// the command lines for the ProcessBuilder
212	final List<String> ltsminCommandLine = Lists.newArrayList(// 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✔
UNCOV 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✔
UNCOV 246	} catch (IOException ioe) {	×
247	throw new ModelCheckingException(ioe);	×
248	}	2✔
249
250	final List<String> convertCommandLine = Lists.newArrayList(// 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✔
UNCOV 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✔
UNCOV 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 {
UNCOV 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✔
UNCOV 279	LOGGER.warn("Could not delete file: " + etf.getAbsolutePath());	×
280	}
281	if (!ltlFile.delete()) {	2✔
UNCOV 282	LOGGER.warn("Could not delete file: " + ltlFile.getAbsolutePath());	×
283	}
284	if (!gcf.delete()) {	2✔
UNCOV 285	LOGGER.warn("Could not delete file: " + gcf.getAbsolutePath());	×
286	}
287	}
288	}
289	}
290
291	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✔
UNCOV 295	} catch (IOException \| InterruptedException e) {	×
296	throw new ModelCheckingException(e);	×
297	}
298	}
299	}

LearnLib / automatalib / 6763327895

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