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

97.14

/examples/src/main/java/net/automatalib/example/modelchecking/LTSminMonitorExample.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.monitor.LTSminMonitorIO;
import net.automatalib.modelchecker.ltsmin.monitor.LTSminMonitorIOBuilder;
import net.automatalib.util.automaton.builder.AutomatonBuilders;
import org.slf4j.Logger;
import org.slf4j.LoggerFactory;

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

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

    private LTSminMonitorExample() {
        // prevent instantiation
    }

    public static void main(String[] args) {

        if (!LTSminUtil.supports(LTSminVersion.of(3, 1, 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

        // 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");

        // do LTL model checking with monitors
        final LTSminMonitorIO<Character, Character> ltsminMonitor =
                new LTSminMonitorIOBuilder<Character, Character>().withString2Input(s -> s.charAt(0))
                                                                  .withString2Output(s -> s.charAt(0))
                                                                  .create();

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

        final MealyMachine<?, Character, ?, Character> ce1m =
                ltsminMonitor.findCounterExample(mealy, inputAlphabet, p1);

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

        final MealyMachine<?, Character, ?, Character> ce2m =
                ltsminMonitor.findCounterExample(mealy, inputAlphabet, p2);

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

        final MealyMachine<?, Character, ?, Character> ce3m =
                ltsminMonitor.findCounterExample(mealy, inputAlphabet, p3);

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

        final MealyMachine<?, Character, ?, Character> ce4m =
                ltsminMonitor.findCounterExample(mealy, inputAlphabet, p4);

        LOGGER.info("Fourth property is satisfied: {}", Objects.isNull(ce4m));
        if (ce4m != null) {
            LOGGER.info("Counterexample length: {}", ce4m.size());
        }
    }
}

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.monitor.LTSminMonitorIO;
27	import net.automatalib.modelchecker.ltsmin.monitor.LTSminMonitorIOBuilder;
28	import net.automatalib.util.automaton.builder.AutomatonBuilders;
29	import org.slf4j.Logger;
30	import org.slf4j.LoggerFactory;
31
32	/**
33	* Example for using LTSmin to perform modelchecking using monitors. Make sure to correctly set up your LTSmin
34	* installation.
35	* <p>
36	* This example requires at least an LTSmin version ≥ 3.1.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 LTSminMonitorExample {
42
43	private static final Logger LOGGER = LoggerFactory.getLogger(LTSminMonitorExample.class);	1✔
44
45	private LTSminMonitorExample() {
46	// prevent instantiation
47	}
48
49	public static void main(String[] args) {
50
51	if (!LTSminUtil.supports(LTSminVersion.of(3, 1, 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	// There is only a 'b' transition possible in the next state
67	final String p1 = "X input == \"b\"";	1✔
68
69	// Globally, whenever we output a '1' the next output must be '2'
70	final String p2 = "[] (output == \"1\" -> X output == \"2\")";	1✔
71
72	// Eventually, we observe output '2' when performing input 'a'
73	final String p3 = "<> (input == \"a\" && output == \"2\")";	1✔
74
75	// In the first step we don't see output '1'.
76	final String p4 = "! output == \"1\"";	1✔
77
78	LOGGER.info("performing LTL model checking with Buchi automata");	1✔
79
80	// do LTL model checking with monitors
81	final LTSminMonitorIO<Character, Character> ltsminMonitor =	1✔
82	new LTSminMonitorIOBuilder<Character, Character>().withString2Input(s -> s.charAt(0))	1✔
83	.withString2Output(s -> s.charAt(0))	1✔
84	.create();	1✔
85
86	LOGGER.info("performing LTL model checking with monitors");	1✔
87
88	final MealyMachine<?, Character, ?, Character> ce1m =	1✔
89	ltsminMonitor.findCounterExample(mealy, inputAlphabet, p1);	1✔
90
91	LOGGER.info("First property is satisfied: {}", Objects.isNull(ce1m));	1✔
92
93	final MealyMachine<?, Character, ?, Character> ce2m =	1✔
94	ltsminMonitor.findCounterExample(mealy, inputAlphabet, p2);	1✔
95
96	LOGGER.info("Second property is satisfied: {}", Objects.isNull(ce2m));	1✔
97
98	final MealyMachine<?, Character, ?, Character> ce3m =	1✔
99	ltsminMonitor.findCounterExample(mealy, inputAlphabet, p3);	1✔
100
101	LOGGER.info("Third property is satisfied: {}", Objects.isNull(ce3m));	1✔
102
103	final MealyMachine<?, Character, ?, Character> ce4m =	1✔
104	ltsminMonitor.findCounterExample(mealy, inputAlphabet, p4);	1✔
105
106	LOGGER.info("Fourth property is satisfied: {}", Objects.isNull(ce4m));	1✔
107	if (ce4m != null) {	1✔
108	LOGGER.info("Counterexample length: {}", ce4m.size());	1✔
109	}
110	}	1✔
111	}

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