resolving merge issues

ftsrg · Oct 31, 2024 · 2d2ceba · 2d2ceba
1 parent 1050170
commit 2d2ceba
Show file tree

Hide file tree

Showing 2 changed files with 9 additions and 16 deletions.
diff --git a/...jects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/oc/XcfaOcChecker.kt b/...jects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/oc/XcfaOcChecker.kt
@@ -15,15 +15,15 @@
  */
 package hu.bme.mit.theta.xcfa.analysis.oc
 
-import hu.bme.mit.theta.analysis.Trace
+import hu.bme.mit.theta.analysis.Cex
+import hu.bme.mit.theta.analysis.EmptyCex
 import hu.bme.mit.theta.analysis.algorithm.EmptyProof
 import hu.bme.mit.theta.analysis.algorithm.SafetyChecker
 import hu.bme.mit.theta.analysis.algorithm.SafetyResult
 import hu.bme.mit.theta.analysis.algorithm.oc.EventType
 import hu.bme.mit.theta.analysis.algorithm.oc.OcChecker
 import hu.bme.mit.theta.analysis.algorithm.oc.Relation
 import hu.bme.mit.theta.analysis.algorithm.oc.RelationType
-import hu.bme.mit.theta.analysis.ptr.PtrState
 import hu.bme.mit.theta.analysis.unit.UnitPrec
 import hu.bme.mit.theta.common.logging.Logger
 import hu.bme.mit.theta.core.decl.ConstDecl
@@ -48,9 +48,7 @@ import hu.bme.mit.theta.core.utils.indexings.VarIndexingFactory
 import hu.bme.mit.theta.solver.Solver
 import hu.bme.mit.theta.solver.SolverStatus
 import hu.bme.mit.theta.xcfa.*
-import hu.bme.mit.theta.xcfa.analysis.XcfaAction
 import hu.bme.mit.theta.xcfa.analysis.XcfaPrec
-import hu.bme.mit.theta.xcfa.analysis.XcfaState
 import hu.bme.mit.theta.xcfa.model.*
 import hu.bme.mit.theta.xcfa.passes.AssumeFalseRemovalPass
 import hu.bme.mit.theta.xcfa.passes.AtomicReadsOneWritePass
@@ -63,7 +61,7 @@ class XcfaOcChecker(
     xcfa: XCFA, decisionProcedure: OcDecisionProcedureType, private val logger: Logger,
     conflictInput: String?, private val outputConflictClauses: Boolean, nonPermissiveValidation: Boolean,
     private val autoConflictConfig: AutoConflictFinderConfig
-) : SafetyChecker<EmptyProof, Trace<XcfaState<out PtrState<*>>, XcfaAction>, XcfaPrec<UnitPrec>> {
+) : SafetyChecker<EmptyProof, Cex, XcfaPrec<UnitPrec>> {
 
     private val xcfa: XCFA = xcfa.optimizeFurther(
         listOf(AssumeFalseRemovalPass(), MutexToVarPass(), AtomicReadsOneWritePass())
@@ -86,17 +84,15 @@ class XcfaOcChecker(
 
     override fun check(
         prec: XcfaPrec<UnitPrec>?
-    ): SafetyResult<EmptyProof, Trace<XcfaState<out PtrState<*>>, XcfaAction>> = let {
+    ): SafetyResult<EmptyProof, Cex> = let {
         if (xcfa.initProcedures.size > 1)
             exit("multiple entry points")
 
         logger.writeln(Logger.Level.MAINSTEP, "Adding constraints...")
         xcfa.initProcedures.forEach { ThreadProcessor(Thread(procedure = it.first)).process() }
         addCrossThreadRelations()
         if (!addToSolver(ocChecker.solver))
-            return@let SafetyResult.safe<EmptyProof, Trace<XcfaState<out PtrState<*>>, XcfaAction>>(
-                EmptyProof.getInstance()
-            ) // no violations in the model
+            return@let SafetyResult.safe(EmptyProof.getInstance())
 
         // "Manually" add some conflicts
         logger.writeln(Logger.Level.INFO, "Auto conflict time (ms): " + measureTime {
@@ -132,9 +128,9 @@ class XcfaOcChecker(
 
             status?.isSat == true -> {
                 if (ocChecker is XcfaOcCorrectnessValidator)
-                    return SafetyResult.unsafe(EmptyCex.getInstance(), EmptyWitness.getInstance())
+                    return SafetyResult.unsafe(EmptyCex.getInstance(), EmptyProof.getInstance())
                 val trace = XcfaOcTraceExtractor(xcfa, ocChecker, threads, events, violations, pos).trace
-                SafetyResult.unsafe(trace, EmptyProof.getInstance())
+                SafetyResult.unsafe<EmptyProof, Cex>(trace, EmptyProof.getInstance())
             }
 
             else -> SafetyResult.unknown()

diff --git a/...jects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToOcChecker.kt b/...jects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToOcChecker.kt
@@ -15,15 +15,12 @@
  */
 package hu.bme.mit.theta.xcfa.cli.checkers
 
-import hu.bme.mit.theta.analysis.Trace
+import hu.bme.mit.theta.analysis.Cex
 import hu.bme.mit.theta.analysis.algorithm.EmptyProof
 import hu.bme.mit.theta.analysis.algorithm.SafetyChecker
-import hu.bme.mit.theta.analysis.ptr.PtrState
 import hu.bme.mit.theta.common.logging.Logger
 import hu.bme.mit.theta.graphsolver.patterns.constraints.MCM
-import hu.bme.mit.theta.xcfa.analysis.XcfaAction
 import hu.bme.mit.theta.xcfa.analysis.XcfaPrec
-import hu.bme.mit.theta.xcfa.analysis.XcfaState
 import hu.bme.mit.theta.xcfa.analysis.oc.XcfaOcChecker
 import hu.bme.mit.theta.xcfa.cli.params.OcConfig
 import hu.bme.mit.theta.xcfa.cli.params.XcfaConfig
@@ -34,7 +31,7 @@ fun getOcChecker(
   mcm: MCM,
   config: XcfaConfig<*, *>,
   logger: Logger,
-): SafetyChecker<EmptyProof, Trace<XcfaState<out PtrState<*>>, XcfaAction>, XcfaPrec<*>> {
+): SafetyChecker<EmptyProof, Cex, XcfaPrec<*>> {
   val ocConfig = config.backendConfig.specConfig as OcConfig
   val ocChecker =
     XcfaOcChecker(