Generify NBA and GNBA, minor performance improvement

paultristanwagner · Oct 2, 2023 · 25a41d9 · 25a41d9
1 parent fe67275
commit 25a41d9
Show file tree

Hide file tree

Showing 15 changed files with 269 additions and 170 deletions.
diff --git a/README.md b/README.md
@@ -163,7 +163,7 @@ at: [paultristanwagner@gmail.com](mailto:paultristanwagner@gmail.com).
 
 - Improve UI / UX
 - Implement implication and equivalence operators in LTL, CTL, and CTL* grammar
-- Implement bisimulation quotienting algorithm 
+- Implement bisimulation quotienting algorithm
 - Write tests for the LTL, CTL, and CTL* model checking algorithms
 - Optimize the lookup of the next states in the transition system
 - Implement linear-time fixpoint computation in CTL model checking

diff --git a/src/main/java/me/paultristanwagner/modelchecking/automaton/GNBA.java b/src/main/java/me/paultristanwagner/modelchecking/automaton/GNBA.java
@@ -1,45 +1,36 @@
 package me.paultristanwagner.modelchecking.automaton;
 
+import static me.paultristanwagner.modelchecking.util.GsonUtil.GSON;
 import static me.paultristanwagner.modelchecking.util.TupleUtil.stringTuple;
 
-import com.google.gson.Gson;
-import com.google.gson.GsonBuilder;
+import java.lang.reflect.Type;
 import java.util.HashSet;
 import java.util.Set;
 
-public final class GNBA {
+public class GNBA<ActionType> {
 
-  private static final Gson GSON;
   private final Set<String> states;
   private final Set<String> alphabet;
   private final Set<String> initialStates;
   private final Set<Set<String>> acceptingSets;
-  private final Set<NBATransition> transitions;
+  private final Set<NBATransition<ActionType>> transitions;
 
   public GNBA(
       Set<String> states,
       Set<String> alphabet,
       Set<String> initialStates,
       Set<Set<String>> acceptingSets,
-      Set<NBATransition> transitions) {
+      Set<NBATransition<ActionType>> transitions) {
     this.states = states;
     this.alphabet = alphabet;
     this.initialStates = initialStates;
     this.acceptingSets = acceptingSets;
     this.transitions = transitions;
   }
 
-  static {
-    GSON =
-        new GsonBuilder()
-            .registerTypeAdapter(NBATransition.class, new NBATransition.NBATransitionAdapter())
-            .setPrettyPrinting()
-            .create();
-  }
-
   public Set<String> getSuccessors(String state) {
     Set<String> successors = new HashSet<>();
-    for (NBATransition transition : transitions) {
+    for (NBATransition<ActionType> transition : transitions) {
       if (transition.getFrom().equals(state)) {
         successors.add(transition.getTo());
       }
@@ -49,20 +40,20 @@ public Set<String> getSuccessors(String state) {
 
   public Set<String> getSuccessors(String state, String action) {
     Set<String> successors = new HashSet<>();
-    for (NBATransition transition : transitions) {
+    for (NBATransition<ActionType> transition : transitions) {
       if (transition.getFrom().equals(state) && transition.getAction().equals(action)) {
         successors.add(transition.getTo());
       }
     }
     return successors;
   }
 
-  public NBA convertToNBA() {
+  public NBA<ActionType> convertToNBA() {
     if (acceptingSets.size() <= 1) {
       return getCanonicalNBA();
     }
 
-    NBABuilder builder = new NBABuilder();
+    NBABuilder<ActionType> builder = new NBABuilder<>();
     builder.setAlphabet(alphabet);
 
     for (String state : states) {
@@ -85,7 +76,7 @@ public NBA convertToNBA() {
       }
     }
 
-    for (NBATransition transition : transitions) {
+    for (NBATransition<ActionType> transition : transitions) {
       int i = 0;
       for (Set<String> acceptingSet : acceptingSets) {
         String nbaFrom = stringTuple(transition.getFrom(), i + 1);
@@ -104,12 +95,12 @@ public NBA convertToNBA() {
     return builder.build();
   }
 
-  private NBA getCanonicalNBA() {
+  private NBA<ActionType> getCanonicalNBA() {
     if (acceptingSets.size() > 1) {
       throw new IllegalStateException("GNBA has more than one accepting set");
     }
 
-    NBABuilder builder = new NBABuilder();
+    NBABuilder<ActionType> builder = new NBABuilder<>();
     builder.setAlphabet(alphabet);
     for (String state : states) {
       builder.addState(state);
@@ -129,7 +120,7 @@ private NBA getCanonicalNBA() {
       }
     }
 
-    for (NBATransition transition : transitions) {
+    for (NBATransition<ActionType> transition : transitions) {
       builder.addTransition(transition.getFrom(), transition.getAction(), transition.getTo());
     }
 
@@ -140,8 +131,8 @@ public String toJson() {
     return GSON.toJson(this);
   }
 
-  public static GNBA fromJson(String json) {
-    return GSON.fromJson(json, GNBA.class);
+  public static <ActionType> GNBA<ActionType> fromJson(String json, Type type) {
+    return GSON.fromJson(json, type);
   }
 
   public Set<String> getStates() {
@@ -160,7 +151,7 @@ public Set<Set<String>> getAcceptingSets() {
     return acceptingSets;
   }
 
-  public Set<NBATransition> getTransitions() {
+  public Set<NBATransition<ActionType>> getTransitions() {
     return transitions;
   }
 }
diff --git a/src/main/java/me/paultristanwagner/modelchecking/automaton/GNBABuilder.java b/src/main/java/me/paultristanwagner/modelchecking/automaton/GNBABuilder.java
@@ -3,13 +3,13 @@
 import java.util.HashSet;
 import java.util.Set;
 
-public class GNBABuilder {
+public class GNBABuilder<ActionType> {
 
   private final Set<String> states;
   private final Set<String> alphabet;
   private final Set<String> initialStates;
   private final Set<Set<String>> acceptingSets;
-  private final Set<NBATransition> transitions;
+  private final Set<NBATransition<ActionType>> transitions;
 
   public GNBABuilder() {
     this.states = new HashSet<>();
@@ -19,41 +19,41 @@ public GNBABuilder() {
     this.transitions = new HashSet<>();
   }
 
-  public GNBABuilder addStates(String... states) {
+  public GNBABuilder<ActionType> addStates(String... states) {
     for (String state : states) {
       addState(state);
     }
 
     return this;
   }
 
-  public GNBABuilder addState(String state) {
+  public GNBABuilder<ActionType> addState(String state) {
     this.states.add(state);
     return this;
   }
 
-  public GNBABuilder setAlphabet(Set<String> alphabet) {
+  public GNBABuilder<ActionType> setAlphabet(Set<String> alphabet) {
     this.alphabet.clear();
     this.alphabet.addAll(alphabet);
     return this;
   }
 
-  public GNBABuilder addInitialState(String initialState) {
+  public GNBABuilder<ActionType> addInitialState(String initialState) {
     this.initialStates.add(initialState);
     return this;
   }
 
-  public GNBABuilder addAcceptingSet(Set<String> acceptingSet) {
+  public GNBABuilder<ActionType> addAcceptingSet(Set<String> acceptingSet) {
     this.acceptingSets.add(new HashSet<>(acceptingSet));
     return this;
   }
 
-  public GNBABuilder addTransition(String from, String action, String to) {
+  public GNBABuilder<ActionType> addTransition(String from, ActionType action, String to) {
     this.transitions.add(NBATransition.of(from, action, to));
     return this;
   }
 
-  public GNBA build() {
-    return new GNBA(states, alphabet, initialStates, acceptingSets, transitions);
+  public GNBA<ActionType> build() {
+    return new GNBA<>(states, alphabet, initialStates, acceptingSets, transitions);
   }
 }
diff --git a/src/main/java/me/paultristanwagner/modelchecking/automaton/NBA.java b/src/main/java/me/paultristanwagner/modelchecking/automaton/NBA.java
@@ -1,72 +1,89 @@
 package me.paultristanwagner.modelchecking.automaton;
 
+import static me.paultristanwagner.modelchecking.util.GsonUtil.GSON;
+import static me.paultristanwagner.modelchecking.util.Pair.pair;
 import static me.paultristanwagner.modelchecking.util.TupleUtil.stringTuple;
 
-import com.google.gson.Gson;
-import com.google.gson.GsonBuilder;
+import java.lang.reflect.Type;
 import java.util.*;
-import me.paultristanwagner.modelchecking.ts.CyclePath;
 
-public class NBA {
+import com.google.gson.annotations.SerializedName;
+import me.paultristanwagner.modelchecking.ts.CyclePath;
+import me.paultristanwagner.modelchecking.util.Pair;
 
-  private static final Gson GSON;
-
-  static {
-    GSON =
-        new GsonBuilder()
-            .registerTypeAdapter(NBATransition.class, new NBATransition.NBATransitionAdapter())
-            .setPrettyPrinting()
-            .create();
-  }
+public class NBA<ActionType> {
 
   private final Set<String> states;
   private final Set<String> alphabet;
   private final Set<String> initialStates;
   private final Set<String> acceptingStates;
-  private final Set<NBATransition> transitions;
+  private final Set<NBATransition<ActionType>> transitions;
+
+  private final transient Map<String, Set<String>> successorCache;
+  private final transient Map<Pair<String, ActionType>, Set<String>> successorActionCache;
+
+  private NBA() {
+    this.states = new HashSet<>();
+    this.alphabet = new HashSet<>();
+    this.initialStates = new HashSet<>();
+    this.acceptingStates = new HashSet<>();
+    this.transitions = new HashSet<>();
+
+    this.successorCache = new HashMap<>();
+    this.successorActionCache = new HashMap<>();
+  }
 
   public NBA(
       Set<String> states,
       Set<String> alphabet,
       Set<String> initialStates,
       Set<String> acceptingStates,
-      Set<NBATransition> transitions) {
+      Set<NBATransition<ActionType>> transitions) {
     this.states = states;
     this.alphabet = alphabet;
     this.initialStates = initialStates;
     this.acceptingStates = acceptingStates;
     this.transitions = transitions;
+
+    this.successorCache = new HashMap<>();
+    this.successorActionCache = new HashMap<>();
   }
 
   public Set<String> getSuccessors(String state) {
+    if(successorCache.containsKey(state)) {
+      return successorCache.get(state);
+    }
+
     Set<String> successors = new HashSet<>();
-    for (NBATransition transition : transitions) {
+    for (NBATransition<ActionType> transition : transitions) {
       if (transition.getFrom().equals(state)) {
         successors.add(transition.getTo());
       }
     }
+
+    successorCache.put(state, successors);
+
     return successors;
   }
 
-  public Set<String> getSuccessors(String state, String action) {
+  public Set<String> getSuccessors(String state, ActionType action) {
+    if(successorActionCache.containsKey(pair(state, action))) {
+      return successorActionCache.get(pair(state, action));
+    }
+
     Set<String> successors = new HashSet<>();
-    for (NBATransition transition : transitions) {
+    for (NBATransition<ActionType> transition : transitions) {
       if (!transition.getFrom().equals(state)) {
         continue;
       }
 
-      // todo: make this more efficient
-      String a = transition.getAction();
-      String b = action;
-      Set<String> left = new HashSet<>(Arrays.asList(a.substring(1, a.length() - 1).split(", ")));
-      Set<String> right = new HashSet<>(Arrays.asList(b.substring(1, b.length() - 1).split(", ")));
-
-      boolean actionMatches = left.equals(right);
-
-      if (actionMatches) {
+      if (transition.getAction().equals(action)) {
         successors.add(transition.getTo());
       }
     }
+
+    successorActionCache.put(pair(state, action), successors);
+
     return successors;
   }
 
@@ -137,20 +154,20 @@ public NBAEmptinessResult checkEmptiness() {
     return NBAEmptinessResult.empty();
   }
 
-  public GNBA toGNBA() {
+  public GNBA<ActionType> toGNBA() {
     Set<String> states = new HashSet<>(this.states);
     Set<String> alphabet = new HashSet<>(this.alphabet);
     Set<String> initialStates = new HashSet<>(this.initialStates);
-    Set<NBATransition> transitions = new HashSet<>(this.transitions);
+    Set<NBATransition<ActionType>> transitions = new HashSet<>(this.transitions);
 
     Set<Set<String>> acceptingSets = new HashSet<>();
     acceptingSets.add(new HashSet<>(this.acceptingStates));
 
-    return new GNBA(states, alphabet, initialStates, acceptingSets, transitions);
+    return new GNBA<>(states, alphabet, initialStates, acceptingSets, transitions);
   }
 
-  public GNBA product(NBA other) {
-    GNBABuilder builder = new GNBABuilder();
+  public GNBA<ActionType> product(NBA<ActionType> other) {
+    GNBABuilder<ActionType> builder = new GNBABuilder<>();
     builder.setAlphabet(alphabet);
 
     for (String state1 : states) {
@@ -167,8 +184,8 @@ public GNBA product(NBA other) {
       }
     }
 
-    for (NBATransition transition : transitions) {
-      for (NBATransition otherTransition : other.transitions) {
+    for (NBATransition<ActionType> transition : transitions) {
+      for (NBATransition<ActionType> otherTransition : other.transitions) {
         if (!transition.getAction().equals(otherTransition.getAction())) {
           continue;
         }
@@ -205,8 +222,8 @@ public String toJson() {
     return GSON.toJson(this);
   }
 
-  public static NBA fromJson(String json) {
-    return GSON.fromJson(json, NBA.class);
+  public static <ActionType> NBA<ActionType> fromJson(String json, Type type) {
+    return GSON.fromJson(json, type);
   }
 
   public Set<String> getStates() {
@@ -225,7 +242,7 @@ public Set<String> getAcceptingStates() {
     return acceptingStates;
   }
 
-  public Set<NBATransition> getTransitions() {
+  public Set<NBATransition<ActionType>> getTransitions() {
     return transitions;
   }
 }