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

71.05

/modelchecking/ltsmin/src/main/java/net/automatalib/modelchecker/ltsmin/LTSminUtil.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.IOException;
import java.io.StringWriter;
import java.nio.file.Paths;

import net.automatalib.common.setting.AutomataLibProperty;
import net.automatalib.common.setting.AutomataLibSettings;
import net.automatalib.common.util.process.ProcessUtil;
import org.checkerframework.checker.nullness.qual.EnsuresNonNullIf;
import org.checkerframework.checker.nullness.qual.Nullable;
import org.slf4j.Logger;
import org.slf4j.LoggerFactory;

/**
 * A utility class that encapsulates certain technical aspects of LTSmin (e.g. accessibility of the binary, etc.)
 */
public final class LTSminUtil {

    /**
     * Path to the "etf2lts-mc" binary.
     */
    public static final String ETF2LTS_MC;

    /**
     * Path to the "ltsmin-convert" binary.
     */
    public static final String LTSMIN_CONVERT;

    private static final String ETF2LTS_MC_BINARY = "etf2lts-mc";

    private static final String LTSMIN_CONVERT_BINARY = "ltsmin-convert";

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

    private static final String CHECK = "Could not find binary '{}' of the LTSmin installation. " +
                                        "LTSmin can be obtained at https://ltsmin.utwente.nl. " +
                                        "If you installed LTSmin in a non standard location you can set the property: " +
                                        "'" + AutomataLibProperty.LTSMIN_PATH.getPropertyKey() + "'. " +
                                        "Setting the $PATH variable works too.";

    /**
     * The exit code for running an LTSmin binary with --version.
     */
    private static final int VERSION_EXIT = 255;

    /**
     * A flag for triggering verbose LTSmin output.
     */
    private static boolean verbose;

    private static @Nullable LTSminVersion detectedVersion;

    static {
        AutomataLibSettings settings = AutomataLibSettings.getInstance();

        final String ltsMinPath = settings.getProperty(AutomataLibProperty.LTSMIN_PATH, "");

        ETF2LTS_MC = Paths.get(ltsMinPath, ETF2LTS_MC_BINARY).toString();
        LTSMIN_CONVERT = Paths.get(ltsMinPath, LTSMIN_CONVERT_BINARY).toString();

        verbose = !"false".equalsIgnoreCase(settings.getProperty(AutomataLibProperty.LTSMIN_VERBOSE,
                                                                 Boolean.toString(LOGGER.isDebugEnabled())));

        detectLTSmin();
    }

    private LTSminUtil() {
        // prevent instantiation
    }

    /**
     * Returns whether an LTSmin installation was detected.
     *
     * @return {@code true} if an LTSmin installation was detected, {@code false} otherwise.
     */
    @EnsuresNonNullIf(expression = "detectedVersion", result = true)
    public static boolean isInstalled() {
        return detectedVersion != null;
    }

    /**
     * Returns the detected version of the LTSmin installation. {@code null} if LTSmin is not installed.
     *
     * @return the detected version of the LTSmin installation. {@code null} if LTSmin is not installed.
     *
     * @see #isInstalled()
     */
    public static @Nullable LTSminVersion getVersion() {
        return detectedVersion;
    }

    /**
     * Checks whether the currently detected LTSmin installation supports the queried version.
     *
     * @param requiredVersion
     *         the required version
     *
     * @return {@code true} if LTSmin is installed in the proper version, {@code false} otherwise.
     */
    public static boolean supports(LTSminVersion requiredVersion) {
        return isInstalled() && detectedVersion.supports(requiredVersion);
    }

    /**
     * Returns whether to make LTSmin's output more verbose.
     *
     * @return whether to make LTSmin's output more verbose
     */
    public static boolean isVerbose() {
        return verbose;
    }

    /**
     * Programmatically set, whether to make LTSmin's output more verbose.
     *
     * @param verbose
     *         whether to make LTSmin's output more verbose
     */
    public static void setVerbose(boolean verbose) {
        LTSminUtil.verbose = verbose;
    }

    /**
     * (Re-)Checks whether the required binaries for the {@link AbstractLTSmin LTSmin modelchecker} can be executed, by
     * performing a version check. The results to these checks can be accessed by {@link #isInstalled()} and {@link
     * #getVersion()}.
     *
     * @see #ETF2LTS_MC
     * @see #LTSMIN_CONVERT
     */
    public static void detectLTSmin() {
        final LTSminVersion etf2ltsVersion = detectLTSmin(ETF2LTS_MC);
        final LTSminVersion ltsminConvertVersion = detectLTSmin(LTSMIN_CONVERT);

        if (etf2ltsVersion == null) {
            LOGGER.info(CHECK, ETF2LTS_MC_BINARY);
        }
        if (ltsminConvertVersion == null) {
            LOGGER.info(CHECK, LTSMIN_CONVERT_BINARY);
        }
        if (etf2ltsVersion != null && ltsminConvertVersion != null) {
            if (!etf2ltsVersion.equals(ltsminConvertVersion)) {
                LOGGER.warn("Found differing {} version '{}' and {} version '{}'. Choosing the former",
                            ETF2LTS_MC_BINARY,
                            etf2ltsVersion,
                            LTSMIN_CONVERT_BINARY,
                            ltsminConvertVersion);
            }
            detectedVersion = etf2ltsVersion;
        }
    }

    private static @Nullable LTSminVersion detectLTSmin(String bin) {

        // the command lines for the ProcessBuilder
        final String[] commandLine = {bin, // add the binary
                                      "--version" // just run a version check
        };

        final StringWriter stringWriter = new StringWriter();

        try {
            final int exitValue = ProcessUtil.invokeProcess(commandLine, stringWriter::append);

            if (exitValue != VERSION_EXIT) {
                LOGGER.debug("Command '{} --version' did not exit with {}", bin, VERSION_EXIT);
                return null;
            } else {
                return LTSminVersion.parse(stringWriter.toString());
            }
        } catch (IOException | InterruptedException e) {
            LOGGER.debug(String.format("Could not execute command '%s'", bin), e);
            return null;
        }
    }
}

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.IOException;
19	import java.io.StringWriter;
20	import java.nio.file.Paths;
21
22	import net.automatalib.common.setting.AutomataLibProperty;
23	import net.automatalib.common.setting.AutomataLibSettings;
24	import net.automatalib.common.util.process.ProcessUtil;
25	import org.checkerframework.checker.nullness.qual.EnsuresNonNullIf;
26	import org.checkerframework.checker.nullness.qual.Nullable;
27	import org.slf4j.Logger;
28	import org.slf4j.LoggerFactory;
29
30	/**
31	* A utility class that encapsulates certain technical aspects of LTSmin (e.g. accessibility of the binary, etc.)
32	*/
33	public final class LTSminUtil {
34
35	/**
36	* Path to the "etf2lts-mc" binary.
37	*/
38	public static final String ETF2LTS_MC;
39
40	/**
41	* Path to the "ltsmin-convert" binary.
42	*/
43	public static final String LTSMIN_CONVERT;
44
45	private static final String ETF2LTS_MC_BINARY = "etf2lts-mc";
46
47	private static final String LTSMIN_CONVERT_BINARY = "ltsmin-convert";
48
49	private static final Logger LOGGER = LoggerFactory.getLogger(LTSminUtil.class);	2✔
50
51	private static final String CHECK = "Could not find binary '{}' of the LTSmin installation. " +	2✔
52	"LTSmin can be obtained at https://ltsmin.utwente.nl. " +
53	"If you installed LTSmin in a non standard location you can set the property: " +
54	"'" + AutomataLibProperty.LTSMIN_PATH.getPropertyKey() + "'. " +	2✔
55	"Setting the $PATH variable works too.";
56
57	/**
58	* The exit code for running an LTSmin binary with --version.
59	*/
60	private static final int VERSION_EXIT = 255;
61
62	/**
63	* A flag for triggering verbose LTSmin output.
64	*/
65	private static boolean verbose;
66
67	private static @Nullable LTSminVersion detectedVersion;
68
69	static {
70	AutomataLibSettings settings = AutomataLibSettings.getInstance();	2✔
71
72	final String ltsMinPath = settings.getProperty(AutomataLibProperty.LTSMIN_PATH, "");	2✔
73
74	ETF2LTS_MC = Paths.get(ltsMinPath, ETF2LTS_MC_BINARY).toString();	2✔
75	LTSMIN_CONVERT = Paths.get(ltsMinPath, LTSMIN_CONVERT_BINARY).toString();	2✔
76
77	verbose = !"false".equalsIgnoreCase(settings.getProperty(AutomataLibProperty.LTSMIN_VERBOSE,	2✔
78	Boolean.toString(LOGGER.isDebugEnabled())));	2✔
79
80	detectLTSmin();	2✔
81	}	2✔
82
83	private LTSminUtil() {
84	// prevent instantiation
85	}
86
87	/**
88	* Returns whether an LTSmin installation was detected.
89	*
90	* @return {@code true} if an LTSmin installation was detected, {@code false} otherwise.
91	*/
92	@EnsuresNonNullIf(expression = "detectedVersion", result = true)
93	public static boolean isInstalled() {
94	return detectedVersion != null;	2✔
95	}
96
97	/**
98	* Returns the detected version of the LTSmin installation. {@code null} if LTSmin is not installed.
99	*
100	* @return the detected version of the LTSmin installation. {@code null} if LTSmin is not installed.
101	*
102	* @see #isInstalled()
103	*/
104	public static @Nullable LTSminVersion getVersion() {
105	return detectedVersion;	×
106	}
107
108	/**
109	* Checks whether the currently detected LTSmin installation supports the queried version.
110	*
111	* @param requiredVersion
112	* the required version
113	*
114	* @return {@code true} if LTSmin is installed in the proper version, {@code false} otherwise.
115	*/
116	public static boolean supports(LTSminVersion requiredVersion) {
117	return isInstalled() && detectedVersion.supports(requiredVersion);	2✔
118	}
119
120	/**
121	* Returns whether to make LTSmin's output more verbose.
122	*
123	* @return whether to make LTSmin's output more verbose
124	*/
125	public static boolean isVerbose() {
126	return verbose;	2✔
127	}
128
129	/**
130	* Programmatically set, whether to make LTSmin's output more verbose.
131	*
132	* @param verbose
133	* whether to make LTSmin's output more verbose
134	*/
135	public static void setVerbose(boolean verbose) {
136	LTSminUtil.verbose = verbose;	×
137	}	×
138
139	/**
140	* (Re-)Checks whether the required binaries for the {@link AbstractLTSmin LTSmin modelchecker} can be executed, by
141	* performing a version check. The results to these checks can be accessed by {@link #isInstalled()} and {@link
142	* #getVersion()}.
143	*
144	* @see #ETF2LTS_MC
145	* @see #LTSMIN_CONVERT
146	*/
147	public static void detectLTSmin() {
148	final LTSminVersion etf2ltsVersion = detectLTSmin(ETF2LTS_MC);	2✔
149	final LTSminVersion ltsminConvertVersion = detectLTSmin(LTSMIN_CONVERT);	2✔
150
151	if (etf2ltsVersion == null) {	2✔
152	LOGGER.info(CHECK, ETF2LTS_MC_BINARY);	×
153	}
154	if (ltsminConvertVersion == null) {	2✔
155	LOGGER.info(CHECK, LTSMIN_CONVERT_BINARY);	×
156	}
157	if (etf2ltsVersion != null && ltsminConvertVersion != null) {	2✔
158	if (!etf2ltsVersion.equals(ltsminConvertVersion)) {	2✔
159	LOGGER.warn("Found differing {} version '{}' and {} version '{}'. Choosing the former",	×
160	ETF2LTS_MC_BINARY,
161	etf2ltsVersion,
162	LTSMIN_CONVERT_BINARY,
163	ltsminConvertVersion);
164	}
165	detectedVersion = etf2ltsVersion;	2✔
166	}
167	}	2✔
168
169	private static @Nullable LTSminVersion detectLTSmin(String bin) {
170
171	// the command lines for the ProcessBuilder
172	final String[] commandLine = {bin, // add the binary	2✔
173	"--version" // just run a version check
174	};
175
176	final StringWriter stringWriter = new StringWriter();	2✔
177
178	try {
179	final int exitValue = ProcessUtil.invokeProcess(commandLine, stringWriter::append);	2✔
180
181	if (exitValue != VERSION_EXIT) {	2✔
NEW 182	LOGGER.debug("Command '{} --version' did not exit with {}", bin, VERSION_EXIT);	×
183	return null;	×
184	} else {
185	return LTSminVersion.parse(stringWriter.toString());	2✔
186	}
187	} catch (IOException \| InterruptedException e) {	×
188	LOGGER.debug(String.format("Could not execute command '%s'", bin), e);	×
189	return null;	×
190	}
191	}
192	}

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