First tests completed about clock predicate abstraction

ftsrg · Mar 14, 2024 · fd1a5cd · fd1a5cd
1 parent 3dc717f
commit fd1a5cd
Show file tree

Hide file tree

Showing 20 changed files with 386 additions and 82 deletions.
diff --git a/...rojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/ArgBuilder.java b/...rojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/ArgBuilder.java
@@ -88,7 +88,6 @@ public Collection<ArgNode<S, A>> init(final ARG<S, A> arg, final P prec) {
 	public Collection<ArgNode<S, A>> expand(final ArgNode<S, A> node, final P prec) {
 		checkNotNull(node);
 		checkNotNull(prec);
-
 		final Collection<ArgNode<S, A>> newSuccNodes = new ArrayList<>();
 		final S state = node.getState();
 		final Collection<? extends A> actions = lts.getEnabledActionsFor(state);

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
@@ -123,4 +123,6 @@ public void add(VarDecl<RatType> x, VarDecl<RatType> y,Integer b){
         map.get(key).add(b);
 
     }
+
+
 }
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
@@ -61,6 +61,7 @@ private ZoneState(final Builder ops) {
 
 	////
 
+	public static ZoneState of(DBM dbm){return new ZoneState(dbm);}
 	public static ZoneState region(final Valuation valuation, final Collection<VarDecl<RatType>> vars) {
 		checkNotNull(valuation);
 		final Iterable<VarDecl<RatType>> constrainedVars = Iterables.filter(vars, v -> valuation.eval(v).isPresent());

diff --git a/...ects/common/core/src/main/java/hu/bme/mit/theta/core/type/abstracttype/AbstractExprs.java b/...ects/common/core/src/main/java/hu/bme/mit/theta/core/type/abstracttype/AbstractExprs.java
@@ -17,6 +17,7 @@
 
 import static com.google.common.base.Preconditions.checkArgument;
 
+import java.math.BigInteger;
 import java.util.List;
 
 import com.google.common.collect.ImmutableList;
@@ -29,6 +30,9 @@
 import hu.bme.mit.theta.core.type.anytype.Exprs;
 import hu.bme.mit.theta.core.type.anytype.IteExpr;
 import hu.bme.mit.theta.core.type.booltype.BoolType;
+import hu.bme.mit.theta.core.type.booltype.TrueExpr;
+import hu.bme.mit.theta.core.type.inttype.IntLitExpr;
+import hu.bme.mit.theta.core.type.inttype.IntType;
 
 public final class AbstractExprs {
 
@@ -283,7 +287,6 @@ private static <T extends Type, T1 extends Type, T2 extends Type, C extends Cast
 				return bind(expr1, t1Expr2);
 			}
 		}
-
 		throw new ClassCastException("Types " + expr1.getType() + " and " + expr2.getType() + " can not be unified");
 	}
 

diff --git a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/inttype/IntExprs.java b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/inttype/IntExprs.java
@@ -18,6 +18,7 @@
 import com.google.common.collect.ImmutableList;
 
 import hu.bme.mit.theta.core.type.Expr;
+import hu.bme.mit.theta.core.type.booltype.BoolType;
 
 import java.math.BigInteger;
 
@@ -46,6 +47,7 @@ public static IntToRatExpr ToRat(final Expr<IntType> op) {
 		return IntToRatExpr.of(op);
 	}
 
+
 	public static IntAddExpr Add(final Iterable<? extends Expr<IntType>> ops) {
 		return IntAddExpr.of(ops);
 	}

diff --git a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/inttype/IntType.java b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/inttype/IntType.java
@@ -18,8 +18,13 @@
 import hu.bme.mit.theta.core.type.Expr;
 import hu.bme.mit.theta.core.type.Type;
 import hu.bme.mit.theta.core.type.abstracttype.*;
+import hu.bme.mit.theta.core.type.booltype.BoolType;
+import hu.bme.mit.theta.core.type.booltype.FalseExpr;
+import hu.bme.mit.theta.core.type.booltype.TrueExpr;
 import hu.bme.mit.theta.core.type.rattype.RatType;
 
+import java.math.BigInteger;
+
 public final class IntType implements Additive<IntType>, Multiplicative<IntType>, Divisible<IntType>, Equational<IntType>, Ordered<IntType>,
 		Castable<IntType> {
 
@@ -126,7 +131,13 @@ public <TargetType extends Type> Expr<TargetType> Cast(final Expr<IntType> op, f
 		if (type instanceof RatType) {
 			@SuppressWarnings("unchecked") final Expr<TargetType> result = (Expr<TargetType>) IntExprs.ToRat(op);
 			return result;
-		} else {
+		}
+		if(type instanceof BoolType){
+			IntLitExpr intLitExpr = (IntLitExpr) op;
+			if(intLitExpr.getValue().compareTo(BigInteger.ZERO) == 1) return (Expr<TargetType>) TrueExpr.getInstance();
+			return (Expr<TargetType>) FalseExpr.getInstance();
+		}
+		else {
 			throw new ClassCastException("Int cannot be cast to " + type);
 		}
 	}

diff --git a/...xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/ClockPred/ClockPredAnalysis.java b/...xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/ClockPred/ClockPredAnalysis.java
@@ -4,30 +4,27 @@
 import hu.bme.mit.theta.analysis.InitFunc;
 import hu.bme.mit.theta.analysis.PartialOrd;
 import hu.bme.mit.theta.analysis.TransFunc;
-import hu.bme.mit.theta.analysis.zone.ClockPredPrec;
-import hu.bme.mit.theta.analysis.zone.ZoneOrd;
-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.xta.analysis.XtaAction;
 
 import java.time.Clock;
 
 public class ClockPredAnalysis implements Analysis<ZoneState,XtaAction,ClockPredPrec> {
 
-    private static final ClockPredAnalysis INSTANCE = new ClockPredAnalysis();
-
-    private ClockPredAnalysis(){
+    private final InitFunc<ZoneState, ClockPredPrec> initFunc;
 
+    private ClockPredAnalysis(DBM initDBM){
+        this.initFunc = ClockPredInitFunc.create(initDBM);
     }
-    public static ClockPredAnalysis getInstance(){return INSTANCE;}
+    public static ClockPredAnalysis create(DBM initDBM){return new ClockPredAnalysis(initDBM);}
     @Override
     public PartialOrd<ZoneState> getPartialOrd() {
         return ZoneOrd.getInstance();
     }
 
     @Override
     public InitFunc<ZoneState, ClockPredPrec> getInitFunc() {
-        return ClockPredInitFunc.getInstance();
+        return initFunc;
     }
 
     @Override

diff --git a/...xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/ClockPred/ClockPredInitFunc.java b/...xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/ClockPred/ClockPredInitFunc.java
@@ -2,6 +2,7 @@
 
 import hu.bme.mit.theta.analysis.InitFunc;
 import hu.bme.mit.theta.analysis.zone.ClockPredPrec;
+import hu.bme.mit.theta.analysis.zone.DBM;
 import hu.bme.mit.theta.analysis.zone.ZoneState;
 
 import java.util.Collection;
@@ -11,15 +12,20 @@
 
 public class ClockPredInitFunc implements InitFunc<ZoneState, ClockPredPrec> {
 
+    final DBM initdbm;
+    private ClockPredInitFunc(DBM initdbm){
+        this.initdbm = initdbm;
+    }
 
-    private static ClockPredInitFunc INSTANCE = new ClockPredInitFunc();
-    private ClockPredInitFunc(){}
-
-    static ClockPredInitFunc getInstance(){ return INSTANCE;}
+    public static ClockPredInitFunc create(DBM initdbm){
+        return new ClockPredInitFunc(initdbm);
+    }
     @Override
     public Collection<ZoneState> getInitStates(ClockPredPrec prec)
     {
         checkNotNull(prec);
-        return Collections.singleton(ZoneState.zero(prec.getVars()).transform().up().build());
+        Collection<ZoneState> initstates = Collections.singleton(ZoneState.of(initdbm));
+        initstates.stream().forEach(zoneState -> zoneState.clockPredicate(prec));
+        return initstates;
     }
 }
diff --git a/...ta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/ClockPred/ClockPredTransFunc.java b/...ta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/ClockPred/ClockPredTransFunc.java
@@ -19,7 +19,9 @@ public Collection<? extends ZoneState> getSuccStates(ZoneState state, XtaAction
 
         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

diff --git a/...analysis/src/main/java/hu/bme/mit/theta/xta/analysis/ClockPred/SingleXtaTraceRefiner.java b/...analysis/src/main/java/hu/bme/mit/theta/xta/analysis/ClockPred/SingleXtaTraceRefiner.java
@@ -20,6 +20,8 @@
 import hu.bme.mit.theta.xta.analysis.XtaState;
 import hu.bme.mit.theta.xta.analysis.prec.XtaPrec;
 
+import java.util.ArrayList;
+import java.util.Collections;
 import java.util.List;
 import java.util.Optional;
 import java.util.stream.Collectors;
@@ -74,10 +76,16 @@ public RefinerResult<XtaState<Prod2State<S, ZoneState>>, XtaAction, XtaPrec<Prod
 
         List<ZoneState> zoneStates = cexToConcretize.nodes().stream().map(ArgNode::getState).map(XtaState::getState).map(Prod2State::getState2).collect(Collectors.toList());
         List<XtaAction> actions = cexToConcretize.edges().stream().map(ArgEdge::getAction).toList();
+        List<XtaAction> zoneActions = actions;
+        ArrayList<XtaAction> exprActions = new ArrayList<XtaAction>();
+        for(final XtaAction action : actions){
+
+            exprActions.add(action.pruneClocks());
+        }
         List<S> exprStates = cexToConcretize.nodes().stream().map(ArgNode::getState).map(XtaState::getState).map(Prod2State::getState1).collect(Collectors.toList());
-        //elvesztődnek az xta state infok, a exprtrace nél amikor megadom a configba át kell adni az init valuation okat
-        final Trace<ZoneState, XtaAction> zoneTrace = Trace.of(zoneStates, actions);
-        final Trace<S, XtaAction> exprTrace = Trace.of(exprStates, actions);
+
+        final Trace<ZoneState, XtaAction> zoneTrace = Trace.of(zoneStates, zoneActions);
+        final Trace<S, XtaAction> exprTrace = Trace.of(exprStates, exprActions);
 
 
         final ExprTraceStatus<ZoneRefutation> cexZoneStatus = zoneTraceChecker.check(zoneTrace);

diff --git a/...a/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/ClockPred/XtaTraceChecker.java b/...a/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/ClockPred/XtaTraceChecker.java
@@ -8,6 +8,7 @@
 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.Prod2State;
+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;
@@ -24,6 +25,7 @@
 import hu.bme.mit.theta.xta.analysis.zone.XtaZoneUtils;
 
 import java.util.ArrayList;
+import java.util.Collections;
 import java.util.List;
 
 import static com.google.common.base.Preconditions.checkNotNull;
@@ -36,16 +38,19 @@ public class XtaTraceChecker {
 
     private final Expr<BoolType> target;
 
+    private final DBM initDBM;
+
     private final ZonePrec clocks;
-    private XtaTraceChecker(final Expr<BoolType> init, final Expr<BoolType> target, final ItpSolver solver,ZonePrec clocks ) {
+    private 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;
         this.clocks = clocks;
+        this.initDBM = initDBM;
     }
 
-    public static XtaTraceChecker create(final Expr<BoolType> init, final Expr<BoolType> target, final ItpSolver solver, ZonePrec clocks) {
-        return new XtaTraceChecker(init, target, solver, clocks);
+    public static XtaTraceChecker create(final Expr<BoolType> init, DBM initDBM, final Expr<BoolType> target, final ItpSolver solver, ZonePrec clocks) {
+        return new XtaTraceChecker(init, initDBM, target, solver, clocks);
     }
     /*
     interpoláns az utolsó zonestate dbm-e és a a konkrét között amit itt számolok ki
@@ -57,25 +62,27 @@ public ExprTraceStatus<ZoneRefutation> check(Trace<ZoneState, XtaAction> trace)
         final List<ZoneState> abstractPreZoneStates = new ArrayList<>(stateCount);
 
         abstractPreZoneStates.add( trace.getState(stateCount-1));
-        concreteZoneStates.add(trace.getState(0));
+        concreteZoneStates.add(ZoneState.of(initDBM));
 
         for(int i = 1; i < stateCount; i++){
-            concreteZoneStates.add(XtaZoneUtils.post(trace.getState(i), trace.getAction(i-1), clocks));
+            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),
                     trace.getState(stateCount-1-i)));
         }
-        //szerintem elég lenne az elsőt megnézni ahol a metszet bottom
         int maxindex = 0;
         boolean concretizable = true;
+        Collections.reverse(abstractPreZoneStates);
         for (int i = stateCount-1; i >=0; i--){
-            if(ZoneState.intersection(concreteZoneStates.get(i), abstractPreZoneStates.get(stateCount - 1 - i)).isBottom()){
-                maxindex = i; concretizable = false; break;
+            if(ZoneState.intersection(concreteZoneStates.get(i), abstractPreZoneStates.get(i)).isBottom()){
+                maxindex = i;
+                concretizable = false;
+                break;
             }
         }
         if(concretizable){
             return ExprTraceStatus.feasible(null);
         }
-        ZoneState interpolant = ZoneState.interpolant(concreteZoneStates.get(maxindex), abstractPreZoneStates.get(stateCount - 1 - maxindex));
+        ZoneState interpolant = ZoneState.interpolant(concreteZoneStates.get(maxindex), abstractPreZoneStates.get(maxindex));
         return ExprTraceStatus.infeasible(ZoneRefutation.binary(maxindex, interpolant, clocks.getVars().stream().toList() ,stateCount));
     }
 

diff --git a/subprojects/xta/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/XtaAction.java b/subprojects/xta/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/XtaAction.java
@@ -27,13 +27,10 @@
 import hu.bme.mit.theta.core.type.booltype.BoolType;
 import hu.bme.mit.theta.core.type.booltype.SmartBoolExprs;
 import hu.bme.mit.theta.core.type.rattype.RatType;
-import hu.bme.mit.theta.xta.Guard;
-import hu.bme.mit.theta.xta.Label;
-import hu.bme.mit.theta.xta.Sync;
+import hu.bme.mit.theta.xta.*;
 import hu.bme.mit.theta.xta.XtaProcess.Edge;
 import hu.bme.mit.theta.xta.XtaProcess.Loc;
 import hu.bme.mit.theta.xta.XtaProcess.LocKind;
-import hu.bme.mit.theta.xta.XtaSystem;
 
 import java.util.Collection;
 import java.util.Iterator;
@@ -66,6 +63,12 @@ private XtaAction(final XtaSystem system, final List<Loc> source) {
 		this.clockVars = system.getClockVars();
 		this.sourceLocs = ImmutableList.copyOf(checkNotNull(source));
 	}
+	private XtaAction(final Collection<VarDecl<RatType>> clocks, final List<Loc> source){
+		checkNotNull(clocks);
+		checkNotNull((source));
+		this.clockVars = clocks;
+		this.sourceLocs=source;
+	}
 
 	public static BasicXtaAction basic(final XtaSystem system, final List<Loc> sourceLocs, final Edge edge) {
 		return new BasicXtaAction(system, sourceLocs, edge);
@@ -80,6 +83,7 @@ public static BroadcastXtaAction broadcast(final XtaSystem system, final List<Lo
 											   final List<Edge> recvEdges) {
 		return new BroadcastXtaAction(system, sourceLocs, emitEdge, recvEdges);
 	}
+	public abstract XtaAction pruneClocks();
 
 	public Collection<VarDecl<RatType>> getClockVars() {
 		return clockVars;
@@ -115,6 +119,8 @@ public BroadcastXtaAction asBroadcast() {
 		throw new ClassCastException();
 	}
 
+
+
 	public static final class BasicXtaAction extends XtaAction {
 		private final Edge edge;
 		private final List<Loc> targetLocs;
@@ -141,11 +147,24 @@ private BasicXtaAction(final XtaSystem system, final List<Loc> sourceLocs, final
 			checkArgument(matched);
 			targetLocs = builder.build();
 		}
+		private BasicXtaAction(final Collection<VarDecl<RatType>> clocks, final List<Loc> sourceLocs, final List<Loc> targetLocs, final Edge edge){
+			super(clocks, sourceLocs);
+			this.edge = checkNotNull(edge);
+
+
+			this.targetLocs = checkNotNull(targetLocs);
+		}
+
 
 		public Edge getEdge() {
 			return edge;
 		}
 
+		@Override
+		public XtaAction pruneClocks() {
+			return new BasicXtaAction(getClockVars(), getSourceLocs(), getTargetLocs(), edge.pruneClocksFromEdge());
+		}
+
 		@Override
 		public List<Loc> getTargetLocs() {
 			return targetLocs;
@@ -195,6 +214,13 @@ public static final class BinaryXtaAction extends XtaAction {
 
 		private volatile List<Stmt> stmts = null;
 
+		private BinaryXtaAction(final Collection<VarDecl<RatType>> clocks, final List<Loc> sourceLocs, final List<Loc> targetLocs,
+								final Edge emitEdge, final Edge recvEdge){
+			super(clocks,sourceLocs);
+			this.emitEdge = checkNotNull(emitEdge);
+			this.recvEdge = checkNotNull(recvEdge);
+			this.targetLocs = checkNotNull(targetLocs);
+		}
 		private BinaryXtaAction(final XtaSystem system, final List<Loc> sourceLocs, final Edge emitEdge,
 								final Edge recvEdge) {
 			super(system, sourceLocs);
@@ -240,6 +266,12 @@ public Edge getRecvEdge() {
 			return recvEdge;
 		}
 
+		@Override
+		public XtaAction pruneClocks() {
+			return new BinaryXtaAction(getClockVars(), getSourceLocs(), this.targetLocs, emitEdge.pruneClocksFromEdge(),
+					recvEdge.pruneClocksFromEdge());
+		}
+
 		@Override
 		public List<Loc> getTargetLocs() {
 			return targetLocs;
@@ -294,6 +326,8 @@ public static final class BroadcastXtaAction extends XtaAction {
 
 		private volatile List<Stmt> stmts = null;
 
+//		private BroadcastXtaAction(final Collection<VarDecl<RatType>> clocks, final List<Loc> sourceLocs, final List<Loc> targetLocs,
+//								   final Edge emitEdge, final List<Edge> recvEdge, List<>)
 		private BroadcastXtaAction(final XtaSystem system, final List<Loc> sourceLocs, final Edge emitEdge, List<Edge> recvEdges) {
 			super(system, sourceLocs);
 			this.emitEdge = checkNotNull(emitEdge);
@@ -385,6 +419,11 @@ public List<Collection<Edge>> getNonRecvEdges() {
 			return nonRecvEdges;
 		}
 
+		@Override
+		public XtaAction pruneClocks() {
+			throw new UnsupportedOperationException();
+		}
+
 		@Override
 		public List<Loc> getTargetLocs() {
 			return targetLocs;