generify some nomenclature

Author: mtf90

api/src/main/java/net/automatalib/modelchecking/ModelChecker.java

@@ -23,27 +23,26 @@
 import org.checkerframework.checker.nullness.qual.Nullable;
 
 /**
- * A model-checker checks whether a given automaton satisfies a given property. If the property can not be satisfied it
- * provides counter examples. In fact, the counter examples is an automaton which language is a subset of the language
- * of the given automaton.
+ * A model-checker checks whether a given model satisfies a given property. If the property can not be satisfied it
+ * provides counter examples.
  *
  * @param <I>
  *         the input type
- * @param <A>
- *         the automaton type
+ * @param <M>
+ *         the model type
  * @param <P>
  *         the property type
  * @param <R>
  *         the type of counterexample
  */
 @FunctionalInterface
-public interface ModelChecker<I, A, P, R> {
+public interface ModelChecker<I, M, P, R> {
 
     /**
-     * Try to find counter examples for the given {@code property} and {@code automaton}.
+     * Try to find counter examples for the given {@code property} and {@code model}.
      *
-     * @param automaton
-     *         the automaton to check the property on.
+     * @param model
+     *         the model to check the property on.
      * @param inputs
      *         the alphabet.
      * @param property
@@ -54,16 +53,16 @@ public interface ModelChecker<I, A, P, R> {
      * @throws ModelCheckingException
      *         when this model checker can not check the property.
      */
-    @Nullable R findCounterExample(A automaton, Collection<? extends I> inputs, P property);
+    @Nullable R findCounterExample(M model, Collection<? extends I> inputs, P property);
 
     @FunctionalInterface
     interface DFAModelChecker<I, P, R> extends ModelChecker<I, DFA<?, I>, P, R> {}
 
     /**
      * A model checker for Mealy machines. Key about the {@link MealyMachine} type here is that it may not be
      * input-complete. Implementations of {@link MealyMachine}s should in these cases not return any output for a given
-     * input sequence. I.e. {@link MealyMachine#computeOutput(Iterable)} should return null when its argument is not
-     * accepted.
+     * input sequence, i.e., {@link MealyMachine#computeOutput(Iterable)} should return {@code null} when its argument
+     * is not accepted.
      *
      * @see ModelChecker
      */

core/src/main/java/net/automatalib/modelchecking/impl/SizeModelCheckerCache.java

@@ -21,7 +21,7 @@
 import java.util.Optional;
 import java.util.function.Function;
 
-import net.automatalib.automaton.simple.SimpleAutomaton;
+import net.automatalib.automaton.concept.FiniteRepresentation;
 import net.automatalib.common.util.Pair;
 import net.automatalib.modelchecking.ModelChecker;
 import net.automatalib.modelchecking.ModelCheckerCache;
@@ -32,14 +32,14 @@
  *
  * @param <I>
  *         the input type
- * @param <A>
- *         the automaton type
+ * @param <M>
+ *         the model type
  * @param <P>
  *         the property type
  * @param <R>
- *         the result type of call to {@link #findCounterExample(SimpleAutomaton, Collection, Object)}.
+ *         the result type of call to {@link #findCounterExample(FiniteRepresentation, Collection, Object)}.
  */
-class SizeModelCheckerCache<I, A extends SimpleAutomaton<?, I>, P, R> implements ModelCheckerCache<I, A, P, R> {
+class SizeModelCheckerCache<I, M extends FiniteRepresentation, P, R> implements ModelCheckerCache<I, M, P, R> {
 
     /**
      * The actual cache. We need to wrap R in an {@link Optional} because {@link Map#computeIfAbsent(Object, Function)}
@@ -56,15 +56,15 @@ class SizeModelCheckerCache<I, A extends SimpleAutomaton<?, I>, P, R> implements
     /**
      * A function to any ModelChecker.findCounterExample.
      */
-    private final ModelChecker<I, A, P, R> modelChecker;
+    private final ModelChecker<I, M, P, R> modelChecker;
 
     /**
      * Constructs a new {@link SizeModelCheckerCache}.
      *
      * @param modelChecker
      *         a function to any ModelChecker.findCounterExample.
      */
-    SizeModelCheckerCache(ModelChecker<I, A, P, R> modelChecker) {
+    SizeModelCheckerCache(ModelChecker<I, M, P, R> modelChecker) {
         this.modelChecker = modelChecker;
     }
 
@@ -74,16 +74,18 @@ class SizeModelCheckerCache<I, A extends SimpleAutomaton<?, I>, P, R> implements
      * @see ModelChecker#findCounterExample(Object, Collection, Object)
      */
     @Override
-    public @Nullable R findCounterExample(A automaton, Collection<? extends I> inputs, P property) {
-        if (automaton.size() > size) {
+    public @Nullable R findCounterExample(M model, Collection<? extends I> inputs, P property) {
+        if (model.size() > size) {
             counterExamples.clear();
         }
 
-        size = automaton.size();
+        size = model.size();
 
-        return counterExamples.computeIfAbsent(
-                Pair.of(inputs, property),
-                key -> Optional.ofNullable(modelChecker.findCounterExample(automaton, inputs, property))).orElse(null);
+        return counterExamples.computeIfAbsent(Pair.of(inputs, property),
+                                               key -> Optional.ofNullable(modelChecker.findCounterExample(model,
+                                                                                                          inputs,
+                                                                                                          property)))
+                              .orElse(null);
     }
 
     @Override

core/src/test/java/net/automatalib/modelchecking/impl/cache/ModelCheckerMock.java

@@ -52,8 +52,8 @@ public int getChecks() {
     }
 
     @Override
-    public @Nullable R findCounterExample(A automaton, Collection<? extends I> inputs, P property) {
-        Assert.assertSame(automaton, this.automaton);
+    public @Nullable R findCounterExample(A model, Collection<? extends I> inputs, P property) {
+        Assert.assertSame(model, this.automaton);
         Assert.assertSame(property, this.property);
         checks++;
         return this.counterexample;

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

@@ -64,7 +64,7 @@ protected AbstractLTSminLTL(boolean keepFiles,
         unfolder = new AbstractUnfoldingModelChecker<>(minimumUnfolds, multiplier) {
 
             @Override
-            public @Nullable L findCounterExample(A automaton, Collection<? extends I> inputs, String property) {
+            public @Nullable L findCounterExample(A model, Collection<? extends I> inputs, String property) {
                 return null;
             }
         };