Merge branch 'xcfa-refactor' into xcfa-coi

# Conflicts:
#	subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/CegarChecker.java
#	subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/por/XcfaAasporLts.kt
#	subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/por/XcfaSporLts.kt
#	subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/XcfaCli.kt

.gitignore

@@ -16,3 +16,6 @@ dest/
 .idea/
 *.iml
 *.iws
+
+# Other
+wdl-output.json

subprojects/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);
-        }
-    }
-
 }

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);
@@ -278,7 +286,11 @@ public boolean equals(Object o) {
         if (this == o) return true;
         if (o == null || getClass() != o.getClass()) return false;
         ArgNode<?, ?> argNode = (ArgNode<?, ?>) o;
-        return id == argNode.id;
+        return depth == argNode.depth &&
+                state.equals(argNode.state) &&
+                coveringNode.equals(argNode.coveringNode) &&
+                Set.copyOf(outEdges).equals(Set.copyOf(argNode.outEdges)) &&
+                target == argNode.target;
     }
 
     @Override

subprojects/common/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;
             }

subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/CegarChecker.java

@@ -23,11 +23,15 @@
 import hu.bme.mit.theta.analysis.algorithm.SafetyChecker;
 import hu.bme.mit.theta.analysis.algorithm.SafetyResult;
 import hu.bme.mit.theta.analysis.runtimemonitor.MonitorCheckpoint;
+import hu.bme.mit.theta.analysis.utils.ArgVisualizer;
 import hu.bme.mit.theta.common.Utils;
 import hu.bme.mit.theta.common.logging.Logger;
 import hu.bme.mit.theta.common.logging.Logger.Level;
 import hu.bme.mit.theta.common.logging.NullLogger;
 
+import hu.bme.mit.theta.common.visualization.writer.JSONWriter;
+import hu.bme.mit.theta.common.visualization.writer.WebDebuggerLogger;
+
 import java.util.concurrent.TimeUnit;
 
 import static com.google.common.base.Preconditions.checkNotNull;
@@ -76,7 +80,7 @@ public SafetyResult<S, A> check(final P initPrec) {
         AbstractorResult abstractorResult = null;
         P prec = initPrec;
         int iteration = 0;
-//        WebDebuggerLogger wdl = WebDebuggerLogger.getInstance();
+        WebDebuggerLogger wdl = WebDebuggerLogger.getInstance();
         do {
             ++iteration;
 
@@ -87,10 +91,11 @@ public SafetyResult<S, A> check(final P initPrec) {
             abstractorTime += stopwatch.elapsed(TimeUnit.MILLISECONDS) - abstractorStartTime;
             logger.write(Level.MAINSTEP, "| Checking abstraction done, result: %s%n", abstractorResult);
 
-//            String argGraph = JSONWriter.getInstance().writeString(ArgVisualizer.getDefault().visualize(arg));
-//            String precString = prec.toString();
-
-//            wdl.addIteration(iteration, argGraph, precString);
+            if (WebDebuggerLogger.enabled()) {
+                String argGraph = JSONWriter.getInstance().writeString(ArgVisualizer.getDefault().visualize(arg));
+                String precString = prec.toString();
+                wdl.addIteration(iteration, argGraph, precString);
+            }
 
             if (abstractorResult.isUnsafe()) {
                 MonitorCheckpoint.Checkpoints.execute("CegarChecker.unsafeARG");