init copy

Move to CegarChecker Convert AcceptancePredicate to kotlin Add exceptions Move LDG to kotlin Move refinement to kotlin Move abstracting, visualizer, utils to kotlin
ftsrg · Oct 29, 2024 · 91bb03b · 91bb03b
1 parent 529352a
commit 91bb03b
Show file tree

Hide file tree

Showing 77 changed files with 4,661 additions and 28 deletions.
diff --git a/buildSrc/gradle.properties b/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,5 @@ 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
diff --git a/buildSrc/src/main/kotlin/Deps.kt b/buildSrc/src/main/kotlin/Deps.kt
@@ -79,4 +79,6 @@ object Deps {
     }
 
     val clikt = "com.github.ajalt.clikt:clikt:${Versions.clikt}"
+
+    val jbdd = "de.tum.in:jbdd:${Versions.jbdd}"
 }
diff --git a/lib/jhoafparser-1.1.1.jar b/lib/jhoafparser-1.1.1.jar
diff --git a/lib/owl-21.0.jar b/lib/owl-21.0.jar
diff --git a/settings.gradle.kts b/settings.gradle.kts
@@ -21,6 +21,7 @@ include(
     "common/core",
     "common/grammar",
     "common/multi-tests",
+    "common/ltl",
 
     "frontends/c-frontend",
     "frontends/petrinet-frontend/petrinet-model",

diff --git a/...cts/cfa/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/utils/CfaVisualizer.java b/...cts/cfa/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/utils/CfaVisualizer.java
@@ -15,33 +15,27 @@
  */
 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.Shape;
+import hu.bme.mit.theta.common.visualization.*;
 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 {
 
     private static final String CFA_LABEL = "";
@@ -51,6 +45,7 @@ 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() {
@@ -64,7 +59,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;
     }
@@ -102,10 +97,10 @@ private static void addLocation(final Graph graph, final CFA cfa, final Loc loc,
         graph.addNode(id, nAttrs);
     }
 
-    private static void addEdge(final Graph graph, final Edge edge, final Map<Loc, String> ids) {
+    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(EDGE_LINE_STYLE).font(EDGE_FONT).build();
+                .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);
     }
 

diff --git a/subprojects/cfa/cfa/build.gradle.kts b/subprojects/cfa/cfa/build.gradle.kts
@@ -22,4 +22,5 @@ plugins {
 dependencies {
     implementation(project(":theta-common"))
     implementation(project(":theta-core"))
+    implementation(Deps.jbdd)
 }
diff --git a/subprojects/cfa/cfa/src/main/antlr/LTLGrammar.g4 b/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;
+
diff --git a/subprojects/cfa/cfa/src/main/java/hu/bme/mit/theta/cfa/CFA.java b/subprojects/cfa/cfa/src/main/java/hu/bme/mit/theta/cfa/CFA.java
@@ -15,23 +15,20 @@
  */
 package hu.bme.mit.theta.cfa;
 
-import static com.google.common.base.Preconditions.checkArgument;
-import static com.google.common.base.Preconditions.checkNotNull;
-import static com.google.common.base.Preconditions.checkState;
-import static com.google.common.collect.ImmutableSet.toImmutableSet;
-import static java.lang.String.format;
-
-import java.util.*;
-
 import com.google.common.collect.ImmutableList;
 import com.google.common.collect.ImmutableSet;
-
 import hu.bme.mit.theta.common.Utils;
 import hu.bme.mit.theta.common.container.Containers;
 import hu.bme.mit.theta.core.decl.VarDecl;
 import hu.bme.mit.theta.core.stmt.Stmt;
 import hu.bme.mit.theta.core.utils.StmtUtils;
 
+import java.util.*;
+
+import static com.google.common.base.Preconditions.*;
+import static com.google.common.collect.ImmutableSet.toImmutableSet;
+import static java.lang.String.format;
+
 /**
  * Represents an immutable Control Flow Automata (CFA). Use the builder class to create a new
  * instance.
@@ -45,6 +42,7 @@ public final class CFA {
     private final Collection<VarDecl<?>> vars;
     private final Collection<Loc> locs;
     private final Collection<Edge> edges;
+    private final Collection<Edge> acceptingEdges;
 
     private CFA(final Builder builder) {
         initLoc = builder.initLoc;
@@ -60,6 +58,7 @@ private CFA(final Builder builder) {
                     "Variable with name '" + v.getName() + "' already exists in the CFA.");
             varNames.add(v.getName());
         }
+        acceptingEdges = builder.acceptingEdges;
     }
 
     public Loc getInitLoc() {
@@ -89,6 +88,10 @@ public Collection<Edge> getEdges() {
         return edges;
     }
 
+    public Collection<Edge> getAcceptingEdges() {
+        return acceptingEdges;
+    }
+
     public static Builder builder() {
         return new Builder();
     }
@@ -185,6 +188,7 @@ public static final class Builder {
 
         private final Collection<Loc> locs;
         private final Collection<Edge> edges;
+        private final Collection<Edge> acceptingEdges;
 
         private final Set<String> locNames;
 
@@ -196,6 +200,7 @@ private Builder() {
             locs = Containers.createSet();
             locNames = Containers.createSet();
             edges = new LinkedList<>();
+            acceptingEdges = Containers.createSet();
             built = false;
         }
 
@@ -264,6 +269,13 @@ public Edge createEdge(final Loc source, final Loc target, final Stmt stmt) {
             return edge;
         }
 
+        public void setAcceptingEdge(final Edge acceptingEdge) {
+            checkNotBuilt();
+            checkNotNull(acceptingEdge);
+            checkArgument(edges.contains(acceptingEdge), "Accepting edge not present in CFA.");
+            acceptingEdges.add(acceptingEdge);
+        }
+
         public CFA build() {
             checkState(initLoc != null, "Initial location must be set.");
             if (finalLoc != null) {