added basic trace metadata collection; tracegen refactored to clikt

ftsrg · Sep 20, 2024 · 9b8c51e · 9b8c51e
1 parent 37089d3
commit 9b8c51e
Show file tree

Hide file tree

Showing 14 changed files with 189 additions and 124 deletions.
diff --git a/...s/src/main/java/hu/bme/mit/theta/analysis/algorithm/tracegeneration/AdvancedArgTrace.java b/...s/src/main/java/hu/bme/mit/theta/analysis/algorithm/tracegeneration/AdvancedArgTrace.java
@@ -3,8 +3,8 @@
 import hu.bme.mit.theta.analysis.Action;
 import hu.bme.mit.theta.analysis.State;
 import hu.bme.mit.theta.analysis.Trace;
-import hu.bme.mit.theta.analysis.algorithm.ArgEdge;
-import hu.bme.mit.theta.analysis.algorithm.ArgNode;
+import hu.bme.mit.theta.analysis.algorithm.arg.ArgEdge;
+import hu.bme.mit.theta.analysis.algorithm.arg.ArgNode;
 
 import java.util.*;
 import java.util.stream.Collectors;

diff --git a/...alysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/tracegeneration/PatchArgTrace.kt b/...alysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/tracegeneration/PatchArgTrace.kt
@@ -2,8 +2,8 @@ package hu.bme.mit.theta.analysis.algorithm.tracegeneration
 
 import hu.bme.mit.theta.analysis.Action
 import hu.bme.mit.theta.analysis.State
-import hu.bme.mit.theta.analysis.algorithm.ArgNode
-import hu.bme.mit.theta.analysis.algorithm.ArgTrace
+import hu.bme.mit.theta.analysis.algorithm.arg.ArgNode
+import hu.bme.mit.theta.analysis.algorithm.arg.ArgTrace
 
 /**
  * Traces built on ArgTraces, but capable of handling traces going through covered nodes

diff --git a/...c/main/java/hu/bme/mit/theta/analysis/algorithm/tracegeneration/TraceGenerationChecker.kt b/...c/main/java/hu/bme/mit/theta/analysis/algorithm/tracegeneration/TraceGenerationChecker.kt
@@ -1,28 +1,27 @@
 package hu.bme.mit.theta.analysis.algorithm.tracegeneration
 
 import com.google.common.base.Preconditions
-import hu.bme.mit.theta.analysis.Prec
-import hu.bme.mit.theta.analysis.Trace
+import hu.bme.mit.theta.analysis.*
 import hu.bme.mit.theta.analysis.algorithm.*
-import hu.bme.mit.theta.analysis.algorithm.arg.ARG
+import hu.bme.mit.theta.analysis.algorithm.SafetyResult
 import hu.bme.mit.theta.analysis.algorithm.arg.ArgNode
 import hu.bme.mit.theta.analysis.algorithm.arg.ArgTrace
 import hu.bme.mit.theta.analysis.algorithm.cegar.Abstractor
-import hu.bme.mit.theta.analysis.expr.ExprAction
-import hu.bme.mit.theta.analysis.expr.ExprState
 import hu.bme.mit.theta.common.logging.Logger
+import java.util.*
 import java.util.function.Consumer
+import kotlin.collections.ArrayList
 
 
-class TraceGenerationChecker<S : ExprState?, A : ExprAction?, P : Prec?>(
+class TraceGenerationChecker<S : State, A : Action, P : Prec?>(
     private val logger: Logger,
     private val abstractor: Abstractor<S, A, P>,
     private val getFullTraces : Boolean,
-) : SafetyChecker<ARG<S, A>, Trace<S, A>, P> { // TODO refactor templates?
+) : SafetyChecker<TraceGenerationResult<S, A>, EmptyCex, P> { // TODO refactor templates?
     private var traces: List<Trace<S, A>> = ArrayList()
 
     companion object {
-        fun <S : ExprState?, A : ExprAction?, P : Prec?> create(
+        fun <S : State, A : Action, P : Prec?> create(
             logger: Logger,
             abstractor: Abstractor<S, A, P>,
             getFullTraces: Boolean
@@ -31,7 +30,7 @@ class TraceGenerationChecker<S : ExprState?, A : ExprAction?, P : Prec?>(
         }
     }
 
-    override fun check(prec: P): SafetyResult<ARG<S, A>, Trace<S, A>> {
+    override fun check(prec: P): SafetyResult<TraceGenerationResult<S, A>, EmptyCex> {
         logger.write(Logger.Level.SUBSTEP, "Printing prec for trace generation...\n" + System.lineSeparator())
         logger.write(Logger.Level.SUBSTEP, prec.toString())
 
@@ -70,6 +69,12 @@ class TraceGenerationChecker<S : ExprState?, A : ExprAction?, P : Prec?>(
                 )
             }.toList())
 
+        // TODO does not work with full traces (see below - modification should be done to arg traces?)
+        assert(!getFullTraces)
+        val metadataBuilder = TraceGenerationMetadataBuilder<S, A>()
+        argTraces.forEach { trace -> metadataBuilder.addTrace(trace) }
+        val traceMetadata = metadataBuilder.build()
+
         // filter 2, optional, to get full traces even where there is coverage
         // why?: otherwise we stop at the leaf, which is covered in many traces by other nodes
         traces = if (getFullTraces) {
@@ -87,8 +92,8 @@ class TraceGenerationChecker<S : ExprState?, A : ExprAction?, P : Prec?>(
         )
         logger.write(Logger.Level.SUBSTEP, "-- Trace generation done --\n")
 
-        return SafetyResult.traces(traces)
-
+        // TODO return unsafe if coverage not full? (is that known here? not yet)
+        return SafetyResult.safe(TraceGenerationResult(traceMetadata, traces))
     }
 
     private fun filterEndNodes(

diff --git a/...rc/main/java/hu/bme/mit/theta/analysis/algorithm/tracegeneration/TraceGenerationResult.kt b/...rc/main/java/hu/bme/mit/theta/analysis/algorithm/tracegeneration/TraceGenerationResult.kt
@@ -0,0 +1,27 @@
+/*
+ *  Copyright 2024 Budapest University of Technology and Economics
+ *
+ *  Licensed under the Apache License, Version 2.0 (the "License");
+ *  you may not use this file except in compliance with the License.
+ *  You may obtain a copy of the License at
+ *
+ *      http://www.apache.org/licenses/LICENSE-2.0
+ *
+ *  Unless required by applicable law or agreed to in writing, software
+ *  distributed under the License is distributed on an "AS IS" BASIS,
+ *  WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ *  See the License for the specific language governing permissions and
+ *  limitations under the License.
+ */
+
+package hu.bme.mit.theta.analysis.algorithm.tracegeneration
+
+import hu.bme.mit.theta.analysis.Action
+import hu.bme.mit.theta.analysis.State
+import hu.bme.mit.theta.analysis.Trace
+import hu.bme.mit.theta.analysis.algorithm.Witness
+
+data class TraceGenerationResult<S : State, A : Action> (
+    val metadata: Collection<TraceMetadata<S, A>>,
+    val traces: Collection<Trace<S, A>>
+) : Witness
diff --git a/...alysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/tracegeneration/TraceMetadata.kt b/...alysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/tracegeneration/TraceMetadata.kt
@@ -4,6 +4,7 @@ import hu.bme.mit.theta.analysis.Action
 import hu.bme.mit.theta.analysis.State
 import hu.bme.mit.theta.analysis.algorithm.arg.ArgNode
 import hu.bme.mit.theta.analysis.algorithm.arg.ArgTrace
+import kotlin.jvm.optionals.getOrNull
 
 class TraceGenerationMetadataBuilder<S : State, A : Action> {
 
@@ -50,13 +51,13 @@ class TraceGenerationMetadataBuilder<S : State, A : Action> {
                 metadataTraces.keys.forEach { trace ->
                     metadataStates[Pair(trace, coveredNode)]?.let { coveredMetaState ->
                         if (coveredMetaState != state) {
-                            coveredMetaState.coveringState.add(state)
+                            coveredMetaState.coveredState.add(state)
                         }
                     }
                 }
             }
 
-            node.coveringNode.get().let { coveringNode ->
+            node.coveringNode.getOrNull()?.let { coveringNode ->
                 metadataTraces.keys.forEach { trace ->
                     metadataStates[Pair(trace, coveringNode)]?.let { coveredMetaState ->
                         if (coveredMetaState != state) {
@@ -66,6 +67,15 @@ class TraceGenerationMetadataBuilder<S : State, A : Action> {
                 }
             }
         }
+
+        var missingCover = false
+        for (stateMetadata in metadataStates.values) {
+            stateMetadata.coveringState.forEach { coveringState -> if(!coveringState.coveredState.contains(stateMetadata)) missingCover = true  }
+            stateMetadata.coveredState.forEach { coveredState -> if(!coveredState.coveringState.contains(stateMetadata)) missingCover = true  }
+        }
+
+        assert(!missingCover
+        ) { "Some coverages are only stored in one direction (covering not stored in covered or vica versa)" }
     }
 }
 
@@ -107,7 +117,18 @@ class StateMetadata<S : State, A: Action> (val state: State, val id : Long = cou
     }
 
     override fun toString(): String {
-        return "S$id"
+        val sb = StringBuilder()
+        sb.append("S$id{")
+        if(coveredState.isNotEmpty()) {
+            sb.append("covering: ")
+            coveredState.forEach { coveringState -> sb.append("S${coveringState.id} ") }
+        }
+        if(coveringState.isNotEmpty()) {
+            sb.append("covered by: ")
+            coveringState.forEach { coveredState -> sb.append("S${coveredState.id} ") }
+        }
+        sb.append("}")
+        return sb.toString()
     }
 }
 

diff --git a/...in/java/hu/bme/mit/theta/analysis/algorithm/tracegeneration/XstsDoubleEndNodeRemover.java b/...in/java/hu/bme/mit/theta/analysis/algorithm/tracegeneration/XstsDoubleEndNodeRemover.java
@@ -1,10 +1,10 @@
 package hu.bme.mit.theta.analysis.algorithm.tracegeneration;
 
+import hu.bme.mit.theta.analysis.Action;
+import hu.bme.mit.theta.analysis.State;
 import hu.bme.mit.theta.analysis.Trace;
-import hu.bme.mit.theta.analysis.algorithm.ARG;
-import hu.bme.mit.theta.analysis.algorithm.ArgNode;
-import hu.bme.mit.theta.analysis.expr.ExprAction;
-import hu.bme.mit.theta.analysis.expr.ExprState;
+import hu.bme.mit.theta.analysis.algorithm.arg.ARG;
+import hu.bme.mit.theta.analysis.algorithm.arg.ArgNode;
 import hu.bme.mit.theta.analysis.expr.StmtAction;
 
 import java.io.BufferedReader;
@@ -13,8 +13,8 @@
 import java.util.ArrayList;
 import java.util.List;
 
-public class XstsDoubleEndNodeRemover<S extends ExprState, A extends ExprAction> {
-    static <S extends ExprState, A extends ExprAction> List<ArgNode<S,A>> collectBadLeaves(ARG<S,A> arg) {
+public class XstsDoubleEndNodeRemover<S extends State, A extends Action> {
+    static <S extends State, A extends Action> List<ArgNode<S,A>> collectBadLeaves(ARG<S,A> arg) {
         // TODO XSTS SPECIFIC for now! collecting nodes that look like there should be traces to it, but shouldn't ("not firing anything" nodes)
         XstsDoubleEndNodeRemover<S, A> instance = new XstsDoubleEndNodeRemover<S, A>();
         List<ArgNode<S, A>> badNodes = new ArrayList<>();
@@ -63,7 +63,7 @@ private boolean isBadLeaf(ArgNode<S, A> node) {
         }
     }
 
-    static <S extends ExprState, A extends StmtAction> Trace<S, A> filterSuperfluousEndNode(Trace<S, A> trace) {
+    static <S extends State, A extends StmtAction> Trace<S, A> filterSuperfluousEndNode(Trace<S, A> trace) {
         if(trace.getStates().size()>3) {
             boolean transitionFired = false;
             int size = trace.getStates().size();

diff --git a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/utils/StmtAssumeCollector.java b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/utils/StmtAssumeCollector.java
diff --git a/...nalysis/src/main/java/hu/bme/mit/theta/xsts/analysis/initprec/XstsTracegenPredInitPrec.kt b/...nalysis/src/main/java/hu/bme/mit/theta/xsts/analysis/initprec/XstsTracegenPredInitPrec.kt
@@ -3,7 +3,6 @@ package hu.bme.mit.theta.xsts.analysis.initprec
 import hu.bme.mit.theta.analysis.expl.ExplPrec
 import hu.bme.mit.theta.analysis.pred.PredPrec
 import hu.bme.mit.theta.analysis.prod2.Prod2Prec
-import hu.bme.mit.theta.core.utils.StmtAssumeCollector
 import hu.bme.mit.theta.core.utils.StmtAtomCollector
 import hu.bme.mit.theta.xsts.XSTS
 

diff --git a/...lysis/src/main/java/hu/bme/mit/theta/xsts/analysis/tracegeneration/XstsTracegenBuilder.kt b/...lysis/src/main/java/hu/bme/mit/theta/xsts/analysis/tracegeneration/XstsTracegenBuilder.kt
@@ -1,17 +1,17 @@
 package hu.bme.mit.theta.xsts.analysis.tracegeneration
 
 import com.google.common.base.Preconditions
+import hu.bme.mit.theta.analysis.Action
 import hu.bme.mit.theta.analysis.Prec
-import hu.bme.mit.theta.analysis.algorithm.ArgBuilder
+import hu.bme.mit.theta.analysis.State
+import hu.bme.mit.theta.analysis.algorithm.arg.ArgBuilder
 import hu.bme.mit.theta.analysis.algorithm.cegar.Abstractor
 import hu.bme.mit.theta.analysis.algorithm.cegar.BasicAbstractor
 import hu.bme.mit.theta.analysis.algorithm.cegar.abstractor.StopCriterions
 import hu.bme.mit.theta.analysis.algorithm.tracegeneration.TraceGenerationChecker.Companion.create
 import hu.bme.mit.theta.analysis.expl.*
 import hu.bme.mit.theta.analysis.expr.ExprAction
 import hu.bme.mit.theta.analysis.expr.ExprState
-import hu.bme.mit.theta.analysis.expr.ExprStatePredicate
-import hu.bme.mit.theta.analysis.pred.*
 import hu.bme.mit.theta.analysis.waitlist.PriorityWaitlist
 import hu.bme.mit.theta.common.logging.Logger
 import hu.bme.mit.theta.common.logging.NullLogger
@@ -24,7 +24,6 @@ import hu.bme.mit.theta.xsts.XSTS
 import hu.bme.mit.theta.xsts.analysis.*
 import hu.bme.mit.theta.xsts.analysis.config.XstsConfigBuilder
 import hu.bme.mit.theta.xsts.analysis.initprec.XstsAllVarsInitPrec
-import hu.bme.mit.theta.xsts.analysis.initprec.XstsTracegenPredInitPrec
 import hu.bme.mit.theta.xsts.analysis.initprec.XstsVarListInitPrec
 import java.io.File
 import java.io.IOException
@@ -57,7 +56,7 @@ class XstsTracegenBuilder(
         return this
     }
 
-    private fun buildExpl(xsts: XSTS) : XstsTracegenConfig<out ExprState?, out ExprAction?, out ExplPrec?> {
+    private fun buildExpl(xsts: XSTS) : XstsTracegenConfig<out ExprState, out ExprAction, out ExplPrec> {
         val solver2 =
             solverFactory.createSolver() // abstraction // TODO handle separate solvers in a nicer way
 
@@ -70,7 +69,7 @@ class XstsTracegenBuilder(
         val argBuilder = ArgBuilder.create(lts, analysis, target, true)
 
         if (abstraction==TracegenerationAbstraction.VARLIST) {
-            val abstractor: Abstractor<XstsState<ExplState>?, XstsAction?, ExplPrec?> =
+            val abstractor: Abstractor<XstsState<ExplState>, XstsAction, ExplPrec> =
                 BasicAbstractor.builder(argBuilder)
                     .waitlist(PriorityWaitlist.create(XstsConfigBuilder.Search.DFS.comparator))
                     .stopCriterion(StopCriterions.fullExploration())
@@ -106,7 +105,7 @@ class XstsTracegenBuilder(
             }
         } else {
             assert(abstraction==TracegenerationAbstraction.NONE)
-            val abstractor: Abstractor<XstsState<ExplState>?, XstsAction?, ExplPrec?> =
+            val abstractor: Abstractor<XstsState<ExplState>, XstsAction, ExplPrec> =
                 BasicAbstractor.builder(argBuilder)
                     .waitlist(PriorityWaitlist.create(XstsConfigBuilder.Search.DFS.comparator))
                     .stopCriterion(StopCriterions.fullExploration())
@@ -154,7 +153,7 @@ class XstsTracegenBuilder(
     }
     */
 
-    fun build(xsts: XSTS): XstsTracegenConfig<out ExprState?, out ExprAction?, out Prec?> {
+    fun build(xsts: XSTS): XstsTracegenConfig<out State, out Action, out Prec> {
         val solver2 =
             solverFactory.createSolver() // abstraction // TODO handle separate solvers in a nicer way