Fix bug in synchronous product and ts.copy()

paultristanwagner · Sep 30, 2023 · 9aff317 · 9aff317
1 parent e7e13c5
commit 9aff317
Show file tree

Hide file tree

Showing 13 changed files with 432 additions and 30 deletions.
diff --git a/examples/bug.json b/examples/bug.json
@@ -0,0 +1,32 @@
+{
+  "states": [
+    "s0",
+    "s1"
+  ],
+  "transitions": [
+    [
+      "s0",
+      "s1"
+    ],
+    [
+      "s1",
+      "s1"
+    ]
+  ],
+  "initialStates": [
+    "s0"
+  ],
+  "atomicPropositions": [
+    "a",
+    "a_0",
+    "a_1"
+  ],
+  "labelingFunction": {
+    "s0": [],
+    "s1": [
+      "a",
+      "a_0",
+      "a_1"
+    ]
+  }
+}
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/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,16 @@ 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);

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,7 +23,7 @@ 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);

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,23 @@ 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 +88,16 @@ 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 +273,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,35 @@
+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);
+  }
+}
diff --git a/src/main/java/me/paultristanwagner/modelchecking/util/Symbol.java b/src/main/java/me/paultristanwagner/modelchecking/util/Symbol.java
@@ -20,4 +20,7 @@ public class Symbol {
 
   public static final String MODELS_SYMBOL = "⊨";
   public static final String NOT_MODELS_SYMBOL = "⊭";
+
+  public static final String CHECKMARK = "✓";
+  public static final String CROSS = "✗";
 }