Convert ltl expression to buchi automaton

CFA is now extended with optional accepting edges. Classes are available that convert LTL string to such CFA.

buildSrc/gradle.properties

@@ -17,7 +17,7 @@
 javaVersion=17
 kotlinVersion=1.9.25
 shadowVersion=7.1.2
-antlrVersion=4.9.2
+antlrVersion=4.12.0
 guavaVersion=31.1-jre
 jcommanderVersion=1.72
 z3Version=4.5.0
@@ -40,4 +40,6 @@ gsonVersion=2.9.1
 javasmtVersion=4.1.1
 sosylabVersion=0.3000-569-g89796f98
 cliktVersion=4.4.0
-spotlessVersion=6.25.0
+spotlessVersion=6.25.0
+jbddVersion=0.5.2
+nuprocessVersion=2.0.6

buildSrc/src/main/kotlin/Deps.kt

@@ -79,4 +79,8 @@ object Deps {
     }
 
     val clikt = "com.github.ajalt.clikt:clikt:${Versions.clikt}"
+
+    val jbdd = "de.tum.in:jbdd:${Versions.jbdd}"
+
+    val nuprocess = "com.zaxxer:nuprocess:${Versions.nuprocess}"
 }

subprojects/cfa/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/utils/CfaVisualizer.java

@@ -15,32 +15,25 @@
  */
 package hu.bme.mit.theta.cfa.analysis.utils;
 
-import java.awt.Color;
-
-import hu.bme.mit.theta.common.container.Containers;
-
-import java.util.LinkedHashSet;
-import java.util.Map;
-import java.util.Optional;
-import java.util.Set;
-
 import hu.bme.mit.theta.analysis.Trace;
 import hu.bme.mit.theta.analysis.expl.ExplState;
 import hu.bme.mit.theta.cfa.CFA;
 import hu.bme.mit.theta.cfa.CFA.Edge;
 import hu.bme.mit.theta.cfa.CFA.Loc;
 import hu.bme.mit.theta.cfa.analysis.CfaAction;
 import hu.bme.mit.theta.cfa.analysis.CfaState;
+import hu.bme.mit.theta.common.container.Containers;
 import hu.bme.mit.theta.common.table.TableWriter;
-import hu.bme.mit.theta.common.visualization.Alignment;
-import hu.bme.mit.theta.common.visualization.EdgeAttributes;
-import hu.bme.mit.theta.common.visualization.Graph;
-import hu.bme.mit.theta.common.visualization.LineStyle;
-import hu.bme.mit.theta.common.visualization.NodeAttributes;
+import hu.bme.mit.theta.common.visualization.*;
 import hu.bme.mit.theta.common.visualization.Shape;
 import hu.bme.mit.theta.core.decl.Decl;
 import hu.bme.mit.theta.core.decl.VarDecl;
 import hu.bme.mit.theta.core.dsl.CoreDslManager;
+import java.awt.*;
+import java.util.LinkedHashSet;
+import java.util.Map;
+import java.util.Optional;
+import java.util.Set;
 
 public final class CfaVisualizer {
 
@@ -51,10 +44,10 @@ public final class CfaVisualizer {
     private static final Color LINE_COLOR = Color.BLACK;
     private static final LineStyle LOC_LINE_STYLE = LineStyle.NORMAL;
     private static final LineStyle EDGE_LINE_STYLE = LineStyle.NORMAL;
+    private static final LineStyle ACC_EDGE_LINE_STYLE = LineStyle.DASHED;
     private static final String EDGE_FONT = "courier";
 
-    private CfaVisualizer() {
-    }
+    private CfaVisualizer() {}
 
     public static Graph visualize(final CFA cfa) {
         final Graph graph = new Graph(CFA_ID, CFA_LABEL);
@@ -64,7 +57,7 @@ public static Graph visualize(final CFA cfa) {
             addLocation(graph, cfa, loc, ids);
         }
         for (final Edge edge : cfa.getEdges()) {
-            addEdge(graph, edge, ids);
+            addEdge(graph, edge, cfa.getAcceptingEdges().contains(edge), ids);
         }
         return graph;
     }
@@ -74,16 +67,20 @@ private static void addVars(final Graph graph, final CFA cfa) {
         for (final VarDecl<?> var : cfa.getVars()) {
             sb.append('\n').append(var.getName()).append(": ").append(var.getType());
         }
-        final NodeAttributes attrs = NodeAttributes.builder().label(sb.toString())
-                .shape(Shape.RECTANGLE)
-                .fillColor(FILL_COLOR).lineColor(LINE_COLOR).lineStyle(LineStyle.DASHED)
-                .alignment(Alignment.LEFT)
-                .build();
+        final NodeAttributes attrs =
+                NodeAttributes.builder()
+                        .label(sb.toString())
+                        .shape(Shape.RECTANGLE)
+                        .fillColor(FILL_COLOR)
+                        .lineColor(LINE_COLOR)
+                        .lineStyle(LineStyle.DASHED)
+                        .alignment(Alignment.LEFT)
+                        .build();
         graph.addNode(CFA_ID + "_vars", attrs);
     }
 
-    private static void addLocation(final Graph graph, final CFA cfa, final Loc loc,
-                                    final Map<Loc, String> ids) {
+    private static void addLocation(
+            final Graph graph, final CFA cfa, final Loc loc, final Map<Loc, String> ids) {
         final String id = LOC_ID_PREFIX + ids.size();
         ids.put(loc, id);
         String label = loc.getName();
@@ -96,21 +93,34 @@ private static void addLocation(final Graph graph, final CFA cfa, final Loc loc,
             label += " (error)";
         }
         final int peripheries = isError ? 2 : 1;
-        final NodeAttributes nAttrs = NodeAttributes.builder().label(label).fillColor(FILL_COLOR)
-                .lineColor(LINE_COLOR)
-                .lineStyle(LOC_LINE_STYLE).peripheries(peripheries).build();
+        final NodeAttributes nAttrs =
+                NodeAttributes.builder()
+                        .label(label)
+                        .fillColor(FILL_COLOR)
+                        .lineColor(LINE_COLOR)
+                        .lineStyle(LOC_LINE_STYLE)
+                        .peripheries(peripheries)
+                        .build();
         graph.addNode(id, nAttrs);
     }
 
-    private static void addEdge(final Graph graph, final Edge edge, final Map<Loc, String> ids) {
-        final EdgeAttributes eAttrs = EdgeAttributes.builder()
-                .label(new CoreDslManager().writeStmt(edge.getStmt()))
-                .color(LINE_COLOR).lineStyle(EDGE_LINE_STYLE).font(EDGE_FONT).build();
+    private static void addEdge(
+            final Graph graph,
+            final Edge edge,
+            final boolean accepting,
+            final Map<Loc, String> ids) {
+        final EdgeAttributes eAttrs =
+                EdgeAttributes.builder()
+                        .label(new CoreDslManager().writeStmt(edge.getStmt()))
+                        .color(LINE_COLOR)
+                        .lineStyle(accepting ? ACC_EDGE_LINE_STYLE : EDGE_LINE_STYLE)
+                        .font(EDGE_FONT)
+                        .build();
         graph.addEdge(ids.get(edge.getSource()), ids.get(edge.getTarget()), eAttrs);
     }
 
-    public static void printTraceTable(final Trace<CfaState<ExplState>, CfaAction> trace,
-                                       final TableWriter writer) {
+    public static void printTraceTable(
+            final Trace<CfaState<ExplState>, CfaAction> trace, final TableWriter writer) {
         final Set<Decl<?>> allVars = new LinkedHashSet<>();
         for (final CfaState<ExplState> state : trace.getStates()) {
             allVars.addAll(state.getState().getDecls());
@@ -132,7 +142,8 @@ public static void printTraceTable(final Trace<CfaState<ExplState>, CfaAction> t
             writer.newRow();
             if (i < trace.getActions().size()) {
                 final StringBuilder sb = new StringBuilder();
-                trace.getAction(i).getStmts()
+                trace.getAction(i)
+                        .getStmts()
                         .forEach(s -> sb.append(s.toString()).append(System.lineSeparator()));
                 writer.cell(sb.toString(), nCols);
                 writer.newRow();

subprojects/cfa/cfa/build.gradle.kts

@@ -22,4 +22,5 @@ plugins {
 dependencies {
     implementation(project(":theta-common"))
     implementation(project(":theta-core"))
+    implementation(Deps.jbdd)
 }

subprojects/cfa/cfa/src/main/antlr/LTLGrammar.g4

@@ -0,0 +1,138 @@
+/*
+ * To change this license header, choose License Headers in Project Properties.
+ * To change this template file, choose Tools | Templates
+ * and open the template in the editor.
+ */
+
+grammar LTLGrammar;
+
+model:
+	rules+=implyExpression*;
+
+implyExpression:
+	ops+=orExpr (IMPLIES ops+=orExpr)?
+;
+
+orExpr:
+	ops+=andExpr (OR ops+=andExpr)*
+;
+
+andExpr:
+	ops+=notExpr (AND ops+=notExpr)*
+;
+
+notExpr:
+	binaryLtlExpr|
+	NOT ops+=notExpr
+;
+
+binaryLtlExpr:
+    ltlExpr |
+    ops+=binaryLtlExpr type=binaryLtlOp ops+=binaryLtlExpr;
+
+binaryLtlOp:
+    M_OP | W_OP | U_OP | R_OP;
+
+ltlExpr:
+	eqExpr |
+	type=ltlOp ops+=ltlExpr
+;
+
+ltlOp:
+         F_OP|G_OP|X_OP
+     ;
+
+eqExpr:
+	ops+=relationExpr (oper=eqOperator ops+=relationExpr)?
+;
+
+eqOperator:
+	EQ|NEQ
+;
+
+relationExpr:
+	ops+=additiveExpr (oper=relationOperator ops+=additiveExpr)?
+;
+
+relationOperator:
+	LT|GT|LEQ|GEQ
+;
+
+additiveExpr:
+	ops+=multiplicativeExpr (opers+=additiveOperator ops+=multiplicativeExpr)*
+;
+
+additiveOperator:
+	PLUS|MINUS
+;
+
+multiplicativeExpr:
+	ops+=negExpr (opers+=multiplicativeOperator ops+=negExpr)*
+;
+
+multiplicativeOperator:
+	MUL|DIV|MOD
+;
+
+negExpr:
+	primaryExpr|
+	MINUS ops+=negExpr
+;
+
+primaryExpr:
+	boolLitExpr|
+	intLitExpr|
+	enumLitExpr|
+	parenExpr
+;
+
+boolLitExpr:
+	value=BOOLLIT
+;
+
+parenExpr:
+	LPAREN ops+=implyExpression RPAREN | variable
+;
+
+intLitExpr:
+	value=INTLIT
+;
+
+enumLitExpr:
+    type=ID DOT lit=ID
+;
+
+variable:
+	name=ID
+;
+
+AND: 'and' | '&&';
+OR: 'or' | '|' | '||';
+IMPLIES: '->' | '=>';
+NOT: 'not' | '!';
+EQ: '=' | '==';
+NEQ: '/=' | '!=';
+LT: '<';
+GT: '>';
+LEQ: '<=';
+GEQ: '>=';
+PLUS: '+';
+MINUS: '-';
+MUL: '*';
+DIV: '/';
+MOD: '%';
+LPAREN: '(';
+RPAREN: ')';
+F_OP: 'F';
+G_OP: 'G';
+U_OP: 'U';
+W_OP: 'W';
+M_OP: 'M';
+R_OP: 'R';
+X_OP: 'X';
+INTLIT: [0-9]+;
+BOOLLIT: 'true' | 'false';
+ID: [a-zA-Z][a-zA-Z0-9_]*;
+DOT: '.';
+WS: (' '| '\t' | '\n' | '\r') -> skip;
+