diff --git a/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/timed/ControlFlowSplitUtil.java b/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/timed/ControlFlowSplitUtil.java index f9fa0a6c50..d18638e3c9 100644 --- a/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/timed/ControlFlowSplitUtil.java +++ b/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/timed/ControlFlowSplitUtil.java @@ -29,42 +29,43 @@ public class ControlFlowSplitUtil { private ControlFlowSplitUtil() { } - public static ControlFlowSplitResult splitCF(final Stmt stmt) { + public static ControlFlowSplitResult splitControlFlows(final Stmt stmt) { final List> flags = new ArrayList<>(); - final List> flagConstraints = new ArrayList<>(); + final List> controlFlowConstraints = new ArrayList<>(); - final ControlFlowFlagsHelper helper = new ControlFlowFlagsHelper(flags, flagConstraints); - final Stmt flaggedStmt = helper.flagStmt(stmt); + final ControlFlowEncodingHelper helper = new ControlFlowEncodingHelper(flags, controlFlowConstraints); + final Stmt flaggedStmt = helper.encodeControlFlows(stmt); for (final VarDecl flag : Lists.reverse(flags)) { VarPoolUtil.returnBool(flag); } - return ControlFlowSplitResult.of(flaggedStmt, flags, flagConstraints); + return ControlFlowSplitResult.of(flaggedStmt, flags, controlFlowConstraints); } - private static final class ControlFlowFlagsHelper implements StmtVisitor, Stmt> { + private static final class ControlFlowEncodingHelper implements StmtVisitor, Stmt> { private final List> flags; - private final List> flagConstraints; + private final List> controlFlowConstraints; private final AssumeTransformationHelper assumeHelper; - private ControlFlowFlagsHelper(final List> flags, final List> flagConstraints) { + private ControlFlowEncodingHelper(final List> flags, + final List> controlFlowConstraints) { this.flags = flags; - this.flagConstraints = flagConstraints; + this.controlFlowConstraints = controlFlowConstraints; assumeHelper = new AssumeTransformationHelper(); } - public Stmt flagStmt(final Stmt stmt) { + public Stmt encodeControlFlows(final Stmt stmt) { final VarDecl root = VarPoolUtil.requestBool(); flags.add(root); - flagConstraints.add(root.getRef()); + controlFlowConstraints.add(root.getRef()); - final Stmt flaggedStmt = stmt.accept(this, root); - final AssumeStmt flagConstraintsAssume = Stmts.Assume(And(flagConstraints)); + final Stmt transformedStmt = stmt.accept(this, root); + final AssumeStmt controlFlowAssumptions = Stmts.Assume(And(controlFlowConstraints)); - return Stmts.SequenceStmt(List.of(flaggedStmt, flagConstraintsAssume)); + return Stmts.SequenceStmt(List.of(transformedStmt, controlFlowAssumptions)); } @Override @@ -105,10 +106,10 @@ public Stmt visit(HavocStmt stmt, VarDecl parent) { - final List flaggedSubStmts = stmt.getStmts().stream() + final List transformedSubStmts = stmt.getStmts().stream() .map(subStmt -> subStmt.accept(this, parent)) .toList(); - return SequenceStmt(flaggedSubStmts); + return SequenceStmt(transformedSubStmts); } @Override @@ -125,17 +126,17 @@ public Stmt visit(NonDetStmt stmt, VarDecl parent) { } final List> localFlags = new ArrayList<>(branchCnt); - final List flaggedBranches = new ArrayList<>(branchCnt); + final List transformedBranches = new ArrayList<>(branchCnt); for (final Stmt branch : branches) { final VarDecl flag = VarPoolUtil.requestBool(); localFlags.add(flag); flags.add(flag); - flagConstraints.add(Imply(Not(parent.getRef()), Not(flag.getRef()))); + controlFlowConstraints.add(Imply(Not(parent.getRef()), Not(flag.getRef()))); - final Stmt flaggedBranchBody = branch.accept(this, flag); - final IfStmt flaggedBranch = IfStmt(flag.getRef(), flaggedBranchBody); - flaggedBranches.add(flaggedBranch); + final Stmt transformedBranchBody = branch.accept(this, flag); + final IfStmt transformedBranch = IfStmt(flag.getRef(), transformedBranchBody); + transformedBranches.add(transformedBranch); } final List> branchExprs = new ArrayList<>(); @@ -147,9 +148,9 @@ public Stmt visit(NonDetStmt stmt, VarDecl parent) { } branchExprs.add(And(flagsForCurrentBranch)); } - flagConstraints.add(Imply(parent.getRef(), Or(branchExprs))); + controlFlowConstraints.add(Imply(parent.getRef(), Or(branchExprs))); - return SequenceStmt(flaggedBranches); + return SequenceStmt(transformedBranches); } @Override @@ -173,7 +174,7 @@ public Stmt visit(IfStmt stmt, VarDecl parent) { condToBranch.put(Not(stmt.getCond()), stmt.getElze()); final List> localFlags = new ArrayList<>(2); - final List flaggedBranches = new ArrayList<>(2); + final List transformedBranches = new ArrayList<>(2); for (final Map.Entry, Stmt> branch : condToBranch.entrySet()) { final VarDecl flag = VarPoolUtil.requestBool(); @@ -183,20 +184,20 @@ public Stmt visit(IfStmt stmt, VarDecl parent) { final Expr cond = branch.getKey(); final Stmt branchBody = branch.getValue(); final Stmt newBranchBody = SequenceStmt(List.of(Assume(cond), branchBody)); - final Stmt flaggedBranchBody = newBranchBody.accept(this, flag); + final Stmt transformedBranchBody = newBranchBody.accept(this, flag); - final IfStmt flaggedBranch = IfStmt(flag.getRef(), flaggedBranchBody); - flaggedBranches.add(flaggedBranch); + final IfStmt transformedBranch = IfStmt(flag.getRef(), transformedBranchBody); + transformedBranches.add(transformedBranch); } final Expr p = parent.getRef(); final Expr b1 = localFlags.get(0).getRef(); final Expr b2 = localFlags.get(1).getRef(); - flagConstraints.add(Imply(p, Xor(b1, b2))); - flagConstraints.add(Imply(Not(p), Not(b1))); - flagConstraints.add(Imply(Not(p), Not(b2))); + controlFlowConstraints.add(Imply(p, Xor(b1, b2))); + controlFlowConstraints.add(Imply(Not(p), Not(b1))); + controlFlowConstraints.add(Imply(Not(p), Not(b2))); - return SequenceStmt(flaggedBranches); + return SequenceStmt(transformedBranches); } @Override @@ -238,20 +239,20 @@ private Stmt transformAssume(final Expr cond, final VarDecl private Stmt transformAnd(final AndExpr andExpr, final VarDecl parent) { final List assumes = andExpr.getOps().stream().map(Stmts::Assume).collect(toList()); final Stmt transformed = SequenceStmt(assumes); - return transformed.accept(ControlFlowSplitUtil.ControlFlowFlagsHelper.this, parent); + return transformed.accept(ControlFlowEncodingHelper.this, parent); } private Stmt transformOr(final OrExpr orExpr, final VarDecl parent) { final List assumes = orExpr.getOps().stream().map(Stmts::Assume).collect(toList()); final Stmt transformed = NonDetStmt(assumes); - return transformed.accept(ControlFlowSplitUtil.ControlFlowFlagsHelper.this, parent); + return transformed.accept(ControlFlowEncodingHelper.this, parent); } private Stmt transformImply(final ImplyExpr implyExpr, final VarDecl parent) { final Expr a = implyExpr.getLeftOp(); final Expr b = implyExpr.getRightOp(); final Stmt transformed = Assume(Or(Not(a), b)); - return transformed.accept(ControlFlowSplitUtil.ControlFlowFlagsHelper.this, parent); + return transformed.accept(ControlFlowEncodingHelper.this, parent); } private Stmt transformIff(final IffExpr iffExpr, final VarDecl parent) { @@ -260,7 +261,7 @@ private Stmt transformIff(final IffExpr iffExpr, final VarDecl parent) final Expr imply1 = Or(Not(a), b); final Expr imply2 = Or(Not(b), a); final Stmt transformed = Assume(And(imply1, imply2)); - return transformed.accept(ControlFlowSplitUtil.ControlFlowFlagsHelper.this, parent); + return transformed.accept(ControlFlowEncodingHelper.this, parent); } private Stmt transformXor(final XorExpr xorExpr, final VarDecl parent) { @@ -269,7 +270,7 @@ private Stmt transformXor(final XorExpr xorExpr, final VarDecl parent) final Expr case1 = And(Not(a), b); final Expr case2 = And(a, Not(b)); final Stmt transformed = Assume(Or(case1, case2)); - return transformed.accept(ControlFlowSplitUtil.ControlFlowFlagsHelper.this, parent); + return transformed.accept(ControlFlowEncodingHelper.this, parent); } private Stmt transformNot(final NotExpr notExpr, final VarDecl parent) { @@ -312,26 +313,26 @@ private Stmt transformNegatedClockConstraint(final ClockConstraintExpr negatedCl private Stmt transformNegatedNot(final NotExpr negatedNotExpr, final VarDecl parent) { final Stmt transformed = Assume(negatedNotExpr.getOp()); - return transformed.accept(ControlFlowSplitUtil.ControlFlowFlagsHelper.this, parent); + return transformed.accept(ControlFlowEncodingHelper.this, parent); } private Stmt transformNegatedAnd(final AndExpr negatedAndExpr, final VarDecl parent) { final List negatedOps = negatedAndExpr.getOps().stream().map(BoolExprs::Not).toList(); final Stmt transformed = Assume(Or(negatedOps)); - return transformed.accept(ControlFlowSplitUtil.ControlFlowFlagsHelper.this, parent); + return transformed.accept(ControlFlowEncodingHelper.this, parent); } private Stmt transformNegatedOr(final OrExpr negatedOrExpr, final VarDecl parent) { final List negatedOps = negatedOrExpr.getOps().stream().map(BoolExprs::Not).toList(); final Stmt transformed = Assume(And(negatedOps)); - return transformed.accept(ControlFlowSplitUtil.ControlFlowFlagsHelper.this, parent); + return transformed.accept(ControlFlowEncodingHelper.this, parent); } private Stmt transformNegatedImply(final ImplyExpr negatedImplyExpr, final VarDecl parent) { final Expr a = negatedImplyExpr.getLeftOp(); final Expr b = negatedImplyExpr.getRightOp(); final Stmt transformed = Assume(And(a, Not(b))); - return transformed.accept(ControlFlowSplitUtil.ControlFlowFlagsHelper.this, parent); + return transformed.accept(ControlFlowEncodingHelper.this, parent); } private Stmt transformNegatedIff(final IffExpr negatedIffExpr, final VarDecl parent) { @@ -340,7 +341,7 @@ private Stmt transformNegatedIff(final IffExpr negatedIffExpr, final VarDecl notImply1 = And(a, Not(b)); final Expr notImply2 = And(b, Not(a)); final Stmt transformed = Assume(Or(notImply1, notImply2)); - return transformed.accept(ControlFlowSplitUtil.ControlFlowFlagsHelper.this, parent); + return transformed.accept(ControlFlowEncodingHelper.this, parent); } private Stmt transformNegatedXor(final XorExpr negatedXorExpr, final VarDecl parent) { @@ -349,21 +350,21 @@ private Stmt transformNegatedXor(final XorExpr negatedXorExpr, final VarDecl same1 = And(a, b); final Expr same2 = And(Not(a), Not(b)); final Stmt transformed = Assume(Or(same1, same2)); - return transformed.accept(ControlFlowSplitUtil.ControlFlowFlagsHelper.this, parent); + return transformed.accept(ControlFlowEncodingHelper.this, parent); } private Stmt transformNegatedExists(final ExistsExpr negatedExistsExpr, final VarDecl parent) { final List> params = negatedExistsExpr.getParamDecls(); final Expr op = negatedExistsExpr.getOp(); final Stmt transformed = Assume(Forall(params, Not(op))); - return transformed.accept(ControlFlowSplitUtil.ControlFlowFlagsHelper.this, parent); + return transformed.accept(ControlFlowEncodingHelper.this, parent); } private Stmt transformNegatedForall(final ForallExpr negatedForallExpr, final VarDecl parent) { final List> params = negatedForallExpr.getParamDecls(); final Expr op = negatedForallExpr.getOp(); final Stmt transformed = Assume(Exists(params, Not(op))); - return transformed.accept(ControlFlowSplitUtil.ControlFlowFlagsHelper.this, parent); + return transformed.accept(ControlFlowEncodingHelper.this, parent); } } } diff --git a/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/timed/ControlFlowSplitXstsLts.java b/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/timed/ControlFlowSplitXstsLts.java index e3c0a39782..3450717b41 100644 --- a/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/timed/ControlFlowSplitXstsLts.java +++ b/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/timed/ControlFlowSplitXstsLts.java @@ -45,7 +45,6 @@ public class ControlFlowSplitXstsLts implements LTS valExtractor) { this.solver = solver; @@ -76,15 +75,14 @@ public static ControlFlowSplitXstsLts create(final XSTS @Override public Collection getEnabledActionsFor(XstsState state) { reset(); - splitCF(state); - return getEnabledActions(); - } - - public Collection getEnabledActionsFor(XstsState state, ExprState abstrState) { - reset(); - splitCF(state); - filterCF(abstrState); - return getEnabledActions(); + splitControlFlows(state, false); + final List actions = new ArrayList<>(); + Optional action = getNextEnabledAction(); + while (action.isPresent()) { + actions.add(action.get()); + action = getNextEnabledAction(); + } + return actions; } public void reset() { @@ -92,33 +90,31 @@ public void reset() { solver.pop(); } lastState = null; - stmtInSolver = false; } - public void splitCF(final XstsState state) { - final Stmt xstsStep; - if (!state.isInitialized()) xstsStep = init; - else if (state.lastActionWasEnv()) xstsStep = tran; - else xstsStep = env; + public void splitControlFlows(final XstsState state, final boolean feasibleOnly) { + final Stmt enabledSet; + if (!state.isInitialized()) enabledSet = init; + else if (state.lastActionWasEnv()) enabledSet = tran; + else enabledSet = env; final Valuation ctrlVal = valExtractor.extractValuationForVars(state.getState(), ctrlVars); - final Stmt simplifiedStmt = StmtSimplifier.simplifyStmt(ctrlVal, xstsStep); - cfSplitResult = cfSplitCache.computeIfAbsent(simplifiedStmt, ControlFlowSplitUtil::splitCF); + final Stmt simplifiedStmt = StmtSimplifier.simplifyStmt(ctrlVal, enabledSet); + cfSplitResult = cfSplitCache.computeIfAbsent(simplifiedStmt, ControlFlowSplitUtil::splitControlFlows); solver.push(); solver.add(cfSplitResult.getIndexedFlagConstraintExpr()); + if (feasibleOnly) { + final Stmt stmtWithoutClocks = stmtClockTransformer.apply(cfSplitResult.getFlaggedStmt()); + StmtUtils.toExpr(stmtWithoutClocks, VarIndexingFactory.indexing(0)).getExprs() + .forEach(expr -> solver.add(PathUtils.unfold(expr, 0))); + } } - public void filterCF(final ExprState state) { + public void updateSourceAbstractState(final ExprState state) { if (state != lastState) { solver.add(PathUtils.unfold(state.toExpr(), 0)); } - if (!stmtInSolver) { - final Stmt stmtWithoutClocks = stmtClockTransformer.apply(cfSplitResult.getFlaggedStmt()); - StmtUtils.toExpr(stmtWithoutClocks, VarIndexingFactory.indexing(0)).getExprs() - .forEach(expr -> solver.add(PathUtils.unfold(expr, 0))); - stmtInSolver = true; - } } public Optional getNextEnabledAction() { @@ -152,14 +148,4 @@ public Optional getNextEnabledAction() { return Optional.empty(); } } - - private Collection getEnabledActions() { - final List actions = new ArrayList<>(); - Optional action = getNextEnabledAction(); - while (action.isPresent()) { - actions.add(action.get()); - action = getNextEnabledAction(); - } - return actions; - } } diff --git a/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/timed/ControlFlowSplitLazyAbstractor.java b/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/timed/XstsLazyAbstractor.java similarity index 89% rename from subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/timed/ControlFlowSplitLazyAbstractor.java rename to subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/timed/XstsLazyAbstractor.java index fa4cafadf8..e0c4ab0992 100644 --- a/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/timed/ControlFlowSplitLazyAbstractor.java +++ b/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/timed/XstsLazyAbstractor.java @@ -27,7 +27,7 @@ import static com.google.common.base.Preconditions.checkNotNull; -public final class ControlFlowSplitLazyAbstractor +public final class XstsLazyAbstractor implements Abstractor, XstsState>, XstsAction, P> { private final ControlFlowSplitXstsLts lts; @@ -35,20 +35,20 @@ public final class ControlFlowSplitLazyAbstractor, XstsState>, XstsAction> lazyStrategy; private final Analysis, XstsState>, XstsAction, P> analysis; private final Predicate> isTarget; - private final boolean filterInfeasibleCF; - - public ControlFlowSplitLazyAbstractor(final ControlFlowSplitXstsLts lts, - final SearchStrategy searchStrategy, - final LazyStrategy, XstsState>, XstsAction> lazyStrategy, - final LazyAnalysis, XstsState, XstsAction, P> analysis, - final Predicate> isTarget, - final boolean filterInfeasibleCF) { + private final boolean feasibleActionsOnly; + + public XstsLazyAbstractor(final ControlFlowSplitXstsLts lts, + final SearchStrategy searchStrategy, + final LazyStrategy, XstsState>, XstsAction> lazyStrategy, + final LazyAnalysis, XstsState, XstsAction, P> analysis, + final Predicate> isTarget, + final boolean feasibleActionsOnly) { this.lts = checkNotNull(lts); this.searchStrategy = checkNotNull(searchStrategy); this.lazyStrategy = checkNotNull(lazyStrategy); this.analysis = checkNotNull(analysis); this.isTarget = isTarget; - this.filterInfeasibleCF = filterInfeasibleCF; + this.feasibleActionsOnly = feasibleActionsOnly; } @Override @@ -158,9 +158,9 @@ private AbstractorResult expand(final ArgNode, XstsS final LazyState, XstsState> state = node.getState(); lts.reset(); - lts.splitCF(state.getConcrState()); - if (filterInfeasibleCF) { - lts.filterCF(state.getAbstrState()); + lts.splitControlFlows(state.getConcrState(), feasibleActionsOnly); + if (feasibleActionsOnly) { + lts.updateSourceAbstractState(state.getAbstrState()); } Optional nextAction = lts.getNextEnabledAction(); @@ -179,8 +179,8 @@ private AbstractorResult expand(final ArgNode, XstsS lazyStrategy.disable(node, action, succState, uncoveredNodes); waiting.addAll(uncoveredNodes); - if (filterInfeasibleCF) { - lts.filterCF(node.getState().getAbstrState()); + if (feasibleActionsOnly) { + lts.updateSourceAbstractState(node.getState().getAbstrState()); } } else { final boolean target = isTarget.test(succState.getConcrState());