Updated the ignored tests on CircleCI

.circleci/config.yml

@@ -26,7 +26,7 @@ jobs:
           key: FalCAuN-{{ checksum "pom.xml" }}
       - run: MATLAB_HOME=/tmp/matlab_root mvn clean
       - run: MATLAB_HOME=/tmp/matlab_root mvn install -DskipTests=True
-      - run: MATLAB_HOME=/tmp/matlab_root mvn test -Dtest='!%regex[.*((Simulink((SULVerifier)|(SUL)))|(MembershipOracle))Test.*]' -DskipTests=False
+      - run: MATLAB_HOME=/tmp/matlab_root mvn test -Dtest='!%regex[.*((Simulink((SULVerifier)|(SUL|Model)))|(MembershipOracle))Test.*]' -DskipTests=False
       - store_artifacts:
           path: target
       - save_cache:

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

@@ -253,9 +253,9 @@ public class ArgParser {
         dotFile = cl.getOptionValue('o', null);
         etfFile = cl.getOptionValue("output-etf", null);
         if (cl.hasOption("signal-mapper")) {
-            sigMap = SignalMapper.parse(cl.getOptionValue("signal-mapper"));
+            sigMap = SimpleSignalMapper.parse(cl.getOptionValue("signal-mapper"));
         } else {
-            sigMap = new SignalMapper();
+            sigMap = new SimpleSignalMapper();
         }
         if (cl.hasOption("disable-adaptive-stl")) {
             adaptiveSTL = false;

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

@@ -21,17 +21,16 @@
  * @author Masaki Waga {@literal <[email protected]>}
  */
 @RequiredArgsConstructor
-public class ExtendedSignalMapper {
+public class ExtendedSignalMapper implements SignalMapper {
     final private List<Function<ExtendedIOSignalPiece<List<Double>>, Double>> sigMap;
 
     public ExtendedSignalMapper() {
         this.sigMap = Collections.emptyList();
     }
 
-
     //@ requires 0 <= index < size()
-    public double apply(int index, ExtendedIOSignalPiece<List<Double>> concreteSignal) {
-        return this.sigMap.get(index).apply(concreteSignal);
+    public double apply(int index, IOSignalPiece<List<Double>> concreteSignal) {
+        return this.sigMap.get(index).apply((ExtendedIOSignalPiece<List<Double>>) concreteSignal);
     }
 
     //@ ensures \result >= 0

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

@@ -2,6 +2,7 @@
 
 import lombok.extern.slf4j.Slf4j;
 
+import java.util.ArrayList;
 import java.util.List;
 import java.util.Objects;
 import java.util.function.Function;
@@ -75,21 +76,23 @@ public Function<ExtendedIOSignalPiece<List<Double>>, Double> visitAtomic(net.mas
                 return (concreteSignal) -> concreteSignal.getPreviousOutputSignals().stream()
                         // Take the elementwise maximum of the previous output signals
                         .reduce((a, b) -> {
+                            List<Double> result = new ArrayList<>();
                             assert a.size() == b.size();
                             for (int i = 0; i < a.size(); i++) {
-                                a.set(i, Math.max(a.get(i), b.get(i)));
+                                result.add(i, Math.max(a.get(i), b.get(i)));
                             }
-                            return a;
+                            return result;
                         }).get().get(sigIndex);
             } else { // PREVIOUS_MIN_OUTPUT
                 return (concreteSignal) -> concreteSignal.getPreviousOutputSignals().stream()
                         // Take the elementwise minimum of the previous output signals
                         .reduce((a, b) -> {
+                            List<Double> result = new ArrayList<>();
                             assert a.size() == b.size();
                             for (int i = 0; i < a.size(); i++) {
-                                a.set(i, Math.min(a.get(i), b.get(i)));
+                                result.add(i, Math.min(a.get(i), b.get(i)));
                             }
-                            return a;
+                            return result;
                         }).get().get(sigIndex);
             }
         } else {

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

@@ -51,6 +51,7 @@ public void processQueries(Collection<? extends Query<String, Word<String>>> que
                         abstractInput.stream().map(mapper::mapInput).collect(Collectors.toList()));
                 assert concreteInput.size() == q.getInput().size();
 
+                // TODO: Fix here to handle ExtendedSignals
                 final Word<List<Double>> concreteOutput;
                 try {
                     concreteOutput = sul.execute(concreteInput);

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

@@ -1,64 +1,14 @@
 package net.maswag;
 
-import lombok.RequiredArgsConstructor;
-import org.antlr.v4.runtime.CharStream;
-import org.antlr.v4.runtime.CharStreams;
-import org.antlr.v4.runtime.CommonTokenStream;
-import org.antlr.v4.runtime.tree.ParseTree;
-
-import java.io.*;
-import java.util.Collections;
 import java.util.List;
-import java.util.function.Function;
-import java.util.stream.Collectors;
 
 /**
- * Class to construct pseudo signals from concrete signals
- *
- * @author Masaki Waga {@literal <[email protected]>}
+ * Interface to construct pseudo signals from concrete signals
  */
-@RequiredArgsConstructor
-public class SignalMapper {
-    final private List<Function<IOSignalPiece<List<Double>>, Double>> sigMap;
-
-    public SignalMapper() {
-        this.sigMap = Collections.emptyList();
-    }
-
-
+public interface SignalMapper {
     //@ requires 0 <= index < size()
-    public double apply(int index, IOSignalPiece<List<Double>> concreteSignal) {
-        return this.sigMap.get(index).apply(concreteSignal);
-    }
+    double apply(int index, IOSignalPiece<List<Double>> concreteSignal);
 
     //@ ensures \result >= 0
-    public int size() {
-        return this.sigMap.size();
-    }
-
-    public static SignalMapper parse(String filename) throws IOException {
-        return SignalMapper.parse(new BufferedReader(
-                new InputStreamReader(new FileInputStream(filename))));
-    }
-
-    public static SignalMapper parse(BufferedReader reader) {
-        List<Function<IOSignalPiece<List<Double>>, Double>> rawList =
-                reader.lines().map(SignalMapper::lineParse).collect(Collectors.toList());
-
-        return new SignalMapper(rawList);
-    }
-
-    static Function<IOSignalPiece<List<Double>>, Double> lineParse(String line) {
-        net.maswag.SignalMapperVisitor<Function<IOSignalPiece<List<Double>>, Double>> visitor = new SignalMapperVisitorImpl();
-        return parseSignalMapperImpl(line, visitor);
-    }
-
-    private static Function<IOSignalPiece<List<Double>>, Double> parseSignalMapperImpl(String line, net.maswag.SignalMapperVisitor<Function<IOSignalPiece<List<Double>>, Double>> visitor) {
-        CharStream stream = CharStreams.fromString(line);
-        net.maswag.SignalMapperLexer lexer = new net.maswag.SignalMapperLexer(stream);
-        CommonTokenStream tokens = new CommonTokenStream(lexer);
-        net.maswag.SignalMapperParser parser = new net.maswag.SignalMapperParser(tokens);
-        ParseTree tree = parser.expr();
-        return visitor.visit(tree);
-    }
+    int size();
 }

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

@@ -0,0 +1,65 @@
+package net.maswag;
+
+import lombok.RequiredArgsConstructor;
+import org.antlr.v4.runtime.CharStream;
+import org.antlr.v4.runtime.CharStreams;
+import org.antlr.v4.runtime.CommonTokenStream;
+import org.antlr.v4.runtime.tree.ParseTree;
+
+import java.io.*;
+import java.util.Collections;
+import java.util.List;
+import java.util.function.Function;
+import java.util.stream.Collectors;
+
+/**
+ * Class to construct pseudo signals from concrete signals
+ *
+ * @author Masaki Waga {@literal <[email protected]>}
+ */
+@RequiredArgsConstructor
+public class SimpleSignalMapper implements SignalMapper {
+    final private List<Function<IOSignalPiece<List<Double>>, Double>> sigMap;
+
+    public SimpleSignalMapper() {
+        this.sigMap = Collections.emptyList();
+    }
+
+    //@ requires 0 <= index < size()
+    @Override
+    public double apply(int index, IOSignalPiece<List<Double>> concreteSignal) {
+        return this.sigMap.get(index).apply(concreteSignal);
+    }
+
+    //@ ensures \result >= 0
+    @Override
+    public int size() {
+        return this.sigMap.size();
+    }
+
+    public static SignalMapper parse(String filename) throws IOException {
+        return SimpleSignalMapper.parse(new BufferedReader(
+                new InputStreamReader(new FileInputStream(filename))));
+    }
+
+    public static SignalMapper parse(BufferedReader reader) {
+        List<Function<IOSignalPiece<List<Double>>, Double>> rawList =
+                reader.lines().map(SimpleSignalMapper::lineParse).collect(Collectors.toList());
+
+        return new SimpleSignalMapper(rawList);
+    }
+
+    static Function<IOSignalPiece<List<Double>>, Double> lineParse(String line) {
+        net.maswag.SignalMapperVisitor<Function<IOSignalPiece<List<Double>>, Double>> visitor = new SignalMapperVisitorImpl();
+        return parseSignalMapperImpl(line, visitor);
+    }
+
+    private static Function<IOSignalPiece<List<Double>>, Double> parseSignalMapperImpl(String line, net.maswag.SignalMapperVisitor<Function<IOSignalPiece<List<Double>>, Double>> visitor) {
+        CharStream stream = CharStreams.fromString(line);
+        net.maswag.SignalMapperLexer lexer = new net.maswag.SignalMapperLexer(stream);
+        CommonTokenStream tokens = new CommonTokenStream(lexer);
+        net.maswag.SignalMapperParser parser = new net.maswag.SignalMapperParser(tokens);
+        ParseTree tree = parser.expr();
+        return visitor.visit(tree);
+    }
+}

core/src/test/java/net/maswag/ExtendedSignalMapperTest.java

@@ -0,0 +1,46 @@
+package net.maswag;
+
+import org.junit.jupiter.api.BeforeEach;
+import org.junit.jupiter.api.Test;
+
+import java.io.BufferedReader;
+import java.io.IOException;
+import java.io.StringReader;
+import java.util.ArrayList;
+import java.util.Arrays;
+import java.util.Collections;
+import java.util.List;
+import java.util.function.Function;
+
+import static java.lang.Math.abs;
+import static org.junit.jupiter.api.Assertions.assertEquals;
+import static org.junit.jupiter.api.Assertions.assertThrows;
+
+class ExtendedSignalMapperTest {
+    SignalMapper sigMap;
+    List<Double> concreteSignal;
+    List<List<Double>> previousValues;
+
+    @BeforeEach
+    void setUp() {
+        concreteSignal = new ArrayList<>();
+        concreteSignal.add(2.0);
+        concreteSignal.add(-4.2);
+        concreteSignal.add(0.4);
+        previousValues = new ArrayList<>();
+        previousValues.add(Arrays.asList(1.0, 2.0, 3.0));
+        previousValues.add(Arrays.asList(4.0, 5.0, 6.0));
+    }
+
+    @Test
+    void parse() throws IOException {
+        String sigMapContent = "previous_max_output(2)\n" + "previous_min_output(2)";
+        BufferedReader reader = new BufferedReader(new StringReader(sigMapContent));
+        sigMap = ExtendedSignalMapper.parse(reader);
+        assertEquals(2, sigMap.size());
+        assertEquals(Math.max(3.0, 6.0), sigMap.apply(0,
+                new ExtendedIOSignalPiece<>(Collections.emptyList(), concreteSignal, previousValues)));
+        assertEquals(Math.min(3.0, 6.0), sigMap.apply(1,
+                new ExtendedIOSignalPiece<>(Collections.emptyList(), concreteSignal, previousValues)));
+    }
+}

core/src/test/java/net/maswag/NumericSULMapperTest.java

@@ -8,16 +8,7 @@
 import java.util.function.Function;
 
 import static org.junit.jupiter.api.Assertions.assertEquals;
-import net.maswag.TemporalAnd.STLAnd;
-import net.maswag.TemporalEventually.STLEventually;
-import net.maswag.TemporalGlobally.STLGlobally;
-import net.maswag.TemporalImply.STLImply;
-import net.maswag.TemporalLogic.STLCost;
-import net.maswag.TemporalNext.STLNext;
-import net.maswag.TemporalOr.STLOr;
-import net.maswag.TemporalRelease.STLRelease;
-import net.maswag.TemporalSub.STLSub;
-import net.maswag.TemporalUntil.STLUntil;
+
 class NumericSULMapperTest {
 
     private List<Map<Character, Double>> inputMapper;
@@ -112,6 +103,6 @@ void setUp() {
             outputMapper = new ArrayList<>(Arrays.asList(mapper1, mapper2, mapper3));
             largest = new ArrayList<>(Arrays.asList('0', '0', 'p'));
         }
-        mapper = new NumericSULMapper(inputMapper, largest, outputMapper, new SignalMapper(sigMap));
+        mapper = new NumericSULMapper(inputMapper, largest, outputMapper, new SimpleSignalMapper(sigMap));
     }
 }

core/src/test/java/net/maswag/SignalMapperTest.java → core/src/test/java/net/maswag/SimpleSignalMapperTest.java

@@ -13,7 +13,7 @@
 import static org.junit.jupiter.api.Assertions.assertEquals;
 import static org.junit.jupiter.api.Assertions.assertThrows;
 
-class SignalMapperTest {
+class SimpleSignalMapperTest {
     private final String PWD = System.getenv("PWD");
     private final String sigMapName = PWD + "/src/test/resources/sigMap.txt";
     SignalMapper sigMap;
@@ -22,7 +22,7 @@ class SignalMapperTest {
     @BeforeEach
     void setUp() {
         Function<IOSignalPiece<List<Double>>, Double> diff = a -> a.getOutputSignal().get(0) - a.getOutputSignal().get(1);
-        sigMap = new SignalMapper(Collections.singletonList(diff));
+        sigMap = new SimpleSignalMapper(Collections.singletonList(diff));
         concreteSignal = new ArrayList<>();
         concreteSignal.add(2.0);
         concreteSignal.add(-4.2);
@@ -44,7 +44,7 @@ void size() {
 
     @Test
     void parse() throws IOException {
-        sigMap = SignalMapper.parse(sigMapName);
+        sigMap = SimpleSignalMapper.parse(sigMapName);
         assertEquals(4, sigMap.size());
         assertEquals(2.0 + 0.4, sigMap.apply(0,
                 new IOSignalPiece<>(Collections.emptyList(), concreteSignal)));

example/kotlin/pacemaker.kts → example/kotlin/pacemaker.main.kts

@@ -1,7 +1,7 @@
 #!/usr/bin/env kscript
 /*****h* kotlin/pacemaker
  *  NAME
- *   pacemaker.kts
+ *   pacemaker.main.kts
  *  DESCRIPTION
  *   Script to falsify the "pacemaker" formula by FalCAuN
  *  AUTHOR
@@ -19,44 +19,51 @@
  *   - The environment variable MATLAB_HOME is set to the root directory of MATLAB, e.g., /Applications/MATLAB_R2024a.app/ or /usr/local/MATLAB/R2024a.
  *
  *  USAGE
- *   ./pacemaker.kts
+ *   ./pacemaker.main.kts
  *  NOTES
  *   By default, this script runs FalCAuN for 50 times. When you want to run for a different interval, specify the range by the first and the second arguments.
  *
  ********/
 
-package net.maswag
-
 // This script depends on FalCAuN-core and FalCAuN-matlab
-@file:DependsOn("net.maswag:FalCAuN-core:1.0-SNAPSHOT", "net.maswag:FalCAuN-matlab:1.0-SNAPSHOT")
+@file:DependsOn("net.maswag:FalCAuN-core:1.0-SNAPSHOT")
+@file:DependsOn("net.maswag:FalCAuN-matlab:1.0-SNAPSHOT")
 // We assume that the MATLAB_HOME environment variable is set
 @file:KotlinOptions("-Djava.library.path=$MATLAB_HOME/bin/maca64/:$MATLAB_HOME/bin/maci64:$MATLAB_HOME/bin/glnxa64")
 
 import net.maswag.*
-import kotlin.streams.toList
+import java.io.BufferedReader
+import java.io.StringReader
 
 // Define the input and output mappers
 val lriValues = listOf(50.0, 90.0)
 val inputMapper = InputMapperReader.make(listOf(lriValues))
 val periodValues = listOf(null)
 val lrlValues = listOf(null)
 val paceCountValues = listOf(8.0, 15.0, null)
-val outputMapperReader = OutputMapperReader(listOf(periodValues, lrlValues, paceCountValues))
+val outputMapperReader = OutputMapperReader(listOf(periodValues, lrlValues, paceCountValues, paceCountValues, paceCountValues))
 outputMapperReader.parse()
-val signalMapper = SignalMapper()
+val mapperString = """previous_max_output(2)
+previous_min_output(2)
+"""
+val signalMapper: ExtendedSignalMapper = ExtendedSignalMapper.parse(BufferedReader(StringReader(mapperString)))
+assert(signalMapper.size() == 2)
 val mapper =
     NumericSULMapper(inputMapper, outputMapperReader.largest, outputMapperReader.outputMapper, signalMapper)
 
 // Define the output signal names
 val period = "signal(0)"
 val LRL = "signal(1)"
 val paceCount = "signal(2)"
+// Pseudo signals representing the maximum and minimum values between sampling points
+val prevMaxPaceCount = "output(3)"
+val prevMinPaceCount = "output(4)"
 
 // Define the STL properties
 val stlFactory = STLFactory()
 val stlList = listOf(
     stlFactory.parse(
-        "(alw_[5,5] $LRL > 0) -> ((alw_[0,5] $paceCount < 15) && (ev_[0,5] $paceCount > 8))",
+        "(alw_[5,5] $LRL > 0) -> ((alw_[0,5] ($paceCount < 15 && $prevMinPaceCount < 15)) && (ev_[0,5] ($paceCount > 8 && $prevMaxPaceCount > 8)))",
         inputMapper,
         outputMapperReader.outputMapper,
         outputMapperReader.largest