13138848026

Committed 04 Feb 2025 02:53PM UTC coverage: 92.108% (+2.2%) from 89.877%

Build # 13138848026

Build Type

push

github

Committed by

mtf90

Commit Message

[maven-release-plugin] prepare release automatalib-0.12.0

Run Details

16609 of 18032 relevant lines covered (92.11%)

1.7 hits per line

Source File
Press 'n' to go to next uncovered line, 'b' for previous

94.12

/modelchecking/ltsmin/src/main/java/net/automatalib/modelchecker/ltsmin/ltl/AbstractLTSminLTL.java

/* Copyright (C) 2013-2025 TU Dortmund University
 * This file is part of AutomataLib <https://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.ltl;

import java.util.Arrays;
import java.util.Collection;
import java.util.Collections;
import java.util.List;
import java.util.function.Function;

import net.automatalib.modelchecker.ltsmin.AbstractLTSmin;
import net.automatalib.modelchecker.ltsmin.LTSminVersion;
import net.automatalib.modelchecking.Lasso;
import net.automatalib.modelchecking.ModelCheckerLasso;
import net.automatalib.modelchecking.impl.AbstractUnfoldingModelChecker;
import org.checkerframework.checker.initialization.qual.UnknownInitialization;
import org.checkerframework.checker.nullness.qual.Nullable;

/**
 * An LTSmin model checker for full LTL.
 *
 * @see <a href="http://ltsmin.utwente.nl/assets/man/etf2lts-mc.html">man etf2lts-mc</a>
 * @see AbstractLTSmin
 */
public abstract class AbstractLTSminLTL<I, A, L extends Lasso<I, ?>> extends AbstractLTSmin<I, A, L>
        implements ModelCheckerLasso<I, A, String, L> {

    public static final LTSminVersion REQUIRED_VERSION = LTSminVersion.of(3, 0, 0);

    private final AbstractUnfoldingModelChecker<I, A, String, L> unfolder;

    /**
     * Constructs a new AbstractLTSminLTL.
     *
     * @param keepFiles
     *         whether to keep the files generated during model checking
     * @param string2Input
     *         the input parsing function
     * @param multiplier
     *         the multiplier
     * @param minimumUnfolds
     *         the minimum number of unfolds
     *
     * @see AbstractLTSmin#AbstractLTSmin(boolean, Function)
     */
    protected AbstractLTSminLTL(boolean keepFiles,
                                Function<String, I> string2Input,
                                int minimumUnfolds,
                                double multiplier) {
        super(keepFiles, string2Input);
        unfolder = new AbstractUnfoldingModelChecker<I, A, String, L>(minimumUnfolds, multiplier) {

            @Override
            public @Nullable L findCounterExample(A automaton, Collection<? extends I> inputs, String property) {
                return null;
            }
        };
    }

    @Override
    protected LTSminVersion getMinimumRequiredVersion(@UnknownInitialization(AbstractLTSmin.class) AbstractLTSminLTL<I, A, L> this) {
        return REQUIRED_VERSION;
    }

    @Override
    protected List<String> getExtraCommandLineOptions() {
        return Arrays.asList(// use Buchi automata created by spot
                             "--buchi-type=spotba",
                             // use the Union-Find strategy
                             "--strategy=ufscc");
    }

    @Override
    public double getMultiplier() {
        return unfolder.getMultiplier();
    }

    @Override
    public void setMultiplier(double multiplier) {
        unfolder.setMultiplier(multiplier);
    }

    @Override
    public int getMinimumUnfolds() {
        return unfolder.getMinimumUnfolds();
    }

    @Override
    public void setMinimumUnfolds(int minimumUnfolds) {
        unfolder.setMinimumUnfolds(minimumUnfolds);
    }

    static final class BuilderDefaults {

        private BuilderDefaults() {
            // prevent instantiation
        }

        static boolean keepFiles() {
            return false;
        }

        static int minimumUnfolds() {
            return 3; // super arbitrary number
        }

        static double multiplier() {
            return 1.0; // quite arbitrary too
        }

        static <O> Collection<? super O> skipOutputs() {
            return Collections.emptyList();
        }
    }
}

1	/* Copyright (C) 2013-2025 TU Dortmund University
2	* This file is part of AutomataLib <https://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.ltl;
17
18	import java.util.Arrays;
19	import java.util.Collection;
20	import java.util.Collections;
21	import java.util.List;
22	import java.util.function.Function;
23
24	import net.automatalib.modelchecker.ltsmin.AbstractLTSmin;
25	import net.automatalib.modelchecker.ltsmin.LTSminVersion;
26	import net.automatalib.modelchecking.Lasso;
27	import net.automatalib.modelchecking.ModelCheckerLasso;
28	import net.automatalib.modelchecking.impl.AbstractUnfoldingModelChecker;
29	import org.checkerframework.checker.initialization.qual.UnknownInitialization;
30	import org.checkerframework.checker.nullness.qual.Nullable;
31
32	/**
33	* An LTSmin model checker for full LTL.
34	*
35	* @see <a href="http://ltsmin.utwente.nl/assets/man/etf2lts-mc.html">man etf2lts-mc</a>
36	* @see AbstractLTSmin
37	*/
38	public abstract class AbstractLTSminLTL<I, A, L extends Lasso<I, ?>> extends AbstractLTSmin<I, A, L>
39	implements ModelCheckerLasso<I, A, String, L> {
40
41	public static final LTSminVersion REQUIRED_VERSION = LTSminVersion.of(3, 0, 0);	2✔
42
43	private final AbstractUnfoldingModelChecker<I, A, String, L> unfolder;
44
45	/**
46	* Constructs a new AbstractLTSminLTL.
47	*
48	* @param keepFiles
49	* whether to keep the files generated during model checking
50	* @param string2Input
51	* the input parsing function
52	* @param multiplier
53	* the multiplier
54	* @param minimumUnfolds
55	* the minimum number of unfolds
56	*
57	* @see AbstractLTSmin#AbstractLTSmin(boolean, Function)
58	*/
59	protected AbstractLTSminLTL(boolean keepFiles,
60	Function<String, I> string2Input,
61	int minimumUnfolds,
62	double multiplier) {
63	super(keepFiles, string2Input);	2✔
64	unfolder = new AbstractUnfoldingModelChecker<I, A, String, L>(minimumUnfolds, multiplier) {	2✔
65
66	@Override
67	public @Nullable L findCounterExample(A automaton, Collection<? extends I> inputs, String property) {
68	return null;	×
69	}
70	};
71	}	2✔
72
73	@Override
74	protected LTSminVersion getMinimumRequiredVersion(@UnknownInitialization(AbstractLTSmin.class) AbstractLTSminLTL<I, A, L> this) {
75	return REQUIRED_VERSION;	2✔
76	}
77
78	@Override
79	protected List<String> getExtraCommandLineOptions() {
80	return Arrays.asList(// use Buchi automata created by spot	2✔
81	"--buchi-type=spotba",
82	// use the Union-Find strategy
83	"--strategy=ufscc");
84	}
85
86	@Override
87	public double getMultiplier() {
88	return unfolder.getMultiplier();	2✔
89	}
90
91	@Override
92	public void setMultiplier(double multiplier) {
93	unfolder.setMultiplier(multiplier);	2✔
94	}	2✔
95
96	@Override
97	public int getMinimumUnfolds() {
98	return unfolder.getMinimumUnfolds();	2✔
99	}
100
101	@Override
102	public void setMinimumUnfolds(int minimumUnfolds) {
103	unfolder.setMinimumUnfolds(minimumUnfolds);	2✔
104	}	2✔
105
106	static final class BuilderDefaults {
107
108	private BuilderDefaults() {
109	// prevent instantiation
110	}
111
112	static boolean keepFiles() {
113	return false;	2✔
114	}
115
116	static int minimumUnfolds() {
117	return 3; // super arbitrary number	2✔
118	}
119
120	static double multiplier() {
121	return 1.0; // quite arbitrary too	2✔
122	}
123
124	static <O> Collection<? super O> skipOutputs() {
125	return Collections.emptyList();	2✔
126	}
127	}
128	}

LearnLib / automatalib / 13138848026

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