Skip to content

Commit

Permalink
separate traces when zone abstraction is used
Browse files Browse the repository at this point in the history
  • Loading branch information
@kopero2000
kopero2000 committed May 21, 2024
1 parent 4336da5 commit 4e07ec8
Show file tree
Hide file tree
Showing 9 changed files with 100 additions and 63 deletions.
9 changes: 8 additions & 1 deletion subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/zone/ClockPredPrec.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;

Expand All @@ -16,14 +17,17 @@ public class ClockPredPrec implements Prec{

private final Map<Pair<VarDecl<RatType>, VarDecl<RatType>>, Set<Integer>> map;
private final Set<VarDecl<RatType>> clocks;
private boolean shouldApplyPredicates;

private ClockPredPrec(final Map<Pair<VarDecl<RatType>, VarDecl<RatType>>, Set<Integer>> map, final Collection<? extends VarDecl<RatType>> clocks){
checkNotNull(clocks);
this.clocks = ImmutableSet.copyOf(clocks);
this.map = map;
sort();
}

public void setShouldApplyPredicates(final boolean shouldApplyPredicates) {
this.shouldApplyPredicates = shouldApplyPredicates;
}

public static ClockPredPrec of(final Collection<? extends VarDecl<RatType>> clocks) {
return ClockPredPrec.emptyPrec(clocks);
Expand Down Expand Up @@ -135,6 +139,9 @@ public void add(VarDecl<RatType> x, VarDecl<RatType> y,Integer b){
map.get(key).add(b);

}
public boolean getShouldApplyPredicates(){
return this.shouldApplyPredicates;
}


}
13 changes: 9 additions & 4 deletions subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/zone/ZonePrec.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -74,14 +74,19 @@ public Collection<VarDecl<?>> getUsedVars() { // This could be way more elegant

@Override
public Prec join(Prec other) {
if(this == other)return this;
if(other instanceof ZonePrec other1){
HashSet<VarDecl<RatType>> 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<VarDecl<RatType>> newclocks = new HashSet<>(clocks);
newclocks.addAll(other.clocks);
return ZonePrec.of(newclocks);

}
}
2 changes: 1 addition & 1 deletion ...ta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/ClockPred/ClockPredTransFunc.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -18,7 +18,7 @@ private ClockPredTransFunc(){}
public Collection<? extends ZoneState> 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);
Expand Down
26 changes: 26 additions & 0 deletions .../xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/ClockPred/NoneTraceChecker.java
View file
Original file line number Diff line number Diff line change
@@ -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<BoolType> init, DBM initDBM, final Expr<BoolType> target, final ItpSolver solver,ZonePrec clocks ) {
super(init, initDBM, target, solver, clocks);
}

public static NoneTraceChecker create(final Expr<BoolType> init, DBM initDBM, final Expr<BoolType> target, final ItpSolver solver, ZonePrec clocks) {
return new NoneTraceChecker(init, initDBM, target, solver, clocks);
}
@Override
public ExprTraceStatus<ZoneRefutation> check(Trace<ZoneState, XtaAction> trace) {
return ExprTraceStatus.feasible(null);
}
}
2 changes: 1 addition & 1 deletion ...a/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/ClockPred/XtaTraceChecker.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -45,7 +45,7 @@ public class XtaTraceChecker {
private final DBM initDBM;

private final ZonePrec clocks;
private XtaTraceChecker(final Expr<BoolType> init, DBM initDBM, final Expr<BoolType> target, final ItpSolver solver,ZonePrec clocks ) {
protected XtaTraceChecker(final Expr<BoolType> init, DBM initDBM, final Expr<BoolType> target, final ItpSolver solver,ZonePrec clocks ) {
this.solver = solver;
this.init = init;
this.target = target;
Expand Down
32 changes: 14 additions & 18 deletions ...alysis/src/main/java/hu/bme/mit/theta/xta/analysis/config/XtaConfigBuilder_ClockPred.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -124,8 +124,12 @@ public abstract <S extends ExprState,P extends Prec, R extends Refutation> 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;
Expand Down Expand Up @@ -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<? extends State, ? extends Action, ? extends Prec> build(final XtaSystem xta) {
final XtaLts lts = XtaLts.create(xta);
//final Expr<BoolType> negProp = xta
Expand Down Expand Up @@ -235,37 +243,23 @@ 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
);
break;
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
);
Expand Down Expand Up @@ -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);

}
Expand Down Expand Up @@ -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 :
Expand Down
Loading

0 comments on commit 4e07ec8

Please sign in to comment.