From af10f8e02e5b73ccdb7b43eb01fdb7e5d3938ada Mon Sep 17 00:00:00 2001 From: DoriCz Date: Wed, 20 Nov 2024 17:54:58 +0100 Subject: [PATCH] Clean up timed XSTS configuration --- ...ilder.java => TimedXstsConfigBuilder.java} | 211 ++++++------------ .../analysis/config/XstsConfigBuilder.java | 36 +-- .../TimedXstsCFSplitCombinedAlgTest.java | 11 +- .../theta/xsts/analysis/TimedXstsTest.java | 2 +- .../hu/bme/mit/theta/xsts/cli/XstsCli.java | 40 ++-- 5 files changed, 115 insertions(+), 185 deletions(-) rename subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/config/{combined/XstsCombinedConfigBuilder.java => TimedXstsConfigBuilder.java} (68%) diff --git a/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/config/combined/XstsCombinedConfigBuilder.java b/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/config/TimedXstsConfigBuilder.java similarity index 68% rename from subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/config/combined/XstsCombinedConfigBuilder.java rename to subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/config/TimedXstsConfigBuilder.java index ab8fe33ccb..bb5237d3c5 100644 --- a/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/config/combined/XstsCombinedConfigBuilder.java +++ b/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/config/TimedXstsConfigBuilder.java @@ -1,4 +1,4 @@ -package hu.bme.mit.theta.xsts.analysis.config.combined; +package hu.bme.mit.theta.xsts.analysis.config; import hu.bme.mit.theta.analysis.*; import hu.bme.mit.theta.analysis.algorithm.SafetyChecker; @@ -20,8 +20,6 @@ import hu.bme.mit.theta.analysis.utils.ValuationExtractor; import hu.bme.mit.theta.analysis.zone.*; import hu.bme.mit.theta.common.Tuple4; -import hu.bme.mit.theta.common.logging.Logger; -import hu.bme.mit.theta.common.logging.NullLogger; import hu.bme.mit.theta.core.decl.VarDecl; import hu.bme.mit.theta.core.model.Valuation; import hu.bme.mit.theta.core.type.Expr; @@ -29,15 +27,13 @@ import hu.bme.mit.theta.core.type.clocktype.ClockType; import hu.bme.mit.theta.core.utils.Lens; import hu.bme.mit.theta.solver.Solver; -import hu.bme.mit.theta.solver.SolverFactory; import hu.bme.mit.theta.xsts.XSTS; import hu.bme.mit.theta.xsts.analysis.*; +import hu.bme.mit.theta.xsts.analysis.timed.XstsCombinedExprTraceChecker; +import hu.bme.mit.theta.xsts.analysis.timed.XstsCombinedPrecRefiner; import hu.bme.mit.theta.xsts.analysis.timed.*; -import hu.bme.mit.theta.xsts.analysis.config.XstsConfig; -import hu.bme.mit.theta.xsts.analysis.config.XstsConfigBuilder; import java.util.Collection; -import java.util.Set; import java.util.function.Function; import java.util.function.Predicate; @@ -46,124 +42,59 @@ import static hu.bme.mit.theta.core.utils.TypeUtils.cast; @SuppressWarnings({"rawtypes", "unchecked"}) -public final class XstsCombinedConfigBuilder { - - public enum Search { - BFS(SearchStrategy.BFS), - - DFS(SearchStrategy.DFS); - - public final SearchStrategy strategy; - - private Search(final SearchStrategy strategy) { - this.strategy = strategy; - } - } +public final class TimedXstsConfigBuilder { public enum ZoneRefinement { BW_ITP, FW_ITP } - - public enum ClockStrategy { - NONE(XstsClockReplacers.None(), false, false), + public enum ControlFlowSplitting { - INT(XstsClockReplacers.Int(), false, false), + OFF(false, false), - RAT(XstsClockReplacers.Rat(), false, false), - - CF_SPLIT_ALL(XstsClockReplacers.None(), true, false), + ALL_ACTIONS(true, false), - CF_SPLIT_FILTERCF(XstsClockReplacers.None(), true, true); + FEASIBLE_ACTIONS_ONLY(true, true); - public final XstsClockReplacers.XstsClockReplacer clockReplacer; public final boolean controlFlowSplitting; - public final boolean filterInfeasibleCF; + public final boolean feasibleActionsOnly; - private ClockStrategy(final XstsClockReplacers.XstsClockReplacer clockReplacer, final boolean controlFlowSplitting, final boolean filterInfeasibleCF) { - this.clockReplacer = clockReplacer; + ControlFlowSplitting(final boolean controlFlowSplitting, final boolean feasibleActionsOnly) { this.controlFlowSplitting = controlFlowSplitting; - this.filterInfeasibleCF = filterInfeasibleCF; + this.feasibleActionsOnly = feasibleActionsOnly; } } - private Logger logger = NullLogger.getInstance(); - private final SolverFactory solverFactory; - private final XstsConfigBuilder.Domain domain; - private final XstsConfigBuilder.Refinement refinement; - private Search search = Search.BFS; - private XstsConfigBuilder.PredSplit predSplit = XstsConfigBuilder.PredSplit.WHOLE; - private int maxEnum = 0; - private XstsConfigBuilder.InitPrec initPrec = XstsConfigBuilder.InitPrec.EMPTY; - private PruneStrategy pruneStrategy = PruneStrategy.LAZY; - private XstsConfigBuilder.OptimizeStmts optimizeStmts = XstsConfigBuilder.OptimizeStmts.ON; - private XstsConfigBuilder.AutoExpl autoExpl = XstsConfigBuilder.AutoExpl.NEWOPERANDS; + private final XstsConfigBuilder xstsConfig; + private final SearchStrategy searchStrategy; private ZoneRefinement zoneRefinement = ZoneRefinement.BW_ITP; private TimedXstsActionProjections timedXstsActionProjections; - private ClockStrategy clockStrategy = ClockStrategy.NONE; - - public XstsCombinedConfigBuilder(final XstsConfigBuilder.Domain domain, final XstsConfigBuilder.Refinement refinement, final SolverFactory solverFactory) { - this.domain = domain; - this.refinement = refinement; - this.solverFactory = solverFactory; - } - - public XstsCombinedConfigBuilder logger(final Logger logger) { - this.logger = logger; - return this; - } - - public XstsCombinedConfigBuilder search(final Search search) { - this.search = search; - return this; - } - - public XstsCombinedConfigBuilder predSplit(final XstsConfigBuilder.PredSplit predSplit) { - this.predSplit = predSplit; - return this; - } - - public XstsCombinedConfigBuilder maxEnum(final int maxEnum) { - this.maxEnum = maxEnum; - return this; - } - - public XstsCombinedConfigBuilder initPrec(final XstsConfigBuilder.InitPrec initPrec) { - this.initPrec = initPrec; - return this; - } + private ControlFlowSplitting controlFlowSplitting = ControlFlowSplitting.OFF; - public XstsCombinedConfigBuilder pruneStrategy(final PruneStrategy pruneStrategy) { - this.pruneStrategy = pruneStrategy; - return this; - } - - public XstsCombinedConfigBuilder optimizeStmts(final XstsConfigBuilder.OptimizeStmts optimizeStmts) { - this.optimizeStmts = optimizeStmts; - return this; - } - - public XstsCombinedConfigBuilder autoExpl(final XstsConfigBuilder.AutoExpl autoExpl) { - this.autoExpl = autoExpl; - return this; + public TimedXstsConfigBuilder(final XstsConfigBuilder xstsConfig) { + this.xstsConfig = xstsConfig; + this.searchStrategy = switch (xstsConfig.search) { + case BFS -> SearchStrategy.BFS; + case DFS -> SearchStrategy.DFS; + }; } - public XstsCombinedConfigBuilder zoneRefinement(final ZoneRefinement zoneRefinement) { + public TimedXstsConfigBuilder zoneRefinement(final ZoneRefinement zoneRefinement) { this.zoneRefinement = zoneRefinement; return this; } - public XstsCombinedConfigBuilder clockStrategy(final ClockStrategy clockStrategy) { - this.clockStrategy = clockStrategy; + public TimedXstsConfigBuilder controlFlowSplitting(final ControlFlowSplitting controlFlowSplitting) { + this.controlFlowSplitting = controlFlowSplitting; return this; } public XstsConfig build(XSTS xsts) { - final Solver abstractionSolver = solverFactory.createSolver(); + final Solver abstractionSolver = xstsConfig.solverFactory.createSolver(); timedXstsActionProjections = TimedXstsActionProjections.create(); - xsts = clockStrategy.clockReplacer.apply(xsts); + xsts = xstsConfig.clockReplacer.clockReplacer.apply(xsts); final Expr initFormula = xsts.getInitFormula(); final Expr negProp = Not(xsts.getProp()); @@ -181,13 +112,13 @@ public XstsCombinedConfigBuilder clockStrategy(final ClockStrategy clockStrategy final XstsCombinedPrecRefiner precRefiner = createPrecRefiner(xsts); final Refiner refiner; - if (refinement == XstsConfigBuilder.Refinement.MULTI_SEQ) { - refiner = MultiExprTraceRefiner.create(traceChecker, precRefiner, pruneStrategy, logger); + if (xstsConfig.refinement == XstsConfigBuilder.Refinement.MULTI_SEQ) { + refiner = MultiExprTraceRefiner.create(traceChecker, precRefiner, xstsConfig.pruneStrategy, xstsConfig.logger); } else { - refiner = SingleExprTraceRefiner.create(traceChecker, precRefiner, pruneStrategy, logger); + refiner = SingleExprTraceRefiner.create(traceChecker, precRefiner, xstsConfig.pruneStrategy, xstsConfig.logger); } - if (domain == XstsConfigBuilder.Domain.EXPL) { + if (xstsConfig.domain == XstsConfigBuilder.Domain.EXPL) { final LazyStrategy lazyDataStrategy = new BasicLazyStrategy<>( XstsLazyLensUtils.createConcrDataLens(), @@ -204,7 +135,7 @@ public XstsCombinedConfigBuilder clockStrategy(final ClockStrategy clockStrategy final Prod2LazyStrategy lazyStrategy = new Prod2LazyStrategy<>(lazyToConcrProd2Lens, lazyDataStrategy, lazyClockStrategy, projection); final TimedXstsProd2Analysis splitProd2Analysis = TimedXstsProd2Analysis.create( - ExplStmtAnalysis.create(abstractionSolver, initFormula, maxEnum), + ExplStmtAnalysis.create(abstractionSolver, initFormula, xstsConfig.maxEnum), ZoneStmtAnalysis.getInstance(), timedXstsActionProjections ); @@ -224,7 +155,7 @@ public XstsCombinedConfigBuilder clockStrategy(final ClockStrategy clockStrategy final Predicate target = new XstsStatePredicate(prod2Target); final XstsStmtOptimizer> stmtOptimizer; - if (optimizeStmts == XstsConfigBuilder.OptimizeStmts.ON) { + if (xstsConfig.optimizeStmts == XstsConfigBuilder.OptimizeStmts.ON) { stmtOptimizer = XstsStmtOptimizer.create(Prod2StmtOptimizer.create( ExplStmtOptimizer.getInstance(), @@ -235,24 +166,24 @@ public XstsCombinedConfigBuilder clockStrategy(final ClockStrategy clockStrategy } final Abstractor abstractor; - if (clockStrategy.controlFlowSplitting) { - final Solver cfSplitSolver = solverFactory.createSolver(); + if (controlFlowSplitting.controlFlowSplitting) { + final Solver cfSplitSolver = xstsConfig.solverFactory.createSolver(); final ValuationExtractor> valExtractor = createDataValExtractor(ExplStateValuationExtractor.getInstance()); final ControlFlowSplitXstsLts> lts = ControlFlowSplitXstsLts.create(xsts, cfSplitSolver, valExtractor); - abstractor = new ControlFlowSplitLazyAbstractor(lts, search.strategy, lazyStrategy, lazyAnalysis, target, clockStrategy.filterInfeasibleCF); + abstractor = new XstsLazyAbstractor(lts, searchStrategy, lazyStrategy, lazyAnalysis, target, controlFlowSplitting.feasibleActionsOnly); } else { final LTS>, XstsAction> lts = XstsLts.create(xsts, stmtOptimizer); - abstractor = new LazyAbstractor(lts, search.strategy, lazyStrategy, lazyAnalysis, target); + abstractor = new LazyAbstractor(lts, searchStrategy, lazyStrategy, lazyAnalysis, target); } final SafetyChecker>, XstsAction, Prod2Prec> - checker = CegarChecker.create(abstractor, refiner, logger); - final Prod2Prec prec = Prod2Prec.of(initPrec.builder.createExpl(xsts), zonePrec); + checker = CegarChecker.create(abstractor, refiner, xstsConfig.logger); + final Prod2Prec prec = Prod2Prec.of(xstsConfig.initPrec.builder.createExpl(xsts), zonePrec); return XstsConfig.create(checker, prec); - } else if (domain == XstsConfigBuilder.Domain.PRED_BOOL || domain == XstsConfigBuilder.Domain.PRED_CART || domain == XstsConfigBuilder.Domain.PRED_SPLIT) { + } else if (xstsConfig.domain == XstsConfigBuilder.Domain.PRED_BOOL || xstsConfig.domain == XstsConfigBuilder.Domain.PRED_CART || xstsConfig.domain == XstsConfigBuilder.Domain.PRED_SPLIT) { final LazyStrategy lazyDataStrategy = new BasicLazyStrategy<>( XstsLazyLensUtils.createConcrDataLens(), @@ -268,11 +199,11 @@ public XstsCombinedConfigBuilder clockStrategy(final ClockStrategy clockStrategy final Prod2LazyStrategy lazyStrategy = new Prod2LazyStrategy<>(lazyToConcrProd2Lens, lazyDataStrategy, lazyClockStrategy, projection); - PredAbstractors.PredAbstractor predAbstractor = switch (domain) { + PredAbstractors.PredAbstractor predAbstractor = switch (xstsConfig.domain) { case PRED_BOOL -> PredAbstractors.booleanAbstractor(abstractionSolver); case PRED_SPLIT -> PredAbstractors.booleanSplitAbstractor(abstractionSolver); case PRED_CART -> PredAbstractors.cartesianAbstractor(abstractionSolver); - default -> throw new UnsupportedOperationException(domain + " domain is not supported."); + default -> throw new UnsupportedOperationException(xstsConfig.domain + " domain is not supported."); }; final TimedXstsProd2Analysis splitProd2Analysis = TimedXstsProd2Analysis.create( @@ -296,7 +227,7 @@ public XstsCombinedConfigBuilder clockStrategy(final ClockStrategy clockStrategy final Predicate>> target = new XstsStatePredicate<>(prod2Target); final XstsStmtOptimizer> stmtOptimizer; - if (optimizeStmts == XstsConfigBuilder.OptimizeStmts.ON) { + if (xstsConfig.optimizeStmts == XstsConfigBuilder.OptimizeStmts.ON) { stmtOptimizer = XstsStmtOptimizer.create(Prod2StmtOptimizer.create( PredStmtOptimizer.getInstance(), DefaultStmtOptimizer.create())); @@ -305,24 +236,24 @@ public XstsCombinedConfigBuilder clockStrategy(final ClockStrategy clockStrategy } final Abstractor abstractor; - if (clockStrategy.controlFlowSplitting) { - final Solver cfSplitSolver = solverFactory.createSolver(); + if (controlFlowSplitting != ControlFlowSplitting.OFF) { + final Solver cfSplitSolver = xstsConfig.solverFactory.createSolver(); final ValuationExtractor> valExtractor = createDataValExtractor(PredStateValuationExtractor.getInstance()); final ControlFlowSplitXstsLts> lts = ControlFlowSplitXstsLts.create(xsts, cfSplitSolver, valExtractor); - abstractor = new ControlFlowSplitLazyAbstractor(lts, search.strategy, lazyStrategy, lazyAnalysis, target, clockStrategy.filterInfeasibleCF); + abstractor = new XstsLazyAbstractor(lts, searchStrategy, lazyStrategy, lazyAnalysis, target, controlFlowSplitting.feasibleActionsOnly); } else { final LTS>, XstsAction> lts = XstsLts.create(xsts, stmtOptimizer); - abstractor = new LazyAbstractor<>(lts, search.strategy, lazyStrategy, lazyAnalysis, target); + abstractor = new LazyAbstractor<>(lts, searchStrategy, lazyStrategy, lazyAnalysis, target); } final SafetyChecker>, XstsAction, Prod2Prec> - checker = CegarChecker.create(abstractor, refiner, logger); - final Prod2Prec prec = Prod2Prec.of(initPrec.builder.createPred(xsts), zonePrec); + checker = CegarChecker.create(abstractor, refiner, xstsConfig.logger); + final Prod2Prec prec = Prod2Prec.of(xstsConfig.initPrec.builder.createPred(xsts), zonePrec); return XstsConfig.create(checker, prec); - } else if (domain == XstsConfigBuilder.Domain.EXPL_PRED_BOOL || domain == XstsConfigBuilder.Domain.EXPL_PRED_CART || domain == XstsConfigBuilder.Domain.EXPL_PRED_COMBINED || domain == XstsConfigBuilder.Domain.EXPL_PRED_SPLIT) { + } else if (xstsConfig.domain == XstsConfigBuilder.Domain.EXPL_PRED_BOOL || xstsConfig.domain == XstsConfigBuilder.Domain.EXPL_PRED_CART || xstsConfig.domain == XstsConfigBuilder.Domain.EXPL_PRED_COMBINED || xstsConfig.domain == XstsConfigBuilder.Domain.EXPL_PRED_SPLIT) { final LazyStrategy lazyDataStrategy = new BasicLazyStrategy<>( XstsLazyLensUtils.createConcrDataLens(), @@ -341,23 +272,23 @@ public XstsCombinedConfigBuilder clockStrategy(final ClockStrategy clockStrategy final Analysis, StmtAction, Prod2Prec> dataAnalysis; - if (domain == XstsConfigBuilder.Domain.EXPL_PRED_BOOL || domain == XstsConfigBuilder.Domain.EXPL_PRED_CART || domain == XstsConfigBuilder.Domain.EXPL_PRED_SPLIT) { - final PredAbstractors.PredAbstractor predAbstractor = switch (domain) { + if (xstsConfig.domain == XstsConfigBuilder.Domain.EXPL_PRED_BOOL || xstsConfig.domain == XstsConfigBuilder.Domain.EXPL_PRED_CART || xstsConfig.domain == XstsConfigBuilder.Domain.EXPL_PRED_SPLIT) { + final PredAbstractors.PredAbstractor predAbstractor = switch (xstsConfig.domain) { case EXPL_PRED_BOOL -> PredAbstractors.booleanAbstractor(abstractionSolver); case EXPL_PRED_SPLIT -> PredAbstractors.booleanSplitAbstractor(abstractionSolver); case EXPL_PRED_CART -> PredAbstractors.cartesianAbstractor(abstractionSolver); - default -> throw new UnsupportedOperationException(domain + " domain is not supported."); + default -> throw new UnsupportedOperationException(xstsConfig.domain + " domain is not supported."); }; dataAnalysis = Prod2Analysis.create( - ExplStmtAnalysis.create(abstractionSolver, xsts.getInitFormula(), maxEnum), - PredAnalysis.create(abstractionSolver, predAbstractor, xsts.getInitFormula()), + ExplStmtAnalysis.create(abstractionSolver, initFormula, xstsConfig.maxEnum), + PredAnalysis.create(abstractionSolver, predAbstractor, initFormula), Prod2ExplPredPreStrengtheningOperator.create(), Prod2ExplPredStrengtheningOperator.create(abstractionSolver)); } else { final Prod2ExplPredAbstractors.Prod2ExplPredAbstractor prodAbstractor = Prod2ExplPredAbstractors.booleanAbstractor(abstractionSolver); dataAnalysis = Prod2ExplPredAnalysis.create( - ExplAnalysis.create(abstractionSolver, xsts.getInitFormula()), - PredAnalysis.create(abstractionSolver, PredAbstractors.booleanAbstractor(abstractionSolver), xsts.getInitFormula()), + ExplAnalysis.create(abstractionSolver, initFormula), + PredAnalysis.create(abstractionSolver, PredAbstractors.booleanAbstractor(abstractionSolver), initFormula), Prod2ExplPredStrengtheningOperator.create(abstractionSolver), prodAbstractor); } @@ -381,7 +312,7 @@ public XstsCombinedConfigBuilder clockStrategy(final ClockStrategy clockStrategy final Predicate, ZoneState>>> target = new XstsStatePredicate<>(prod2Target); final XstsStmtOptimizer, ZoneState>> stmtOptimizer; - if (optimizeStmts == XstsConfigBuilder.OptimizeStmts.ON) { + if (xstsConfig.optimizeStmts == XstsConfigBuilder.OptimizeStmts.ON) { stmtOptimizer = XstsStmtOptimizer.create(Prod2StmtOptimizer.create( Prod2ExplPredStmtOptimizer.create(ExplStmtOptimizer.getInstance()), DefaultStmtOptimizer.create())); @@ -390,26 +321,26 @@ public XstsCombinedConfigBuilder clockStrategy(final ClockStrategy clockStrategy } final Abstractor abstractor; - if (clockStrategy.controlFlowSplitting) { - final Solver cfSplitSolver = solverFactory.createSolver(); + if (controlFlowSplitting != ControlFlowSplitting.OFF) { + final Solver cfSplitSolver = xstsConfig.solverFactory.createSolver(); final ValuationExtractor, ZoneState>> valExtractor = createDataValExtractor(Prod2ExplPredStateValuationExtractor.create(ExplStateValuationExtractor.getInstance())); final ControlFlowSplitXstsLts, ZoneState>> lts = ControlFlowSplitXstsLts.create(xsts, cfSplitSolver, valExtractor); - abstractor = new ControlFlowSplitLazyAbstractor(lts, search.strategy, lazyStrategy, lazyAnalysis, target, clockStrategy.filterInfeasibleCF); + abstractor = new XstsLazyAbstractor(lts, searchStrategy, lazyStrategy, lazyAnalysis, target, controlFlowSplitting.feasibleActionsOnly); } else { final LTS, ZoneState>>, XstsAction> lts = XstsLts.create(xsts, stmtOptimizer); - abstractor = new LazyAbstractor<>(lts, search.strategy, lazyStrategy, lazyAnalysis, target); + abstractor = new LazyAbstractor<>(lts, searchStrategy, lazyStrategy, lazyAnalysis, target); } final SafetyChecker, ZoneState>>, XstsAction, Prod2Prec, ZonePrec>> - checker = CegarChecker.create(abstractor, refiner, logger); - final Prod2Prec, ZonePrec> prec = Prod2Prec.of(initPrec.builder.createProd2ExplPred(xsts), zonePrec); + checker = CegarChecker.create(abstractor, refiner, xstsConfig.logger); + final Prod2Prec, ZonePrec> prec = Prod2Prec.of(xstsConfig.initPrec.builder.createProd2ExplPred(xsts), zonePrec); return XstsConfig.create(checker, prec); } else { - throw new UnsupportedOperationException(domain + " domain is not supported."); + throw new UnsupportedOperationException(xstsConfig.domain + " domain is not supported."); } } @@ -452,22 +383,22 @@ public Valuation extractValuationForVars(Prod2State state, Col private XstsCombinedExprTraceChecker createTraceChecker(final Expr initFormula, final Expr negProp, final Lens lens) { final XstsCombinedExprTraceChecker traceChecker = new XstsCombinedExprTraceChecker( - switch (refinement) { - case FW_BIN_ITP -> ExprTraceFwBinItpChecker.create(initFormula, negProp, solverFactory.createItpSolver()); - case BW_BIN_ITP -> ExprTraceBwBinItpChecker.create(initFormula, negProp, solverFactory.createItpSolver()); - case SEQ_ITP, MULTI_SEQ -> ExprTraceSeqItpChecker.create(initFormula, negProp, solverFactory.createItpSolver()); - case UNSAT_CORE -> ExprTraceUnsatCoreChecker.create(initFormula, negProp, solverFactory.createUCSolver()); + switch (xstsConfig.refinement) { + case FW_BIN_ITP -> ExprTraceFwBinItpChecker.create(initFormula, negProp, xstsConfig.solverFactory.createItpSolver()); + case BW_BIN_ITP -> ExprTraceBwBinItpChecker.create(initFormula, negProp, xstsConfig.solverFactory.createItpSolver()); + case SEQ_ITP, MULTI_SEQ -> ExprTraceSeqItpChecker.create(initFormula, negProp, xstsConfig.solverFactory.createItpSolver()); + case UNSAT_CORE -> ExprTraceUnsatCoreChecker.create(initFormula, negProp, xstsConfig.solverFactory.createUCSolver()); }, lens, timedXstsActionProjections); return traceChecker; } private XstsCombinedPrecRefiner createPrecRefiner(final XSTS xsts) { final XstsCombinedPrecRefiner precRefiner = new XstsCombinedPrecRefiner( - switch (domain) { + switch (xstsConfig.domain) { case EXPL -> new ItpRefToExplPrec(); - case PRED_BOOL, PRED_CART, PRED_SPLIT -> new ItpRefToPredPrec(predSplit.splitter); + case PRED_BOOL, PRED_CART, PRED_SPLIT -> new ItpRefToPredPrec(xstsConfig.predSplit.splitter); case EXPL_PRED_BOOL, EXPL_PRED_CART, EXPL_PRED_COMBINED, EXPL_PRED_SPLIT -> - AutomaticItpRefToProd2ExplPredPrec.create(autoExpl.builder.create(xsts), predSplit.splitter); + AutomaticItpRefToProd2ExplPredPrec.create(xstsConfig.autoExpl.builder.create(xsts), xstsConfig.predSplit.splitter); }); return precRefiner; } diff --git a/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/config/XstsConfigBuilder.java b/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/config/XstsConfigBuilder.java index f225115ff6..dfa9d14819 100644 --- a/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/config/XstsConfigBuilder.java +++ b/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/config/XstsConfigBuilder.java @@ -162,8 +162,8 @@ public enum OptimizeStmts { ON, OFF } - public enum ClockImpl { - CLOCK(XstsClockReplacers.None()), + public enum ClockReplacer { + NONE(XstsClockReplacers.None()), INT(XstsClockReplacers.Int()), @@ -171,21 +171,21 @@ public enum ClockImpl { public final XstsClockReplacers.XstsClockReplacer clockReplacer; - private ClockImpl(final XstsClockReplacers.XstsClockReplacer clockReplacer) { this.clockReplacer = clockReplacer; } + private ClockReplacer(final XstsClockReplacers.XstsClockReplacer clockReplacer) { this.clockReplacer = clockReplacer; } } - private Logger logger = NullLogger.getInstance(); - private final SolverFactory solverFactory; - private final Domain domain; - private final Refinement refinement; - private Search search = Search.BFS; - private PredSplit predSplit = PredSplit.WHOLE; - private int maxEnum = 0; - private InitPrec initPrec = InitPrec.EMPTY; - private PruneStrategy pruneStrategy = PruneStrategy.LAZY; - private OptimizeStmts optimizeStmts = OptimizeStmts.ON; - private AutoExpl autoExpl = AutoExpl.NEWOPERANDS; - private ClockImpl clockImpl = ClockImpl.CLOCK; + Logger logger = NullLogger.getInstance(); + final SolverFactory solverFactory; + final Domain domain; + final Refinement refinement; + Search search = Search.BFS; + PredSplit predSplit = PredSplit.WHOLE; + int maxEnum = 0; + InitPrec initPrec = InitPrec.EMPTY; + PruneStrategy pruneStrategy = PruneStrategy.LAZY; + OptimizeStmts optimizeStmts = OptimizeStmts.ON; + AutoExpl autoExpl = AutoExpl.NEWOPERANDS; + ClockReplacer clockReplacer = ClockReplacer.NONE; public XstsConfigBuilder(final Domain domain, final Refinement refinement, final SolverFactory solverFactory) { this.domain = domain; @@ -233,15 +233,15 @@ public XstsConfigBuilder autoExpl(final AutoExpl autoExpl) { return this; } - public XstsConfigBuilder clockImpl(final ClockImpl clockImpl) { - this.clockImpl = clockImpl; + public XstsConfigBuilder clockReplacer(final ClockReplacer clockReplacer) { + this.clockReplacer = clockReplacer; return this; } public XstsConfig build(XSTS xsts) { final Solver abstractionSolver = solverFactory.createSolver(); - xsts = clockImpl.clockReplacer.apply(xsts); + xsts = clockReplacer.clockReplacer.apply(xsts); final Expr negProp = Not(xsts.getProp()); diff --git a/subprojects/xsts/xsts-analysis/src/test/java/hu/bme/mit/theta/xsts/analysis/TimedXstsCFSplitCombinedAlgTest.java b/subprojects/xsts/xsts-analysis/src/test/java/hu/bme/mit/theta/xsts/analysis/TimedXstsCFSplitCombinedAlgTest.java index f3aea5d6cd..76b5e208b7 100644 --- a/subprojects/xsts/xsts-analysis/src/test/java/hu/bme/mit/theta/xsts/analysis/TimedXstsCFSplitCombinedAlgTest.java +++ b/subprojects/xsts/xsts-analysis/src/test/java/hu/bme/mit/theta/xsts/analysis/TimedXstsCFSplitCombinedAlgTest.java @@ -9,7 +9,7 @@ import hu.bme.mit.theta.xsts.XSTS; import hu.bme.mit.theta.xsts.analysis.config.XstsConfig; import hu.bme.mit.theta.xsts.analysis.config.XstsConfigBuilder; -import hu.bme.mit.theta.xsts.analysis.config.combined.XstsCombinedConfigBuilder; +import hu.bme.mit.theta.xsts.analysis.config.TimedXstsConfigBuilder; import hu.bme.mit.theta.xsts.dsl.XstsDslManager; import org.junit.Test; import org.junit.runner.RunWith; @@ -106,15 +106,16 @@ public void test() throws IOException { try (InputStream inputStream = new SequenceInputStream(new FileInputStream(filePath), new FileInputStream(propPath))) { xsts = XstsDslManager.createXsts(inputStream); } - - final XstsConfig configuration = new XstsCombinedConfigBuilder(domain, XstsConfigBuilder.Refinement.SEQ_ITP, Z3SolverFactory.getInstance()) + final XstsConfigBuilder xstsConfigBuilder = new XstsConfigBuilder(domain, XstsConfigBuilder.Refinement.SEQ_ITP, Z3SolverFactory.getInstance()) .initPrec(XstsConfigBuilder.InitPrec.CTRL) .optimizeStmts(XstsConfigBuilder.OptimizeStmts.ON) .predSplit(XstsConfigBuilder.PredSplit.CONJUNCTS) .maxEnum(250) .pruneStrategy(PruneStrategy.FULL) - .clockStrategy(XstsCombinedConfigBuilder.ClockStrategy.CF_SPLIT_ALL) - .logger(logger) + .clockReplacer(XstsConfigBuilder.ClockReplacer.NONE) + .logger(logger); + final XstsConfig configuration = new TimedXstsConfigBuilder(xstsConfigBuilder) + .controlFlowSplitting(TimedXstsConfigBuilder.ControlFlowSplitting.FEASIBLE_ACTIONS_ONLY) .build(xsts); final SafetyResult status = configuration.check(); if (safe) { diff --git a/subprojects/xsts/xsts-analysis/src/test/java/hu/bme/mit/theta/xsts/analysis/TimedXstsTest.java b/subprojects/xsts/xsts-analysis/src/test/java/hu/bme/mit/theta/xsts/analysis/TimedXstsTest.java index 9d72d4806b..a1f79c698d 100644 --- a/subprojects/xsts/xsts-analysis/src/test/java/hu/bme/mit/theta/xsts/analysis/TimedXstsTest.java +++ b/subprojects/xsts/xsts-analysis/src/test/java/hu/bme/mit/theta/xsts/analysis/TimedXstsTest.java @@ -101,7 +101,7 @@ public void test() throws IOException { .predSplit(XstsConfigBuilder.PredSplit.CONJUNCTS) .maxEnum(250) .autoExpl(XstsConfigBuilder.AutoExpl.NEWOPERANDS) - .clockImpl(XstsConfigBuilder.ClockImpl.RAT) + .clockReplacer(XstsConfigBuilder.ClockReplacer.RAT) .pruneStrategy(PruneStrategy.FULL) .logger(logger) .build(xsts); diff --git a/subprojects/xsts/xsts-cli/src/main/java/hu/bme/mit/theta/xsts/cli/XstsCli.java b/subprojects/xsts/xsts-cli/src/main/java/hu/bme/mit/theta/xsts/cli/XstsCli.java index 07ac40ba92..7204388100 100644 --- a/subprojects/xsts/xsts-cli/src/main/java/hu/bme/mit/theta/xsts/cli/XstsCli.java +++ b/subprojects/xsts/xsts-cli/src/main/java/hu/bme/mit/theta/xsts/cli/XstsCli.java @@ -18,6 +18,7 @@ import hu.bme.mit.theta.common.table.TableWriter; import hu.bme.mit.theta.common.visualization.Graph; import hu.bme.mit.theta.common.visualization.writer.GraphvizWriter; +import hu.bme.mit.theta.core.type.clocktype.ClockType; import hu.bme.mit.theta.solver.z3.Z3SolverFactory; import hu.bme.mit.theta.xsts.XSTS; import hu.bme.mit.theta.xsts.analysis.XstsAction; @@ -27,7 +28,9 @@ import hu.bme.mit.theta.xsts.analysis.config.XstsConfig; import hu.bme.mit.theta.xsts.analysis.config.XstsConfigBuilder; import hu.bme.mit.theta.xsts.analysis.config.XstsConfigBuilder.*; -import hu.bme.mit.theta.xsts.analysis.config.combined.XstsCombinedConfigBuilder; +import hu.bme.mit.theta.xsts.analysis.config.TimedXstsConfigBuilder; +import hu.bme.mit.theta.xsts.analysis.config.TimedXstsConfigBuilder.ControlFlowSplitting; +import hu.bme.mit.theta.xsts.analysis.config.TimedXstsConfigBuilder.ZoneRefinement; import hu.bme.mit.theta.xsts.dsl.XstsDslManager; import hu.bme.mit.theta.xsts.pnml.PnmlParser; import hu.bme.mit.theta.xsts.pnml.PnmlToXSTS; @@ -104,19 +107,13 @@ public class XstsCli { String dotfile = null; @Parameter(names = {"--clockreplacement"}, description = "Clock replacement type") - ClockImpl clockImpl = ClockImpl.RAT; + ClockReplacer clockReplacer = ClockReplacer.RAT; - @Parameter(names = {"--combined"}, description = "Run combined abstraction") - boolean combinedAlgorithm = false; - - @Parameter(names = {"--combinedsearch"}, description = "Search strategy for combined abstraction") - XstsCombinedConfigBuilder.Search combinedSearch = XstsCombinedConfigBuilder.Search.BFS; - - @Parameter(names = {"--clockstrategy"}, description = "Clock strategy for combined abstraction") - XstsCombinedConfigBuilder.ClockStrategy clockStrategy = XstsCombinedConfigBuilder.ClockStrategy.NONE; + @Parameter(names = {"--controlflowsplitting"}, description = "Clock replacement type") + ControlFlowSplitting controlFlowSplitting = ControlFlowSplitting.OFF; @Parameter(names = {"--zonerefinement"}, description = "Refinement strategy for zone states") - XstsCombinedConfigBuilder.ZoneRefinement zoneRefinement = XstsCombinedConfigBuilder.ZoneRefinement.BW_ITP; + ZoneRefinement zoneRefinement = ZoneRefinement.BW_ITP; private Logger logger; @@ -216,17 +213,18 @@ private XSTS loadModel() throws Exception { private XstsConfig buildConfiguration(final XSTS xsts) throws Exception { try { - if (combinedAlgorithm) { - return new XstsCombinedConfigBuilder(domain, refinement, Z3SolverFactory.getInstance()) - .maxEnum(maxEnum).autoExpl(autoExpl).initPrec(initPrec).pruneStrategy(pruneStrategy) - .search(combinedSearch).predSplit(predSplit).optimizeStmts(optimizeStmts) - .clockStrategy(clockStrategy).zoneRefinement(zoneRefinement) - .logger(logger).build(xsts); + XstsConfigBuilder xstsConfigBuilder = new XstsConfigBuilder(domain, refinement, Z3SolverFactory.getInstance()) + .maxEnum(maxEnum).autoExpl(autoExpl).initPrec(initPrec).pruneStrategy(pruneStrategy) + .search(search).predSplit(predSplit).optimizeStmts(optimizeStmts).clockReplacer(clockReplacer) + .logger(logger); + final boolean timedXsts = clockReplacer == ClockReplacer.NONE && + xsts.getVars().stream().anyMatch(varDecl -> varDecl.getType() instanceof ClockType); + if (timedXsts) { + return new TimedXstsConfigBuilder(xstsConfigBuilder) + .zoneRefinement(zoneRefinement).controlFlowSplitting(controlFlowSplitting) + .build(xsts); } else { - return new XstsConfigBuilder(domain, refinement, Z3SolverFactory.getInstance()) - .maxEnum(maxEnum).autoExpl(autoExpl).initPrec(initPrec).pruneStrategy(pruneStrategy) - .search(search).predSplit(predSplit).optimizeStmts(optimizeStmts).clockImpl(clockImpl) - .logger(logger).build(xsts); + return xstsConfigBuilder.build(xsts); } } catch (final Exception ex) { throw new Exception("Could not create configuration: " + ex.getMessage(), ex);