Implement implication in LTL

paultristanwagner · Sep 29, 2023 · 69af078 · 69af078
1 parent ee28e16
commit 69af078
Show file tree

Hide file tree

Showing 6 changed files with 118 additions and 29 deletions.
diff --git a/README.md b/README.md
@@ -161,8 +161,12 @@ at: [paultristanwagner@gmail.com](mailto:paultristanwagner@gmail.com).
 
 ## Ideas for future work
 
-- Write tests for the CTL and LTL model checking algorithms
+- Improve UI / UX
+- Implement implication and equivalence operators in LTL, CTL, and CTL* grammar
+- 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
 - Implication and equivalence operators in CTL and LTL grammar
 - Parser for ω-regular expressions
+- ...
diff --git a/src/main/java/me/paultristanwagner/modelchecking/ltl/BasicLTLModelChecker.java b/src/main/java/me/paultristanwagner/modelchecking/ltl/BasicLTLModelChecker.java
@@ -276,6 +276,18 @@ 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) {
+          continue;
+        }
+
         if (formula instanceof LTLAndFormula andFormula) {
           lhs = isAssumed(andFormula);
 
@@ -298,6 +310,16 @@ public boolean isMaximallyConsistent(Set<LTLFormula> closure) {
           if (lhs != rhs) {
             return false;
           }
+        } else if(formula instanceof LTLImplicationFormula implicationFormula) {
+          lhs = isAssumed(implicationFormula);
+
+          rhs = !isAssumed(implicationFormula.getLeft()) || isAssumed(implicationFormula.getRight());
+
+          if (lhs != rhs) {
+            return false;
+          }
+        } else {
+          throw new UnsupportedOperationException("Unsupported formula: " + formula);
         }
       }
 

diff --git a/src/main/java/me/paultristanwagner/modelchecking/ltl/formula/LTLImplicationFormula.java b/src/main/java/me/paultristanwagner/modelchecking/ltl/formula/LTLImplicationFormula.java
@@ -0,0 +1,57 @@
+package me.paultristanwagner.modelchecking.ltl.formula;
+
+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;
+  private final LTLFormula right;
+
+  private LTLImplicationFormula(LTLFormula left, LTLFormula right) {
+    this.left = left;
+    this.right = right;
+  }
+
+  public static LTLImplicationFormula implies(LTLFormula left, LTLFormula right) {
+    return new LTLImplicationFormula(left, right);
+  }
+
+  @Override
+  public List<LTLFormula> getAllSubformulas() {
+    List<LTLFormula> subformulas = new ArrayList<>();
+    subformulas.add(this);
+    subformulas.addAll(left.getAllSubformulas());
+    subformulas.addAll(right.getAllSubformulas());
+    return subformulas;
+  }
+
+  public LTLFormula getLeft() {
+    return left;
+  }
+
+  public LTLFormula getRight() {
+    return right;
+  }
+
+  @Override
+  public String toString() {
+    return "(" + left + " " + IMPLICATION_SYMBOL + " " + right + ")";
+  }
+
+  @Override
+  public boolean equals(Object o) {
+    if (this == o) return true;
+    if (o == null || getClass() != o.getClass()) return false;
+    LTLImplicationFormula that = (LTLImplicationFormula) o;
+    return Objects.equals(left, that.left) && Objects.equals(right, that.right);
+  }
+
+  @Override
+  public int hashCode() {
+    return Objects.hash(left, right);
+  }
+}
diff --git a/src/main/java/me/paultristanwagner/modelchecking/ltl/parse/LTLLexer.java b/src/main/java/me/paultristanwagner/modelchecking/ltl/parse/LTLLexer.java
@@ -14,6 +14,8 @@ public class LTLLexer extends Lexer {
   static final TokenType NOT = TokenType.of("not", "^(" + NOT_SYMBOL + "|!|not|NOT|~)");
   static final TokenType AND = TokenType.of("and", "^(" + AND_SYMBOL + "|&|and|AND)");
   static final TokenType OR = TokenType.of("or", "^(" + OR_SYMBOL + "|\\||or|OR)");
+  static final TokenType IMPLICATION =
+      TokenType.of("implication", "^(" + IMPLICATION_SYMBOL + "|->|implies|IMPLIES)");
   static final TokenType NEXT = TokenType.of("next", "^(" + NEXT_SYMBOL + "|next|NEXT|O)");
   static final TokenType UNTIL = TokenType.of("until", "^(" + UNTIL_SYMBOL + "|until|UNTIL)");
   static final TokenType EVENTUALLY =
@@ -27,7 +29,7 @@ public LTLLexer(String input) {
     super(input);
 
     registerTokenTypes(
-        LPAREN, RPAREN, TRUE, FALSE, NOT, AND, OR, 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/ltl/parse/LTLParser.java b/src/main/java/me/paultristanwagner/modelchecking/ltl/parse/LTLParser.java
@@ -11,18 +11,7 @@
 import static me.paultristanwagner.modelchecking.ltl.formula.LTLParenthesisFormula.parenthesis;
 import static me.paultristanwagner.modelchecking.ltl.formula.LTLTrueFormula.TRUE;
 import static me.paultristanwagner.modelchecking.ltl.formula.LTLUntilFormula.until;
-import static me.paultristanwagner.modelchecking.ltl.parse.LTLLexer.ALWAYS;
-import static me.paultristanwagner.modelchecking.ltl.parse.LTLLexer.AND;
-import static me.paultristanwagner.modelchecking.ltl.parse.LTLLexer.EVENTUALLY;
-import static me.paultristanwagner.modelchecking.ltl.parse.LTLLexer.FALSE;
-import static me.paultristanwagner.modelchecking.ltl.parse.LTLLexer.IDENTIFIER;
-import static me.paultristanwagner.modelchecking.ltl.parse.LTLLexer.LPAREN;
-import static me.paultristanwagner.modelchecking.ltl.parse.LTLLexer.NEXT;
-import static me.paultristanwagner.modelchecking.ltl.parse.LTLLexer.NOT;
-import static me.paultristanwagner.modelchecking.ltl.parse.LTLLexer.OR;
-import static me.paultristanwagner.modelchecking.ltl.parse.LTLLexer.RPAREN;
-import static me.paultristanwagner.modelchecking.ltl.parse.LTLLexer.TRUE;
-import static me.paultristanwagner.modelchecking.ltl.parse.LTLLexer.UNTIL;
+import static me.paultristanwagner.modelchecking.ltl.parse.LTLLexer.*;
 
 import java.util.ArrayList;
 import java.util.List;
@@ -41,12 +30,14 @@ public class LTLParser implements Parser<LTLFormula> {
    * LTL Grammar:
    *
    *    <A> ::= <B>
-   *        | <A> OR <B>
+   *        | <B> IMPLICATION <A>
    *    <B> ::= <C>
-   *        | <B> AND <C>
-   *    <C> :: <D>
-   *        | <C> UNTIL <D>
-   *    <D> ::= NOT <D>
+   *        | <B> OR <C>
+   *    <C> ::= <D>
+   *        | <C> AND <D>
+   *    <D> :: <E>
+   *        | <D> UNTIL <E>
+   *    <E> ::= NOT <E>
    *        | NEXT <A>
    *        | ALWAYS <A>
    *        | EVENTUALLY <A>
@@ -75,13 +66,25 @@ private LTLFormula parseLTLFormula(LTLLexer lexer) {
   }
 
   private LTLFormula A(LTLLexer lexer) {
+    LTLFormula left = B(lexer);
+
+    if (lexer.hasNextToken() && lexer.getLookahead().getType() == IMPLICATION) {
+      lexer.consume(IMPLICATION);
+      LTLFormula second = A(lexer);
+      left = LTLImplicationFormula.implies(left, second);
+    }
+
+    return left;
+  }
+
+  private LTLFormula B(LTLLexer lexer) {
     List<LTLFormula> components = new ArrayList<>();
-    LTLFormula first = B(lexer);
+    LTLFormula first = C(lexer);
     components.add(first);
 
     while (lexer.hasNextToken() && lexer.getLookahead().getType() == LTLLexer.OR) {
       lexer.consume(OR);
-      components.add(B(lexer));
+      components.add(C(lexer));
     }
 
     if (components.size() == 1) {
@@ -91,14 +94,14 @@ private LTLFormula A(LTLLexer lexer) {
     return or(components);
   }
 
-  private LTLFormula B(LTLLexer lexer) {
+  private LTLFormula C(LTLLexer lexer) {
     List<LTLFormula> components = new ArrayList<>();
-    LTLFormula first = C(lexer);
+    LTLFormula first = D(lexer);
     components.add(first);
 
     while (lexer.hasNextToken() && lexer.getLookahead().getType() == AND) {
       lexer.consume(AND);
-      components.add(C(lexer));
+      components.add(D(lexer));
     }
 
     if (components.size() == 1) {
@@ -108,19 +111,19 @@ private LTLFormula B(LTLLexer lexer) {
     return and(components);
   }
 
-  private LTLFormula C(LTLLexer lexer) {
-    LTLFormula formula = D(lexer);
+  private LTLFormula D(LTLLexer lexer) {
+    LTLFormula formula = E(lexer);
 
     while (lexer.hasNextToken() && lexer.getLookahead().getType() == UNTIL) {
       lexer.consume(UNTIL);
-      LTLFormula second = D(lexer);
+      LTLFormula second = E(lexer);
       formula = until(formula, second);
     }
 
     return formula;
   }
 
-  private LTLFormula D(LTLLexer lexer) {
+  private LTLFormula E(LTLLexer lexer) {
     lexer.requireNextToken();
 
     Token lookahead = lexer.getLookahead();
@@ -150,7 +153,7 @@ private LTLFormula D(LTLLexer lexer) {
 
   private LTLNotFormula parseNot(LTLLexer lexer) {
     lexer.consume(NOT);
-    return not(D(lexer));
+    return not(E(lexer));
   }
 
   private LTLNextFormula parseNext(LTLLexer lexer) {

diff --git a/src/main/java/me/paultristanwagner/modelchecking/util/Symbol.java b/src/main/java/me/paultristanwagner/modelchecking/util/Symbol.java
@@ -5,6 +5,7 @@ public class Symbol {
   public static final String NOT_SYMBOL = "¬";
   public static final String AND_SYMBOL = "∧";
   public static final String OR_SYMBOL = "∨";
+  public static final String IMPLICATION_SYMBOL = "→";
   public static final String NEXT_SYMBOL = "◯";
   public static final String UNTIL_SYMBOL = "U";
   public static final String EVENTUALLY_SYMBOL = "◊";