Skip to content

Commit

Permalink
collect diffs instead of constr from DBM, ZoneState.isBottom changed
Browse files Browse the repository at this point in the history
  • Loading branch information
@kopero2000
kopero2000 committed May 19, 2024
1 parent 4eb4a45 commit 4336da5
Show file tree
Hide file tree
Showing 11 changed files with 74 additions and 55 deletions.
22 changes: 17 additions & 5 deletions 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
@@ -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;
Expand Down Expand Up @@ -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;
}
Expand All @@ -70,20 +71,31 @@ public static ClockPredPrec of(final Map<Pair<VarDecl<RatType>, VarDecl<RatType>
}



private HashMap<Pair<VarDecl<RatType>, VarDecl<RatType>>, Set<Integer>> copyMap(Map<Pair<VarDecl<RatType>, VarDecl<RatType>>, Set<Integer>> mapToCopy) {
final HashMap<Pair<VarDecl<RatType>, VarDecl<RatType>>, Set<Integer>> newmap = new HashMap<>();
for(Map.Entry<Pair<VarDecl<RatType>, VarDecl<RatType>>, Set<Integer>> entry: mapToCopy.entrySet()){
final Set<Integer> copySet = new HashSet<>(entry.getValue());
newmap.put(entry.getKey(), copySet);
}
return newmap;
}
public ClockPredPrec join(final ClockPredPrec other){
//addClocks(other.getVars());
final HashMap<Pair<VarDecl<RatType>, VarDecl<RatType>>, Set<Integer>> newmap = this.copyMap(map);
for(Map.Entry<Pair<VarDecl<RatType>, VarDecl<RatType>>, Set<Integer>> 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
Expand Down
43 changes: 28 additions & 15 deletions subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/zone/DBM.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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<Pair<Pair<VarDecl<RatType>, VarDecl<RatType>>, Integer>> getDiffBounds() {
final Collection<Pair<Pair<VarDecl<RatType>, VarDecl<RatType>>, Integer>> result = Containers.createSet();

for (final VarDecl<RatType> leftVar : signature) {
for (final VarDecl<RatType> rightVar : signature) {
final int b = get(leftVar, rightVar);
final ClockConstr constr = DiffBounds.toConstr(leftVar, rightVar, b);
Pair<VarDecl<RatType>, VarDecl<RatType>> pair;
if(rightVar.equals(ZeroVar.getInstance())) {
pair = new Pair<VarDecl<RatType>, VarDecl<RatType>>(leftVar);
}
else pair = new Pair<VarDecl<RatType>, VarDecl<RatType>>(leftVar,rightVar);
if (constr instanceof TrueConstr) {
continue;
} else if (constr instanceof FalseConstr) {
return Collections.singleton(new Pair<Pair<VarDecl<RatType>, VarDecl<RatType>>, Integer>(pair, b));
} else {
result.add(new Pair<Pair<VarDecl<RatType>, VarDecl<RatType>>, Integer>(pair, b));
}
}
}

return result;
}


Expand Down
3 changes: 2 additions & 1 deletion subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/zone/ZoneState.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down Expand Up @@ -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) {
Expand Down
10 changes: 3 additions & 7 deletions ...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,13 +18,9 @@ private ClockPredTransFunc(){}
public Collection<? extends ZoneState> 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);
}
}
16 changes: 7 additions & 9 deletions ...c/main/java/hu/bme/mit/theta/xta/analysis/ClockPred/Prod2RefToProd2ExplClockPredPrec.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand All @@ -28,18 +29,15 @@ public class Prod2RefToProd2ExplClockPredPrec implements RefutationToPrec<Prod2P
public Prod2Prec<ExplPrec, ClockPredPrec> toPrec(Prod2Refutation<ItpRefutation, ZoneRefutation> 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<ClockConstr> 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<Pair<Pair<VarDecl<RatType>, VarDecl<RatType>>, Integer>> diffBounds = zone.getDbm().getDiffBounds();
for (Pair<Pair<VarDecl<RatType>, VarDecl<RatType>>, 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());
}
}
}
Expand Down
21 changes: 9 additions & 12 deletions ...c/main/java/hu/bme/mit/theta/xta/analysis/ClockPred/Prod2RefToProd2PredClockPredPrec.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand All @@ -37,15 +37,12 @@ public Prod2Prec<PredPrec, ClockPredPrec> toPrec(Prod2Refutation<ItpRefutation,
if(refutation.getRefutation2().getPruneIndex() >= 0) {
final ZoneState zone = refutation.getRefutation2().get(index);
if (!(zone.isBottom() || zone.isTop())) {
Iterator<ClockConstr> 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<Pair<Pair<VarDecl<RatType>, VarDecl<RatType>>, Integer>> diffBounds = zone.getDbm().getDiffBounds();
for (Pair<Pair<VarDecl<RatType>, VarDecl<RatType>>, 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());
}
}
}
Expand Down
3 changes: 1 addition & 2 deletions ...analysis/src/main/java/hu/bme/mit/theta/xta/analysis/ClockPred/SingleXtaTraceRefiner.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand All @@ -42,8 +43,6 @@ public final class SingleXtaTraceRefiner <S extends ExprState, P extends Prec, R

private final R emptyRefutation;



private SingleXtaTraceRefiner(XtaTraceChecker zoneTraceChecker,
ExprTraceChecker<R> exprTraceChecker,
PrecRefiner<XtaState<Prod2State<S, ZoneState>>,
Expand Down
5 changes: 4 additions & 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 @@ -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;
Expand All @@ -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;
Expand Down Expand Up @@ -63,7 +67,6 @@ public ExprTraceStatus<ZoneRefutation> check(Trace<ZoneState, XtaAction> 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),
Expand Down
2 changes: 1 addition & 1 deletion subprojects/xta/xta-analysis/src/test/resources/model/dipterv/ClockPredTest.xta
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down
2 changes: 1 addition & 1 deletion subprojects/xta/xta-analysis/src/test/resources/model/dipterv/bs16y.aag_4L_200.xta
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down
2 changes: 1 addition & 1 deletion subprojects/xta/xta-cli/src/main/java/hu/bme/mit/theta/xta/cli/XtaCli.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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";
Expand Down

0 comments on commit 4336da5

Please sign in to comment.