xcfa projection + separate mayCover versions for CEGAR and other algo…

…rithms (impact)
ftsrg · Sep 20, 2023 · 53a611a · 53a611a
1 parent c43d0a1
commit 53a611a
Show file tree

Hide file tree

Showing 4 changed files with 10 additions and 10 deletions.
diff --git a/...rojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/ArgBuilder.java b/...rojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/ArgBuilder.java
@@ -109,13 +109,4 @@ public Collection<ArgNode<S, A>> expand(final ArgNode<S, A> node, final P prec)
         return newSuccNodes;
     }
 
-    public void close(final ArgNode<S, A> node) {
-        checkNotNull(node);
-        if (!node.isSubsumed()) {
-            final ARG<S, A> arg = node.arg;
-            final Optional<ArgNode<S, A>> nodeToCoverWith = arg.getNodes().filter(n -> n.mayCover(node)).findFirst();
-            nodeToCoverWith.ifPresent(node::cover);
-        }
-    }
-
 }
diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/ArgNode.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/ArgNode.java
@@ -92,6 +92,14 @@ public boolean mayCover(final ArgNode<S, A> node) {
         }
     }
 
+    public boolean mayCoverStandard(final ArgNode<S, A> node) {
+        if (arg.getPartialOrd().isLeq(node.getState(), this.getState())) {
+            return !(this.equals(node) || this.isSubsumed()); // no need to check ancestors in CEGAR
+        } else {
+            return false;
+        }
+    }
+
     public void setCoveringNode(final ArgNode<S, A> node) {
         if (!node.canCover) return;
         checkNotNull(node);

diff --git a/...mon/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/BasicAbstractor.java b/...mon/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/BasicAbstractor.java
@@ -127,7 +127,7 @@ private void close(final ArgNode<S, A> node, final Collection<ArgNode<S, A>> can
             return;
         }
         for (final ArgNode<S, A> candidate : candidates) {
-            if (candidate.mayCover(node)) {
+            if (candidate.mayCoverStandard(node)) {
                 node.cover(candidate);
                 return;
             }

diff --git a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaAnalysis.kt b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaAnalysis.kt
@@ -192,6 +192,7 @@ fun <S : XcfaState<out ExprState>, P : XcfaPrec<out Prec>> getXcfaAbstractor(
     BasicAbstractor.builder(getXcfaArgBuilder(analysis, lts, errorDetection))
         .waitlist(waitlist as Waitlist<ArgNode<S, XcfaAction>>) // TODO: can we do this nicely?
         .stopCriterion(stopCriterion as StopCriterion<S, XcfaAction>).logger(logger)
+        .projection { it.processes }
         .build() // TODO: can we do this nicely?
 
 /// EXPL