From 4e07ec8e66dbd2032d01284db69134ebb9a67698 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Vizi=20B=C3=A9la=20=C3=81kos?= Date: Tue, 21 May 2024 22:01:37 +0200 Subject: [PATCH] separate traces when zone abstraction is used --- .../theta/analysis/zone/ClockPredPrec.java | 9 ++- .../bme/mit/theta/analysis/zone/ZonePrec.java | 13 +++-- .../ClockPred/ClockPredTransFunc.java | 2 +- .../analysis/ClockPred/NoneTraceChecker.java | 26 +++++++++ .../analysis/ClockPred/XtaTraceChecker.java | 2 +- .../config/XtaConfigBuilder_ClockPred.java | 32 +++++------ .../config/XtaConfigBuilder_Zone.java | 56 ++++++++++--------- .../java/hu/bme/mit/theta/xta/cli/XtaCli.java | 12 +--- .../bme/mit/theta/xta/dsl/XtaInitialiser.java | 11 +++- 9 files changed, 100 insertions(+), 63 deletions(-) create mode 100644 subprojects/xta/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/ClockPred/NoneTraceChecker.java diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/zone/ClockPredPrec.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/zone/ClockPredPrec.java index ef78a0ccb1..6e01ae8abf 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/zone/ClockPredPrec.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/zone/ClockPredPrec.java @@ -7,6 +7,7 @@ import hu.bme.mit.theta.core.decl.VarDecl; import hu.bme.mit.theta.core.type.rattype.RatType; +import java.time.Clock; import java.util.*; import java.util.stream.Collectors; @@ -16,6 +17,7 @@ public class ClockPredPrec implements Prec{ private final Map, VarDecl>, Set> map; private final Set> clocks; + private boolean shouldApplyPredicates; private ClockPredPrec(final Map, VarDecl>, Set> map, final Collection> clocks){ checkNotNull(clocks); @@ -23,7 +25,9 @@ private ClockPredPrec(final Map, VarDecl>, Set> clocks) { return ClockPredPrec.emptyPrec(clocks); @@ -135,6 +139,9 @@ public void add(VarDecl x, VarDecl y,Integer b){ map.get(key).add(b); } + public boolean getShouldApplyPredicates(){ + return this.shouldApplyPredicates; + } } diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/zone/ZonePrec.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/zone/ZonePrec.java index b80fc4f949..bb6827418c 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/zone/ZonePrec.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/zone/ZonePrec.java @@ -74,14 +74,19 @@ public Collection> getUsedVars() { // This could be way more elegant @Override public Prec join(Prec other) { + if(this == other)return this; if(other instanceof ZonePrec other1){ - HashSet> newclocks = new HashSet<>(clocks); - - newclocks.addAll(other1.clocks); - return ZonePrec.of(newclocks); + return join(other1); } else{ throw new IllegalArgumentException(); } } + + public ZonePrec join(final ZonePrec other) { + HashSet> newclocks = new HashSet<>(clocks); + newclocks.addAll(other.clocks); + return ZonePrec.of(newclocks); + + } } diff --git a/subprojects/xta/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/ClockPred/ClockPredTransFunc.java b/subprojects/xta/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/ClockPred/ClockPredTransFunc.java index 43bf9ad304..21844bcead 100644 --- a/subprojects/xta/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/ClockPred/ClockPredTransFunc.java +++ b/subprojects/xta/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/ClockPred/ClockPredTransFunc.java @@ -18,7 +18,7 @@ private ClockPredTransFunc(){} public Collection getSuccStates(ZoneState state, XtaAction action, ClockPredPrec prec) { ZoneState succState = XtaClockPredUtils.post(state, action, prec); - if(!succState.isBottom()){ + if(!succState.isBottom() && prec.getShouldApplyPredicates()){ succState.clockPredicate(prec); } return ImmutableList.of(succState); diff --git a/subprojects/xta/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/ClockPred/NoneTraceChecker.java b/subprojects/xta/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/ClockPred/NoneTraceChecker.java new file mode 100644 index 0000000000..636e06c247 --- /dev/null +++ b/subprojects/xta/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/ClockPred/NoneTraceChecker.java @@ -0,0 +1,26 @@ +package hu.bme.mit.theta.xta.analysis.ClockPred; + +import hu.bme.mit.theta.analysis.Trace; +import hu.bme.mit.theta.analysis.expr.refinement.ExprTraceStatus; +import hu.bme.mit.theta.analysis.expr.refinement.ZoneRefutation; +import hu.bme.mit.theta.analysis.zone.DBM; +import hu.bme.mit.theta.analysis.zone.ZonePrec; +import hu.bme.mit.theta.analysis.zone.ZoneState; +import hu.bme.mit.theta.core.type.Expr; +import hu.bme.mit.theta.core.type.booltype.BoolType; +import hu.bme.mit.theta.solver.ItpSolver; +import hu.bme.mit.theta.xta.analysis.XtaAction; + +public class NoneTraceChecker extends XtaTraceChecker{ + private NoneTraceChecker(final Expr init, DBM initDBM, final Expr target, final ItpSolver solver,ZonePrec clocks ) { + super(init, initDBM, target, solver, clocks); + } + + public static NoneTraceChecker create(final Expr init, DBM initDBM, final Expr target, final ItpSolver solver, ZonePrec clocks) { + return new NoneTraceChecker(init, initDBM, target, solver, clocks); + } + @Override + public ExprTraceStatus check(Trace trace) { + return ExprTraceStatus.feasible(null); + } +} diff --git a/subprojects/xta/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/ClockPred/XtaTraceChecker.java b/subprojects/xta/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/ClockPred/XtaTraceChecker.java index 374844260d..c86195929f 100644 --- a/subprojects/xta/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/ClockPred/XtaTraceChecker.java +++ b/subprojects/xta/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/ClockPred/XtaTraceChecker.java @@ -45,7 +45,7 @@ public class XtaTraceChecker { private final DBM initDBM; private final ZonePrec clocks; - private XtaTraceChecker(final Expr init, DBM initDBM, final Expr target, final ItpSolver solver,ZonePrec clocks ) { + protected XtaTraceChecker(final Expr init, DBM initDBM, final Expr target, final ItpSolver solver,ZonePrec clocks ) { this.solver = solver; this.init = init; this.target = target; diff --git a/subprojects/xta/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/config/XtaConfigBuilder_ClockPred.java b/subprojects/xta/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/config/XtaConfigBuilder_ClockPred.java index ce7fb62890..9bc2bd8967 100644 --- a/subprojects/xta/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/config/XtaConfigBuilder_ClockPred.java +++ b/subprojects/xta/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/config/XtaConfigBuilder_ClockPred.java @@ -124,8 +124,12 @@ public abstract Prec private int maxEnum = 0; private InitPrec initPrec = InitPrec.EMPTY; private PruneStrategy pruneStrategy = PruneStrategy.LAZY; + private boolean clockPredAbstraction = false; - + public XtaConfigBuilder_ClockPred setClockPred(boolean clockPredAbstraction) { + this.clockPredAbstraction = clockPredAbstraction; + return this; + } public XtaConfigBuilder_ClockPred(final Domain domain, final Refinement refinement, final SolverFactory solverFactory) { this.domain = domain; this.refinement = refinement; @@ -185,6 +189,10 @@ public XtaConfigBuilder_ClockPred pruneStrategy(final PruneStrategy pruneStrateg this.pruneStrategy = pruneStrategy; return this; } + public XtaConfigBuilder_ClockPred pruneStrategy(final String pruneStrategy) { + this.pruneStrategy = PruneStrategy.valueOf(pruneStrategy); + return this; + } public XtaConfig build(final XtaSystem xta) { final XtaLts lts = XtaLts.create(xta); //final Expr negProp = xta @@ -235,7 +243,7 @@ public XtaConfigBuilder_ClockPred pruneStrategy(final PruneStrategy pruneStrateg case BW_BIN_ITP: refiner = SingleXtaTraceRefiner.create( XtaTraceChecker.create(initval, initDBM, True(), refinementSolverFactory.createItpSolver(), ZonePrec.of(xta.getClockVars())), - ExprTraceFwBinItpChecker.create(initval, True(), refinementSolverFactory.createItpSolver()), + ExprTraceBwBinItpChecker.create(initval, True(), refinementSolverFactory.createItpSolver()), precGranularity.createRefiner(reftoprec), pruneStrategy, logger, emptyRefutation ); @@ -243,29 +251,15 @@ public XtaConfigBuilder_ClockPred pruneStrategy(final PruneStrategy pruneStrateg case SEQ_ITP: refiner =SingleXtaTraceRefiner.create( XtaTraceChecker.create(initval,initDBM, True(), refinementSolverFactory.createItpSolver(), ZonePrec.of(xta.getClockVars())), - ExprTraceFwBinItpChecker.create(initval, True(), refinementSolverFactory.createItpSolver()), - precGranularity.createRefiner(reftoprec), - pruneStrategy, logger, emptyRefutation - ); - break; - case MULTI_SEQ: - refiner =SingleXtaTraceRefiner.create( - XtaTraceChecker.create(initval, initDBM, True(), refinementSolverFactory.createItpSolver(), ZonePrec.of(xta.getClockVars())), - ExprTraceFwBinItpChecker.create(initval, True(), refinementSolverFactory.createItpSolver()), + ExprTraceSeqItpChecker.create(initval, True(), refinementSolverFactory.createItpSolver()), precGranularity.createRefiner(reftoprec), pruneStrategy, logger, emptyRefutation ); break; - //TODO - /* - case UNSAT_CORE: - refiner = SingleExprTraceRefiner.create(ExprTraceUnsatCoreChecker.create(True(), True(), refinementSolverFactory.createUCSolver()), - precGranularity.createRefiner(new VarsRefToExplPrec()), pruneStrategy, logger); - break;*/ case UCB: refiner =SingleXtaTraceRefiner.create( XtaTraceChecker.create(initval, initDBM, True(), refinementSolverFactory.createItpSolver(), ZonePrec.of(xta.getClockVars())), - ExprTraceFwBinItpChecker.create(initval, True(), refinementSolverFactory.createItpSolver()), + ExprTraceUCBChecker.create(initval, True(), refinementSolverFactory.createUCSolver()), precGranularity.createRefiner(reftoprec), pruneStrategy, logger, emptyRefutation ); @@ -379,6 +373,7 @@ public XtaConfigBuilder_ClockPred pruneStrategy(final PruneStrategy pruneStrateg throw new UnsupportedOperationException(initPrec + " initial precision is not supported with " + domain + " domain"); } + prec.getPrec(xta.getInitLocs()).getPrec2().setShouldApplyPredicates(clockPredAbstraction); return XtaConfig.create(checker, prec); } @@ -509,6 +504,7 @@ public XtaConfigBuilder_ClockPred pruneStrategy(final PruneStrategy pruneStrateg throw new UnsupportedOperationException(initPrec + " initial precision is not supported with " + domain + " domain"); } + prec.getPrec(xta.getInitLocs()).getPrec2().setShouldApplyPredicates(clockPredAbstraction); return XtaConfig.create(checker, prec); } //TODO : diff --git a/subprojects/xta/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/config/XtaConfigBuilder_Zone.java b/subprojects/xta/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/config/XtaConfigBuilder_Zone.java index a504d28d09..7fb7e28415 100644 --- a/subprojects/xta/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/config/XtaConfigBuilder_Zone.java +++ b/subprojects/xta/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/config/XtaConfigBuilder_Zone.java @@ -24,6 +24,8 @@ import hu.bme.mit.theta.analysis.zone.ZoneState; import hu.bme.mit.theta.common.logging.Logger; import hu.bme.mit.theta.common.logging.NullLogger; +import hu.bme.mit.theta.core.type.Expr; +import hu.bme.mit.theta.core.type.booltype.BoolType; import hu.bme.mit.theta.xta.XtaProcess; import hu.bme.mit.theta.xta.XtaSystem; import hu.bme.mit.theta.xta.analysis.*; @@ -181,7 +183,7 @@ public XtaConfigBuilder_Zone pruneStrategy(final PruneStrategy pruneStrategy) { } public XtaConfig build(final XtaSystem xta) { final XtaLts lts = XtaLts.create(xta); - //final Expr negProp = xta + final Expr initval = xta.getInitVal().toExpr(); if(domain == Domain.EXPL){ final Analysis, XtaAction, Prod2Prec> prod2Analysis = Prod2Analysis.create( ExplStmtAnalysis.create(abstractionSolverFactory.createSolver(), xta.getInitVal().toExpr(), maxEnum), @@ -200,29 +202,29 @@ public XtaConfigBuilder_Zone pruneStrategy(final PruneStrategy pruneStrategy) { final RefutationToPrec, ItpRefutation> reftoprec = new ItpRefToProd2ExplZonePrec(); switch (refinement) { case FW_BIN_ITP: - refiner = SingleExprTraceRefiner.create(ExprTraceFwBinItpChecker.create(True(), True(), refinementSolverFactory.createItpSolver()), + refiner = SingleExprTraceRefiner.create(ExprTraceFwBinItpChecker.create(initval, True(), refinementSolverFactory.createItpSolver()), precGranularity.createRefiner(reftoprec ), pruneStrategy, logger); break; case BW_BIN_ITP: - refiner = SingleExprTraceRefiner.create(ExprTraceBwBinItpChecker.create(True(), True(), refinementSolverFactory.createItpSolver()), + refiner = SingleExprTraceRefiner.create(ExprTraceBwBinItpChecker.create(initval, True(), refinementSolverFactory.createItpSolver()), precGranularity.createRefiner(reftoprec ), pruneStrategy, logger); break; case SEQ_ITP: - refiner = SingleExprTraceRefiner.create(ExprTraceSeqItpChecker.create(True(), True(), refinementSolverFactory.createItpSolver()), + refiner = SingleExprTraceRefiner.create(ExprTraceSeqItpChecker.create(initval, True(), refinementSolverFactory.createItpSolver()), precGranularity.createRefiner(reftoprec ), pruneStrategy, logger); break; case MULTI_SEQ: - refiner = MultiExprTraceRefiner.create(ExprTraceSeqItpChecker.create(True(), True(), refinementSolverFactory.createItpSolver()), + refiner = MultiExprTraceRefiner.create(ExprTraceSeqItpChecker.create(initval, True(), refinementSolverFactory.createItpSolver()), precGranularity.createRefiner(reftoprec ), pruneStrategy, logger); break; //TODO /* case UNSAT_CORE: - refiner = SingleExprTraceRefiner.create(ExprTraceUnsatCoreChecker.create(True(), True(), refinementSolverFactory.createUCSolver()), + refiner = SingleExprTraceRefiner.create(ExprTraceUnsatCoreChecker.create(initval, True(), refinementSolverFactory.createUCSolver()), precGranularity.createRefiner(new VarsRefToExplPrec()), pruneStrategy, logger); break;*/ case UCB: - refiner = SingleExprTraceRefiner.create(ExprTraceUCBChecker.create(True(), True(), refinementSolverFactory.createUCSolver()), + refiner = SingleExprTraceRefiner.create(ExprTraceUCBChecker.create(initval, True(), refinementSolverFactory.createUCSolver()), precGranularity.createRefiner(reftoprec ), pruneStrategy, logger); break; case NWT_SP: @@ -235,7 +237,7 @@ public XtaConfigBuilder_Zone pruneStrategy(final PruneStrategy pruneStrategy) { break; case NWT_WP: refiner = SingleExprTraceRefiner.create( - ExprTraceNewtonChecker.create(True(), True(), refinementSolverFactory.createUCSolver()).withoutIT().withWP().withoutLV(), + ExprTraceNewtonChecker.create(initval, True(), refinementSolverFactory.createUCSolver()).withoutIT().withWP().withoutLV(), precGranularity.createRefiner(reftoprec ), pruneStrategy, logger @@ -243,7 +245,7 @@ public XtaConfigBuilder_Zone pruneStrategy(final PruneStrategy pruneStrategy) { break; case NWT_SP_LV: refiner = SingleExprTraceRefiner.create( - ExprTraceNewtonChecker.create(True(), True(), refinementSolverFactory.createUCSolver()).withoutIT().withSP().withLV(), + ExprTraceNewtonChecker.create(initval, True(), refinementSolverFactory.createUCSolver()).withoutIT().withSP().withLV(), precGranularity.createRefiner(reftoprec ), pruneStrategy, logger @@ -251,7 +253,7 @@ public XtaConfigBuilder_Zone pruneStrategy(final PruneStrategy pruneStrategy) { break; case NWT_WP_LV: refiner = SingleExprTraceRefiner.create( - ExprTraceNewtonChecker.create(True(), True(), refinementSolverFactory.createUCSolver()).withoutIT().withWP().withLV(), + ExprTraceNewtonChecker.create(initval, True(), refinementSolverFactory.createUCSolver()).withoutIT().withWP().withLV(), precGranularity.createRefiner(reftoprec), pruneStrategy, logger @@ -259,7 +261,7 @@ public XtaConfigBuilder_Zone pruneStrategy(final PruneStrategy pruneStrategy) { break; case NWT_IT_SP: refiner = SingleExprTraceRefiner.create( - ExprTraceNewtonChecker.create(True(), True(), refinementSolverFactory.createUCSolver()).withIT().withSP().withoutLV(), + ExprTraceNewtonChecker.create(initval, True(), refinementSolverFactory.createUCSolver()).withIT().withSP().withoutLV(), precGranularity.createRefiner(reftoprec ), pruneStrategy, logger @@ -267,7 +269,7 @@ public XtaConfigBuilder_Zone pruneStrategy(final PruneStrategy pruneStrategy) { break; case NWT_IT_WP: refiner = SingleExprTraceRefiner.create( - ExprTraceNewtonChecker.create(True(), True(), refinementSolverFactory.createUCSolver()).withIT().withWP().withoutLV(), + ExprTraceNewtonChecker.create(initval, True(), refinementSolverFactory.createUCSolver()).withIT().withWP().withoutLV(), precGranularity.createRefiner(reftoprec ), pruneStrategy, logger @@ -275,7 +277,7 @@ public XtaConfigBuilder_Zone pruneStrategy(final PruneStrategy pruneStrategy) { break; case NWT_IT_SP_LV: refiner = SingleExprTraceRefiner.create( - ExprTraceNewtonChecker.create(True(), True(), refinementSolverFactory.createUCSolver()).withIT().withSP().withLV(), + ExprTraceNewtonChecker.create(initval, True(), refinementSolverFactory.createUCSolver()).withIT().withSP().withLV(), precGranularity.createRefiner( reftoprec ), pruneStrategy, logger @@ -283,7 +285,7 @@ public XtaConfigBuilder_Zone pruneStrategy(final PruneStrategy pruneStrategy) { break; case NWT_IT_WP_LV: refiner = SingleExprTraceRefiner.create( - ExprTraceNewtonChecker.create(True(), True(), refinementSolverFactory.createUCSolver()).withIT().withWP().withLV(), + ExprTraceNewtonChecker.create(initval, True(), refinementSolverFactory.createUCSolver()).withIT().withWP().withLV(), precGranularity.createRefiner(reftoprec ), pruneStrategy, logger @@ -359,43 +361,43 @@ public XtaConfigBuilder_Zone pruneStrategy(final PruneStrategy pruneStrategy) { ExprTraceChecker exprTraceChecker; switch (refinement) { case FW_BIN_ITP: - exprTraceChecker = ExprTraceFwBinItpChecker.create(True(), True(), refinementSolverFactory.createItpSolver()); + exprTraceChecker = ExprTraceFwBinItpChecker.create(initval, True(), refinementSolverFactory.createItpSolver()); break; case BW_BIN_ITP: - exprTraceChecker = ExprTraceBwBinItpChecker.create(True(), True(), refinementSolverFactory.createItpSolver()); + exprTraceChecker = ExprTraceBwBinItpChecker.create(initval, True(), refinementSolverFactory.createItpSolver()); break; case SEQ_ITP: - exprTraceChecker = ExprTraceSeqItpChecker.create(True(), True(), refinementSolverFactory.createItpSolver()); + exprTraceChecker = ExprTraceSeqItpChecker.create(initval, True(), refinementSolverFactory.createItpSolver()); break; case MULTI_SEQ: - exprTraceChecker = ExprTraceSeqItpChecker.create(True(), True(), refinementSolverFactory.createItpSolver()); + exprTraceChecker = ExprTraceSeqItpChecker.create(initval, True(), refinementSolverFactory.createItpSolver()); break; case UCB: - exprTraceChecker = ExprTraceUCBChecker.create(True(), True(), refinementSolverFactory.createUCSolver()); + exprTraceChecker = ExprTraceUCBChecker.create(initval, True(), refinementSolverFactory.createUCSolver()); break; case NWT_SP: - exprTraceChecker = ExprTraceNewtonChecker.create(True(), True(), refinementSolverFactory.createUCSolver()).withoutIT().withSP().withoutLV(); + exprTraceChecker = ExprTraceNewtonChecker.create(initval, True(), refinementSolverFactory.createUCSolver()).withoutIT().withSP().withoutLV(); break; case NWT_WP: - exprTraceChecker = ExprTraceNewtonChecker.create(True(), True(), refinementSolverFactory.createUCSolver()).withoutIT().withWP().withoutLV(); + exprTraceChecker = ExprTraceNewtonChecker.create(initval, True(), refinementSolverFactory.createUCSolver()).withoutIT().withWP().withoutLV(); break; case NWT_SP_LV: - exprTraceChecker = ExprTraceNewtonChecker.create(True(), True(), refinementSolverFactory.createUCSolver()).withoutIT().withSP().withLV(); + exprTraceChecker = ExprTraceNewtonChecker.create(initval, True(), refinementSolverFactory.createUCSolver()).withoutIT().withSP().withLV(); break; case NWT_WP_LV: - exprTraceChecker = ExprTraceNewtonChecker.create(True(), True(), refinementSolverFactory.createUCSolver()).withoutIT().withWP().withLV(); + exprTraceChecker = ExprTraceNewtonChecker.create(initval, True(), refinementSolverFactory.createUCSolver()).withoutIT().withWP().withLV(); break; case NWT_IT_SP: - exprTraceChecker = ExprTraceNewtonChecker.create(True(), True(), refinementSolverFactory.createUCSolver()).withIT().withSP().withoutLV(); + exprTraceChecker = ExprTraceNewtonChecker.create(initval, True(), refinementSolverFactory.createUCSolver()).withIT().withSP().withoutLV(); break; case NWT_IT_WP: - exprTraceChecker = ExprTraceNewtonChecker.create(True(), True(), refinementSolverFactory.createUCSolver()).withIT().withWP().withoutLV(); + exprTraceChecker = ExprTraceNewtonChecker.create(initval, True(), refinementSolverFactory.createUCSolver()).withIT().withWP().withoutLV(); break; case NWT_IT_SP_LV: - exprTraceChecker = ExprTraceNewtonChecker.create(True(), True(), refinementSolverFactory.createUCSolver()).withIT().withSP().withLV(); + exprTraceChecker = ExprTraceNewtonChecker.create(initval, True(), refinementSolverFactory.createUCSolver()).withIT().withSP().withLV(); break; case NWT_IT_WP_LV: - exprTraceChecker = ExprTraceNewtonChecker.create(True(), True(), refinementSolverFactory.createUCSolver()).withIT().withWP().withLV(); + exprTraceChecker = ExprTraceNewtonChecker.create(initval, True(), refinementSolverFactory.createUCSolver()).withIT().withWP().withLV(); break; default: throw new UnsupportedOperationException( diff --git a/subprojects/xta/xta-cli/src/main/java/hu/bme/mit/theta/xta/cli/XtaCli.java b/subprojects/xta/xta-cli/src/main/java/hu/bme/mit/theta/xta/cli/XtaCli.java index 20899d538e..0e3605129b 100644 --- a/subprojects/xta/xta-cli/src/main/java/hu/bme/mit/theta/xta/cli/XtaCli.java +++ b/subprojects/xta/xta-cli/src/main/java/hu/bme/mit/theta/xta/cli/XtaCli.java @@ -138,7 +138,7 @@ public enum Algorithm { String initPrec = "EMPTY"; @Parameter(names = "--prunestrategy", description = "Strategy for pruning the ARG after refinement") - PruneStrategy pruneStrategy = PruneStrategy.LAZY; + String pruneStrategy = "LAZY"; @Parameter(names = "--cex", description = "Write concrete counterexample to a file") String cexfile = null; @@ -353,20 +353,12 @@ private void Eager_Cegar_check(XtaSystem xta){ } private XtaConfig buildConfiguration(final XtaSystem xta, final SolverFactory abstractionSolverFactory, final SolverFactory refinementSolverFactory) throws Exception { try { - if (clockpred) { XtaConfigBuilder_ClockPred.Domain domainEnum = XtaConfigBuilder_ClockPred.Domain.valueOf(domain); XtaConfigBuilder_ClockPred.Refinement refinementEnum = XtaConfigBuilder_ClockPred.Refinement.valueOf(refinement); return new XtaConfigBuilder_ClockPred(domainEnum, refinementEnum, abstractionSolverFactory, refinementSolverFactory) .precGranularity(precGranularity).search(search) - .predSplit(predSplit).maxEnum(maxEnum).initPrec(initPrec) + .predSplit(predSplit).maxEnum(maxEnum).initPrec(initPrec).setClockPred(clockpred) .pruneStrategy(pruneStrategy).logger(logger).build(xta); - } - XtaConfigBuilder_Zone.Domain domainEnum = XtaConfigBuilder_Zone.Domain.valueOf(domain); - XtaConfigBuilder_Zone.Refinement refinementEnum = XtaConfigBuilder_Zone.Refinement.valueOf(refinement); - return new XtaConfigBuilder_Zone(domainEnum, refinementEnum, abstractionSolverFactory, refinementSolverFactory) - .precGranularity(precGranularity).search(search) - .predSplit(predSplit).maxEnum(maxEnum).initPrec(initPrec) - .pruneStrategy(pruneStrategy).logger(logger).build(xta); } catch (final Exception ex) { throw new Exception("Could not create configuration: " + ex.getMessage(), ex); } diff --git a/subprojects/xta/xta/src/main/java/hu/bme/mit/theta/xta/dsl/XtaInitialiser.java b/subprojects/xta/xta/src/main/java/hu/bme/mit/theta/xta/dsl/XtaInitialiser.java index 299767c498..54f68b5c70 100644 --- a/subprojects/xta/xta/src/main/java/hu/bme/mit/theta/xta/dsl/XtaInitialiser.java +++ b/subprojects/xta/xta/src/main/java/hu/bme/mit/theta/xta/dsl/XtaInitialiser.java @@ -19,6 +19,9 @@ import hu.bme.mit.theta.common.dsl.Scope; import hu.bme.mit.theta.core.type.Expr; import hu.bme.mit.theta.core.type.Type; +import hu.bme.mit.theta.core.type.booltype.BoolLitExpr; +import hu.bme.mit.theta.core.type.booltype.BoolType; +import hu.bme.mit.theta.core.type.inttype.IntLitExpr; import hu.bme.mit.theta.xta.dsl.gen.XtaDslBaseVisitor; import hu.bme.mit.theta.xta.dsl.gen.XtaDslParser.CompoundInitialiserContext; import hu.bme.mit.theta.xta.dsl.gen.XtaDslParser.InitialiserContext; @@ -39,7 +42,13 @@ public XtaInitialiser(final Scope scope, final InitialiserContext context) { public Expr instantiate(final Type type, final Env env) { final InitialiserInstantiationVisitor visitor = new InitialiserInstantiationVisitor(env); - final Expr expr = context.accept(visitor); + Expr expr = context.accept(visitor); + if(type instanceof BoolType){ + if(expr instanceof IntLitExpr){ + if(((IntLitExpr) expr).getValue().intValue() <= 0) expr = BoolLitExpr.of(false); + else expr = BoolLitExpr.of(true); + } + } checkArgument(expr.getType().equals(type)); return expr; }