Prototype for CTL*

src/main/java/me/paultristanwagner/modelchecking/ctl/formula/path/CTLNextFormula.java

@@ -6,24 +6,24 @@
 import me.paultristanwagner.modelchecking.ctl.formula.state.CTLParenthesisFormula;
 
 public class CTLNextFormula extends CTLPathFormula {
-  
+
   private final CTLFormula stateFormula;
-  
-  private CTLNextFormula( CTLFormula stateFormula ) {
+
+  private CTLNextFormula(CTLFormula stateFormula) {
     this.stateFormula = stateFormula;
   }
-  
-  public static CTLNextFormula next(CTLFormula stateFormula ) {
-    return new CTLNextFormula( stateFormula );
+
+  public static CTLNextFormula next(CTLFormula stateFormula) {
+    return new CTLNextFormula(stateFormula);
   }
-  
+
   public CTLFormula getStateFormula() {
     return stateFormula;
   }
-  
+
   @Override
   public String toString() {
-    if(stateFormula instanceof CTLParenthesisFormula ) {
+    if (stateFormula instanceof CTLParenthesisFormula) {
       return NEXT_SYMBOL + stateFormula;
     } else {
       return NEXT_SYMBOL + "(" + stateFormula + ")";

src/main/java/me/paultristanwagner/modelchecking/ctl/formula/state/CTLOrFormula.java

@@ -8,36 +8,36 @@
 public class CTLOrFormula extends CTLFormula {
 
   private final List<CTLFormula> components;
-  
+
   private CTLOrFormula(List<CTLFormula> components) {
     this.components = components;
   }
-  
+
   public static CTLOrFormula or(CTLFormula... components) {
-    return new CTLOrFormula( Arrays.asList( components ) );
+    return new CTLOrFormula(Arrays.asList(components));
   }
-  
+
   public static CTLOrFormula or(List<CTLFormula> components) {
-    return new CTLOrFormula( components );
+    return new CTLOrFormula(components);
   }
-  
+
   public List<CTLFormula> getComponents() {
     return components;
   }
-  
+
   @Override
   public String toString() {
     StringBuilder builder = new StringBuilder();
     for (int i = 0; i < components.size(); i++) {
-      builder.append( components.get( i ).toString() );
-      
+      builder.append(components.get(i).toString());
+
       if (i < components.size() - 1) {
-        builder.append( " " );
-        builder.append( OR_SYMBOL );
-        builder.append( " " );
+        builder.append(" ");
+        builder.append(OR_SYMBOL);
+        builder.append(" ");
       }
     }
-    
+
     return builder.toString();
   }
 }

src/main/java/me/paultristanwagner/modelchecking/ctlstar/formula/CTLStarAndFormula.java

@@ -0,0 +1,43 @@
+package me.paultristanwagner.modelchecking.ctlstar.formula;
+
+import static me.paultristanwagner.modelchecking.util.Symbol.AND_SYMBOL;
+
+import java.util.Arrays;
+import java.util.List;
+
+public class CTLStarAndFormula extends CTLStarFormula {
+
+  private final List<CTLStarFormula> components;
+
+  private CTLStarAndFormula(List<CTLStarFormula> components) {
+    this.components = components;
+  }
+
+  public static CTLStarAndFormula and(List<CTLStarFormula> components) {
+    return new CTLStarAndFormula(components);
+  }
+
+  public static CTLStarAndFormula and(CTLStarFormula... components) {
+    return new CTLStarAndFormula(Arrays.asList(components));
+  }
+
+  public List<CTLStarFormula> getComponents() {
+    return components;
+  }
+
+  @Override
+  public String toString() {
+    StringBuilder builder = new StringBuilder();
+    for (int i = 0; i < components.size(); i++) {
+      builder.append(components.get(i).toString());
+
+      if (i < components.size() - 1) {
+        builder.append(" ");
+        builder.append(AND_SYMBOL);
+        builder.append(" ");
+      }
+    }
+
+    return builder.toString();
+  }
+}

src/main/java/me/paultristanwagner/modelchecking/ctlstar/formula/CTLStarExistsFormula.java

@@ -0,0 +1,25 @@
+package me.paultristanwagner.modelchecking.ctlstar.formula;
+
+import static me.paultristanwagner.modelchecking.util.Symbol.EXISTENTIAL_QUANTIFIER_SYMBOL;
+
+public class CTLStarExistsFormula extends CTLStarFormula {
+
+  private final CTLStarFormula formula;
+
+  private CTLStarExistsFormula(CTLStarFormula formula) {
+    this.formula = formula;
+  }
+
+  public static CTLStarExistsFormula exists(CTLStarFormula formula) {
+    return new CTLStarExistsFormula(formula);
+  }
+
+  public CTLStarFormula getFormula() {
+    return formula;
+  }
+
+  @Override
+  public String toString() {
+    return EXISTENTIAL_QUANTIFIER_SYMBOL + formula;
+  }
+}

src/main/java/me/paultristanwagner/modelchecking/ctlstar/formula/CTLStarFormula.java

@@ -0,0 +1,3 @@
+package me.paultristanwagner.modelchecking.ctlstar.formula;
+
+public class CTLStarFormula {}

src/main/java/me/paultristanwagner/modelchecking/ctlstar/formula/CTLStarIdentifierFormula.java

@@ -0,0 +1,23 @@
+package me.paultristanwagner.modelchecking.ctlstar.formula;
+
+public class CTLStarIdentifierFormula extends CTLStarFormula {
+
+  private final String identifier;
+
+  private CTLStarIdentifierFormula(String identifier) {
+    this.identifier = identifier;
+  }
+
+  public static CTLStarIdentifierFormula identifier(String identifier) {
+    return new CTLStarIdentifierFormula(identifier);
+  }
+
+  public String getIdentifier() {
+    return identifier;
+  }
+
+  @Override
+  public String toString() {
+    return identifier;
+  }
+}

src/main/java/me/paultristanwagner/modelchecking/ctlstar/formula/CTLStarNextFormula.java

@@ -0,0 +1,25 @@
+package me.paultristanwagner.modelchecking.ctlstar.formula;
+
+import static me.paultristanwagner.modelchecking.util.Symbol.NEXT_SYMBOL;
+
+public class CTLStarNextFormula extends CTLStarFormula {
+
+  private final CTLStarFormula formula;
+
+  private CTLStarNextFormula(CTLStarFormula formula) {
+    this.formula = formula;
+  }
+
+  public static CTLStarNextFormula next(CTLStarFormula formula) {
+    return new CTLStarNextFormula(formula);
+  }
+
+  public CTLStarFormula getFormula() {
+    return formula;
+  }
+
+  @Override
+  public String toString() {
+    return NEXT_SYMBOL + formula;
+  }
+}

src/main/java/me/paultristanwagner/modelchecking/ctlstar/formula/CTLStarNotFormula.java

@@ -0,0 +1,25 @@
+package me.paultristanwagner.modelchecking.ctlstar.formula;
+
+import static me.paultristanwagner.modelchecking.util.Symbol.NOT_SYMBOL;
+
+public class CTLStarNotFormula extends CTLStarFormula {
+
+  private final CTLStarFormula formula;
+
+  private CTLStarNotFormula(CTLStarFormula formula) {
+    this.formula = formula;
+  }
+
+  public static CTLStarNotFormula not(CTLStarFormula formula) {
+    return new CTLStarNotFormula(formula);
+  }
+
+  public CTLStarFormula getFormula() {
+    return formula;
+  }
+
+  @Override
+  public String toString() {
+    return NOT_SYMBOL + formula;
+  }
+}

src/main/java/me/paultristanwagner/modelchecking/ctlstar/formula/CTLStarParenthesisFormula.java

@@ -0,0 +1,23 @@
+package me.paultristanwagner.modelchecking.ctlstar.formula;
+
+public class CTLStarParenthesisFormula extends CTLStarFormula {
+
+  private final CTLStarFormula formula;
+
+  private CTLStarParenthesisFormula(CTLStarFormula formula) {
+    this.formula = formula;
+  }
+
+  public static CTLStarParenthesisFormula parenthesis(CTLStarFormula formula) {
+    return new CTLStarParenthesisFormula(formula);
+  }
+
+  public CTLStarFormula getFormula() {
+    return formula;
+  }
+
+  @Override
+  public String toString() {
+    return "(" + formula + ")";
+  }
+}

src/main/java/me/paultristanwagner/modelchecking/ctlstar/formula/CTLStarTrueFormula.java

@@ -0,0 +1,15 @@
+package me.paultristanwagner.modelchecking.ctlstar.formula;
+
+public class CTLStarTrueFormula extends CTLStarFormula {
+
+  private CTLStarTrueFormula() {}
+
+  public static CTLStarTrueFormula TRUE() {
+    return new CTLStarTrueFormula();
+  }
+
+  @Override
+  public String toString() {
+    return "true";
+  }
+}

src/main/java/me/paultristanwagner/modelchecking/ctlstar/formula/CTLStarUntilFormula.java

@@ -0,0 +1,30 @@
+package me.paultristanwagner.modelchecking.ctlstar.formula;
+
+public class CTLStarUntilFormula extends CTLStarFormula {
+
+  private final CTLStarFormula left;
+  private final CTLStarFormula right;
+
+  private CTLStarUntilFormula(CTLStarFormula left, CTLStarFormula right) {
+    this.left = left;
+    this.right = right;
+  }
+
+  public static CTLStarUntilFormula until(CTLStarFormula left, CTLStarFormula right) {
+    return new CTLStarUntilFormula(left, right);
+  }
+
+  public CTLStarFormula getLeft() {
+    return left;
+  }
+
+  public CTLStarFormula getRight() {
+    return right;
+  }
+
+  @Override
+  public String toString() {
+    // todo: add brackets, but also possibility to parse them properly
+    return left + " U " + right;
+  }
+}

src/main/java/me/paultristanwagner/modelchecking/ctlstar/parse/CTLStarLexer.java

@@ -0,0 +1,41 @@
+package me.paultristanwagner.modelchecking.ctlstar.parse;
+
+import static me.paultristanwagner.modelchecking.util.Symbol.*;
+
+import me.paultristanwagner.modelchecking.parse.Lexer;
+import me.paultristanwagner.modelchecking.parse.TokenType;
+
+public class CTLStarLexer extends Lexer {
+
+  static final TokenType LPAREN = TokenType.of("(", "^\\(");
+  static final TokenType RPAREN = TokenType.of(")", "^\\)");
+  static final TokenType TRUE = TokenType.of("true", "^(true|TRUE)");
+  // static final TokenType FALSE = TokenType.of("false", "^(false|FALSE)");
+  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 NEXT = TokenType.of("next", "^(" + NEXT_SYMBOL + "|next|NEXT|O)");
+  static final TokenType UNTIL = TokenType.of("until", "^(" + UNTIL_SYMBOL + "|until|UNTIL)");
+  // static final TokenType EVENTUALLY = TokenType.of("eventually", "^(" + EVENTUALLY_SYMBOL +
+  // "|eventually|EVENTUALLY|diamond|DIAMOND)");
+  // static final TokenType ALWAYS = TokenType.of("always", "^(" + ALWAYS_SYMBOL +
+  // "|always|ALWAYS|box|BOX)");
+  // static final TokenType ALL = TokenType.of("all", "^(" + UNIVERSAL_QUANTIFIER_SYMBOL +
+  // "|all|ALL|A)");
+  static final TokenType EXISTS =
+      TokenType.of("exists", "^(" + EXISTENTIAL_QUANTIFIER_SYMBOL + "|exists|EXISTS|ex|EX|E)");
+  static final TokenType IDENTIFIER = TokenType.of("identifier", "^[a-z]");
+
+  public CTLStarLexer(String input) {
+    super(input);
+
+    /* registerTokenTypes(
+            LPAREN, RPAREN, TRUE, FALSE, NOT, AND, OR,
+            NEXT, UNTIL, EVENTUALLY, ALWAYS, ALL, EXISTS, IDENTIFIER
+    ); */
+
+    registerTokenTypes(LPAREN, RPAREN, TRUE, NOT, AND, NEXT, UNTIL, EXISTS, IDENTIFIER);
+
+    this.initialize(input);
+  }
+}