Fix bug in synchronous product and ts.copy()

paultristanwagner · Sep 30, 2023 · 08634df · 08634df
1 parent e7e13c5
commit 08634df
Show file tree

Hide file tree

Showing 15 changed files with 440 additions and 53 deletions.
diff --git a/src/main/java/me/paultristanwagner/modelchecking/Main.java b/src/main/java/me/paultristanwagner/modelchecking/Main.java
@@ -5,8 +5,10 @@
 import static me.paultristanwagner.modelchecking.util.Symbol.MODELS_SYMBOL;
 import static me.paultristanwagner.modelchecking.util.Symbol.NOT_MODELS_SYMBOL;
 
+import com.google.gson.JsonSyntaxException;
 import java.io.*;
 import java.nio.file.Files;
+import java.util.Arrays;
 import java.util.NoSuchElementException;
 import java.util.Optional;
 import java.util.Scanner;
@@ -15,6 +17,7 @@
 import me.paultristanwagner.modelchecking.ctl.formula.state.CTLFormula;
 import me.paultristanwagner.modelchecking.ctl.parse.CTLParser;
 import me.paultristanwagner.modelchecking.ctlstar.BasicCTLStarModelChecker;
+import me.paultristanwagner.modelchecking.ctlstar.CTLStarModelChecker;
 import me.paultristanwagner.modelchecking.ctlstar.formula.CTLStarFormula;
 import me.paultristanwagner.modelchecking.ctlstar.parse.CTLStarParser;
 import me.paultristanwagner.modelchecking.ltl.BasicLTLModelChecker;
@@ -25,6 +28,7 @@
 import me.paultristanwagner.modelchecking.parse.SyntaxError;
 import me.paultristanwagner.modelchecking.ts.CyclePath;
 import me.paultristanwagner.modelchecking.ts.TransitionSystem;
+import me.paultristanwagner.modelchecking.ts.TransitionSystemLoader;
 import me.paultristanwagner.modelchecking.util.Symbol;
 
 public class Main {
@@ -35,6 +39,7 @@ public class Main {
 
   public static void main(String[] args) {
     TransitionSystem ts = enterTransitionSystem();
+    ts.verifyNoNullLabels();
 
     while (true) {
       OUT.print("Enter formula: ");
@@ -82,7 +87,7 @@ public static void main(String[] args) {
 
         OUT.println(phiSymbol + " := " + formula + GRAY + " (CTL*)" + RESET);
 
-        BasicCTLStarModelChecker modelChecker = new BasicCTLStarModelChecker();
+        CTLStarModelChecker modelChecker = new BasicCTLStarModelChecker();
         result = modelChecker.check(ts, ctlStarFormula);
       } else {
         OUT.println(RED + "Unknown formula type" + RESET);
@@ -100,6 +105,7 @@ public static void main(String[] args) {
       long after = System.currentTimeMillis();
 
       long time_ms = after - before;
+      OUT.flush();
       OUT.println(GRAY + "(" + time_ms + " ms)" + RESET);
       OUT.println();
     }
@@ -209,22 +215,22 @@ private static TransitionSystem enterTransitionSystem() {
     TransitionSystem ts = null;
     while (ts == null) {
       File file = null;
+      String fileName = null;
       while (file == null) {
         OUT.print("Enter file for Transition System: ");
-        String input;
         try {
-          input = SCANNER.nextLine();
+          fileName = SCANNER.nextLine();
         } catch (NoSuchElementException e) {
           return null;
         }
 
-        file = new File(input);
+        file = new File(fileName);
         if (!file.exists()) {
-          OUT.println(RED + "Error: File does not exist!" + RESET);
+          OUT.println(RED + "Error: File '" + fileName + "' does not exist!" + RESET);
           OUT.println();
           file = null;
         } else if (file.isDirectory()) {
-          OUT.println(RED + "Error: File is a directory!" + RESET);
+          OUT.println(RED + "Error: File '" + fileName + "' is a directory!" + RESET);
           OUT.println();
           file = null;
         }
@@ -234,16 +240,17 @@ private static TransitionSystem enterTransitionSystem() {
       try {
         fileContent = new String(Files.readAllBytes(file.toPath()));
       } catch (IOException e) {
-        OUT.println(RED + "Error: Could not read file" + RESET);
+        OUT.println(RED + "Error: Could not read file '" + fileName + "'" + RESET);
         continue;
       }
 
       try {
-        ts = TransitionSystem.fromJson(fileContent);
+        ts = TransitionSystemLoader.fromJson(fileContent);
         OUT.println(GREEN + "Transition System loaded!" + RESET);
-      } catch (SyntaxError error) {
-        OUT.print(RED);
-        error.printWithContext();
+      } catch (JsonSyntaxException error) {
+        OUT.print(RED + "Error: Could not parse Transition System: ");
+        error.printStackTrace(OUT);
+        OUT.println(Arrays.toString(error.getStackTrace()));
         OUT.print(RESET);
       }
     }

diff --git a/src/main/java/me/paultristanwagner/modelchecking/automaton/NBA.java b/src/main/java/me/paultristanwagner/modelchecking/automaton/NBA.java
@@ -51,7 +51,19 @@ public Set<String> getSuccessors(String state) {
   public Set<String> getSuccessors(String state, String action) {
     Set<String> successors = new HashSet<>();
     for (NBATransition transition : transitions) {
-      if (transition.getFrom().equals(state) && transition.getAction().equals(action)) {
+      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) {
         successors.add(transition.getTo());
       }
     }

diff --git a/src/main/java/me/paultristanwagner/modelchecking/ctlstar/BasicCTLStarModelChecker.java b/src/main/java/me/paultristanwagner/modelchecking/ctlstar/BasicCTLStarModelChecker.java
@@ -13,6 +13,7 @@ public class BasicCTLStarModelChecker implements CTLStarModelChecker {
 
   @Override
   public CTLStarModelCheckingResult check(TransitionSystem ts, CTLStarFormula formula) {
+    ts = ts.copy();
     while (true) {
       Set<CTLStarFormula> stateSubFormulas = getNonTrivialMinimalStateSubFormulas(formula);
 

diff --git a/src/main/java/me/paultristanwagner/modelchecking/ctlstar/formula/CTLStarFalseFormula.java b/src/main/java/me/paultristanwagner/modelchecking/ctlstar/formula/CTLStarFalseFormula.java
@@ -8,15 +8,12 @@
 
 public class CTLStarFalseFormula extends CTLStarFormula {
 
-  private CTLStarFalseFormula() {
-
-  }
+  private CTLStarFalseFormula() {}
 
   public static CTLStarFalseFormula FALSE() {
     return new CTLStarFalseFormula();
   }
 
-
   @Override
   public int getDepth() {
     return 1;

diff --git a/src/main/java/me/paultristanwagner/modelchecking/ctlstar/formula/CTLStarOrFormula.java b/src/main/java/me/paultristanwagner/modelchecking/ctlstar/formula/CTLStarOrFormula.java
@@ -10,16 +10,16 @@ public class CTLStarOrFormula extends CTLStarFormula {
 
   private final List<CTLStarFormula> components;
 
-  private CTLStarOrFormula( List<CTLStarFormula> components ) {
+  private CTLStarOrFormula(List<CTLStarFormula> components) {
     this.components = components;
   }
 
-  public static CTLStarOrFormula or( List<CTLStarFormula> components ) {
-    return new CTLStarOrFormula( components );
+  public static CTLStarOrFormula or(List<CTLStarFormula> components) {
+    return new CTLStarOrFormula(components);
   }
 
-  public static CTLStarOrFormula or( CTLStarFormula... components ) {
-    return new CTLStarOrFormula( List.of( components ) );
+  public static CTLStarOrFormula or(CTLStarFormula... components) {
+    return new CTLStarOrFormula(List.of(components));
   }
 
   @Override

diff --git a/src/main/java/me/paultristanwagner/modelchecking/ltl/BasicLTLModelChecker.java b/src/main/java/me/paultristanwagner/modelchecking/ltl/BasicLTLModelChecker.java
@@ -18,6 +18,8 @@ public class BasicLTLModelChecker implements LTLModelChecker {
 
   @Override
   public LTLModelCheckingResult check(TransitionSystem ts, LTLFormula formula) {
+    ts = ts.copy();
+
     LTLFormula negation = formula.negate();
 
     GNBA gnba = computeGNBA(ts, negation);
@@ -42,20 +44,19 @@ public Set<String> sat(TransitionSystem ts, LTLFormula formula) {
     Set<String> result = new HashSet<>();
 
     LTLFormula negation = formula.negate();
-
     GNBA gnba = computeGNBA(ts, negation);
-
     NBA nba = gnba.convertToNBA();
 
-    Set<String> persistentStates = new HashSet<>(nba.getStates());
-    nba.getAcceptingStates().forEach(persistentStates::remove);
-
-    TransitionSystem copy = ts.copy();
     for (String state : ts.getStates()) {
-      copy.clearInitialStates();
-      copy.addInitialState(state);
+      TransitionSystem initial = ts.copy();
+      initial.clearInitialStates();
+      initial.addInitialState(state);
+
+      TransitionSystem synchronousProduct = initial.reachableSynchronousProduct(nba);
+
+      Set<String> persistentStates = new HashSet<>(nba.getStates());
+      nba.getAcceptingStates().forEach(persistentStates::remove);
 
-      TransitionSystem synchronousProduct = copy.reachableSynchronousProduct(nba);
       TSPersistenceResult persistenceResult = synchronousProduct.checkPersistence(persistentStates);
       if (persistenceResult.isPersistent()) {
         result.add(state);
@@ -204,6 +205,17 @@ private Set<Guess> computeElementarySets(
 
     Assignment assignment = new Assignment();
 
+    // todo: figure out what to do with this
+    for (LTLFormula ltlFormula : closure) {
+      if (ltlFormula instanceof LTLIdentifierFormula identifierFormula) {
+        String identifier = identifierFormula.getIdentifier();
+        if (!atomicPropositions.contains(identifier)) {
+          throw new IllegalStateException(
+              "Identifier '" + identifier + "' not in atomic propositions");
+        }
+      }
+    }
+
     // add all atomic propositions to the closure, even if they don't occur in the formula
     for (String atomicProposition : atomicPropositions) {
       LTLFormula atomicPropositionFormula = identifier(atomicProposition);
@@ -276,15 +288,15 @@ public boolean isMaximallyConsistent(Set<LTLFormula> closure) {
         boolean lhs;
         boolean rhs;
 
-        if(formula instanceof LTLTrueFormula
-          || formula instanceof LTLFalseFormula
-          || formula instanceof LTLIdentifierFormula
-          || formula instanceof LTLParenthesisFormula
-          || formula instanceof LTLNextFormula
-          || formula instanceof LTLUntilFormula
-          || formula instanceof LTLEventuallyFormula
-          || formula instanceof LTLAlwaysFormula
-          || formula instanceof LTLNotFormula) {
+        if (formula instanceof LTLTrueFormula
+            || formula instanceof LTLFalseFormula
+            || formula instanceof LTLIdentifierFormula
+            || formula instanceof LTLParenthesisFormula
+            || formula instanceof LTLNextFormula
+            || formula instanceof LTLUntilFormula
+            || formula instanceof LTLEventuallyFormula
+            || formula instanceof LTLAlwaysFormula
+            || formula instanceof LTLNotFormula) {
           continue;
         }
 
@@ -310,10 +322,11 @@ public boolean isMaximallyConsistent(Set<LTLFormula> closure) {
           if (lhs != rhs) {
             return false;
           }
-        } else if(formula instanceof LTLImplicationFormula implicationFormula) {
+        } else if (formula instanceof LTLImplicationFormula implicationFormula) {
           lhs = isAssumed(implicationFormula);
 
-          rhs = !isAssumed(implicationFormula.getLeft()) || isAssumed(implicationFormula.getRight());
+          rhs =
+              !isAssumed(implicationFormula.getLeft()) || isAssumed(implicationFormula.getRight());
 
           if (lhs != rhs) {
             return false;

diff --git a/src/main/java/me/paultristanwagner/modelchecking/ltl/formula/LTLImplicationFormula.java b/src/main/java/me/paultristanwagner/modelchecking/ltl/formula/LTLImplicationFormula.java
@@ -1,11 +1,11 @@
 package me.paultristanwagner.modelchecking.ltl.formula;
 
+import static me.paultristanwagner.modelchecking.util.Symbol.IMPLICATION_SYMBOL;
+
 import java.util.ArrayList;
 import java.util.List;
 import java.util.Objects;
 
-import static me.paultristanwagner.modelchecking.util.Symbol.IMPLICATION_SYMBOL;
-
 public class LTLImplicationFormula extends LTLFormula {
 
   private final LTLFormula left;

diff --git a/src/main/java/me/paultristanwagner/modelchecking/ltl/parse/LTLLexer.java b/src/main/java/me/paultristanwagner/modelchecking/ltl/parse/LTLLexer.java
@@ -23,13 +23,25 @@ public class LTLLexer extends Lexer {
           "eventually", "^(" + EVENTUALLY_SYMBOL + "|eventually|EVENTUALLY|diamond|DIAMOND)");
   static final TokenType ALWAYS =
       TokenType.of("always", "^(" + ALWAYS_SYMBOL + "|always|ALWAYS|box|BOX)");
-  static final TokenType IDENTIFIER = TokenType.of("identifier", "^[a-z]");
+  static final TokenType IDENTIFIER = TokenType.of("identifier", "^[a-zA-Z_][a-zA-Z0-9_]*");
 
   public LTLLexer(String input) {
     super(input);
 
     registerTokenTypes(
-        LPAREN, RPAREN, TRUE, FALSE, NOT, AND, OR, IMPLICATION, NEXT, UNTIL, EVENTUALLY, ALWAYS, IDENTIFIER);
+        LPAREN,
+        RPAREN,
+        TRUE,
+        FALSE,
+        NOT,
+        AND,
+        OR,
+        IMPLICATION,
+        NEXT,
+        UNTIL,
+        EVENTUALLY,
+        ALWAYS,
+        IDENTIFIER);
 
     this.initialize(input);
   }

diff --git a/src/main/java/me/paultristanwagner/modelchecking/ts/TransitionSystem.java b/src/main/java/me/paultristanwagner/modelchecking/ts/TransitionSystem.java
@@ -47,12 +47,24 @@ public TransitionSystem(
     }
   }
 
+  public void verifyNoNullLabels() {
+    labelingFunction.forEach(
+        (state, labels) -> {
+          if (labels.contains(null)) {
+            throw new IllegalStateException("Null label for state " + state);
+          }
+        });
+  }
+
   public TransitionSystem copy() {
     List<String> states = new ArrayList<>(this.states);
     List<TSTransition> transitions = new ArrayList<>(this.transitions);
     List<String> initialStates = new ArrayList<>(this.initialStates);
     List<String> atomicPropositions = new ArrayList<>(this.atomicPropositions);
-    Map<String, List<String>> labelingFunction = new HashMap<>(this.labelingFunction);
+
+    Map<String, List<String>> labelingFunction = new HashMap<>();
+    this.labelingFunction.forEach(
+        (state, labels) -> labelingFunction.put(state, new ArrayList<>(labels)));
 
     return new TransitionSystem(
         states, transitions, initialStates, atomicPropositions, labelingFunction);
@@ -77,8 +89,17 @@ public TransitionSystem reachableSynchronousProduct(NBA nba) {
 
         String q = nbaTransition.getTo();
 
-        // todo: match actions and labels more carefully
-        if (!nbaTransition.getAction().equals(label.toString())) {
+        String a = nbaTransition.getAction();
+        String b = label.toString();
+
+        // todo: make this more efficient
+        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) {
           continue;
         }
 
@@ -254,8 +275,4 @@ public List<String> getLabel(String state) {
   public String toJson() {
     return GSON.toJson(this);
   }
-
-  public static TransitionSystem fromJson(String string) {
-    return GSON.fromJson(string, TransitionSystem.class);
-  }
 }
diff --git a/src/main/java/me/paultristanwagner/modelchecking/ts/TransitionSystemLoader.java b/src/main/java/me/paultristanwagner/modelchecking/ts/TransitionSystemLoader.java
@@ -0,0 +1,34 @@
+package me.paultristanwagner.modelchecking.ts;
+
+import com.google.gson.Gson;
+import com.google.gson.GsonBuilder;
+import java.io.File;
+import java.io.IOException;
+import java.nio.file.Files;
+
+public class TransitionSystemLoader {
+
+  private static final Gson GSON;
+
+  static {
+    GSON =
+        new GsonBuilder()
+            .registerTypeAdapter(TSTransition.class, new TSTransition.TSTransitionAdapter())
+            .setPrettyPrinting()
+            .create();
+  }
+
+  public static TransitionSystem load(String path) throws IOException {
+    File file = new File(path);
+    return load(file);
+  }
+
+  public static TransitionSystem load(File file) throws IOException {
+    String fileContent = new String(Files.readAllBytes(file.toPath()));
+    return fromJson(fileContent);
+  }
+
+  public static TransitionSystem fromJson(String string) {
+    return GSON.fromJson(string, TransitionSystem.class);
+  }
+}