Skip to content

Commit

Permalink
examples: replace sys.out with slf4j logging
Browse files Browse the repository at this point in the history
  • Loading branch information
mtf90 committed Feb 7, 2020
1 parent 95efb9a commit 96dc14f
Show file tree
Hide file tree
Showing 10 changed files with 67 additions and 52 deletions.
4 changes: 4 additions & 0 deletions examples/pom.xml
Original file line number Diff line number Diff line change
Expand Up @@ -85,6 +85,10 @@ limitations under the License.
<groupId>dk.brics.automaton</groupId>
<artifactId>automaton</artifactId>
</dependency>
<dependency>
<groupId>org.slf4j</groupId>
<artifactId>slf4j-api</artifactId>
</dependency>

<!-- test -->
<dependency>
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -25,15 +25,17 @@
import net.automatalib.visualization.Visualization;
import net.automatalib.words.Alphabet;
import net.automatalib.words.impl.Alphabets;
import org.slf4j.Logger;
import org.slf4j.LoggerFactory;

/**
* A small example for computing and displaying adaptive distinguishing sequences.
*
* @author frohme
*/
@SuppressWarnings("PMD.SystemPrintln") // for examples, this is fine
public final class ADSExample {

private static final Logger LOGGER = LoggerFactory.getLogger(ADSExample.class);
private static final Alphabet<Character> ALPHABET = Alphabets.characters('a', 'b');

private ADSExample() {}
Expand All @@ -48,7 +50,7 @@ public static void main(String[] args) {
if (adsOpt.isPresent()) {
Visualization.visualize(adsOpt.get());
} else {
System.out.println("ADS does not exist");
LOGGER.info("ADS does not exist");
}
}

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -24,10 +24,13 @@
import net.automatalib.brics.BricsNFA;
import net.automatalib.visualization.Visualization;
import net.automatalib.words.Word;
import org.slf4j.Logger;
import org.slf4j.LoggerFactory;

@SuppressWarnings("PMD.SystemPrintln") // for examples, this is fine
public final class SimpleBricsExample {

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

private SimpleBricsExample() {}

public static void main(String[] args) {
Expand All @@ -47,7 +50,7 @@ public static void main(String[] args) {
Word.fromString("ade"));

for (Word<Character> tw : testWords) {
System.out.println("Output for " + tw + " is " + ba.computeOutput(tw));
LOGGER.info("Output for {} is {}", tw, ba.computeOutput(tw));
}
}

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -22,22 +22,22 @@
import net.automatalib.words.Alphabet;
import net.automatalib.words.Word;
import net.automatalib.words.impl.Alphabets;
import org.slf4j.Logger;
import org.slf4j.LoggerFactory;

@SuppressWarnings("PMD.SystemPrintln") // for examples, this is fine
public final class IncrementalDFAExample {

private static final Logger LOGGER = LoggerFactory.getLogger(IncrementalDFAExample.class);
private static final Alphabet<Character> ALPHABET = Alphabets.characters('a', 'c');

private IncrementalDFAExample() {}

public static void main(String[] args) {
System.out.println("Incremental construction using a Tree");
LOGGER.info("Incremental construction using a Tree");
IncrementalDFABuilder<Character> incDfaTree = new IncrementalDFATreeBuilder<>(ALPHABET);
build(incDfaTree);

System.out.println();

System.out.println("Incremental construction using a DAG");
LOGGER.info("Incremental construction using a DAG");
IncrementalDFABuilder<Character> incDfaDag = new IncrementalDFADAGBuilder<>(ALPHABET);
build(incDfaDag);
}
Expand All @@ -48,19 +48,19 @@ public static void build(IncrementalDFABuilder<Character> incDfa) {
Word<Character> w3 = Word.fromString("acb");
Word<Character> w4 = Word.epsilon();

System.out.println(" Inserting " + w1 + " as accepted");
LOGGER.info(" Inserting {} as accepted", w1);
incDfa.insert(w1, true);
Visualization.visualize(incDfa.asGraph());

System.out.println(" Inserting " + w2 + " as rejected");
LOGGER.info(" Inserting {} as rejected", w2);
incDfa.insert(w2, false);
Visualization.visualize(incDfa.asGraph());

System.out.println(" Inserting " + w3 + " as accepted");
LOGGER.info(" Inserting {} as accepted", w3);
incDfa.insert(w3, true);
Visualization.visualize(incDfa.asGraph());

System.out.println(" Inserting " + w4 + " as accepted");
LOGGER.info(" Inserting {} as accepted", w4);
incDfa.insert(w4, true);
Visualization.visualize(incDfa.asGraph());
}
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -22,10 +22,13 @@
import net.automatalib.words.Alphabet;
import net.automatalib.words.Word;
import net.automatalib.words.impl.Alphabets;
import org.slf4j.Logger;
import org.slf4j.LoggerFactory;

@SuppressWarnings("PMD.SystemPrintln") // for examples, this is fine
public final class IncrementalMealyExample {

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

private static final Alphabet<Character> ALPHABET = Alphabets.characters('a', 'c');
private static final Word<Character> W_1 = Word.fromString("abc");
private static final Word<Character> W_1_O = Word.fromString("xyz");
Expand All @@ -37,27 +40,25 @@ public final class IncrementalMealyExample {
private IncrementalMealyExample() {}

public static void main(String[] args) {
System.out.println("Incremental construction using a tree");
LOGGER.info("Incremental construction using a tree");
IncrementalMealyBuilder<Character, Character> incMealyTree = new IncrementalMealyTreeBuilder<>(ALPHABET);
build(incMealyTree);

System.out.println();

System.out.println("Incremental construction using a DAG");
LOGGER.info("Incremental construction using a DAG");
IncrementalMealyBuilder<Character, Character> incMealyDag = new IncrementalMealyDAGBuilder<>(ALPHABET);
build(incMealyDag);
}

public static void build(IncrementalMealyBuilder<Character, Character> incMealy) {
System.out.println(" Inserting " + W_1 + " / " + W_1_O);
LOGGER.info(" Inserting {} / {}", W_1, W_1_O);
incMealy.insert(W_1, W_1_O);
Visualization.visualize(incMealy.asGraph());

System.out.println(" Inserting " + W_2 + " / " + W_2_O);
LOGGER.info(" Inserting {} / {}", W_2, W_2_O);
incMealy.insert(W_2, W_2_O);
Visualization.visualize(incMealy.asGraph());

System.out.println(" Inserting " + W_3 + " / " + W_3_O);
LOGGER.info(" Inserting {} / {}", W_3, W_3_O);
incMealy.insert(W_3, W_3_O);
Visualization.visualize(incMealy.asGraph());
}
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -22,22 +22,22 @@
import net.automatalib.words.Alphabet;
import net.automatalib.words.Word;
import net.automatalib.words.impl.Alphabets;
import org.slf4j.Logger;
import org.slf4j.LoggerFactory;

@SuppressWarnings("PMD.SystemPrintln") // for examples, this is fine
public final class IncrementalPCDFAExample {

private static final Logger LOGGER = LoggerFactory.getLogger(IncrementalPCDFAExample.class);
private static final Alphabet<Character> ALPHABET = Alphabets.characters('a', 'c');

private IncrementalPCDFAExample() {}

public static void main(String[] args) {
System.out.println("Incremental construction using a tree");
LOGGER.info("Incremental construction using a tree");
IncrementalDFABuilder<Character> incPcDfaTree = new IncrementalPCDFATreeBuilder<>(ALPHABET);
build(incPcDfaTree);

System.out.println();

System.out.println("Incremental construction using a DAG");
LOGGER.info("Incremental construction using a DAG");
IncrementalDFABuilder<Character> incPcDfaDag = new IncrementalPCDFADAGBuilder<>(ALPHABET);
build(incPcDfaDag);
}
Expand All @@ -47,15 +47,15 @@ public static void build(IncrementalDFABuilder<Character> incPcDfa) {
Word<Character> w2 = Word.fromString("acb");
Word<Character> w3 = Word.fromString("ac");

System.out.println(" Inserting " + w1 + " as accepted");
LOGGER.info(" Inserting {} as accepted", w1);
incPcDfa.insert(w1, true);
Visualization.visualize(incPcDfa.asGraph());

System.out.println(" Inserting " + w2 + " as rejected");
LOGGER.info(" Inserting {} as rejected", w2);
incPcDfa.insert(w2, false);
Visualization.visualize(incPcDfa.asGraph());

System.out.println(" Inserting " + w3 + " as accepted");
LOGGER.info(" Inserting {} as accepted", w3);
incPcDfa.insert(w3, true);
Visualization.visualize(incPcDfa.asGraph());
}
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -26,6 +26,8 @@
import net.automatalib.util.automata.builders.AutomatonBuilders;
import net.automatalib.words.Alphabet;
import net.automatalib.words.impl.Alphabets;
import org.slf4j.Logger;
import org.slf4j.LoggerFactory;

/**
* Example for using LTSmin to perform modelchecking. Make sure to correctly setup your LTSmin installation.
Expand All @@ -37,9 +39,10 @@
* @see <a href="http://ltsmin.utwente.nl">http://ltsmin.utwente.nl</a>
* @see net.automatalib.AutomataLibProperty#LTSMIN_PATH
*/
@SuppressWarnings("PMD.SystemPrintln") // for examples, this is fine
public final class LTSminExample {

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

private LTSminExample() {
// prevent instantiation
}
Expand Down Expand Up @@ -80,29 +83,28 @@ public static void main(String[] args) {
// In the first step we don't see output '1'.
final String p4 = "! output == \"1\"";

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

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

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

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

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

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

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

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

System.out.println("Fourth property is satisfied: " + Objects.isNull(ce4b));
LOGGER.info("Fourth property is satisfied: {}", Objects.isNull(ce4b));
if (ce4b != null) {
System.out.println("Counterexample prefix+loop: " + ce4b.getPrefix() + ':' + ce4b.getLoop());
LOGGER.info("Counterexample prefix+loop: {}:{}", ce4b.getPrefix(), ce4b.getLoop());
}
}
}
Original file line number Diff line number Diff line change
Expand Up @@ -25,6 +25,8 @@
import net.automatalib.util.automata.builders.AutomatonBuilders;
import net.automatalib.words.Alphabet;
import net.automatalib.words.impl.Alphabets;
import org.slf4j.Logger;
import org.slf4j.LoggerFactory;

/**
* Example for using LTSmin to perform modelchecking using monitors. Make sure to correctly setup your LTSmin
Expand All @@ -37,9 +39,10 @@
* @see <a href="http://ltsmin.utwente.nl">http://ltsmin.utwente.nl</a>
* @see net.automatalib.AutomataLibProperty#LTSMIN_PATH
*/
@SuppressWarnings("PMD.SystemPrintln") // for examples, this is fine
public final class LTSminMonitorExample {

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

private LTSminMonitorExample() {
// prevent instantiation
}
Expand Down Expand Up @@ -73,40 +76,37 @@ public static void main(String[] args) {
// In the first step we don't see output '1'.
final String p4 = "! output == \"1\"";

System.out.println("performing LTL model checking with Buchi automata");
System.out.println();
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();

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

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

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

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

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

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

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

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

System.out.println("Fourth property is satisfied: " + Objects.isNull(ce4m));
LOGGER.info("Fourth property is satisfied: {}", Objects.isNull(ce4m));
if (ce4m != null) {
System.out.println("Counterexample length: " + ce4m.size());
LOGGER.info("Counterexample length: {}", ce4m.size());
}
}
}
Original file line number Diff line number Diff line change
Expand Up @@ -22,16 +22,18 @@
import net.automatalib.words.Word;
import net.automatalib.words.impl.Alphabets;
import net.automatalib.words.impl.DefaultVPDAlphabet;
import org.slf4j.Logger;
import org.slf4j.LoggerFactory;

/**
* A small example for constructing a {@link net.automatalib.automata.vpda.OneSEVPA visibly pushdown automaton} and
* displaying it.
*
* @author frohme
*/
@SuppressWarnings("PMD.SystemPrintln") // for examples, this is fine
public final class OneSEVPAExample {

private static final Logger LOGGER = LoggerFactory.getLogger(OneSEVPAExample.class);
private static final VPDAlphabet<Character> ALPHABET =
new DefaultVPDAlphabet<>(Alphabets.singleton('i'), Alphabets.singleton('c'), Alphabets.singleton('r'));

Expand All @@ -55,7 +57,7 @@ public static void main(String[] args) {
private static void traceVisiblePushdownWords(DefaultOneSEVPA<Character> vpa, String input) {
final boolean accept = vpa.accepts(Word.fromCharSequence(input));

System.out.println("The VPA does " + (accept ? "" : "not ") + "accept the word '" + input + "'");
LOGGER.info("The VPA does {}accept the word '{}'", accept ? "" : "not ", input);
}

/**
Expand Down
3 changes: 2 additions & 1 deletion examples/src/main/resources/logback.xml
Original file line number Diff line number Diff line change
@@ -1,7 +1,8 @@
<configuration>
<appender name="STDOUT" class="ch.qos.logback.core.ConsoleAppender">
<encoder>
<pattern>%d{HH:mm:ss.SSS} [%thread] %-5level %30.30(%logger{30}) - %msg%n</pattern>
<!--pattern>%d{HH:mm:ss.SSS} [%thread] %-5level %30.30(%logger{30}) - %msg%n</pattern-->
<pattern>[%-4level] %logger{0}: %msg%n</pattern>
</encoder>
</appender>

Expand Down

0 comments on commit 96dc14f

Please sign in to comment.