Skip to content

Commit

Permalink
last modifications in progress check
Browse files Browse the repository at this point in the history
  • Loading branch information
@AdamZsofi
AdamZsofi committed Oct 27, 2023
1 parent d6778fd commit 275ee53
Show file tree
Hide file tree
Showing 3 changed files with 33 additions and 45 deletions.
9 changes: 7 additions & 2 deletions ...ects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/runtimemonitor/CexMonitor.kt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -24,8 +24,13 @@ import hu.bme.mit.theta.common.exception.NotSolvableException
import hu.bme.mit.theta.common.logging.Logger
import java.lang.RuntimeException


// TODO implement mitigation
/**
* This monitor checks whether a new counterexample is found during the current iteration of CEGAR.
* In most cases, finding the same counterexample again means that refinement is not progressing.
* Warning: With some configurations (e.g. lazy pruning) it is NOT impossible that analysis will
* progress even if in some iterations a new cex is not found, but seems to be rare.
* However, if you think analysis should NOT be stopped by this monitor, disable it and check results.
*/
class CexMonitor<S : State?, A : Action?> constructor(
private val mitigate: Boolean, private val logger: Logger, private val arg: ARG<S, A>
) : Monitor {
Expand Down
40 changes: 20 additions & 20 deletions subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/ConfigOptions.kt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -157,98 +157,99 @@ enum class Domain(
}

enum class Refinement(
val refiner: (solverFactory: SolverFactory) -> ExprTraceChecker<out Refutation>,
val stopCriterion: StopCriterion<XcfaState<out ExprState>, XcfaAction>
val refiner: (solverFactory: SolverFactory, monitorOption: CexMonitorOptions) -> ExprTraceChecker<out Refutation>,
val stopCriterion: StopCriterion<XcfaState<out ExprState>, XcfaAction>,
) {

FW_BIN_ITP(
refiner = { s ->
refiner = { s, _ ->
ExprTraceFwBinItpChecker.create(BoolExprs.True(), BoolExprs.True(), s.createItpSolver())
},
stopCriterion = StopCriterions.firstCex()
stopCriterion = StopCriterions.firstCex(),
),
BW_BIN_ITP(
refiner = { s ->
refiner = { s, _ ->
ExprTraceBwBinItpChecker.create(BoolExprs.True(), BoolExprs.True(), s.createItpSolver())
},
stopCriterion = StopCriterions.firstCex()
),
SEQ_ITP(
refiner = { s ->
refiner = { s, _ ->
ExprTraceSeqItpChecker.create(BoolExprs.True(), BoolExprs.True(), s.createItpSolver())
},
stopCriterion = StopCriterions.firstCex()
),
MULTI_SEQ(
refiner = { s ->
refiner = { s, m ->
if(m == CexMonitorOptions.CHECK) error("CexMonitor is not implemented for MULTI_SEQ")
ExprTraceSeqItpChecker.create(BoolExprs.True(), BoolExprs.True(), s.createItpSolver())
},
stopCriterion = StopCriterions.fullExploration()
),
UNSAT_CORE(
refiner = { s ->
refiner = { s, _ ->
ExprTraceUnsatCoreChecker.create(BoolExprs.True(), BoolExprs.True(), s.createUCSolver())
},
stopCriterion = StopCriterions.firstCex()
),
UCB(
refiner = { s ->
refiner = { s, _ ->
ExprTraceUCBChecker.create(BoolExprs.True(), BoolExprs.True(), s.createUCSolver())
},
stopCriterion = StopCriterions.firstCex()
),

NWT_SP(
refiner = { s ->
refiner = { s, _ ->
ExprTraceNewtonChecker.create(BoolExprs.True(), BoolExprs.True(), s.createUCSolver())
.withoutIT().withSP().withoutLV()
},
stopCriterion = StopCriterions.firstCex()
),
NWT_WP(
refiner = { s ->
refiner = { s, _ ->
ExprTraceNewtonChecker.create(BoolExprs.True(), BoolExprs.True(), s.createUCSolver())
.withoutIT().withWP().withoutLV()
},
stopCriterion = StopCriterions.firstCex()
),
NWT_SP_LV(
refiner = { s ->
refiner = { s, _ ->
ExprTraceNewtonChecker.create(BoolExprs.True(), BoolExprs.True(), s.createUCSolver())
.withoutIT().withSP().withLV()
},
stopCriterion = StopCriterions.firstCex()
),
NWT_WP_LV(
refiner = { s ->
refiner = { s, _ ->
ExprTraceNewtonChecker.create(BoolExprs.True(), BoolExprs.True(), s.createUCSolver())
.withoutIT().withWP().withLV()
},
stopCriterion = StopCriterions.firstCex()
),
NWT_IT_WP(
refiner = { s ->
refiner = { s, _ ->
ExprTraceNewtonChecker.create(BoolExprs.True(), BoolExprs.True(), s.createUCSolver())
.withIT().withWP().withoutLV()
},
stopCriterion = StopCriterions.firstCex()
),
NWT_IT_SP(
refiner = { s ->
refiner = { s, _ ->
ExprTraceNewtonChecker.create(BoolExprs.True(), BoolExprs.True(), s.createUCSolver())
.withIT().withSP().withoutLV()
},
stopCriterion = StopCriterions.firstCex()
),
NWT_IT_WP_LV(
refiner = { s ->
refiner = { s, _ ->
ExprTraceNewtonChecker.create(BoolExprs.True(), BoolExprs.True(), s.createUCSolver())
.withIT().withWP().withLV()
},
stopCriterion = StopCriterions.firstCex()
),
NWT_IT_SP_LV(
refiner = { s ->
refiner = { s, _ ->
ExprTraceNewtonChecker.create(BoolExprs.True(), BoolExprs.True(), s.createUCSolver())
.withIT().withSP().withLV()
},
Expand Down Expand Up @@ -335,10 +336,9 @@ enum class ConeOfInfluenceMode(
var porLts: LTS<XcfaState<out ExprState>, XcfaAction>? = null
}

// TODO CexMonitor: disable for multi_seq?
// TODO CexMonitor: disable for multi_seq
// TODO add new monitor to xsts cli
enum class CexMonitorOptions {

CHECK,
MITIGATE,
DISABLE
}
29 changes: 6 additions & 23 deletions subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/XcfaCegarConfig.kt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -90,7 +90,9 @@ data class XcfaCegarConfig(
@Parameter(names = ["--prunestrategy"],
description = "Strategy for pruning the ARG after refinement")
var pruneStrategy: PruneStrategy = PruneStrategy.LAZY,
@Parameter(names = ["--cex-monitor"])
@Parameter(names = ["--cex-monitor"],
description = "Warning: With some configurations (e.g. lazy pruning) it is POSSIBLE (but rare) that analysis is stopped, " +
"even though it could still progress. If in doubt, disable this monitor and check results.")
var cexMonitor: CexMonitorOptions = CexMonitorOptions.DISABLE,
@Parameter(names = ["--timeout-ms"],
description = "Timeout for verification (only valid with --strategy SERVER), use 0 for no timeout")
Expand Down Expand Up @@ -135,7 +137,7 @@ data class XcfaCegarConfig(
) as Abstractor<ExprState, ExprAction, Prec>

val ref: ExprTraceChecker<Refutation> =
refinement.refiner(refinementSolverFactory)
refinement.refiner(refinementSolverFactory, cexMonitor)
as ExprTraceChecker<Refutation>
val precRefiner: PrecRefiner<ExprState, ExprAction, Prec, Refutation> =
domain.itpPrecRefiner(exprSplitter.exprSplitter)
Expand All @@ -155,19 +157,6 @@ data class XcfaCegarConfig(
else
SingleExprTraceRefiner.create(ref, precRefiner, pruneStrategy, logger)

/*
// set up stopping analysis if it is stuck on same ARGs and precisions
if (disableCexMonitor) {
ArgCexCheckHandler.instance.setArgCexCheck(false, false, mitigation)
} else {
if(checkArg) {
ArgCexCheckHandler.instance.setArgCexCheck(true, true, mitigation)
} else {
ArgCexCheckHandler.instance.setArgCexCheck(true, false, mitigation)
}
}
*/

val cegarChecker = if (porLevel == POR.AASPOR)
CegarChecker.create(
abstractor,
Expand All @@ -183,14 +172,8 @@ data class XcfaCegarConfig(
}

private fun initializeMonitors(cc: CegarChecker<ExprState, ExprAction, Prec>, logger: Logger) {
if (cexMonitor != CexMonitorOptions.DISABLE) {
val cm = if (cexMonitor == CexMonitorOptions.MITIGATE) {
throw RuntimeException(
"Mitigation is temporarily unusable, use DISABLE or CHECK instead")
// CexMonitor(true, logger, cc.arg)
} else { // CHECK
CexMonitor(false, logger, cc.arg)
}
if (cexMonitor == CexMonitorOptions.CHECK) {
val cm = CexMonitor(false, logger, cc.arg)
MonitorCheckpoint.register(cm, "CegarChecker.unsafeARG")
}
}
Expand Down

0 comments on commit 275ee53

Please sign in to comment.