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 8f42c38cfb..ef78a0ccb1 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 @@ -1,5 +1,6 @@ package hu.bme.mit.theta.analysis.zone; +import com.google.common.collect.ImmutableMap; import com.google.common.collect.ImmutableSet; import hu.bme.mit.theta.analysis.Prec; import hu.bme.mit.theta.common.Utils; @@ -48,7 +49,7 @@ public boolean equals(final Object obj) { return true; } else if (obj instanceof ClockPredPrec) { final ClockPredPrec that = (ClockPredPrec) obj; - return this.getVars().equals(that.getVars()); + return this.getVars().equals(that.getVars()) && this.map.equals(that.map); } else { return false; } @@ -70,20 +71,31 @@ public static ClockPredPrec of(final Map, VarDecl } - + private HashMap, VarDecl>, Set> copyMap(Map, VarDecl>, Set> mapToCopy) { + final HashMap, VarDecl>, Set> newmap = new HashMap<>(); + for(Map.Entry, VarDecl>, Set> entry: mapToCopy.entrySet()){ + final Set copySet = new HashSet<>(entry.getValue()); + newmap.put(entry.getKey(), copySet); + } + return newmap; + } public ClockPredPrec join(final ClockPredPrec other){ //addClocks(other.getVars()); + final HashMap, VarDecl>, Set> newmap = this.copyMap(map); for(Map.Entry, VarDecl>, Set> entry: other.map.entrySet()){ if(map.containsKey(entry.getKey())){ - map.get(entry.getKey()).addAll(entry.getValue()); + newmap.get(entry.getKey()).addAll(entry.getValue()); } else{ - map.put(entry.getKey(), entry.getValue()); + newmap.put(entry.getKey(), entry.getValue()); } } sort(); - return this; + if(newmap.equals(map)){ + return this; + } + return of(newmap, clocks); } @Override diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/zone/DBM.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/zone/DBM.java index f2f06872f6..4481c96133 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/zone/DBM.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/zone/DBM.java @@ -861,26 +861,39 @@ public void setIfGreater(ClockPredPrec prec){ newdbm.set(i, j, b); break; } - -// if (DiffBounds.isStrict(b)) { -// if (DiffBounds.getBound(b) > DiffBounds.getBound(currval)) { -// -// } -// } else { -// if (DiffBounds.getBound(b) >= DiffBounds.getBound(currval)) { -// newdbm.set(i, j, b); -// break; -// } -// } } - //if(newdbm.get(i,j) == dbm.get(i,j)) newdbm.set(i,j, DiffBounds.Inf()); - dbm.set(i,j,newdbm.get(i,j)); + // dbm.set(i,j,newdbm.get(i,j)); } for(int i = 0; i < dbm.size(); i++){ - for(int j = 1; j < dbm.size(); j++){ - dbm.set(i,j,newdbm.get(i,j)); + for(int j = 0; j < dbm.size(); j++){ + if(i != j) + dbm.set(i,j,newdbm.get(i,j)); + } + } + } + public Collection, VarDecl>, Integer>> getDiffBounds() { + final Collection, VarDecl>, Integer>> result = Containers.createSet(); + + for (final VarDecl leftVar : signature) { + for (final VarDecl rightVar : signature) { + final int b = get(leftVar, rightVar); + final ClockConstr constr = DiffBounds.toConstr(leftVar, rightVar, b); + Pair, VarDecl> pair; + if(rightVar.equals(ZeroVar.getInstance())) { + pair = new Pair, VarDecl>(leftVar); + } + else pair = new Pair, VarDecl>(leftVar,rightVar); + if (constr instanceof TrueConstr) { + continue; + } else if (constr instanceof FalseConstr) { + return Collections.singleton(new Pair, VarDecl>, Integer>(pair, b)); + } else { + result.add(new Pair, VarDecl>, Integer>(pair, b)); + } } } + + return result; } diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/zone/ZoneState.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/zone/ZoneState.java index 473ac407eb..5bbb7c749b 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/zone/ZoneState.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/zone/ZoneState.java @@ -19,6 +19,7 @@ import hu.bme.mit.theta.analysis.expr.ExprState; import hu.bme.mit.theta.common.Utils; import hu.bme.mit.theta.core.clock.constr.ClockConstr; +import hu.bme.mit.theta.core.clock.constr.ClockConstrs; import hu.bme.mit.theta.core.clock.op.ClockOp; import hu.bme.mit.theta.core.decl.VarDecl; import hu.bme.mit.theta.core.model.Valuation; @@ -159,7 +160,7 @@ public boolean isTop() { @Override public boolean isBottom() { - return !dbm.isConsistent(); + return !dbm.isConsistent() || dbm.getConstrs().stream().anyMatch(c -> c.equals(ClockConstrs.False())); } public boolean isLeq(final ZoneState that) { 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 bde377a5f3..43bf9ad304 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,13 +18,9 @@ private ClockPredTransFunc(){} public Collection getSuccStates(ZoneState state, XtaAction action, ClockPredPrec prec) { ZoneState succState = XtaClockPredUtils.post(state, action, prec); - -// if(action.getTargetLocs().stream().map(loc -> loc.getName()).toList().contains("Circuit_UpdatedLbenchn13_becomes1")){ -// int x= 0; -// } - //ne legyen x-y inf - succState.clockPredicate(prec); -//új változó debughoz + if(!succState.isBottom()){ + succState.clockPredicate(prec); + } return ImmutableList.of(succState); } } diff --git a/subprojects/xta/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/ClockPred/Prod2RefToProd2ExplClockPredPrec.java b/subprojects/xta/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/ClockPred/Prod2RefToProd2ExplClockPredPrec.java index f85352e33e..334317ff69 100644 --- a/subprojects/xta/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/ClockPred/Prod2RefToProd2ExplClockPredPrec.java +++ b/subprojects/xta/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/ClockPred/Prod2RefToProd2ExplClockPredPrec.java @@ -14,6 +14,7 @@ import hu.bme.mit.theta.core.decl.VarDecl; import hu.bme.mit.theta.core.type.Expr; import hu.bme.mit.theta.core.type.booltype.BoolType; +import hu.bme.mit.theta.core.type.rattype.RatType; import hu.bme.mit.theta.core.utils.ExprUtils; import java.util.Collection; @@ -28,18 +29,15 @@ public class Prod2RefToProd2ExplClockPredPrec implements RefutationToPrec toPrec(Prod2Refutation refutation, int index) { ClockPredPrec clockPredPrec = ClockPredPrec.emptyPrec(refutation.getRefutation2().getClocks()); ExplPrec explPrec = ExplPrec.empty(); - if(refutation.getRefutation2().getPruneIndex()>=0) { + if(refutation.getRefutation2().getPruneIndex() >= 0) { final ZoneState zone = refutation.getRefutation2().get(index); if (!(zone.isBottom() || zone.isTop())) { - Iterator iterator = zone.getDbm().getConstrs().iterator(); - while (iterator.hasNext()) { - ClockConstr constr = iterator.next(); - - if (constr instanceof DiffLtConstr ltconstr) { - clockPredPrec.add(ltconstr.getLeftVar(), ltconstr.getRightVar(), DiffBounds.Lt(ltconstr.getBound())); - } else if (constr instanceof DiffLeqConstr leqconstr) { - clockPredPrec.add(leqconstr.getLeftVar(), leqconstr.getRightVar(), DiffBounds.Leq(leqconstr.getBound())); + Collection, VarDecl>, Integer>> diffBounds = zone.getDbm().getDiffBounds(); + for (Pair, VarDecl>, Integer> diffBound: diffBounds) { + if (diffBound.getKey().NoValue()){ + clockPredPrec.add(diffBound.getKey().getKey(), diffBound.getValue()); } + else clockPredPrec.add(diffBound.getKey().getKey(), diffBound.getKey().getValue(), diffBound.getValue()); } } } diff --git a/subprojects/xta/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/ClockPred/Prod2RefToProd2PredClockPredPrec.java b/subprojects/xta/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/ClockPred/Prod2RefToProd2PredClockPredPrec.java index 2372f8a9bc..2f2119a332 100644 --- a/subprojects/xta/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/ClockPred/Prod2RefToProd2PredClockPredPrec.java +++ b/subprojects/xta/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/ClockPred/Prod2RefToProd2PredClockPredPrec.java @@ -7,16 +7,16 @@ import hu.bme.mit.theta.analysis.pred.ExprSplitters; import hu.bme.mit.theta.analysis.pred.PredPrec; import hu.bme.mit.theta.analysis.prod2.Prod2Prec; -import hu.bme.mit.theta.analysis.zone.ClockPredPrec; -import hu.bme.mit.theta.analysis.zone.DiffBounds; -import hu.bme.mit.theta.analysis.zone.ZonePrec; -import hu.bme.mit.theta.analysis.zone.ZoneState; +import hu.bme.mit.theta.analysis.zone.*; import hu.bme.mit.theta.core.clock.constr.ClockConstr; import hu.bme.mit.theta.core.clock.constr.DiffLeqConstr; import hu.bme.mit.theta.core.clock.constr.DiffLtConstr; +import hu.bme.mit.theta.core.decl.VarDecl; import hu.bme.mit.theta.core.type.Expr; import hu.bme.mit.theta.core.type.booltype.BoolType; +import hu.bme.mit.theta.core.type.rattype.RatType; +import java.util.Collection; import java.util.Collections; import java.util.Iterator; import java.util.stream.Collectors; @@ -37,15 +37,12 @@ public Prod2Prec toPrec(Prod2Refutation= 0) { final ZoneState zone = refutation.getRefutation2().get(index); if (!(zone.isBottom() || zone.isTop())) { - Iterator iterator = zone.getDbm().getConstrs().iterator(); - while (iterator.hasNext()) { - ClockConstr constr = iterator.next(); - - if (constr instanceof DiffLtConstr ltconstr) { - clockPredPrec.add(ltconstr.getLeftVar(), ltconstr.getRightVar(), DiffBounds.Lt(ltconstr.getBound())); - } else if (constr instanceof DiffLeqConstr leqconstr) { - clockPredPrec.add(leqconstr.getLeftVar(), leqconstr.getRightVar(), DiffBounds.Leq(leqconstr.getBound())); + Collection, VarDecl>, Integer>> diffBounds = zone.getDbm().getDiffBounds(); + for (Pair, VarDecl>, Integer> diffBound: diffBounds) { + if (diffBound.getKey().NoValue()){ + clockPredPrec.add(diffBound.getKey().getKey(), diffBound.getValue()); } + else clockPredPrec.add(diffBound.getKey().getKey(), diffBound.getKey().getValue(), diffBound.getValue()); } } } diff --git a/subprojects/xta/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/ClockPred/SingleXtaTraceRefiner.java b/subprojects/xta/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/ClockPred/SingleXtaTraceRefiner.java index 189322a796..2efa66a1ff 100644 --- a/subprojects/xta/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/ClockPred/SingleXtaTraceRefiner.java +++ b/subprojects/xta/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/ClockPred/SingleXtaTraceRefiner.java @@ -20,6 +20,7 @@ import hu.bme.mit.theta.xta.analysis.XtaState; import hu.bme.mit.theta.xta.analysis.prec.XtaPrec; +import java.time.Clock; import java.util.ArrayList; import java.util.Collections; import java.util.List; @@ -42,8 +43,6 @@ public final class SingleXtaTraceRefiner exprTraceChecker, PrecRefiner>, 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 dbf11db58c..374844260d 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 @@ -7,7 +7,9 @@ import hu.bme.mit.theta.analysis.expr.refinement.ExprTraceStatus; import hu.bme.mit.theta.analysis.expr.refinement.Refutation; import hu.bme.mit.theta.analysis.expr.refinement.ZoneRefutation; +import hu.bme.mit.theta.analysis.prod2.Prod2Prec; import hu.bme.mit.theta.analysis.prod2.Prod2State; +import hu.bme.mit.theta.analysis.zone.ClockPredPrec; import hu.bme.mit.theta.analysis.zone.DBM; import hu.bme.mit.theta.analysis.zone.ZonePrec; import hu.bme.mit.theta.analysis.zone.ZoneState; @@ -21,9 +23,11 @@ import hu.bme.mit.theta.solver.ItpSolver; import hu.bme.mit.theta.xta.analysis.XtaAction; import hu.bme.mit.theta.xta.analysis.XtaState; +import hu.bme.mit.theta.xta.analysis.prec.GlobalXtaPrec; import hu.bme.mit.theta.xta.analysis.prec.XtaPrec; import hu.bme.mit.theta.xta.analysis.zone.XtaZoneUtils; +import java.time.Clock; import java.util.ArrayList; import java.util.Collections; import java.util.List; @@ -63,7 +67,6 @@ public ExprTraceStatus check(Trace trace) abstractPreZoneStates.add( trace.getState(stateCount-1)); concreteZoneStates.add(ZoneState.of(initDBM)); - for(int i = 1; i < stateCount; i++){ concreteZoneStates.add(XtaZoneUtils.post(trace.getState(i-1), trace.getAction(i-1), clocks)); abstractPreZoneStates.add(ZoneState.intersection(XtaZoneUtils.pre( abstractPreZoneStates.get(i-1), trace.getAction(actionCount-i), clocks), diff --git a/subprojects/xta/xta-analysis/src/test/resources/model/dipterv/ClockPredTest.xta b/subprojects/xta/xta-analysis/src/test/resources/model/dipterv/ClockPredTest.xta index cbe46eec4a..a4474d02c8 100644 --- a/subprojects/xta/xta-analysis/src/test/resources/model/dipterv/ClockPredTest.xta +++ b/subprojects/xta/xta-analysis/src/test/resources/model/dipterv/ClockPredTest.xta @@ -17,7 +17,7 @@ process P1(){ trans idle -> A {guard x <= 5; assign y = 0;}, - A -> B {guard x >= 6 ;assign a = 3;}; + A -> B {guard x >= 7 ;assign a = 3;}; } system P1; diff --git a/subprojects/xta/xta-analysis/src/test/resources/model/dipterv/bs16y.aag_4L_200.xta b/subprojects/xta/xta-analysis/src/test/resources/model/dipterv/bs16y.aag_4L_200.xta index f16bb223c9..1c5921e938 100644 --- a/subprojects/xta/xta-analysis/src/test/resources/model/dipterv/bs16y.aag_4L_200.xta +++ b/subprojects/xta/xta-analysis/src/test/resources/model/dipterv/bs16y.aag_4L_200.xta @@ -102,7 +102,7 @@ trans UpdatedLbenchr_1__out -> UpdatedLbenchr_2__out_becomes1 { guard Lbenchr_2__out == 0 && Lbenchr_2__out != !(!(((Lbenchr_2__out) && (Lbenchn13)) && !(Icontrollable_do_shift)) && !(!(!(!(!(!(!(!(!(((Lbenchr_2__out) && (Lbenchn13)) && !(Ish_0_)) && !(((Lbenchr_1__out) && (Lbenchn13)) && (Ish_0_))) && !(Ish_1_)) && !(!(!(!(!(Lbenchr_0__out) && (Lbenchn13)) && !(Ish_0_)) && !(((Lbenchr_15__out) && (Lbenchn13)) && (Ish_0_))) && (Ish_1_))) && !(Ish_2_)) && !(!(!(!(!(((Lbenchr_14__out) && (Lbenchn13)) && !(Ish_0_)) && !(((Lbenchr_13__out) && (Lbenchn13)) && (Ish_0_))) && !(Ish_1_)) && !(!(!(((Lbenchr_12__out) && (Lbenchn13)) && !(Ish_0_)) && !(((Lbenchr_11__out) && (Lbenchn13)) && (Ish_0_))) && (Ish_1_))) && (Ish_2_))) && !(Ish_3_)) && !(!(!(!(!(!(!(((Lbenchr_10__out) && (Lbenchn13)) && !(Ish_0_)) && !(((Lbenchr_9__out) && (Lbenchn13)) && (Ish_0_))) && !(Ish_1_)) && !(!(!(((Lbenchr_8__out) && (Lbenchn13)) && !(Ish_0_)) && !(((Lbenchr_7__out) && (Lbenchn13)) && (Ish_0_))) && (Ish_1_))) && !(Ish_2_)) && !(!(!(!(!(((Lbenchr_6__out) && (Lbenchn13)) && !(Ish_0_)) && !(((Lbenchr_5__out) && (Lbenchn13)) && (Ish_0_))) && !(Ish_1_)) && !(!(!(((Lbenchr_4__out) && (Lbenchn13)) && !(Ish_0_)) && !(((Lbenchr_3__out) && (Lbenchn13)) && (Ish_0_))) && (Ish_1_))) && (Ish_2_))) && (Ish_3_))) && (Icontrollable_do_shift))) && x_18 < 0; }, UpdatedLbenchr_2__out_becomes1 -> UpdatedLbenchr_2__out { guard x_18 >= 0; assign x_18:=0, Lbenchr_2__out := !(!(((Lbenchr_2__out) && (Lbenchn13)) && !(Icontrollable_do_shift)) && !(!(!(!(!(!(!(!(!(((Lbenchr_2__out) && (Lbenchn13)) && !(Ish_0_)) && !(((Lbenchr_1__out) && (Lbenchn13)) && (Ish_0_))) && !(Ish_1_)) && !(!(!(!(!(Lbenchr_0__out) && (Lbenchn13)) && !(Ish_0_)) && !(((Lbenchr_15__out) && (Lbenchn13)) && (Ish_0_))) && (Ish_1_))) && !(Ish_2_)) && !(!(!(!(!(((Lbenchr_14__out) && (Lbenchn13)) && !(Ish_0_)) && !(((Lbenchr_13__out) && (Lbenchn13)) && (Ish_0_))) && !(Ish_1_)) && !(!(!(((Lbenchr_12__out) && (Lbenchn13)) && !(Ish_0_)) && !(((Lbenchr_11__out) && (Lbenchn13)) && (Ish_0_))) && (Ish_1_))) && (Ish_2_))) && !(Ish_3_)) && !(!(!(!(!(!(!(((Lbenchr_10__out) && (Lbenchn13)) && !(Ish_0_)) && !(((Lbenchr_9__out) && (Lbenchn13)) && (Ish_0_))) && !(Ish_1_)) && !(!(!(((Lbenchr_8__out) && (Lbenchn13)) && !(Ish_0_)) && !(((Lbenchr_7__out) && (Lbenchn13)) && (Ish_0_))) && (Ish_1_))) && !(Ish_2_)) && !(!(!(!(!(((Lbenchr_6__out) && (Lbenchn13)) && !(Ish_0_)) && !(((Lbenchr_5__out) && (Lbenchn13)) && (Ish_0_))) && !(Ish_1_)) && !(!(!(((Lbenchr_4__out) && (Lbenchn13)) && !(Ish_0_)) && !(((Lbenchr_3__out) && (Lbenchn13)) && (Ish_0_))) && (Ish_1_))) && (Ish_2_))) && (Ish_3_))) && (Icontrollable_do_shift))); }, UpdatedLbenchr_2__out -> Init { guard T <= 2000; assign T:=0; }, - UpdatedLbenchr_2__out -> dead { guard T >2000; }; + UpdatedLbenchr_2__out -> dead { guard T > 2000; }; } system Circuit; 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 9b7ff78c1d..20899d538e 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 @@ -132,7 +132,7 @@ public enum Algorithm { String precGranularity = "GLOBAL"; @Parameter(names = "--maxenum", description = "Maximal number of explicitly enumerated successors (0: unlimited)") - Integer maxEnum = 10; + Integer maxEnum = 0; @Parameter(names = "--initprec", description = "Initial precision of abstraction") String initPrec = "EMPTY";