Skip to content

Commit

Permalink
Refactor into StmtAction
Browse files Browse the repository at this point in the history
  • Loading branch information
@RipplB
RipplB committed Feb 22, 2024
1 parent fc844dd commit 4ff2682
Show file tree
Hide file tree
Showing 7 changed files with 53 additions and 61 deletions.
4 changes: 0 additions & 4 deletions ...alysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/LDGTraceChecker.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down Expand Up @@ -239,9 +238,6 @@ private Set<VarDecl<?>> expandUsedVariables(Set<VarDecl<?>> 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);
Expand Down
8 changes: 4 additions & 4 deletions ...ects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/ExprMultiAnalysis.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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<LState extends ExprState, RState extends ExprState, DataState extends ExprState, LBlank extends ExprState, RBlank extends ExprState,
LAction extends ExprAction, RAction extends ExprAction,
LAction extends StmtAction, RAction extends StmtAction,
LPrec extends Prec, RPrec extends Prec, DataPrec extends Prec, LBlankPrec extends Prec, RBlankPrec extends Prec>
extends MultiAnalysis<LState, RState, DataState, LBlank, RBlank, LAction, RAction, LPrec, RPrec, DataPrec, LBlankPrec, RBlankPrec, ExprMultiState<LBlank, RBlank, DataState>, ExprMultiAction<LAction, RAction>> {
extends MultiAnalysis<LState, RState, DataState, LBlank, RBlank, LAction, RAction, LPrec, RPrec, DataPrec, LBlankPrec, RBlankPrec, ExprMultiState<LBlank, RBlank, DataState>, StmtMultiAction<LAction, RAction>> {

private ExprMultiAnalysis(Function<ExprMultiState<LBlank, RBlank, DataState>, MultiSourceSide> defineNextSide, Side<LState, DataState, LBlank, LAction, LPrec, LBlankPrec> leftSide, Side<RState, DataState, RBlank, RAction, RPrec, RBlankPrec> rightSide, InitFunc<DataState, DataPrec> dataInitFunc) {
super(defineNextSide, leftSide, rightSide, dataInitFunc);
}

public static <LState extends ExprState, RState extends ExprState, DataState extends ExprState, LBlank extends ExprState, RBlank extends ExprState,
LAction extends ExprAction, RAction extends ExprAction,
LAction extends StmtAction, RAction extends StmtAction,
LPrec extends Prec, RPrec extends Prec, DataPrec extends Prec, LBlankPrec extends Prec, RBlankPrec extends Prec>
ExprMultiAnalysis<LState, RState, DataState, LBlank, RBlank, LAction, RAction, LPrec, RPrec, DataPrec, LBlankPrec, RBlankPrec>
of(Side<LState, DataState, LBlank, LAction, LPrec, LBlankPrec> leftSide, Side<RState, DataState, RBlank, RAction, RPrec, RBlankPrec> rightSide,
Expand Down
16 changes: 8 additions & 8 deletions subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/ExprMultiLts.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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<LState extends ExprState, RState extends ExprState, DataState extends ExprState, LBlank extends ExprState, RBlank extends ExprState, LAction extends ExprAction, RAction extends ExprAction>
extends MultiLts<LState, RState, DataState, LBlank, RBlank, LAction, RAction, ExprMultiState<LBlank, RBlank, DataState>, ExprMultiAction<LAction, RAction>> {
public final class ExprMultiLts<LState extends ExprState, RState extends ExprState, DataState extends ExprState, LBlank extends ExprState, RBlank extends ExprState, LAction extends StmtAction, RAction extends StmtAction>
extends MultiLts<LState, RState, DataState, LBlank, RBlank, LAction, RAction, ExprMultiState<LBlank, RBlank, DataState>, StmtMultiAction<LAction, RAction>> {

private ExprMultiLts(Function<ExprMultiState<LBlank, RBlank, DataState>, MultiSourceSide> defineNextSide, Side<LState, DataState, LBlank, LAction> left, Side<RState, DataState, RBlank, RAction> right) {
super(defineNextSide, left, right);
}

public static<LState extends ExprState, RState extends ExprState, DataState extends ExprState, LBlank extends ExprState, RBlank extends ExprState, LAction extends ExprAction, RAction extends ExprAction>
public static<LState extends ExprState, RState extends ExprState, DataState extends ExprState, LBlank extends ExprState, RBlank extends ExprState, LAction extends StmtAction, RAction extends StmtAction>
ExprMultiLts<LState, RState, DataState, LBlank, RBlank, LAction, RAction> of(
LTS<? super LState, LAction> leftLts, BiFunction<LBlank, DataState, LState> wrapLeftState,
LTS<? super RState, RAction> rightLts, BiFunction<RBlank, DataState, RState> wrapRightState,
Expand All @@ -38,12 +38,12 @@ ExprMultiLts<LState, RState, DataState, LBlank, RBlank, LAction, RAction> of(
}

@Override
ExprMultiAction<LAction, RAction> wrapLeftAction(LAction action) {
return ExprMultiAction.ofLeftExprAction(action);
StmtMultiAction<LAction, RAction> wrapLeftAction(LAction action) {
return StmtMultiAction.ofLeftStmtAction(action);
}

@Override
ExprMultiAction<LAction, RAction> wrapRightAction(RAction action) {
return ExprMultiAction.ofRightExprAction(action);
StmtMultiAction<LAction, RAction> wrapRightAction(RAction action) {
return StmtMultiAction.ofRightStmtAction(action);
}
}
18 changes: 3 additions & 15 deletions subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/MultiAction.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -18,20 +18,8 @@

import hu.bme.mit.theta.analysis.Action;

public abstract class MultiAction<L extends Action, R extends Action> implements Action {
L leftAction;
R rightAction;
public interface MultiAction<L extends Action, R extends Action> 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();
}
50 changes: 29 additions & 21 deletions ...theta/analysis/multi/ExprMultiAction.java → ...theta/analysis/multi/StmtMultiAction.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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<L extends ExprAction, R extends ExprAction> extends MultiAction<L, R> implements ExprAction {
private ExprMultiAction(L lAction, R rAction) {
super(lAction, rAction);
import java.util.List;

public final class StmtMultiAction<L extends StmtAction, R extends StmtAction> extends StmtAction implements MultiAction<L, R> {
private final L leftAction;
private final R rightAction;
private StmtMultiAction(L lAction, R rAction) {
leftAction = lAction;
rightAction = rAction;
}

public static<L extends ExprAction, R extends ExprAction> ExprMultiAction<L, R> ofLeftExprAction(L action) {
return new ExprMultiAction<>(action, null);
public static<L extends StmtAction, R extends StmtAction> StmtMultiAction<L, R> ofLeftStmtAction(L action) {
return new StmtMultiAction<>(action, null);
}

public static<L extends ExprAction, R extends ExprAction> ExprMultiAction<L, R> ofRightExprAction(R action) {
return new ExprMultiAction<>(null, action);
public static<L extends StmtAction, R extends StmtAction> StmtMultiAction<L, R> ofRightStmtAction(R action) {
return new StmtMultiAction<>(null, action);
}

public ExprAction getAction() {
public StmtAction getAction() {
return getLeftAction() == null ? getRightAction() : getLeftAction();
}

@Override
public Expr<BoolType> toExpr() {
return getAction().toExpr();
public String toString() {
return "ExprMultiAction{" +
"leftAction=" + leftAction +
", rightAction=" + rightAction +
'}';
}

@Override
public VarIndexing nextIndexing() {
return getAction().nextIndexing();
public List<Stmt> 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;
}
}
14 changes: 7 additions & 7 deletions subprojects/common/ltl/src/main/kotlin/hu/bme/mit/theta/common/ltl/LtlCheck.kt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -31,7 +31,7 @@ import hu.bme.mit.theta.core.type.booltype.BoolType
import hu.bme.mit.theta.solver.ItpSolver

object LtlCheck {
fun <RState : ExprState, RBlank : ExprState, RAction : ExprAction, RPrec : Prec, RBlankPrec : Prec, DataPrec : Prec, DataState : ExprState> check(
fun <RState : ExprState, RBlank : ExprState, RAction : StmtAction, RPrec : Prec, RBlankPrec : Prec, DataPrec : Prec, DataState : ExprState> check(
formalismAnalysis: Analysis<RState, RAction, RPrec>,
lts: LTS<in RState, RAction>,
refToPrec: RefutationToPrec<RPrec, ItpRefutation>,
Expand All @@ -51,7 +51,7 @@ object LtlCheck {
logger: Logger,
searchStrategy: SearchStrategy,
refinerStrategy: RefinerStrategy
): SafetyResult<ExprMultiState<RBlank, CfaState<UnitState>, DataState>, ExprMultiAction<RAction, CfaAction>> {
): SafetyResult<ExprMultiState<RBlank, CfaState<UnitState>, DataState>, StmtMultiAction<RAction, CfaAction>> {
return check(
formalismAnalysis,
lts,
Expand All @@ -76,7 +76,7 @@ object LtlCheck {
)
}

fun <RState : ExprState, RBlank : ExprState, RAction : ExprAction, RPrec : Prec, RBlankPrec : Prec, DataPrec : Prec, DataState : ExprState> check(
fun <RState : ExprState, RBlank : ExprState, RAction : StmtAction, RPrec : Prec, RBlankPrec : Prec, DataPrec : Prec, DataState : ExprState> check(
formalismAnalysis: Analysis<RState, RAction, RPrec>,
lts: LTS<in RState, RAction>,
refToPrec: RefutationToPrec<RPrec, ItpRefutation>,
Expand All @@ -97,13 +97,13 @@ object LtlCheck {
logger: Logger,
searchStrategy: SearchStrategy,
refinerStrategy: RefinerStrategy
): SafetyResult<ExprMultiState<RBlank, CfaState<UnitState>, DataState>, ExprMultiAction<RAction, CfaAction>> {
): SafetyResult<ExprMultiState<RBlank, CfaState<UnitState>, DataState>, StmtMultiAction<RAction, CfaAction>> {
val buchiAutomaton = BuchiBuilder.of(ltl, variables, logger)
val cfaAnalysis : Analysis<CfaState<DataState>, CfaAction, CfaPrec<DataPrec>> = 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<DataPrec, ExprMultiState<RBlank, CfaState<UnitState>, DataState>, ExprMultiAction<RAction, CfaAction>>(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<DataPrec, ExprMultiState<RBlank, CfaState<UnitState>, DataState>, StmtMultiAction<RAction, CfaAction>>(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<CfaPrec<DataPrec>, 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)
Expand All @@ -125,7 +125,7 @@ object LtlCheck {
return if (state.sourceSide == MultiSourceSide.LEFT) MultiSourceSide.RIGHT else MultiSourceSide.LEFT
}

private fun <D : ExprState, S : ExprState, A : ExprAction> buchiPredicate(buchiAutomaton: CFA) : AcceptancePredicate<ExprMultiState<S, CfaState<UnitState>, D>, ExprMultiAction<A, CfaAction>> {
private fun <D : ExprState, S : ExprState, A : StmtAction> buchiPredicate(buchiAutomaton: CFA) : AcceptancePredicate<ExprMultiState<S, CfaState<UnitState>, D>, StmtMultiAction<A, CfaAction>> {
return AcceptancePredicate.ofActionPredicate { a -> (a.rightAction != null && a.rightAction.edges.any { e -> buchiAutomaton.acceptingEdges.contains(e) }) }
}

Expand Down
4 changes: 2 additions & 2 deletions subprojects/common/ltl/src/main/kotlin/hu/bme/mit/theta/common/ltl/LtlChecker.kt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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<RState : ExprState, RBlank : ExprState, RAction : ExprAction, RPrec : Prec, RBlankPrec : Prec, DataPrec : Prec, DataState : ExprState> (
class LtlChecker<RState : ExprState, RBlank : ExprState, RAction : StmtAction, RPrec : Prec, RBlankPrec : Prec, DataPrec : Prec, DataState : ExprState> (
private val formalismAnalysis: Analysis<RState, RAction, RPrec>,
private val lts: LTS<in RState, RAction>,
private val refToPrec: RefutationToPrec<RPrec, ItpRefutation>,
Expand Down

0 comments on commit 4ff2682

Please sign in to comment.