Implemented LTL

core/src/main/antlr4/AbstractTemporalLogic.g4

@@ -51,5 +51,5 @@ MINUS : '-';
 FLOAT : NATURAL '.' [0-9]+;
 LPAREN : '(';
 RPAREN : ')';
-INPUT : 'input';
-OUTPUT : 'signal' | 'output';
+// This must be the lowest priority token.
+ID : [a-zA-Z][a-zA-Z0-9]*;

core/src/main/antlr4/LTL.g4

@@ -0,0 +1,25 @@
+grammar LTL;
+
+@header {
+package net.maswag;
+
+import net.maswag.LTLListener;
+import net.maswag.LTLVisitor;
+import net.maswag.LTLParser;
+
+}
+
+import AbstractTemporalLogic;
+
+expr
+     : INPUT EQ ID
+     | OUTPUT EQ ID
+     | left=expr binaryOperator right=expr
+     | unaryOperator expr
+     | unaryTemporalOperator UNDER interval expr
+     | left=expr binaryTemporalOperator UNDER interval right=expr
+     | LPAREN expr RPAREN
+     ;
+
+INPUT : 'input';
+OUTPUT : 'output';

core/src/main/antlr4/STL.g4

@@ -23,4 +23,7 @@ expr
 atomic
        : OUTPUT LPAREN signalID=NATURAL RPAREN comparisonOperator value
        | INPUT LPAREN signalID=NATURAL RPAREN comparisonOperator value
-       ;
+       ;
+
+INPUT : 'input';
+OUTPUT : 'signal' | 'output';

core/src/main/java/net/maswag/AbstractAdaptiveSTLUpdater.java

@@ -24,6 +24,8 @@
 import java.util.stream.Collectors;
 import java.util.stream.Stream;
 
+import net.maswag.TemporalLogic.STLCost;
+
 /**
  * Abstract class for potentially adaptive set of STL formulas
  *
@@ -32,7 +34,7 @@
  * @see NumericSULVerifier
  */
 @Slf4j
-public abstract class AbstractAdaptiveSTLUpdater implements AdaptiveSTLUpdater {
+public abstract class AbstractAdaptiveSTLUpdater<I> implements AdaptiveSTLUpdater<I> {
     protected static final Function<String, String> EDGE_PARSER = s -> s;
     protected EmptinessOracle.MealyEmptinessOracle<String, String> emptinessOracle;
     @NotNull
@@ -41,25 +43,25 @@ public abstract class AbstractAdaptiveSTLUpdater implements AdaptiveSTLUpdater {
     protected MembershipOracle.MealyMembershipOracle<String, String> memOracle;
     @Setter
     protected Alphabet<String> inputAlphabet;
-    private final List<STLCost> STLProperties = new ArrayList<>();
+    private final List<TemporalLogic<I>> STLProperties = new ArrayList<>();
     private final List<PropertyOracle.MealyPropertyOracle<String, String, String>> propertyOracles = new ArrayList<>();
     boolean initialized = false;
     // The list of the STL formulas that are already falsified.
-    private final List<STLCost> reportedFormulas = new ArrayList<>();
+    private final List<TemporalLogic<I>> reportedFormulas = new ArrayList<>();
 
     public AbstractAdaptiveSTLUpdater() {
         // Create model checker
         modelChecker = new LTSminMonitorIOBuilder<String, String>().withString2Input(EDGE_PARSER).withString2Output(EDGE_PARSER).create();
     }
 
     @Override
-    final public List<STLCost> getSTLProperties() {
+    final public List<TemporalLogic<I>> getSTLProperties() {
         return STLProperties;
     }
 
     @Override
     public List<String> getLTLProperties() {
-        return this.getSTLProperties().stream().map(STLCost::toLTLString).collect(Collectors.toList());
+        return this.getSTLProperties().stream().map(TemporalLogic<I>::toLTLString).collect(Collectors.toList());
     }
 
     @Override
@@ -90,7 +92,7 @@ public void setMemOracle(@NotNull MembershipOracle.MealyMembershipOracle<String,
         inclusionOracle = new MealyBFInclusionOracle<>(this.memOracle, multiplier);
     }
 
-    protected void addSTLProperty(STLCost stl) {
+    protected void addSTLProperty(TemporalLogic<I> stl) {
         if (STLProperties.contains(stl)) {
             return;
         }
@@ -102,7 +104,7 @@ protected void addSTLProperty(STLCost stl) {
         }
     }
 
-    protected void addSTLProperties(Collection<? extends STLCost> stlCollection) {
+    protected void addSTLProperties(Collection<? extends TemporalLogic<I>> stlCollection) {
         stlCollection.forEach(this::addSTLProperty);
     }
 
@@ -144,7 +146,7 @@ private void confirmInitialization() {
         }
     }
 
-    public final boolean newlyFalsifiedFormula(STLCost stlFormula) {
+    public final boolean newlyFalsifiedFormula(TemporalLogic<I> stlFormula) {
         return !reportedFormulas.contains(stlFormula);
     }
 

core/src/main/java/net/maswag/AbstractTemporalLogic.java

@@ -0,0 +1,45 @@
+package net.maswag;
+
+import lombok.Getter;
+import net.automatalib.word.Word;
+
+import java.util.Set;
+
+/**
+ * <p>Abstract TemporalLogic<I> class.</p>
+ *
+ * @author Masaki Waga {@literal <[email protected]>}
+ */
+@Getter
+public abstract class AbstractTemporalLogic<I> implements TemporalLogic<I> {
+    boolean nonTemporal;
+    Set<String> atomicStrings;
+
+    public String toLTLString() {
+        return this.toAbstractString();
+    }
+
+    /**
+     * {@inheritDoc}
+     */
+    @Override
+    public Double apply(IOSignal<I> signal) {
+        return getRoSI(signal).getRobustness();
+    }
+
+    @Override
+    public boolean equals(Object o) {
+        if (this == o) return true;
+        if (o == null || getClass() != o.getClass()) return false;
+
+        AbstractTemporalLogic<I> stlCost = (AbstractTemporalLogic<I>) o;
+
+        return this.hashCode() == stlCost.hashCode();
+    }
+
+    @Override
+    public int hashCode() {
+        // Hash code is implemented based on the string representation.
+        return this.toString().hashCode();
+    }
+}