From 4ff2682a721829e0b5001d41e14f0122f2abac4d Mon Sep 17 00:00:00 2001 From: RipplB Date: Thu, 22 Feb 2024 22:04:48 +0100 Subject: [PATCH] Refactor into StmtAction --- .../loopchecker/LDGTraceChecker.java | 4 -- .../analysis/multi/ExprMultiAnalysis.java | 8 +-- .../theta/analysis/multi/ExprMultiLts.java | 16 +++--- .../mit/theta/analysis/multi/MultiAction.java | 18 ++----- ...rMultiAction.java => StmtMultiAction.java} | 50 +++++++++++-------- .../hu/bme/mit/theta/common/ltl/LtlCheck.kt | 14 +++--- .../hu/bme/mit/theta/common/ltl/LtlChecker.kt | 4 +- 7 files changed, 53 insertions(+), 61 deletions(-) rename subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/{ExprMultiAction.java => StmtMultiAction.java} (50%) diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/LDGTraceChecker.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/LDGTraceChecker.java index d59cdc98f3..cf48111ba0 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/LDGTraceChecker.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/LDGTraceChecker.java @@ -26,7 +26,6 @@ import hu.bme.mit.theta.analysis.expr.StmtAction; import hu.bme.mit.theta.analysis.expr.refinement.ExprTraceStatus; import hu.bme.mit.theta.analysis.expr.refinement.ItpRefutation; -import hu.bme.mit.theta.analysis.multi.ExprMultiAction; import hu.bme.mit.theta.common.container.Containers; import hu.bme.mit.theta.common.logging.Logger; import hu.bme.mit.theta.common.logging.NullLogger; @@ -239,9 +238,6 @@ private Set> expandUsedVariables(Set> usedVariables) { .forEach(varDecl -> ldgTrace.getLoop().forEach(edge -> { if (edge.action() instanceof StmtAction action) VarCollectorStmtVisitor.visitAll(action.getStmts(), usedVariables); - if (edge.action() instanceof ExprMultiAction multiAction && (multiAction.getAction() instanceof StmtAction action)) - {VarCollectorStmtVisitor.visitAll(action.getStmts(), usedVariables); - } })); if (usedVariables.size() > currentSize) return expandUsedVariables(usedVariables); diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/ExprMultiAnalysis.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/ExprMultiAnalysis.java index 28fde356d4..e516a5c4c0 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/ExprMultiAnalysis.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/ExprMultiAnalysis.java @@ -17,22 +17,22 @@ import hu.bme.mit.theta.analysis.InitFunc; import hu.bme.mit.theta.analysis.Prec; -import hu.bme.mit.theta.analysis.expr.ExprAction; +import hu.bme.mit.theta.analysis.expr.StmtAction; import hu.bme.mit.theta.analysis.expr.ExprState; import java.util.function.Function; public final class ExprMultiAnalysis - extends MultiAnalysis, ExprMultiAction> { + extends MultiAnalysis, StmtMultiAction> { private ExprMultiAnalysis(Function, MultiSourceSide> defineNextSide, Side leftSide, Side rightSide, InitFunc dataInitFunc) { super(defineNextSide, leftSide, rightSide, dataInitFunc); } public static ExprMultiAnalysis of(Side leftSide, Side rightSide, diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/ExprMultiLts.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/ExprMultiLts.java index 435073f481..75afbdb41d 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/ExprMultiLts.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/ExprMultiLts.java @@ -16,20 +16,20 @@ package hu.bme.mit.theta.analysis.multi; import hu.bme.mit.theta.analysis.LTS; -import hu.bme.mit.theta.analysis.expr.ExprAction; +import hu.bme.mit.theta.analysis.expr.StmtAction; import hu.bme.mit.theta.analysis.expr.ExprState; import java.util.function.BiFunction; import java.util.function.Function; -public final class ExprMultiLts - extends MultiLts, ExprMultiAction> { +public final class ExprMultiLts + extends MultiLts, StmtMultiAction> { private ExprMultiLts(Function, MultiSourceSide> defineNextSide, Side left, Side right) { super(defineNextSide, left, right); } - public static + public static ExprMultiLts of( LTS leftLts, BiFunction wrapLeftState, LTS rightLts, BiFunction wrapRightState, @@ -38,12 +38,12 @@ ExprMultiLts of( } @Override - ExprMultiAction wrapLeftAction(LAction action) { - return ExprMultiAction.ofLeftExprAction(action); + StmtMultiAction wrapLeftAction(LAction action) { + return StmtMultiAction.ofLeftStmtAction(action); } @Override - ExprMultiAction wrapRightAction(RAction action) { - return ExprMultiAction.ofRightExprAction(action); + StmtMultiAction wrapRightAction(RAction action) { + return StmtMultiAction.ofRightStmtAction(action); } } diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/MultiAction.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/MultiAction.java index 64fc43ee1f..c15b71390a 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/MultiAction.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/MultiAction.java @@ -18,20 +18,8 @@ import hu.bme.mit.theta.analysis.Action; -public abstract class MultiAction implements Action { - L leftAction; - R rightAction; +public interface MultiAction extends Action { + L getLeftAction(); - protected MultiAction(L lAction, R rAction) { - leftAction = lAction; - rightAction = rAction; - } - - public L getLeftAction() { - return leftAction; - } - - public R getRightAction() { - return rightAction; - } + R getRightAction(); } diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/ExprMultiAction.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/StmtMultiAction.java similarity index 50% rename from subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/ExprMultiAction.java rename to subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/StmtMultiAction.java index 5b90521c83..e7108c284c 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/ExprMultiAction.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/StmtMultiAction.java @@ -15,43 +15,51 @@ */ package hu.bme.mit.theta.analysis.multi; -import hu.bme.mit.theta.analysis.expr.ExprAction; -import hu.bme.mit.theta.core.type.Expr; -import hu.bme.mit.theta.core.type.booltype.BoolType; -import hu.bme.mit.theta.core.utils.indexings.VarIndexing; +import hu.bme.mit.theta.analysis.expr.StmtAction; +import hu.bme.mit.theta.core.stmt.Stmt; -public final class ExprMultiAction extends MultiAction implements ExprAction { - private ExprMultiAction(L lAction, R rAction) { - super(lAction, rAction); +import java.util.List; + +public final class StmtMultiAction extends StmtAction implements MultiAction { + private final L leftAction; + private final R rightAction; + private StmtMultiAction(L lAction, R rAction) { + leftAction = lAction; + rightAction = rAction; } - public static ExprMultiAction ofLeftExprAction(L action) { - return new ExprMultiAction<>(action, null); + public static StmtMultiAction ofLeftStmtAction(L action) { + return new StmtMultiAction<>(action, null); } - public static ExprMultiAction ofRightExprAction(R action) { - return new ExprMultiAction<>(null, action); + public static StmtMultiAction ofRightStmtAction(R action) { + return new StmtMultiAction<>(null, action); } - public ExprAction getAction() { + public StmtAction getAction() { return getLeftAction() == null ? getRightAction() : getLeftAction(); } @Override - public Expr toExpr() { - return getAction().toExpr(); + public String toString() { + return "ExprMultiAction{" + + "leftAction=" + leftAction + + ", rightAction=" + rightAction + + '}'; } @Override - public VarIndexing nextIndexing() { - return getAction().nextIndexing(); + public List getStmts() { + return getAction().getStmts(); } @Override - public String toString() { - return "ExprMultiAction{" + - "leftAction=" + leftAction + - ", rightAction=" + rightAction + - '}'; + public L getLeftAction() { + return leftAction; + } + + @Override + public R getRightAction() { + return rightAction; } } diff --git a/subprojects/common/ltl/src/main/kotlin/hu/bme/mit/theta/common/ltl/LtlCheck.kt b/subprojects/common/ltl/src/main/kotlin/hu/bme/mit/theta/common/ltl/LtlCheck.kt index c5da2f2f0f..3370ac20bd 100644 --- a/subprojects/common/ltl/src/main/kotlin/hu/bme/mit/theta/common/ltl/LtlCheck.kt +++ b/subprojects/common/ltl/src/main/kotlin/hu/bme/mit/theta/common/ltl/LtlCheck.kt @@ -9,7 +9,7 @@ import hu.bme.mit.theta.analysis.algorithm.loopchecker.AcceptancePredicate import hu.bme.mit.theta.analysis.algorithm.loopchecker.LDGCegarVerifier import hu.bme.mit.theta.analysis.algorithm.loopchecker.RefinerStrategy import hu.bme.mit.theta.analysis.algorithm.loopchecker.SearchStrategy -import hu.bme.mit.theta.analysis.expr.ExprAction +import hu.bme.mit.theta.analysis.expr.StmtAction import hu.bme.mit.theta.analysis.expr.ExprState import hu.bme.mit.theta.analysis.expr.refinement.ItpRefutation import hu.bme.mit.theta.analysis.expr.refinement.RefutationToPrec @@ -31,7 +31,7 @@ import hu.bme.mit.theta.core.type.booltype.BoolType import hu.bme.mit.theta.solver.ItpSolver object LtlCheck { - fun check( + fun check( formalismAnalysis: Analysis, lts: LTS, refToPrec: RefutationToPrec, @@ -51,7 +51,7 @@ object LtlCheck { logger: Logger, searchStrategy: SearchStrategy, refinerStrategy: RefinerStrategy - ): SafetyResult, DataState>, ExprMultiAction> { + ): SafetyResult, DataState>, StmtMultiAction> { return check( formalismAnalysis, lts, @@ -76,7 +76,7 @@ object LtlCheck { ) } - fun check( + fun check( formalismAnalysis: Analysis, lts: LTS, refToPrec: RefutationToPrec, @@ -97,13 +97,13 @@ object LtlCheck { logger: Logger, searchStrategy: SearchStrategy, refinerStrategy: RefinerStrategy - ): SafetyResult, DataState>, ExprMultiAction> { + ): SafetyResult, DataState>, StmtMultiAction> { val buchiAutomaton = BuchiBuilder.of(ltl, variables, logger) val cfaAnalysis : Analysis, CfaAction, CfaPrec> = CfaAnalysis.create(buchiAutomaton.initLoc, dataAnalysis) val product = MultiBuilder .initWithLeftSide(formalismAnalysis, combineStates, stripState, extractDataFromCombinedState, lts, initFunc, stripPrecision) .addRightSide(cfaAnalysis, BuchiLts(), ::combineBlankBuchiStateWithData, ::stripDataFromBuchiState, { s -> s.state}, BuchiInitFunc.of(buchiAutomaton.initLoc), { p -> p.getPrec(buchiAutomaton.initLoc)}) - .build, DataState>, ExprMultiAction>(defineNextSide, dataAnalysis.initFunc, {ls, rs, dns, dif -> ExprMultiAnalysis.of(ls, rs, dns, dif)}, {llts, cls, rlts, crs, dns -> ExprMultiLts.of(llts, cls, rlts, crs, dns)}) + .build, DataState>, StmtMultiAction>(defineNextSide, dataAnalysis.initFunc, { ls, rs, dns, dif -> ExprMultiAnalysis.of(ls, rs, dns, dif)}, { llts, cls, rlts, crs, dns -> ExprMultiLts.of(llts, cls, rlts, crs, dns)}) val buchiRefToPrec : RefutationToPrec, ItpRefutation> = RefutationToGlobalCfaPrec(dataRefToPrec, buchiAutomaton.initLoc) val multiRefToPrec = RefToMultiPrec(refToPrec, buchiRefToPrec, dataRefToPrec) val verifier = LDGCegarVerifier.of(product.analysis, product.lts, buchiPredicate(buchiAutomaton), logger, solver, initExpr ?: True(), multiRefToPrec) @@ -125,7 +125,7 @@ object LtlCheck { return if (state.sourceSide == MultiSourceSide.LEFT) MultiSourceSide.RIGHT else MultiSourceSide.LEFT } - private fun buchiPredicate(buchiAutomaton: CFA) : AcceptancePredicate, D>, ExprMultiAction> { + private fun buchiPredicate(buchiAutomaton: CFA) : AcceptancePredicate, D>, StmtMultiAction> { return AcceptancePredicate.ofActionPredicate { a -> (a.rightAction != null && a.rightAction.edges.any { e -> buchiAutomaton.acceptingEdges.contains(e) }) } } diff --git a/subprojects/common/ltl/src/main/kotlin/hu/bme/mit/theta/common/ltl/LtlChecker.kt b/subprojects/common/ltl/src/main/kotlin/hu/bme/mit/theta/common/ltl/LtlChecker.kt index 2a9d84a9a3..f807e512ad 100644 --- a/subprojects/common/ltl/src/main/kotlin/hu/bme/mit/theta/common/ltl/LtlChecker.kt +++ b/subprojects/common/ltl/src/main/kotlin/hu/bme/mit/theta/common/ltl/LtlChecker.kt @@ -6,7 +6,7 @@ import hu.bme.mit.theta.analysis.algorithm.SafetyChecker import hu.bme.mit.theta.analysis.algorithm.SafetyResult import hu.bme.mit.theta.analysis.algorithm.loopchecker.RefinerStrategy import hu.bme.mit.theta.analysis.algorithm.loopchecker.SearchStrategy -import hu.bme.mit.theta.analysis.expr.ExprAction +import hu.bme.mit.theta.analysis.expr.StmtAction import hu.bme.mit.theta.analysis.expr.ExprState import hu.bme.mit.theta.analysis.expr.refinement.ItpRefutation import hu.bme.mit.theta.analysis.expr.refinement.RefutationToPrec @@ -23,7 +23,7 @@ import hu.bme.mit.theta.core.type.Expr import hu.bme.mit.theta.core.type.booltype.BoolType import hu.bme.mit.theta.solver.ItpSolver -class LtlChecker ( +class LtlChecker ( private val formalismAnalysis: Analysis, private val lts: LTS, private val refToPrec: RefutationToPrec,