diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/runtimemonitor/CexMonitor.kt b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/runtimemonitor/CexMonitor.kt index 610d19d97a..3a92ffba17 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/runtimemonitor/CexMonitor.kt +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/runtimemonitor/CexMonitor.kt @@ -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 constructor( private val mitigate: Boolean, private val logger: Logger, private val arg: ARG ) : Monitor { diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/ConfigOptions.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/ConfigOptions.kt index 3f73d66666..5dda459fa4 100644 --- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/ConfigOptions.kt +++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/ConfigOptions.kt @@ -157,98 +157,99 @@ enum class Domain( } enum class Refinement( - val refiner: (solverFactory: SolverFactory) -> ExprTraceChecker, - val stopCriterion: StopCriterion, XcfaAction> + val refiner: (solverFactory: SolverFactory, monitorOption: CexMonitorOptions) -> ExprTraceChecker, + val stopCriterion: StopCriterion, 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() }, @@ -335,10 +336,9 @@ enum class ConeOfInfluenceMode( var porLts: LTS, 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 } diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/XcfaCegarConfig.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/XcfaCegarConfig.kt index 2532911a10..13b080036f 100644 --- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/XcfaCegarConfig.kt +++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/XcfaCegarConfig.kt @@ -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") @@ -135,7 +137,7 @@ data class XcfaCegarConfig( ) as Abstractor val ref: ExprTraceChecker = - refinement.refiner(refinementSolverFactory) + refinement.refiner(refinementSolverFactory, cexMonitor) as ExprTraceChecker val precRefiner: PrecRefiner = domain.itpPrecRefiner(exprSplitter.exprSplitter) @@ -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, @@ -183,14 +172,8 @@ data class XcfaCegarConfig( } private fun initializeMonitors(cc: CegarChecker, 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") } }