Constraints sdts refactoring

pom.xml

@@ -12,10 +12,11 @@
 
     <properties>
         <project.build.sourceEncoding>UTF-8</project.build.sourceEncoding>
-        <maven.compiler.source>1.8</maven.compiler.source>
-        <maven.compiler.target>1.8</maven.compiler.target>
+        <maven.compiler.source>17</maven.compiler.source>
+        <maven.compiler.target>17</maven.compiler.target>
 
         <!-- Dependency versions appear alphabetically below -->
+        <checker-qual.version>3.49.1</checker-qual.version>
         <commons-lang.version>3.17.0</commons-lang.version>
         <guava.version>33.4.0-jre</guava.version>
         <jakarta-xml.version>4.0.2</jakarta-xml.version>
@@ -119,6 +120,24 @@
                     </descriptorRefs>
                 </configuration>
             </plugin>
+            <plugin>
+                <groupId>org.apache.maven.plugins</groupId>
+                <artifactId>maven-compiler-plugin</artifactId>
+                <configuration>
+                    <release>17</release>
+                    <showWarnings>true</showWarnings>
+                    <compilerArgs>
+                         <arg>--enable-preview</arg>
+                    </compilerArgs>
+                </configuration>
+            </plugin>
+            <plugin>
+                <groupId>org.apache.maven.plugins</groupId>
+                <artifactId>maven-surefire-plugin</artifactId>
+                <configuration>
+                    <argLine>--enable-preview</argLine>
+                </configuration>
+            </plugin>
         </plugins>
     </build>
 
@@ -145,6 +164,12 @@
                 <version>${jaxb-runtime.version}</version>
 	        <scope>runtime</scope>
             </dependency>
+             <!-- checker framework -->
+            <dependency>
+                <groupId>org.checkerframework</groupId>
+                <artifactId>checker-qual</artifactId>
+                <version>${checker-qual.version}</version>
+            </dependency>
         </dependencies>
     </dependencyManagement>
 
@@ -199,6 +224,10 @@
             <groupId>jakarta.xml.bind</groupId>
             <artifactId>jakarta.xml.bind-api</artifactId>
         </dependency>
+        <dependency>
+            <groupId>org.checkerframework</groupId>
+            <artifactId>checker-qual</artifactId>
+        </dependency>
         <dependency>
             <groupId>org.glassfish.jaxb</groupId>
             <artifactId>jaxb-runtime</artifactId>

src/main/java/de/learnlib/ralib/automata/Assignment.java

@@ -16,16 +16,13 @@
  */
 package de.learnlib.ralib.automata;
 
+import java.util.List;
 import java.util.Map.Entry;
 
-import de.learnlib.ralib.data.Constants;
-import de.learnlib.ralib.data.ParValuation;
-import de.learnlib.ralib.data.SymbolicDataValue;
+import de.learnlib.ralib.data.*;
 import de.learnlib.ralib.data.SymbolicDataValue.Constant;
 import de.learnlib.ralib.data.SymbolicDataValue.Parameter;
 import de.learnlib.ralib.data.SymbolicDataValue.Register;
-import de.learnlib.ralib.data.VarMapping;
-import de.learnlib.ralib.data.VarValuation;
 
 /**
  * A parallel assignment for registers.
@@ -40,8 +37,14 @@ public Assignment(VarMapping<Register, ? extends SymbolicDataValue> assignment)
         this.assignment = assignment;
     }
 
-    public VarValuation compute(VarValuation registers, ParValuation parameters, Constants consts) {
-        VarValuation val = new VarValuation(registers);
+    public RegisterValuation compute(RegisterValuation registers, ParameterValuation parameters, Constants consts) {
+        RegisterValuation val = new RegisterValuation();
+        List<String> rNames = assignment.keySet().stream().map(k -> k.getName()).toList();
+        for (Entry<Register, DataValue> e : registers.entrySet()) {
+            if (!rNames.contains(e.getKey().getName())) {
+                val.put(e.getKey(), e.getValue());
+            }
+        }
         for (Entry<Register, ? extends SymbolicDataValue> e : assignment) {
             SymbolicDataValue valp = e.getValue();
             if (valp.isRegister()) {

src/main/java/de/learnlib/ralib/automata/InputTransition.java

@@ -17,14 +17,15 @@
 package de.learnlib.ralib.automata;
 
 import de.learnlib.ralib.words.InputSymbol;
+import gov.nasa.jpf.constraints.api.Expression;
 
 /**
  *
  * @author falk
  */
 public class InputTransition extends Transition {
 
-    public InputTransition(TransitionGuard guard, InputSymbol label, RALocation source, RALocation destination, Assignment assignment) {
+    public InputTransition(Expression<Boolean> guard, InputSymbol label, RALocation source, RALocation destination, Assignment assignment) {
         super(label, guard, source, destination, assignment);
     }
 

src/main/java/de/learnlib/ralib/automata/MutableRegisterAutomaton.java

@@ -23,8 +23,8 @@
 import java.util.Set;
 
 import de.learnlib.ralib.data.Constants;
-import de.learnlib.ralib.data.ParValuation;
-import de.learnlib.ralib.data.VarValuation;
+import de.learnlib.ralib.data.ParameterValuation;
+import de.learnlib.ralib.data.RegisterValuation;
 import de.learnlib.ralib.words.PSymbolInstance;
 import de.learnlib.ralib.words.ParameterizedSymbol;
 import net.automatalib.automaton.MutableDeterministic;
@@ -47,7 +47,7 @@ public class MutableRegisterAutomaton extends RegisterAutomaton
 
     private final Set<RALocation> locations = new LinkedHashSet<>();
 
-    public MutableRegisterAutomaton(Constants consts, VarValuation initialRegisters) {
+    public MutableRegisterAutomaton(Constants consts, RegisterValuation initialRegisters) {
         super(initialRegisters);
         this.constants = consts;
     }
@@ -87,12 +87,12 @@ public Collection<RALocation> getStates() {
     }
 
     protected List<Transition> getTransitions(Word<PSymbolInstance> dw) {
-        VarValuation vars = new VarValuation(getInitialRegisters());
+        RegisterValuation vars = RegisterValuation.copyOf(getInitialRegisters());
         RALocation current = initial;
         List<Transition> tseq = new ArrayList<>();
         for (PSymbolInstance psi : dw) {
 
-            ParValuation pars = new ParValuation(psi);
+            ParameterValuation pars = ParameterValuation.fromPSymbolInstance(psi);
 
             Collection<Transition> candidates =
                     current.getOut(psi.getBaseSymbol());
@@ -119,13 +119,13 @@ protected List<Transition> getTransitions(Word<PSymbolInstance> dw) {
         return tseq;
     }
 
-    protected List<Pair<Transition,VarValuation>> getTransitionsAndValuations(Word<PSymbolInstance> dw) {
-        VarValuation vars = new VarValuation(getInitialRegisters());
+    protected List<Pair<Transition,RegisterValuation>> getTransitionsAndValuations(Word<PSymbolInstance> dw) {
+        RegisterValuation vars = RegisterValuation.copyOf(getInitialRegisters());
         RALocation current = initial;
-        List<Pair<Transition,VarValuation>> tvseq = new ArrayList<>();
+        List<Pair<Transition,RegisterValuation>> tvseq = new ArrayList<>();
         for (PSymbolInstance psi : dw) {
 
-            ParValuation pars = new ParValuation(psi);
+            ParameterValuation pars = ParameterValuation.fromPSymbolInstance(psi);
 
             Collection<Transition> candidates =
                     current.getOut(psi.getBaseSymbol());
@@ -139,7 +139,7 @@ protected List<Pair<Transition,VarValuation>> getTransitionsAndValuations(Word<P
                 if (t.isEnabled(vars, pars, constants)) {
                     vars = t.execute(vars, pars, constants);
                     current = t.getDestination();
-                    tvseq.add(Pair.of(t, new VarValuation(vars)));
+                    tvseq.add(Pair.of(t, RegisterValuation.copyOf(vars)));
                     found = true;
                     break;
                 }

src/main/java/de/learnlib/ralib/automata/RALocation.java

@@ -87,10 +87,7 @@ public boolean equals(Object obj) {
             return false;
         }
         final RALocation other = (RALocation) obj;
-        if (this.id != other.id) {
-            return false;
-        }
-        return true;
+        return this.id == other.id;
     }
 
     @Override

src/main/java/de/learnlib/ralib/automata/RegisterAutomaton.java

@@ -23,8 +23,8 @@
 import java.util.Set;
 
 import de.learnlib.ralib.automata.output.OutputTransition;
+import de.learnlib.ralib.data.RegisterValuation;
 import de.learnlib.ralib.data.SymbolicDataValue.Register;
-import de.learnlib.ralib.data.VarValuation;
 import de.learnlib.ralib.words.PSymbolInstance;
 import de.learnlib.ralib.words.ParameterizedSymbol;
 import net.automatalib.automaton.DeterministicAutomaton;
@@ -37,14 +37,14 @@
 public abstract class RegisterAutomaton
         implements DeterministicAutomaton<RALocation, ParameterizedSymbol, Transition> {
 
-    private final VarValuation initialRegisters;
+    private final RegisterValuation initialRegisters;
 
-    public RegisterAutomaton(VarValuation initialRegisters) {
+    public RegisterAutomaton(RegisterValuation initialRegisters) {
         this.initialRegisters = initialRegisters;
     }
 
     public RegisterAutomaton() {
-        this(new VarValuation());
+        this(new RegisterValuation());
     }
 
 
@@ -75,7 +75,7 @@ public String toString() {
     /**
      * @return the initialRegisters
      */
-    public VarValuation getInitialRegisters() {
+    public RegisterValuation getInitialRegisters() {
         return initialRegisters;
     }
 

src/main/java/de/learnlib/ralib/automata/Transition.java

@@ -17,9 +17,11 @@
 package de.learnlib.ralib.automata;
 
 import de.learnlib.ralib.data.Constants;
-import de.learnlib.ralib.data.ParValuation;
-import de.learnlib.ralib.data.VarValuation;
+import de.learnlib.ralib.data.ParameterValuation;
+import de.learnlib.ralib.data.RegisterValuation;
+import de.learnlib.ralib.smt.SMTUtil;
 import de.learnlib.ralib.words.ParameterizedSymbol;
+import gov.nasa.jpf.constraints.api.Expression;
 
 /**
  * Register Automaton transitions have input symbols, and assignments.
@@ -30,15 +32,15 @@ public class Transition {
 
     protected final ParameterizedSymbol label;
 
-    protected final TransitionGuard guard;
+    protected final Expression<Boolean> guard;
 
     protected final RALocation source;
 
     protected final RALocation destination;
 
     protected final Assignment assignment;
 
-    public Transition(ParameterizedSymbol label, TransitionGuard guard,
+    public Transition(ParameterizedSymbol label, Expression<Boolean> guard,
             RALocation source, RALocation destination, Assignment assignment) {
         this.label = label;
         this.guard = guard;
@@ -47,11 +49,11 @@ public Transition(ParameterizedSymbol label, TransitionGuard guard,
         this.assignment = assignment;
     }
 
-    public boolean isEnabled(VarValuation registers, ParValuation parameters, Constants consts) {
-        return guard.isSatisfied(registers, parameters, consts);
+    public boolean isEnabled(RegisterValuation registers, ParameterValuation parameters, Constants consts) {
+        return guard.evaluateSMT(SMTUtil.compose(registers, parameters, consts));
     }
 
-    public VarValuation execute(VarValuation registers, ParValuation parameters, Constants consts) {
+    public RegisterValuation execute(RegisterValuation registers, ParameterValuation parameters, Constants consts) {
         return this.getAssignment().compute(registers, parameters, consts);
     }
 
@@ -86,7 +88,7 @@ public Assignment getAssignment() {
     /**
      * @return the guard
      */
-    public TransitionGuard getGuard() {
+    public Expression<Boolean> getGuard() {
         return guard;
     }
 

src/main/java/de/learnlib/ralib/automata/TransitionSequenceTransformer.java

@@ -36,6 +36,6 @@ public interface TransitionSequenceTransformer<I> {
      * @param word  the input word
      * @return  the word representing the last passed transition
      */
-    public Word<I> transformTransitionSequence(Word<I> word);
+    Word<I> transformTransitionSequence(Word<I> word);
 
 }