removed logging

ftsrg · Oct 21, 2023 · fffcfe3 · fffcfe3
1 parent 64e1160
commit fffcfe3
Show file tree

Hide file tree

Showing 5 changed files with 3 additions and 117 deletions.
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
@@ -129,7 +129,6 @@ private void close(final ArgNode<S, A> node, final Collection<ArgNode<S, A>> can
         for (final ArgNode<S, A> candidate : candidates) {
             if (candidate.mayCover(node)) {
                 node.cover(candidate);
-                COILogger.incCovers();
                 return;
             }
         }

diff --git a/...ts/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/COILogger.java b/...ts/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/COILogger.java
diff --git a/...common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/CegarChecker.java b/...common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/CegarChecker.java
@@ -23,19 +23,11 @@
 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.Graph;
-import hu.bme.mit.theta.common.visualization.writer.GraphvizWriter;
-import hu.bme.mit.theta.common.visualization.writer.JSONWriter;
-import hu.bme.mit.theta.common.visualization.writer.WebDebuggerLogger;
-
-import java.io.FileWriter;
-import java.io.IOException;
 import java.util.concurrent.TimeUnit;
 
 import static com.google.common.base.Preconditions.checkNotNull;
@@ -99,7 +91,6 @@ public SafetyResult<S, A> check(final P initPrec) {
 //            String precString = prec.toString();
 
 //            wdl.addIteration(iteration, argGraph, precString);
-            COILogger.newIteration();
 
             if (abstractorResult.isUnsafe()) {
                 MonitorCheckpoint.Checkpoints.execute("CegarChecker.unsafeARG");
@@ -141,15 +132,6 @@ public SafetyResult<S, A> check(final P initPrec) {
         assert cegarResult != null;
         logger.write(Level.RESULT, "%s%n", cegarResult);
         logger.write(Level.INFO, "%s%n", stats);
-        System.err.println("Abstractor time: " + stats.getAbstractorTimeMs());
-        System.err.println("Refiner time: " + stats.getRefinerTimeMs());
-        System.err.println("COI time: " + COILogger.coiTimer);
-        System.err.println("TransFunc time: " + COILogger.transFuncTimer);
-        System.err.println("COI NOP labels: " + COILogger.nopsList);
-        System.err.println("COI havoc labels: " + COILogger.havocsList);
-        System.err.println("COI all labels: " + COILogger.allLabelsList);
-        System.err.println("Covers: " + COILogger.coversList);
-        System.err.println("Explored actions: " + COILogger.exploredActionsList);
         return cegarResult;
     }
 

diff --git a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/coi/XcfaCoi.kt b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/coi/XcfaCoi.kt
@@ -3,7 +3,6 @@ package hu.bme.mit.theta.xcfa.analysis.coi
 import hu.bme.mit.theta.analysis.LTS
 import hu.bme.mit.theta.analysis.Prec
 import hu.bme.mit.theta.analysis.TransFunc
-import hu.bme.mit.theta.analysis.algorithm.cegar.COILogger
 import hu.bme.mit.theta.analysis.expr.ExprState
 import hu.bme.mit.theta.core.decl.VarDecl
 import hu.bme.mit.theta.core.stmt.AssignStmt
@@ -38,29 +37,11 @@ abstract class XcfaCoi(protected val xcfa: XCFA) {
     abstract val lts: LTS<S, A>
 
     val transFunc = TransFunc<S, A, XcfaPrec<out Prec>> { state, action, prec ->
-        val a = action.transFuncVersion ?: action
-        action.label.getFlatLabels().forEach {
-            if (it is NopLabel) COILogger.decNops()
-            if (it is StmtLabel && it.stmt is HavocStmt<*>) COILogger.decHavocs()
-        }
-        a.label.getFlatLabels().forEach {
-            COILogger.incAllLabels()
-            if (it is NopLabel) COILogger.incNops()
-            if (it is StmtLabel && it.stmt is HavocStmt<*>) COILogger.incHavocs()
-        }
-        COILogger.incExploredActions()
-
-        COILogger.startTransFuncTimer()
-        val r = coreTransFunc.getSuccStates(state, a, prec)
-        COILogger.stopTransFuncTimer()
-
-        r
+        coreTransFunc.getSuccStates(state, action.transFuncVersion ?: action, prec)
     }
 
     init {
-        COILogger.startCoiTimer()
         xcfa.procedures.forEach { tarjan(it.initLoc) }
-        COILogger.stopCoiTimer()
     }
 
     private fun tarjan(initLoc: XcfaLocation) {

diff --git a/...xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/coi/XcfaCoiMultiThread.kt b/...xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/coi/XcfaCoiMultiThread.kt
@@ -2,7 +2,6 @@ package hu.bme.mit.theta.xcfa.analysis.coi
 
 import hu.bme.mit.theta.analysis.LTS
 import hu.bme.mit.theta.analysis.Prec
-import hu.bme.mit.theta.analysis.algorithm.cegar.COILogger
 import hu.bme.mit.theta.xcfa.getFlatLabels
 import hu.bme.mit.theta.xcfa.getVars
 import hu.bme.mit.theta.xcfa.isWritten
@@ -31,21 +30,13 @@ class XcfaCoiMultiThread(xcfa: XCFA) : XcfaCoi(xcfa) {
     override val lts = object : LTS<S, A> {
         override fun getEnabledActionsFor(state: S): Collection<A> {
             val enabled = coreLts.getEnabledActionsFor(state)
-            COILogger.startCoiTimer()
-            val r = lastPrec?.let { replaceIrrelevantActions(state, enabled, it) } ?: enabled
-            COILogger.stopCoiTimer()
-            return r
+            return lastPrec?.let { replaceIrrelevantActions(state, enabled, it) } ?: enabled
         }
 
         override fun <P : Prec> getEnabledActionsFor(state: S, explored: Collection<A>, prec: P): Collection<A> {
-            COILogger.startCoiTimer()
             if (lastPrec != prec) reinitialize(prec)
-            COILogger.stopCoiTimer()
             val enabled = coreLts.getEnabledActionsFor(state, explored, prec)
-            COILogger.startCoiTimer()
-            val r = replaceIrrelevantActions(state, enabled, prec)
-            COILogger.stopCoiTimer()
-            return r
+            return replaceIrrelevantActions(state, enabled, prec)
         }
 
         private fun replaceIrrelevantActions(state: S, enabled: Collection<A>, prec: Prec): Collection<A> {