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

96.97

/examples/src/main/java/net/automatalib/example/modelchecking/LTSminExample.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.example.modelchecking;

import java.util.Objects;

import net.automatalib.alphabet.Alphabet;
import net.automatalib.alphabet.impl.Alphabets;
import net.automatalib.automaton.transducer.MealyMachine;
import net.automatalib.common.setting.AutomataLibProperty;
import net.automatalib.modelchecker.ltsmin.LTSminUtil;
import net.automatalib.modelchecker.ltsmin.LTSminVersion;
import net.automatalib.modelchecker.ltsmin.ltl.LTSminLTLIO;
import net.automatalib.modelchecker.ltsmin.ltl.LTSminLTLIOBuilder;
import net.automatalib.modelchecking.Lasso.MealyLasso;
import net.automatalib.util.automaton.builder.AutomatonBuilders;
import org.slf4j.Logger;
import org.slf4j.LoggerFactory;

/**
 * Example for using LTSmin to perform modelchecking. Make sure to correctly set up your LTSmin installation.
 * <p>
 * This example requires at least an LTSmin version ≥ 3.0.0.
 *
 * @see <a href="http://ltsmin.utwente.nl">http://ltsmin.utwente.nl</a>
 * @see AutomataLibProperty#LTSMIN_PATH
 */
public final class LTSminExample {

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

    private LTSminExample() {
        // prevent instantiation
    }

    public static void main(String[] args) {

        if (!LTSminUtil.supports(LTSminVersion.of(3, 0, 0))) {
            throw new IllegalStateException("The required version of LTSmin is not supported");
        }

        final Alphabet<Character> inputAlphabet = Alphabets.characters('a', 'c');

        // @formatter:off
        MealyMachine<?, Character, ?, Character> mealy = AutomatonBuilders.<Character, Character>newMealy(inputAlphabet)
                .withInitial("q0")
                .from("q0").on('a').withOutput('1').to("q1")
                .from("q1").on('b').withOutput('2').to("q2")
                .from("q2").on('c').withOutput('3').to("q0")
                .create();
        // @formatter:on

        // do LTL model checking with Buchi automata
        final LTSminLTLIO<Character, Character> ltsminBuchi =
                new LTSminLTLIOBuilder<Character, Character>().withString2Input(s -> s.charAt(0))
                                                              .withString2Output(s -> s.charAt(0))
                                                              .withMinimumUnfolds(3)
                                                              .create();

        // There is only a 'b' transition possible in the next state
        final String p1 = "X input == \"b\"";

        // Globally, whenever we output a '1' the next output must be '2'
        final String p2 = "[] (output == \"1\" -> X output == \"2\")";

        // Eventually, we observe output '2' when performing input 'a'
        final String p3 = "<> (input == \"a\" && output == \"2\")";

        // In the first step we don't see output '1'.
        final String p4 = "! output == \"1\"";

        LOGGER.info("performing LTL model checking with Buchi automata");

        final MealyLasso<Character, Character> ce1b = ltsminBuchi.findCounterExample(mealy, inputAlphabet, p1);

        LOGGER.info("First property is satisfied: {}", Objects.isNull(ce1b));

        final MealyLasso<Character, Character> ce2b = ltsminBuchi.findCounterExample(mealy, inputAlphabet, p2);

        LOGGER.info("Second property is satisfied: {}", Objects.isNull(ce2b));

        final MealyLasso<Character, Character> ce3b = ltsminBuchi.findCounterExample(mealy, inputAlphabet, p3);

        LOGGER.info("Third property is satisfied: {}", Objects.isNull(ce3b));
        if (ce3b != null) {
            LOGGER.info("Counterexample prefix+loop: {}:{}", ce3b.getPrefix(), ce3b.getLoop());
        }

        final MealyLasso<Character, Character> ce4b = ltsminBuchi.findCounterExample(mealy, inputAlphabet, p4);

        LOGGER.info("Fourth property is satisfied: {}", Objects.isNull(ce4b));
        if (ce4b != null) {
            LOGGER.info("Counterexample prefix+loop: {}:{}", ce4b.getPrefix(), ce4b.getLoop());
        }
    }
}

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.example.modelchecking;
17
18	import java.util.Objects;
19
20	import net.automatalib.alphabet.Alphabet;
21	import net.automatalib.alphabet.impl.Alphabets;
22	import net.automatalib.automaton.transducer.MealyMachine;
23	import net.automatalib.common.setting.AutomataLibProperty;
24	import net.automatalib.modelchecker.ltsmin.LTSminUtil;
25	import net.automatalib.modelchecker.ltsmin.LTSminVersion;
26	import net.automatalib.modelchecker.ltsmin.ltl.LTSminLTLIO;
27	import net.automatalib.modelchecker.ltsmin.ltl.LTSminLTLIOBuilder;
28	import net.automatalib.modelchecking.Lasso.MealyLasso;
29	import net.automatalib.util.automaton.builder.AutomatonBuilders;
30	import org.slf4j.Logger;
31	import org.slf4j.LoggerFactory;
32
33	/**
34	* Example for using LTSmin to perform modelchecking. Make sure to correctly set up your LTSmin installation.
35	* <p>
36	* This example requires at least an LTSmin version ≥ 3.0.0.
37	*
38	* @see <a href="http://ltsmin.utwente.nl">http://ltsmin.utwente.nl</a>
39	* @see AutomataLibProperty#LTSMIN_PATH
40	*/
41	public final class LTSminExample {
42
43	private static final Logger LOGGER = LoggerFactory.getLogger(LTSminExample.class);	1✔
44
45	private LTSminExample() {
46	// prevent instantiation
47	}
48
49	public static void main(String[] args) {
50
51	if (!LTSminUtil.supports(LTSminVersion.of(3, 0, 0))) {	1✔
52	throw new IllegalStateException("The required version of LTSmin is not supported");	×
53	}
54
55	final Alphabet<Character> inputAlphabet = Alphabets.characters('a', 'c');	1✔
56
57	// @formatter:off
58	MealyMachine<?, Character, ?, Character> mealy = AutomatonBuilders.<Character, Character>newMealy(inputAlphabet)	1✔
59	.withInitial("q0")	1✔
60	.from("q0").on('a').withOutput('1').to("q1")	1✔
61	.from("q1").on('b').withOutput('2').to("q2")	1✔
62	.from("q2").on('c').withOutput('3').to("q0")	1✔
63	.create();	1✔
64	// @formatter:on
65
66	// do LTL model checking with Buchi automata
67	final LTSminLTLIO<Character, Character> ltsminBuchi =	1✔
68	new LTSminLTLIOBuilder<Character, Character>().withString2Input(s -> s.charAt(0))	1✔
69	.withString2Output(s -> s.charAt(0))	1✔
70	.withMinimumUnfolds(3)	1✔
71	.create();	1✔
72
73	// There is only a 'b' transition possible in the next state
74	final String p1 = "X input == \"b\"";	1✔
75
76	// Globally, whenever we output a '1' the next output must be '2'
77	final String p2 = "[] (output == \"1\" -> X output == \"2\")";	1✔
78
79	// Eventually, we observe output '2' when performing input 'a'
80	final String p3 = "<> (input == \"a\" && output == \"2\")";	1✔
81
82	// In the first step we don't see output '1'.
83	final String p4 = "! output == \"1\"";	1✔
84
85	LOGGER.info("performing LTL model checking with Buchi automata");	1✔
86
87	final MealyLasso<Character, Character> ce1b = ltsminBuchi.findCounterExample(mealy, inputAlphabet, p1);	1✔
88
89	LOGGER.info("First property is satisfied: {}", Objects.isNull(ce1b));	1✔
90
91	final MealyLasso<Character, Character> ce2b = ltsminBuchi.findCounterExample(mealy, inputAlphabet, p2);	1✔
92
93	LOGGER.info("Second property is satisfied: {}", Objects.isNull(ce2b));	1✔
94
95	final MealyLasso<Character, Character> ce3b = ltsminBuchi.findCounterExample(mealy, inputAlphabet, p3);	1✔
96
97	LOGGER.info("Third property is satisfied: {}", Objects.isNull(ce3b));	1✔
98	if (ce3b != null) {	1✔
99	LOGGER.info("Counterexample prefix+loop: {}:{}", ce3b.getPrefix(), ce3b.getLoop());	1✔
100	}
101
102	final MealyLasso<Character, Character> ce4b = ltsminBuchi.findCounterExample(mealy, inputAlphabet, p4);	1✔
103
104	LOGGER.info("Fourth property is satisfied: {}", Objects.isNull(ce4b));	1✔
105	if (ce4b != null) {	1✔
106	LOGGER.info("Counterexample prefix+loop: {}:{}", ce4b.getPrefix(), ce4b.getLoop());	1✔
107	}
108	}	1✔
109	}

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