LTL checking capability

Add possibility of checking LTL properties with CEGAR. CFA is now extended with optional accepting edges. Classes are available that convert LTL string to such CFA.
ftsrg · Nov 20, 2024 · df2306b · df2306b
1 parent 39ba5ac
commit df2306b
Show file tree

Hide file tree

Showing 60 changed files with 3,220 additions and 103 deletions.
diff --git a/build.gradle.kts b/build.gradle.kts
@@ -29,7 +29,7 @@ buildscript {
 
 allprojects {
     group = "hu.bme.mit.theta"
-    version = "6.7.0"
+    version = "6.9.0"
 
     apply(from = rootDir.resolve("gradle/shared-with-buildSrc/mirrors.gradle.kts"))
 }

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
@@ -41,4 +41,5 @@ javasmtVersion=4.1.1
 sosylabVersion=0.3000-569-g89796f98
 cliktVersion=4.4.0
 spotlessVersion=6.25.0
-kamlVersion=0.59.0
+kamlVersion=0.59.0
+nuprocessVersion=2.0.6
diff --git a/buildSrc/src/main/kotlin/Deps.kt b/buildSrc/src/main/kotlin/Deps.kt
@@ -81,4 +81,6 @@ object Deps {
     val clikt = "com.github.ajalt.clikt:clikt:${Versions.clikt}"
 
     val kaml = "com.charleskorn.kaml:kaml:${Versions.kaml}"
+
+    val nuprocess = "com.zaxxer:nuprocess:${Versions.nuprocess}"
 }
diff --git a/lib/jhoafparser-1.1.1.jar b/lib/jhoafparser-1.1.1.jar
diff --git a/settings.gradle.kts b/settings.gradle.kts
@@ -21,6 +21,8 @@ include(
     "common/core",
     "common/grammar",
     "common/multi-tests",
+    "common/ltl",
+    "common/ltl-cli",
 
     "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,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();

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,22 +15,18 @@
  */
 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.base.Preconditions.*;
 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.*;
 
 /**
  * Represents an immutable Control Flow Automata (CFA). Use the builder class to create a new
@@ -45,21 +41,26 @@ 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;
         finalLoc = Optional.ofNullable(builder.finalLoc);
         errorLoc = Optional.ofNullable(builder.errorLoc);
         locs = ImmutableSet.copyOf(builder.locs);
         edges = ImmutableList.copyOf(builder.edges);
-        vars = edges.stream().flatMap(e -> StmtUtils.getVars(e.getStmt()).stream())
-                .collect(toImmutableSet());
+        vars =
+                edges.stream()
+                        .flatMap(e -> StmtUtils.getVars(e.getStmt()).stream())
+                        .collect(toImmutableSet());
         Set<String> varNames = Containers.createSet();
         for (var v : vars) {
-            checkArgument(!varNames.contains(v.getName()),
+            checkArgument(
+                    !varNames.contains(v.getName()),
                     "Variable with name '" + v.getName() + "' already exists in the CFA.");
             varNames.add(v.getName());
         }
+        acceptingEdges = builder.acceptingEdges;
     }
 
     public Loc getInitLoc() {
@@ -74,9 +75,7 @@ public Optional<Loc> getErrorLoc() {
         return errorLoc;
     }
 
-    /**
-     * Get the variables appearing on the edges of the CFA.
-     */
+    /** Get the variables appearing on the edges of the CFA. */
     public Collection<VarDecl<?>> getVars() {
         return vars;
     }
@@ -89,15 +88,23 @@ public Collection<Edge> getEdges() {
         return edges;
     }
 
+    public Collection<Edge> getAcceptingEdges() {
+        return acceptingEdges;
+    }
+
     public static Builder builder() {
         return new Builder();
     }
 
     @Override
     public String toString() {
-        return Utils.lispStringBuilder("process").aligned().addAll(vars).body()
+        return Utils.lispStringBuilder("process")
+                .aligned()
+                .addAll(vars)
+                .body()
                 .addAll(locs.stream().map(this::locToString))
-                .addAll(edges.stream().map(this::edgeToString)).toString();
+                .addAll(edges.stream().map(this::edgeToString))
+                .toString();
     }
 
     private String locToString(final Loc loc) {
@@ -113,9 +120,11 @@ private String locToString(final Loc loc) {
     }
 
     private String edgeToString(final Edge edge) {
-        return Utils.lispStringBuilder("edge").add(edge.getSource().getName())
+        return Utils.lispStringBuilder("edge")
+                .add(edge.getSource().getName())
                 .add(edge.getTarget().getName())
-                .add(edge.getStmt()).toString();
+                .add(edge.getStmt())
+                .toString();
     }
 
     public static final class Loc {
@@ -185,6 +194,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 +206,7 @@ private Builder() {
             locs = Containers.createSet();
             locNames = Containers.createSet();
             edges = new LinkedList<>();
+            acceptingEdges = Containers.createSet();
             built = false;
         }
 
@@ -240,7 +251,8 @@ public void setErrorLoc(final Loc errorLoc) {
 
         public Loc createLoc(final String name) {
             checkNotBuilt();
-            checkArgument(!locNames.contains(name),
+            checkArgument(
+                    !locNames.contains(name),
                     "Location with name '" + name + "' already exists in the CFA.");
             final Loc loc = new Loc(name);
             locs.add(loc);
@@ -264,14 +276,23 @@ 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) {
-                checkState(finalLoc.getOutEdges().isEmpty(),
+                checkState(
+                        finalLoc.getOutEdges().isEmpty(),
                         "Final location cannot have outgoing edges.");
             }
             if (errorLoc != null) {
-                checkState(errorLoc.getOutEdges().isEmpty(),
+                checkState(
+                        errorLoc.getOutEdges().isEmpty(),
                         "Error location cannot have outgoing edges.");
             }
             built = true;
@@ -282,5 +303,4 @@ private void checkNotBuilt() {
             checkState(!built, "A CFA was already built.");
         }
     }
-
 }
diff --git a/...lin/hu/bme/mit/theta/cfa/CFAVarChanger.kt → ...ava/hu/bme/mit/theta/cfa/CFAVarChanger.kt b/...lin/hu/bme/mit/theta/cfa/CFAVarChanger.kt → ...ava/hu/bme/mit/theta/cfa/CFAVarChanger.kt
@@ -13,29 +13,27 @@
  *  See the License for the specific language governing permissions and
  *  limitations under the License.
  */
-
 package hu.bme.mit.theta.cfa
 
 import hu.bme.mit.theta.core.decl.VarDecl
 import hu.bme.mit.theta.core.utils.changeVars
 
 /**
- * Extension function for CFA. Creates a new CFA which looks exactly the same, but any variable whose name is present in
- * the parameter gets replaced to the associated instance.
+ * Extension function for CFA. Creates a new CFA which looks exactly the same, but any variable
+ * whose name is present in the parameter gets replaced to the associated instance.
  */
 fun CFA.copyWithReplacingVars(variableMapping: Map<String, VarDecl<*>>): CFA {
-    val builder = CFA.builder()
-    val locationMap: Map<String, CFA.Loc> = locs.associate { it.name to builder.createLoc(it.name) }
-    builder.initLoc = locationMap[initLoc.name]
-    if (errorLoc.isPresent)
-        builder.errorLoc = locationMap[errorLoc.get().name]
-    if (finalLoc.isPresent)
-        builder.finalLoc = locationMap[finalLoc.get().name]
-    edges.forEach {
-        builder.createEdge(
-            locationMap[it.source.name], locationMap[it.target.name],
-            it.stmt.changeVars(variableMapping)
-        )
-    }
-    return builder.build()
+  val builder = CFA.builder()
+  val locationMap: Map<String, CFA.Loc> = locs.associate { it.name to builder.createLoc(it.name) }
+  builder.initLoc = locationMap[initLoc.name]
+  if (errorLoc.isPresent) builder.errorLoc = locationMap[errorLoc.get().name]
+  if (finalLoc.isPresent) builder.finalLoc = locationMap[finalLoc.get().name]
+  edges.forEach {
+    builder.createEdge(
+      locationMap[it.source.name],
+      locationMap[it.target.name],
+      it.stmt.changeVars(variableMapping),
+    )
+  }
+  return builder.build()
 }