wip tracegen to xcfa

subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/tracegeneration/TraceGenerationChecker.kt

@@ -13,15 +13,15 @@ import hu.bme.mit.theta.common.logging.Logger
 import java.util.function.Consumer
 import kotlin.collections.ArrayList
 
-class TraceGenerationChecker<S : State, A : Action, 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,
 ) : Checker<AbstractTraceSummary<S, A>, P> {
     private var traces: List<Trace<S, A>> = ArrayList()
 
     companion object {
-        fun <S : State, A : Action, P : Prec?> create(
+        fun <S : State, A : Action, P : Prec> create(
             logger: Logger,
             abstractor: Abstractor<S, A, P>,
             getFullTraces: Boolean

subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToChecker.kt

@@ -45,6 +45,7 @@ fun getChecker(xcfa: XCFA, mcm: MCM, config: XcfaConfig<*, *>, parseContext: Par
             Backend.PORTFOLIO -> getPortfolioChecker(xcfa, mcm, config, parseContext, logger, uniqueLogger)
             Backend.NONE -> SafetyChecker<ARG<XcfaState<PtrState<*>>, XcfaAction>, Trace<XcfaState<PtrState<*>>, XcfaAction>, XcfaPrec<*>> { _ -> SafetyResult.unknown() }
             Backend.CHC -> getHornChecker(xcfa, mcm, config, logger)
+            Backend.TRACEGEN -> getTracegenChecker(xcfa, mcm, config, logger)
         }
     }
 

subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToTracegenChecker.kt

@@ -0,0 +1,98 @@
+/*
+ *  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.xcfa.cli.checkers
+
+import hu.bme.mit.theta.analysis.PartialOrd
+import hu.bme.mit.theta.analysis.Prec
+import hu.bme.mit.theta.analysis.Trace
+import hu.bme.mit.theta.analysis.algorithm.Checker
+import hu.bme.mit.theta.analysis.algorithm.SafetyChecker
+import hu.bme.mit.theta.analysis.algorithm.SafetyResult
+import hu.bme.mit.theta.analysis.algorithm.arg.ARG
+import hu.bme.mit.theta.analysis.algorithm.arg.ArgNode
+import hu.bme.mit.theta.analysis.algorithm.cegar.Abstractor
+import hu.bme.mit.theta.analysis.algorithm.cegar.CegarChecker
+import hu.bme.mit.theta.analysis.algorithm.cegar.Refiner
+import hu.bme.mit.theta.analysis.algorithm.cegar.abstractor.StopCriterion
+import hu.bme.mit.theta.analysis.algorithm.cegar.abstractor.StopCriterions
+import hu.bme.mit.theta.analysis.algorithm.tracegeneration.TraceGenerationChecker
+import hu.bme.mit.theta.analysis.algorithm.tracegeneration.summary.AbstractTraceSummary
+import hu.bme.mit.theta.analysis.algorithm.tracegeneration.summary.TraceGenerationResult
+import hu.bme.mit.theta.analysis.expr.ExprAction
+import hu.bme.mit.theta.analysis.expr.ExprState
+import hu.bme.mit.theta.analysis.expr.refinement.*
+import hu.bme.mit.theta.analysis.ptr.PtrState
+import hu.bme.mit.theta.analysis.runtimemonitor.CexMonitor
+import hu.bme.mit.theta.analysis.runtimemonitor.MonitorCheckpoint
+import hu.bme.mit.theta.analysis.waitlist.PriorityWaitlist
+import hu.bme.mit.theta.common.logging.Logger
+import hu.bme.mit.theta.core.decl.VarDecl
+import hu.bme.mit.theta.graphsolver.patterns.constraints.MCM
+import hu.bme.mit.theta.solver.SolverFactory
+import hu.bme.mit.theta.xcfa.analysis.*
+import hu.bme.mit.theta.xcfa.analysis.por.XcfaDporLts
+import hu.bme.mit.theta.xcfa.cli.params.*
+import hu.bme.mit.theta.xcfa.cli.utils.getSolver
+import hu.bme.mit.theta.xcfa.model.XCFA
+
+fun getTracegenChecker(xcfa: XCFA, mcm: MCM,
+    config: XcfaConfig<*, *>,
+    logger: Logger
+): Checker<AbstractTraceSummary<XcfaState<*>, XcfaAction>, XcfaPrec<*>> {
+    val tracegenConfig = config.backendConfig.specConfig as TracegenConfig
+    val ignoredVarRegistry = mutableMapOf<VarDecl<*>, MutableSet<ExprState>>()
+
+    val lts =  ConeOfInfluenceMode.NO_COI.getLts(xcfa, ignoredVarRegistry, POR.NOPOR)
+
+    val abstractionSolverFactory: SolverFactory = getSolver(tracegenConfig.abstractorConfig.abstractionSolver,
+        tracegenConfig.abstractorConfig.validateAbstractionSolver)
+
+    val waitlist = PriorityWaitlist.create<ArgNode<out XcfaState<PtrState<ExprState>>, XcfaAction>>(
+        tracegenConfig.abstractorConfig.search.getComp(xcfa))
+
+    val abstractionSolverInstance = abstractionSolverFactory.createSolver()
+    val globalStatePartialOrd: PartialOrd<PtrState<ExprState>> = tracegenConfig.abstractorConfig.domain.partialOrd(
+        abstractionSolverInstance) as PartialOrd<PtrState<ExprState>>
+    val corePartialOrd: PartialOrd<XcfaState<PtrState<ExprState>>> =
+        if (xcfa.isInlined) getPartialOrder(globalStatePartialOrd)
+        else getStackPartialOrder(globalStatePartialOrd)
+    val abstractor: Abstractor<ExprState, ExprAction, Prec> = tracegenConfig.abstractorConfig.domain.abstractor(
+        xcfa,
+        abstractionSolverInstance,
+        tracegenConfig.abstractorConfig.maxEnum,
+        waitlist,
+        StopCriterions.fullExploration(),
+        logger,
+        lts,
+        config.inputConfig.property,
+        corePartialOrd,
+        tracegenConfig.abstractorConfig.havocMemory
+    ) as Abstractor<ExprState, ExprAction, Prec>
+
+    val tracegenChecker = TraceGenerationChecker.create(logger, abstractor, false)
+
+    return tracegenChecker
+
+    /*object:
+        Checker<XcfaState<*>, XcfaAction, XcfaPrec<*>> {
+        override fun check(
+            prec: XcfaPrec<*>): TraceGenerationResult<AbstractTraceSummary<XcfaState<*>, XcfaAction>, XcfaState<*>, XcfaAction> {
+             return tracegenChecker.check(
+                prec) as TraceGenerationResult<AbstractTraceSummary<XcfaState<*>, XcfaAction>, XcfaState<*>, XcfaAction>
+        }*/
+    }
+}

subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/params/ParamValues.kt

@@ -70,6 +70,7 @@ enum class Backend {
     OC,
     LAZY,
     PORTFOLIO,
+    TRACEGEN,
     NONE,
 }
 
@@ -301,6 +302,11 @@ enum class Search {
     abstract fun getComp(cfa: XCFA): ArgNodeComparator
 }
 
+enum class TracegenAbstraction{
+    NONE,
+    // TODO add EXPL
+}
+
 enum class InitPrec(
     val explPrec: (xcfa: XCFA) -> XcfaPrec<PtrPrec<ExplPrec>>,
     val predPrec: (xcfa: XCFA) -> XcfaPrec<PtrPrec<PredPrec>>,

subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/params/XcfaConfig.kt

@@ -169,6 +169,7 @@ data class BackendConfig<T : SpecBackendConfig>(
             Backend.OC -> OcConfig() as T
             Backend.LAZY -> null
             Backend.PORTFOLIO -> PortfolioConfig() as T
+            Backend.TRACEGEN -> TracegenConfig() as T
             Backend.NONE -> null
         }
     }
@@ -202,6 +203,13 @@ data class CegarConfig(
         listOf(abstractorConfig, refinerConfig).map { it.update() }.any { it }
 }
 
+data class TracegenConfig(
+    @Parameter(names = ["--abstraction"], description = "Abstraction to be used for trace generation")
+    var abstraction: TracegenAbstraction = TracegenAbstraction.NONE,
+
+    val abstractorConfig: CegarAbstractorConfig = CegarAbstractorConfig(),
+) : SpecBackendConfig
+
 data class CegarAbstractorConfig(
     @Parameter(names = ["--abstraction-solver"], description = "Abstraction solver name")
     var abstractionSolver: String = "Z3",

subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/tracegeneration/XstsTracegenConfig.kt

@@ -9,7 +9,7 @@ import hu.bme.mit.theta.analysis.algorithm.tracegeneration.summary.AbstractTrace
 import hu.bme.mit.theta.analysis.expr.ExprAction
 import hu.bme.mit.theta.analysis.expr.ExprState
 
-class XstsTracegenConfig<S : State, A : Action, P : Prec?> private constructor(
+class XstsTracegenConfig<S : State, A : Action, P : Prec> private constructor(
     private val checker: TraceGenerationChecker<S, A, P>,
     private val prec: P
 ) {