From fd1a5cd27b3250943a478d8fa43352fad487efc6 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Vizi=20B=C3=A9la=20=C3=81kos?= Date: Thu, 14 Mar 2024 07:57:31 +0100 Subject: [PATCH] First tests completed about clock predicate abstraction --- .../theta/analysis/algorithm/ArgBuilder.java | 1 - .../theta/analysis/zone/ClockPredPrec.java | 2 + .../mit/theta/analysis/zone/ZoneState.java | 1 + .../core/type/abstracttype/AbstractExprs.java | 5 +- .../mit/theta/core/type/inttype/IntExprs.java | 2 + .../mit/theta/core/type/inttype/IntType.java | 13 ++- .../analysis/ClockPred/ClockPredAnalysis.java | 15 +-- .../analysis/ClockPred/ClockPredInitFunc.java | 16 ++- .../ClockPred/ClockPredTransFunc.java | 4 +- .../ClockPred/SingleXtaTraceRefiner.java | 14 ++- .../analysis/ClockPred/XtaTraceChecker.java | 25 ++-- .../bme/mit/theta/xta/analysis/XtaAction.java | 47 +++++++- .../config/XtaConfigBuilder_ClockPred.java | 63 ++++++---- .../analysis/prec/XtaInitClockPredPrec.java | 108 +++++++++++++++--- .../theta/xta/analysis/Test_ClockPred.java | 2 +- .../test/resources/model/ClockPredTest.xta | 8 +- .../test/resources/model/bs16y.aag_4L_100.xta | 107 +++++++++++++++++ .../resources/property/bs16y.aag_4L_100.prop | 3 + .../property/genbuf2b3unrealy.aag_5L_300.prop | 3 + .../java/hu/bme/mit/theta/xta/XtaProcess.java | 29 ++++- 20 files changed, 386 insertions(+), 82 deletions(-) create mode 100644 subprojects/xta/xta-analysis/src/test/resources/model/bs16y.aag_4L_100.xta create mode 100644 subprojects/xta/xta-analysis/src/test/resources/property/bs16y.aag_4L_100.prop create mode 100644 subprojects/xta/xta-analysis/src/test/resources/property/genbuf2b3unrealy.aag_5L_300.prop diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/ArgBuilder.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/ArgBuilder.java index ff1c653297..d078242ee2 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/ArgBuilder.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/ArgBuilder.java @@ -88,7 +88,6 @@ public Collection> init(final ARG arg, final P prec) { public Collection> expand(final ArgNode node, final P prec) { checkNotNull(node); checkNotNull(prec); - final Collection> newSuccNodes = new ArrayList<>(); final S state = node.getState(); final Collection 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 index 8615b31377..8f42c38cfb 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 @@ -123,4 +123,6 @@ public void add(VarDecl x, VarDecl 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 index cfed6d7aba..473ac407eb 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 @@ -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> vars) { checkNotNull(valuation); final Iterable> constrainedVars = Iterables.filter(vars, v -> valuation.eval(v).isPresent()); diff --git a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/abstracttype/AbstractExprs.java b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/abstracttype/AbstractExprs.java index 564891648b..e786fc2d44 100644 --- a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/abstracttype/AbstractExprs.java +++ b/subprojects/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 op) { return IntToRatExpr.of(op); } + public static IntAddExpr Add(final Iterable> 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 index 6bd4de0561..1033f229c7 100644 --- 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, Multiplicative, Divisible, Equational, Ordered, Castable { @@ -126,7 +131,13 @@ public Expr Cast(final Expr op, f if (type instanceof RatType) { @SuppressWarnings("unchecked") final Expr result = (Expr) IntExprs.ToRat(op); return result; - } else { + } + if(type instanceof BoolType){ + IntLitExpr intLitExpr = (IntLitExpr) op; + if(intLitExpr.getValue().compareTo(BigInteger.ZERO) == 1) return (Expr) TrueExpr.getInstance(); + return (Expr) FalseExpr.getInstance(); + } + else { throw new ClassCastException("Int cannot be cast to " + type); } } diff --git a/subprojects/xta/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/ClockPred/ClockPredAnalysis.java b/subprojects/xta/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/ClockPred/ClockPredAnalysis.java index 0413381304..be3aea309f 100644 --- a/subprojects/xta/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/ClockPred/ClockPredAnalysis.java +++ b/subprojects/xta/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/ClockPred/ClockPredAnalysis.java @@ -4,22 +4,19 @@ 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 { - private static final ClockPredAnalysis INSTANCE = new ClockPredAnalysis(); - - private ClockPredAnalysis(){ + private final InitFunc 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 getPartialOrd() { return ZoneOrd.getInstance(); @@ -27,7 +24,7 @@ public PartialOrd getPartialOrd() { @Override public InitFunc getInitFunc() { - return ClockPredInitFunc.getInstance(); + return initFunc; } @Override diff --git a/subprojects/xta/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/ClockPred/ClockPredInitFunc.java b/subprojects/xta/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/ClockPred/ClockPredInitFunc.java index 93c8af881c..569af53c69 100644 --- a/subprojects/xta/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/ClockPred/ClockPredInitFunc.java +++ b/subprojects/xta/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 { + 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 getInitStates(ClockPredPrec prec) { checkNotNull(prec); - return Collections.singleton(ZoneState.zero(prec.getVars()).transform().up().build()); + Collection initstates = Collections.singleton(ZoneState.of(initdbm)); + initstates.stream().forEach(zoneState -> zoneState.clockPredicate(prec)); + return initstates; } } 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 cd8a0caada..bde377a5f3 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 @@ -19,7 +19,9 @@ public Collection 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/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 59f9024b84..db701ef7a9 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,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>, XtaAction, XtaPrec zoneStates = cexToConcretize.nodes().stream().map(ArgNode::getState).map(XtaState::getState).map(Prod2State::getState2).collect(Collectors.toList()); List actions = cexToConcretize.edges().stream().map(ArgEdge::getAction).toList(); + List zoneActions = actions; + ArrayList exprActions = new ArrayList(); + for(final XtaAction action : actions){ + + exprActions.add(action.pruneClocks()); + } List 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 zoneTrace = Trace.of(zoneStates, actions); - final Trace exprTrace = Trace.of(exprStates, actions); + + final Trace zoneTrace = Trace.of(zoneStates, zoneActions); + final Trace exprTrace = Trace.of(exprStates, exprActions); final ExprTraceStatus cexZoneStatus = zoneTraceChecker.check(zoneTrace); 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 43e5dc40a4..dbf11db58c 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 @@ -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 target; + private final DBM initDBM; + private final ZonePrec clocks; - private XtaTraceChecker(final Expr init, final Expr target, final ItpSolver solver,ZonePrec clocks ) { + private XtaTraceChecker(final Expr init, DBM initDBM, final Expr 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 init, final Expr target, final ItpSolver solver, ZonePrec clocks) { - return new XtaTraceChecker(init, target, solver, clocks); + public static XtaTraceChecker create(final Expr init, DBM initDBM, final Expr 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 check(Trace trace) final List 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 index e062fb7494..9af42df440 100644 --- 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 source) { this.clockVars = system.getClockVars(); this.sourceLocs = ImmutableList.copyOf(checkNotNull(source)); } + private XtaAction(final Collection> clocks, final List source){ + checkNotNull(clocks); + checkNotNull((source)); + this.clockVars = clocks; + this.sourceLocs=source; + } public static BasicXtaAction basic(final XtaSystem system, final List sourceLocs, final Edge edge) { return new BasicXtaAction(system, sourceLocs, edge); @@ -80,6 +83,7 @@ public static BroadcastXtaAction broadcast(final XtaSystem system, final List recvEdges) { return new BroadcastXtaAction(system, sourceLocs, emitEdge, recvEdges); } + public abstract XtaAction pruneClocks(); public Collection> 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 targetLocs; @@ -141,11 +147,24 @@ private BasicXtaAction(final XtaSystem system, final List sourceLocs, final checkArgument(matched); targetLocs = builder.build(); } + private BasicXtaAction(final Collection> clocks, final List sourceLocs, final List 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 getTargetLocs() { return targetLocs; @@ -195,6 +214,13 @@ public static final class BinaryXtaAction extends XtaAction { private volatile List stmts = null; + private BinaryXtaAction(final Collection> clocks, final List sourceLocs, final List 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 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 getTargetLocs() { return targetLocs; @@ -294,6 +326,8 @@ public static final class BroadcastXtaAction extends XtaAction { private volatile List stmts = null; +// private BroadcastXtaAction(final Collection> clocks, final List sourceLocs, final List targetLocs, +// final Edge emitEdge, final List recvEdge, List<>) private BroadcastXtaAction(final XtaSystem system, final List sourceLocs, final Edge emitEdge, List recvEdges) { super(system, sourceLocs); this.emitEdge = checkNotNull(emitEdge); @@ -385,6 +419,11 @@ public List> getNonRecvEdges() { return nonRecvEdges; } + @Override + public XtaAction pruneClocks() { + throw new UnsupportedOperationException(); + } + @Override public List getTargetLocs() { return targetLocs; diff --git a/subprojects/xta/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/config/XtaConfigBuilder_ClockPred.java b/subprojects/xta/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/config/XtaConfigBuilder_ClockPred.java index a58a2590be..9f4ae1e9a8 100644 --- a/subprojects/xta/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/config/XtaConfigBuilder_ClockPred.java +++ b/subprojects/xta/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/config/XtaConfigBuilder_ClockPred.java @@ -21,6 +21,7 @@ import hu.bme.mit.theta.analysis.prod2.Prod2State; import hu.bme.mit.theta.analysis.waitlist.PriorityWaitlist; 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; import hu.bme.mit.theta.common.logging.Logger; @@ -34,6 +35,8 @@ import hu.bme.mit.theta.xta.analysis.ClockPred.*; import hu.bme.mit.theta.xta.analysis.prec.*; +import java.util.List; + import static hu.bme.mit.theta.core.type.booltype.BoolExprs.True; public class XtaConfigBuilder_ClockPred { @@ -168,11 +171,25 @@ public XtaConfigBuilder_ClockPred pruneStrategy(final PruneStrategy pruneStrateg final XtaLts lts = XtaLts.create(xta); //final Expr negProp = xta final Expr initval = xta.getInitVal().toExpr(); + final DBM initDBM = DBM.zero(xta.getClockVars()); + List initLocs = xta.getInitLocs(); + boolean shouldApplyDelay = true; + for(XtaProcess.Loc loc : initLocs){ + if( loc.getKind().equals(XtaProcess.LocKind.COMMITTED) || loc.getKind().equals(XtaProcess.LocKind.URGENT)){ + shouldApplyDelay = false; + + break; + //csinálni egy zero dbm-et majd ezt odaadni bool helyett, a initprec-be kell rakni a <=0-t majd a clockpredprecbe + // egy vetítő függvényt (ExplPrec create state, csak valuation helyett a dbm-em kapja) + } + } + XtaInitClockPredPrec.setShouldApplyDelay(shouldApplyDelay); + if(shouldApplyDelay) initDBM.up(); if(domain == Domain.EXPL){ final Analysis, XtaAction, Prod2Prec> prod2Analysis = Prod2Analysis.create( ExplStmtAnalysis.create(abstractionSolverFactory.createSolver(), xta.getInitVal().toExpr(), maxEnum), - ClockPredAnalysis.getInstance() + ClockPredAnalysis.create(initDBM) ); final Analysis>, XtaAction, XtaPrec>> analysis = XtaAnalysis.create(xta,prod2Analysis); @@ -191,7 +208,7 @@ public XtaConfigBuilder_ClockPred pruneStrategy(final PruneStrategy pruneStrateg switch (refinement) { case FW_BIN_ITP: refiner = SingleXtaTraceRefiner.create( - XtaTraceChecker.create(initval, True(), refinementSolverFactory.createItpSolver(), ZonePrec.of(xta.getClockVars())), + XtaTraceChecker.create(initval, initDBM, True(), refinementSolverFactory.createItpSolver(), ZonePrec.of(xta.getClockVars())), ExprTraceFwBinItpChecker.create(initval, True(), refinementSolverFactory.createItpSolver()), precGranularity.createRefiner(reftoprec), pruneStrategy, logger, emptyRefutation @@ -199,7 +216,7 @@ public XtaConfigBuilder_ClockPred pruneStrategy(final PruneStrategy pruneStrateg break; case BW_BIN_ITP: refiner = SingleXtaTraceRefiner.create( - XtaTraceChecker.create(initval, True(), refinementSolverFactory.createItpSolver(), ZonePrec.of(xta.getClockVars())), + XtaTraceChecker.create(initval, initDBM, True(), refinementSolverFactory.createItpSolver(), ZonePrec.of(xta.getClockVars())), ExprTraceFwBinItpChecker.create(initval, True(), refinementSolverFactory.createItpSolver()), precGranularity.createRefiner(reftoprec), pruneStrategy, logger, emptyRefutation @@ -207,7 +224,7 @@ public XtaConfigBuilder_ClockPred pruneStrategy(final PruneStrategy pruneStrateg break; case SEQ_ITP: refiner =SingleXtaTraceRefiner.create( - XtaTraceChecker.create(initval, True(), refinementSolverFactory.createItpSolver(), ZonePrec.of(xta.getClockVars())), + XtaTraceChecker.create(initval,initDBM, True(), refinementSolverFactory.createItpSolver(), ZonePrec.of(xta.getClockVars())), ExprTraceFwBinItpChecker.create(initval, True(), refinementSolverFactory.createItpSolver()), precGranularity.createRefiner(reftoprec), pruneStrategy, logger, emptyRefutation @@ -215,7 +232,7 @@ public XtaConfigBuilder_ClockPred pruneStrategy(final PruneStrategy pruneStrateg break; case MULTI_SEQ: refiner =SingleXtaTraceRefiner.create( - XtaTraceChecker.create(initval, True(), refinementSolverFactory.createItpSolver(), ZonePrec.of(xta.getClockVars())), + XtaTraceChecker.create(initval, initDBM, True(), refinementSolverFactory.createItpSolver(), ZonePrec.of(xta.getClockVars())), ExprTraceFwBinItpChecker.create(initval, True(), refinementSolverFactory.createItpSolver()), precGranularity.createRefiner(reftoprec), pruneStrategy, logger, emptyRefutation @@ -229,7 +246,7 @@ public XtaConfigBuilder_ClockPred pruneStrategy(final PruneStrategy pruneStrateg break;*/ case UCB: refiner =SingleXtaTraceRefiner.create( - XtaTraceChecker.create(initval, True(), refinementSolverFactory.createItpSolver(), ZonePrec.of(xta.getClockVars())), + XtaTraceChecker.create(initval, initDBM, True(), refinementSolverFactory.createItpSolver(), ZonePrec.of(xta.getClockVars())), ExprTraceFwBinItpChecker.create(initval, True(), refinementSolverFactory.createItpSolver()), precGranularity.createRefiner(reftoprec), pruneStrategy, logger, emptyRefutation @@ -237,13 +254,13 @@ public XtaConfigBuilder_ClockPred pruneStrategy(final PruneStrategy pruneStrateg break; case NWT_SP: refiner =SingleXtaTraceRefiner.create( - XtaTraceChecker.create(initval, True(), refinementSolverFactory.createItpSolver(), ZonePrec.of(xta.getClockVars())), + XtaTraceChecker.create(initval, initDBM, True(), refinementSolverFactory.createItpSolver(), ZonePrec.of(xta.getClockVars())), ExprTraceNewtonChecker.create(initval, True(), refinementSolverFactory.createUCSolver()).withoutIT().withSP().withoutLV(), precGranularity.createRefiner(reftoprec), pruneStrategy, logger, emptyRefutation ); refiner = SingleXtaTraceRefiner.create( - XtaTraceChecker.create(initval, True(), refinementSolverFactory.createItpSolver(), ZonePrec.of(xta.getClockVars())), + XtaTraceChecker.create(initval, initDBM, True(), refinementSolverFactory.createItpSolver(), ZonePrec.of(xta.getClockVars())), ExprTraceNewtonChecker.create(initval, True(), refinementSolverFactory.createUCSolver()).withoutIT().withSP().withoutLV(), precGranularity.createRefiner(reftoprec ), pruneStrategy, @@ -252,7 +269,7 @@ public XtaConfigBuilder_ClockPred pruneStrategy(final PruneStrategy pruneStrateg break; case NWT_WP: refiner = SingleXtaTraceRefiner.create( - XtaTraceChecker.create(initval, True(), refinementSolverFactory.createItpSolver(), ZonePrec.of(xta.getClockVars())), + XtaTraceChecker.create(initval, initDBM, True(), refinementSolverFactory.createItpSolver(), ZonePrec.of(xta.getClockVars())), ExprTraceNewtonChecker.create(initval, True(), refinementSolverFactory.createUCSolver()).withoutIT().withWP().withoutLV(), precGranularity.createRefiner(reftoprec ), pruneStrategy, @@ -261,7 +278,7 @@ public XtaConfigBuilder_ClockPred pruneStrategy(final PruneStrategy pruneStrateg break; case NWT_SP_LV: refiner = SingleXtaTraceRefiner.create( - XtaTraceChecker.create(initval, True(), refinementSolverFactory.createItpSolver(), ZonePrec.of(xta.getClockVars())), + XtaTraceChecker.create(initval, initDBM, True(), refinementSolverFactory.createItpSolver(), ZonePrec.of(xta.getClockVars())), ExprTraceNewtonChecker.create(initval, True(), refinementSolverFactory.createUCSolver()).withoutIT().withSP().withLV(), precGranularity.createRefiner(reftoprec ), pruneStrategy, @@ -270,7 +287,7 @@ public XtaConfigBuilder_ClockPred pruneStrategy(final PruneStrategy pruneStrateg break; case NWT_WP_LV: refiner = SingleXtaTraceRefiner.create( - XtaTraceChecker.create(initval, True(), refinementSolverFactory.createItpSolver(), ZonePrec.of(xta.getClockVars())), + XtaTraceChecker.create(initval,initDBM, True(), refinementSolverFactory.createItpSolver(), ZonePrec.of(xta.getClockVars())), ExprTraceNewtonChecker.create(initval, True(), refinementSolverFactory.createUCSolver()).withoutIT().withWP().withLV(), precGranularity.createRefiner(reftoprec ), pruneStrategy, @@ -279,7 +296,7 @@ public XtaConfigBuilder_ClockPred pruneStrategy(final PruneStrategy pruneStrateg break; case NWT_IT_SP: refiner = SingleXtaTraceRefiner.create( - XtaTraceChecker.create(initval, True(), refinementSolverFactory.createItpSolver(), ZonePrec.of(xta.getClockVars())), + XtaTraceChecker.create(initval, initDBM, True(), refinementSolverFactory.createItpSolver(), ZonePrec.of(xta.getClockVars())), ExprTraceNewtonChecker.create(initval, True(), refinementSolverFactory.createUCSolver()).withIT().withSP().withoutLV(), precGranularity.createRefiner(reftoprec ), pruneStrategy, @@ -288,7 +305,7 @@ public XtaConfigBuilder_ClockPred pruneStrategy(final PruneStrategy pruneStrateg break; case NWT_IT_WP: refiner = SingleXtaTraceRefiner.create( - XtaTraceChecker.create(initval, True(), refinementSolverFactory.createItpSolver(), ZonePrec.of(xta.getClockVars())), + XtaTraceChecker.create(initval, initDBM, True(), refinementSolverFactory.createItpSolver(), ZonePrec.of(xta.getClockVars())), ExprTraceNewtonChecker.create(initval, True(), refinementSolverFactory.createUCSolver()).withIT().withWP().withoutLV(), precGranularity.createRefiner(reftoprec ), pruneStrategy, @@ -297,7 +314,7 @@ public XtaConfigBuilder_ClockPred pruneStrategy(final PruneStrategy pruneStrateg break; case NWT_IT_SP_LV: refiner = SingleXtaTraceRefiner.create( - XtaTraceChecker.create(initval, True(), refinementSolverFactory.createItpSolver(), ZonePrec.of(xta.getClockVars())), + XtaTraceChecker.create(initval, initDBM, True(), refinementSolverFactory.createItpSolver(), ZonePrec.of(xta.getClockVars())), ExprTraceNewtonChecker.create(initval, True(), refinementSolverFactory.createUCSolver()).withIT().withSP().withLV(), precGranularity.createRefiner( reftoprec ), pruneStrategy, @@ -306,7 +323,7 @@ public XtaConfigBuilder_ClockPred pruneStrategy(final PruneStrategy pruneStrateg break; case NWT_IT_WP_LV: refiner = SingleXtaTraceRefiner.create( - XtaTraceChecker.create(initval, True(), refinementSolverFactory.createItpSolver(), ZonePrec.of(xta.getClockVars())), + XtaTraceChecker.create(initval, initDBM, True(), refinementSolverFactory.createItpSolver(), ZonePrec.of(xta.getClockVars())), ExprTraceNewtonChecker.create(initval, True(), refinementSolverFactory.createUCSolver()).withIT().withWP().withLV(), precGranularity.createRefiner(reftoprec ), pruneStrategy, @@ -324,16 +341,16 @@ public XtaConfigBuilder_ClockPred pruneStrategy(final PruneStrategy pruneStrateg switch (initPrec) { case EMPTY: - prec = precGranularity.createPrec(XtaInitClockPredPrec.createEmptyProd2ExplZone(xta)); + prec = precGranularity.createPrec(XtaInitClockPredPrec.createEmptyProd2ExplClockPred(xta)); break; case ALLASSUMES: switch (precGranularity) { case LOCAL: - prec = XtaInitClockPredPrec.collectLocalProd2ExplZone(xta); + prec = XtaInitClockPredPrec.collectLocalProd2ExplClockPred(xta); break; case GLOBAL: //It returns the same as empty prec - prec = XtaInitClockPredPrec.collectGlobalProd2ExplZone(xta); + prec = XtaInitClockPredPrec.collectGlobalProd2ExplClockPred(xta); break; default: throw new UnsupportedOperationException(precGranularity + @@ -368,7 +385,7 @@ public XtaConfigBuilder_ClockPred pruneStrategy(final PruneStrategy pruneStrateg } final Analysis, XtaAction, Prod2Prec> prod2Analysis = Prod2Analysis.create( PredAnalysis.create(analysisSolver, predAbstractor, xta.getInitVal().toExpr()), - ClockPredAnalysis.getInstance() + ClockPredAnalysis.create(initDBM) ); final Analysis>, XtaAction, XtaPrec>> analysis = XtaAnalysis.create(xta,prod2Analysis); @@ -432,7 +449,7 @@ public XtaConfigBuilder_ClockPred pruneStrategy(final PruneStrategy pruneStrateg ItpRefutation emptyRefutation = ItpRefutation.emptyRefutation(); Refiner>, XtaAction, XtaPrec>> refiner = SingleXtaTraceRefiner.create( - XtaTraceChecker.create(initval, True(), refinementSolverFactory.createItpSolver(), ZonePrec.of(xta.getClockVars())), + XtaTraceChecker.create(initval,initDBM, True(), refinementSolverFactory.createItpSolver(), ZonePrec.of(xta.getClockVars())), exprTraceChecker, precGranularity.createRefiner(reftoprec), pruneStrategy, @@ -454,16 +471,16 @@ public XtaConfigBuilder_ClockPred pruneStrategy(final PruneStrategy pruneStrateg XtaPrec> prec; switch (initPrec) { case EMPTY: - prec = precGranularity.createPrec(XtaInitClockPredPrec.createEmptyProd2PredZone(xta)); + prec = precGranularity.createPrec(XtaInitClockPredPrec.createEmptyProd2PredClockPred(xta)); break; case ALLASSUMES: switch (precGranularity) { case LOCAL: - prec = XtaInitClockPredPrec.collectLocalProd2PredZone(xta); + prec = XtaInitClockPredPrec.collectLocalProd2PredClockPred(xta); break; case GLOBAL: //It returns the same as empty prec - prec = XtaInitClockPredPrec.collectGlobalProd2PredZone(xta); + prec = XtaInitClockPredPrec.collectGlobalProd2PredClockPred(xta); break; default: throw new UnsupportedOperationException(precGranularity + diff --git a/subprojects/xta/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/prec/XtaInitClockPredPrec.java b/subprojects/xta/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/prec/XtaInitClockPredPrec.java index 8d57daa85b..1c091a98ee 100644 --- a/subprojects/xta/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/prec/XtaInitClockPredPrec.java +++ b/subprojects/xta/xta-analysis/src/main/java/hu/bme/mit/theta/xta/analysis/prec/XtaInitClockPredPrec.java @@ -4,53 +4,123 @@ 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.ZonePrec; +import hu.bme.mit.theta.analysis.zone.DiffBounds; import hu.bme.mit.theta.common.container.Containers; +import hu.bme.mit.theta.core.decl.VarDecl; +import hu.bme.mit.theta.core.type.rattype.RatType; import hu.bme.mit.theta.xta.XtaProcess; import hu.bme.mit.theta.xta.XtaSystem; -import java.time.Clock; -import java.util.Collections; +import java.util.Collection; import java.util.Map; public class XtaInitClockPredPrec { - public static Prod2Prec createEmptyProd2PredZone(XtaSystem xta){ - return Prod2Prec.of(PredPrec.of(), ClockPredPrec.of(xta.getClockVars())); + private static boolean shouldApplyDelay = false; + + public static void setShouldApplyDelay(boolean _shouldApplyDelay){ + shouldApplyDelay = _shouldApplyDelay; } - public static Prod2Prec createEmptyZoneProd2PredZone(XtaSystem xta) { - return Prod2Prec.of(PredPrec.of(), ClockPredPrec.of(Collections.emptySet())); + private static ClockPredPrec addZeroToClockPredMap(ClockPredPrec prec, Collection> clocks){ + for (VarDecl clock : clocks){ + prec.add(clock, DiffBounds.Leq(0)); + } + return prec; + } + public static Prod2Prec createEmptyProd2PredClockPred(XtaSystem xta){ + PredPrec predPrec = PredPrec.of(); + ClockPredPrec clockPredPrec = ClockPredPrec.of(xta.getClockVars()); + if(!shouldApplyDelay){ + clockPredPrec = addZeroToClockPredMap(clockPredPrec, xta.getClockVars()); + } + return Prod2Prec.of(predPrec, clockPredPrec); } - public static LocalXtaPrec> collectLocalProd2PredZone(XtaSystem xta) { + + public static LocalXtaPrec> collectLocalProd2PredClockPred(XtaSystem xta) { + Map> mapping = Containers.createMap(); + for(XtaProcess proc: xta.getProcesses()){ + for (XtaProcess.Loc l : proc.getActiveClockMap().keySet()){ + + ClockPredPrec clockPredPrec = ClockPredPrec.of(xta.getClockVars()); + if(!shouldApplyDelay && xta.getInitLocs().contains(l)) clockPredPrec = addZeroToClockPredMap(clockPredPrec, xta.getClockVars()); + mapping.put(l, Prod2Prec.of(PredPrec.of(), clockPredPrec)); + } + } + ClockPredPrec clockPredPrec = ClockPredPrec.of(xta.getClockVars()); + if(!shouldApplyDelay) clockPredPrec = addZeroToClockPredMap(clockPredPrec, xta.getClockVars()); + return LocalXtaPrec.create(mapping, Prod2Prec.of(PredPrec.of(), clockPredPrec)); + } + + + public static LocalXtaPrec> collectLocalProd2PredClockPred_Active(XtaSystem xta) { Map> mapping = Containers.createMap(); for(XtaProcess proc: xta.getProcesses()){ for (XtaProcess.Loc l : proc.getActiveClockMap().keySet()){ - mapping.put(l, Prod2Prec.of(PredPrec.of(), ClockPredPrec.of(proc.getActiveClockMap().get(l)))); + ClockPredPrec clockPredPrec = ClockPredPrec.of(proc.getActiveClockMap().get(l)); + if(!shouldApplyDelay && xta.getInitLocs().contains(l)) clockPredPrec = addZeroToClockPredMap(clockPredPrec, proc.getActiveClockMap().get(l)); + + mapping.put(l, Prod2Prec.of(PredPrec.of(), clockPredPrec)); } } - return LocalXtaPrec.create(mapping, Prod2Prec.of(PredPrec.of(), ClockPredPrec.of(xta.getClockVars()))); + ClockPredPrec clockPredPrec = ClockPredPrec.of(xta.getClockVars()); + if(!shouldApplyDelay) clockPredPrec = addZeroToClockPredMap(clockPredPrec, xta.getClockVars()); + return LocalXtaPrec.create(mapping, Prod2Prec.of(PredPrec.of(), clockPredPrec)); } - public static GlobalXtaPrec> collectGlobalProd2PredZone(XtaSystem xta) { - return GlobalXtaPrec.create(Prod2Prec.of(PredPrec.of(), ClockPredPrec.of(xta.getClockVars()))); + public static GlobalXtaPrec> collectGlobalProd2PredClockPred(XtaSystem xta) { + PredPrec predPrec = PredPrec.of(); + ClockPredPrec clockPredPrec = ClockPredPrec.of(xta.getClockVars()); + if(!shouldApplyDelay){ + clockPredPrec = addZeroToClockPredMap(clockPredPrec, xta.getClockVars()); + } + return GlobalXtaPrec.create(Prod2Prec.of(predPrec, clockPredPrec)); } - public static Prod2Prec createEmptyProd2ExplZone(XtaSystem xta) { - return Prod2Prec.of(ExplPrec.empty(), ClockPredPrec.of(xta.getClockVars())); + public static Prod2Prec createEmptyProd2ExplClockPred(XtaSystem xta) { + ExplPrec explPrec = ExplPrec.empty(); + ClockPredPrec clockPredPrec = ClockPredPrec.of(xta.getClockVars()); + if(!shouldApplyDelay){ + clockPredPrec = addZeroToClockPredMap(clockPredPrec, xta.getClockVars()); + } + return Prod2Prec.of(explPrec, clockPredPrec); } - public static XtaPrec> collectLocalProd2ExplZone(XtaSystem xta) { + public static XtaPrec> collectLocalProd2ExplClockPred(XtaSystem xta) { Map> mapping = Containers.createMap(); for(XtaProcess proc: xta.getProcesses()){ for (XtaProcess.Loc l : proc.getActiveClockMap().keySet()){ - mapping.put(l, Prod2Prec.of(ExplPrec.empty(), ClockPredPrec.of(proc.getActiveClockMap().get(l)))); + ClockPredPrec clockPredPrec = ClockPredPrec.of(xta.getClockVars()); + if(!shouldApplyDelay && xta.getInitLocs().contains(l)) clockPredPrec = addZeroToClockPredMap(clockPredPrec, xta.getClockVars()); + + mapping.put(l, Prod2Prec.of(ExplPrec.empty(),clockPredPrec)); } } - return LocalXtaPrec.create(mapping, Prod2Prec.of(ExplPrec.empty(), ClockPredPrec.of(xta.getClockVars()))); + ClockPredPrec clockPredPrec = ClockPredPrec.of(xta.getClockVars()); + if(!shouldApplyDelay) clockPredPrec = addZeroToClockPredMap(clockPredPrec, xta.getClockVars()); + return LocalXtaPrec.create(mapping, Prod2Prec.of(ExplPrec.empty(), clockPredPrec)); + } + public static XtaPrec> collectLocalProd2ExplClockPred_Active(XtaSystem xta) { + Map> mapping = Containers.createMap(); + for(XtaProcess proc: xta.getProcesses()){ + for (XtaProcess.Loc l : proc.getActiveClockMap().keySet()){ + ClockPredPrec clockPredPrec = ClockPredPrec.of(proc.getActiveClockMap().get(l)); + if(!shouldApplyDelay && xta.getInitLocs().contains(l)) clockPredPrec = addZeroToClockPredMap(clockPredPrec, proc.getActiveClockMap().get(l)); + + mapping.put(l, Prod2Prec.of(ExplPrec.empty(),clockPredPrec)); + } + } + ClockPredPrec clockPredPrec = ClockPredPrec.of(xta.getClockVars()); + if(!shouldApplyDelay) clockPredPrec = addZeroToClockPredMap(clockPredPrec, xta.getClockVars()); + return LocalXtaPrec.create(mapping, Prod2Prec.of(ExplPrec.empty(), clockPredPrec)); } - public static XtaPrec> collectGlobalProd2ExplZone(XtaSystem xta) { - return GlobalXtaPrec.create(Prod2Prec.of(ExplPrec.empty(), ClockPredPrec.of(xta.getClockVars()))); + public static XtaPrec> collectGlobalProd2ExplClockPred(XtaSystem xta) { + ExplPrec explPrec = ExplPrec.empty(); + ClockPredPrec clockPredPrec = ClockPredPrec.of(xta.getClockVars()); + if(!shouldApplyDelay){ + clockPredPrec = addZeroToClockPredMap(clockPredPrec, xta.getClockVars()); + } + return GlobalXtaPrec.create(Prod2Prec.of(explPrec, clockPredPrec)); } } diff --git a/subprojects/xta/xta-analysis/src/test/java/hu/bme/mit/theta/xta/analysis/Test_ClockPred.java b/subprojects/xta/xta-analysis/src/test/java/hu/bme/mit/theta/xta/analysis/Test_ClockPred.java index a4048c0afc..5083c915ad 100644 --- a/subprojects/xta/xta-analysis/src/test/java/hu/bme/mit/theta/xta/analysis/Test_ClockPred.java +++ b/subprojects/xta/xta-analysis/src/test/java/hu/bme/mit/theta/xta/analysis/Test_ClockPred.java @@ -38,7 +38,7 @@ public void main(){ } public void check() throws Exception{ - domain = XtaConfigBuilder_ClockPred.Domain.PRED_CART; + domain = XtaConfigBuilder_ClockPred.Domain.PRED_SPLIT; refinement = XtaConfigBuilder_ClockPred.Refinement.SEQ_ITP; SolverManager.registerSolverManager(Z3SolverManager.create()); if(OsHelper.getOs().equals(OsHelper.OperatingSystem.LINUX)) { diff --git a/subprojects/xta/xta-analysis/src/test/resources/model/ClockPredTest.xta b/subprojects/xta/xta-analysis/src/test/resources/model/ClockPredTest.xta index 63e223791a..2d34c8140e 100644 --- a/subprojects/xta/xta-analysis/src/test/resources/model/ClockPredTest.xta +++ b/subprojects/xta/xta-analysis/src/test/resources/model/ClockPredTest.xta @@ -6,16 +6,20 @@ process P1(){ state idle , - A {y <= 2}, + A {y <= 1}, B; + urgent + idle; init idle; + + trans idle -> A {guard x <= 5; assign y = 0;}, - A -> B {guard x >=7 ;assign a = 3;}; + A -> B {guard x >= 7 ;assign a = 3;}; } system P1; \ No newline at end of file diff --git a/subprojects/xta/xta-analysis/src/test/resources/model/bs16y.aag_4L_100.xta b/subprojects/xta/xta-analysis/src/test/resources/model/bs16y.aag_4L_100.xta new file mode 100644 index 0000000000..3cc075b70f --- /dev/null +++ b/subprojects/xta/xta-analysis/src/test/resources/model/bs16y.aag_4L_100.xta @@ -0,0 +1,107 @@ + clock x_12; +clock x_14; +clock x_16; +clock x_18; +clock T; +bool Ish_0_; +bool Ish_1_; +bool Ish_2_; +bool Ish_3_; +bool Icontrollable_do_shift; +bool Lbenchn13; +bool Lbenchr_0__out; +bool Lbenchr_1__out; +bool Lbenchr_2__out; +bool Lbenchr_3__out; +bool Lbenchr_4__out; +bool Lbenchr_5__out; +bool Lbenchr_6__out; +bool Lbenchr_7__out; +bool Lbenchr_8__out; +bool Lbenchr_9__out; +bool Lbenchr_10__out; +bool Lbenchr_11__out; +bool Lbenchr_12__out; +bool Lbenchr_13__out; +bool Lbenchr_14__out; +bool Lbenchr_15__out; + + +process Circuit() { + +state + Init, + JustSetIsh_0_, + JustSetIsh_1_, + JustSetIsh_2_, + JustSetIsh_3_, + JustSetIcontrollable_do_shift, + UpdatedLbenchn13, + UpdatedLbenchn13_becomes0 {x_12 <= 1000}, + UpdatedLbenchn13_becomes1 {x_12 <= 1500}, + UpdatedLbenchr_0__out, + UpdatedLbenchr_0__out_becomes0 {x_14 <= 500}, + UpdatedLbenchr_0__out_becomes1 {x_14 <= 2000}, + UpdatedLbenchr_1__out, + UpdatedLbenchr_1__out_becomes0 {x_16 <= 2000}, + UpdatedLbenchr_1__out_becomes1 {x_16 <= 3000}, + UpdatedLbenchr_2__out, + UpdatedLbenchr_2__out_becomes0 {x_18 <= 3000}, + UpdatedLbenchr_2__out_becomes1 {x_18 <= 0}, + dead; +urgent + Init, + JustSetIsh_0_, + JustSetIsh_1_, + JustSetIsh_2_, + JustSetIsh_3_, + JustSetIcontrollable_do_shift, + UpdatedLbenchn13, + UpdatedLbenchr_0__out, + UpdatedLbenchr_1__out, + UpdatedLbenchr_2__out; +init Init; +trans + Init -> JustSetIsh_0_ { assign Ish_0_ := 0; }, + Init -> JustSetIsh_0_ { assign Ish_0_ := 1; }, + JustSetIsh_0_ -> JustSetIsh_1_ { assign Ish_1_ := 0; }, + JustSetIsh_0_ -> JustSetIsh_1_ { assign Ish_1_ := 1; }, + JustSetIsh_1_ -> JustSetIsh_2_ { assign Ish_2_ := 0; }, + JustSetIsh_1_ -> JustSetIsh_2_ { assign Ish_2_ := 1; }, + JustSetIsh_2_ -> JustSetIsh_3_ { assign Ish_3_ := 0; }, + JustSetIsh_2_ -> JustSetIsh_3_ { assign Ish_3_ := 1; }, + JustSetIsh_3_ -> JustSetIcontrollable_do_shift { assign Icontrollable_do_shift := 0; }, + JustSetIsh_3_ -> JustSetIcontrollable_do_shift { assign Icontrollable_do_shift := 1; }, + JustSetIcontrollable_do_shift -> UpdatedLbenchn13 { guard Lbenchn13 == true; }, + JustSetIcontrollable_do_shift -> UpdatedLbenchn13 { guard Lbenchn13 == true && Lbenchn13 != true && x_12 >= 1000; }, + JustSetIcontrollable_do_shift -> UpdatedLbenchn13 { guard Lbenchn13 == 0 && Lbenchn13 != 1 && x_12 >= 1500; }, + JustSetIcontrollable_do_shift -> UpdatedLbenchn13_becomes0 { guard Lbenchn13 == 1 && Lbenchn13 != 1 && x_12 < 1000; }, + UpdatedLbenchn13_becomes0 -> UpdatedLbenchn13 { guard x_12 >= 1000; assign x_12:=0, Lbenchn13 := 1; }, + JustSetIcontrollable_do_shift -> UpdatedLbenchn13_becomes1 { guard Lbenchn13 == 0 && Lbenchn13 != 1 && x_12 < 1500; }, + UpdatedLbenchn13_becomes1 -> UpdatedLbenchn13 { guard x_12 >= 1500; assign x_12:=0, Lbenchn13 := 1; }, + UpdatedLbenchn13 -> UpdatedLbenchr_0__out { guard Lbenchr_0__out == !(!(!(!(Lbenchr_0__out) && (Lbenchn13)) && !(Icontrollable_do_shift)) && !(!(!(!(!(!(!(!(!(!(!(Lbenchr_0__out) && (Lbenchn13)) && !(Ish_0_)) && !(((Lbenchr_15__out) && (Lbenchn13)) && (Ish_0_))) && !(Ish_1_)) && !(!(!(((Lbenchr_14__out) && (Lbenchn13)) && !(Ish_0_)) && !(((Lbenchr_13__out) && (Lbenchn13)) && (Ish_0_))) && (Ish_1_))) && !(Ish_2_)) && !(!(!(!(!(((Lbenchr_12__out) && (Lbenchn13)) && !(Ish_0_)) && !(((Lbenchr_11__out) && (Lbenchn13)) && (Ish_0_))) && !(Ish_1_)) && !(!(!(((Lbenchr_10__out) && (Lbenchn13)) && !(Ish_0_)) && !(((Lbenchr_9__out) && (Lbenchn13)) && (Ish_0_))) && (Ish_1_))) && (Ish_2_))) && !(Ish_3_)) && !(!(!(!(!(!(!(((Lbenchr_8__out) && (Lbenchn13)) && !(Ish_0_)) && !(((Lbenchr_7__out) && (Lbenchn13)) && (Ish_0_))) && !(Ish_1_)) && !(!(!(((Lbenchr_6__out) && (Lbenchn13)) && !(Ish_0_)) && !(((Lbenchr_5__out) && (Lbenchn13)) && (Ish_0_))) && (Ish_1_))) && !(Ish_2_)) && !(!(!(!(!(((Lbenchr_4__out) && (Lbenchn13)) && !(Ish_0_)) && !(((Lbenchr_3__out) && (Lbenchn13)) && (Ish_0_))) && !(Ish_1_)) && !(!(!(((Lbenchr_2__out) && (Lbenchn13)) && !(Ish_0_)) && !(((Lbenchr_1__out) && (Lbenchn13)) && (Ish_0_))) && (Ish_1_))) && (Ish_2_))) && (Ish_3_))) && (Icontrollable_do_shift))); }, + UpdatedLbenchn13 -> UpdatedLbenchr_0__out { guard Lbenchr_0__out == 1 && Lbenchr_0__out != !(!(!(!(Lbenchr_0__out) && (Lbenchn13)) && !(Icontrollable_do_shift)) && !(!(!(!(!(!(!(!(!(!(!(Lbenchr_0__out) && (Lbenchn13)) && !(Ish_0_)) && !(((Lbenchr_15__out) && (Lbenchn13)) && (Ish_0_))) && !(Ish_1_)) && !(!(!(((Lbenchr_14__out) && (Lbenchn13)) && !(Ish_0_)) && !(((Lbenchr_13__out) && (Lbenchn13)) && (Ish_0_))) && (Ish_1_))) && !(Ish_2_)) && !(!(!(!(!(((Lbenchr_12__out) && (Lbenchn13)) && !(Ish_0_)) && !(((Lbenchr_11__out) && (Lbenchn13)) && (Ish_0_))) && !(Ish_1_)) && !(!(!(((Lbenchr_10__out) && (Lbenchn13)) && !(Ish_0_)) && !(((Lbenchr_9__out) && (Lbenchn13)) && (Ish_0_))) && (Ish_1_))) && (Ish_2_))) && !(Ish_3_)) && !(!(!(!(!(!(!(((Lbenchr_8__out) && (Lbenchn13)) && !(Ish_0_)) && !(((Lbenchr_7__out) && (Lbenchn13)) && (Ish_0_))) && !(Ish_1_)) && !(!(!(((Lbenchr_6__out) && (Lbenchn13)) && !(Ish_0_)) && !(((Lbenchr_5__out) && (Lbenchn13)) && (Ish_0_))) && (Ish_1_))) && !(Ish_2_)) && !(!(!(!(!(((Lbenchr_4__out) && (Lbenchn13)) && !(Ish_0_)) && !(((Lbenchr_3__out) && (Lbenchn13)) && (Ish_0_))) && !(Ish_1_)) && !(!(!(((Lbenchr_2__out) && (Lbenchn13)) && !(Ish_0_)) && !(((Lbenchr_1__out) && (Lbenchn13)) && (Ish_0_))) && (Ish_1_))) && (Ish_2_))) && (Ish_3_))) && (Icontrollable_do_shift))) && x_14 >= 500; }, + UpdatedLbenchn13 -> UpdatedLbenchr_0__out { guard Lbenchr_0__out == 0 && Lbenchr_0__out != !(!(!(!(Lbenchr_0__out) && (Lbenchn13)) && !(Icontrollable_do_shift)) && !(!(!(!(!(!(!(!(!(!(!(Lbenchr_0__out) && (Lbenchn13)) && !(Ish_0_)) && !(((Lbenchr_15__out) && (Lbenchn13)) && (Ish_0_))) && !(Ish_1_)) && !(!(!(((Lbenchr_14__out) && (Lbenchn13)) && !(Ish_0_)) && !(((Lbenchr_13__out) && (Lbenchn13)) && (Ish_0_))) && (Ish_1_))) && !(Ish_2_)) && !(!(!(!(!(((Lbenchr_12__out) && (Lbenchn13)) && !(Ish_0_)) && !(((Lbenchr_11__out) && (Lbenchn13)) && (Ish_0_))) && !(Ish_1_)) && !(!(!(((Lbenchr_10__out) && (Lbenchn13)) && !(Ish_0_)) && !(((Lbenchr_9__out) && (Lbenchn13)) && (Ish_0_))) && (Ish_1_))) && (Ish_2_))) && !(Ish_3_)) && !(!(!(!(!(!(!(((Lbenchr_8__out) && (Lbenchn13)) && !(Ish_0_)) && !(((Lbenchr_7__out) && (Lbenchn13)) && (Ish_0_))) && !(Ish_1_)) && !(!(!(((Lbenchr_6__out) && (Lbenchn13)) && !(Ish_0_)) && !(((Lbenchr_5__out) && (Lbenchn13)) && (Ish_0_))) && (Ish_1_))) && !(Ish_2_)) && !(!(!(!(!(((Lbenchr_4__out) && (Lbenchn13)) && !(Ish_0_)) && !(((Lbenchr_3__out) && (Lbenchn13)) && (Ish_0_))) && !(Ish_1_)) && !(!(!(((Lbenchr_2__out) && (Lbenchn13)) && !(Ish_0_)) && !(((Lbenchr_1__out) && (Lbenchn13)) && (Ish_0_))) && (Ish_1_))) && (Ish_2_))) && (Ish_3_))) && (Icontrollable_do_shift))) && x_14 >= 2000; }, + UpdatedLbenchn13 -> UpdatedLbenchr_0__out_becomes0 { guard Lbenchr_0__out == 1 && Lbenchr_0__out != !(!(!(!(Lbenchr_0__out) && (Lbenchn13)) && !(Icontrollable_do_shift)) && !(!(!(!(!(!(!(!(!(!(!(Lbenchr_0__out) && (Lbenchn13)) && !(Ish_0_)) && !(((Lbenchr_15__out) && (Lbenchn13)) && (Ish_0_))) && !(Ish_1_)) && !(!(!(((Lbenchr_14__out) && (Lbenchn13)) && !(Ish_0_)) && !(((Lbenchr_13__out) && (Lbenchn13)) && (Ish_0_))) && (Ish_1_))) && !(Ish_2_)) && !(!(!(!(!(((Lbenchr_12__out) && (Lbenchn13)) && !(Ish_0_)) && !(((Lbenchr_11__out) && (Lbenchn13)) && (Ish_0_))) && !(Ish_1_)) && !(!(!(((Lbenchr_10__out) && (Lbenchn13)) && !(Ish_0_)) && !(((Lbenchr_9__out) && (Lbenchn13)) && (Ish_0_))) && (Ish_1_))) && (Ish_2_))) && !(Ish_3_)) && !(!(!(!(!(!(!(((Lbenchr_8__out) && (Lbenchn13)) && !(Ish_0_)) && !(((Lbenchr_7__out) && (Lbenchn13)) && (Ish_0_))) && !(Ish_1_)) && !(!(!(((Lbenchr_6__out) && (Lbenchn13)) && !(Ish_0_)) && !(((Lbenchr_5__out) && (Lbenchn13)) && (Ish_0_))) && (Ish_1_))) && !(Ish_2_)) && !(!(!(!(!(((Lbenchr_4__out) && (Lbenchn13)) && !(Ish_0_)) && !(((Lbenchr_3__out) && (Lbenchn13)) && (Ish_0_))) && !(Ish_1_)) && !(!(!(((Lbenchr_2__out) && (Lbenchn13)) && !(Ish_0_)) && !(((Lbenchr_1__out) && (Lbenchn13)) && (Ish_0_))) && (Ish_1_))) && (Ish_2_))) && (Ish_3_))) && (Icontrollable_do_shift))) && x_14 < 500; }, + UpdatedLbenchr_0__out_becomes0 -> UpdatedLbenchr_0__out { guard x_14 >= 500; assign x_14:=0, Lbenchr_0__out := !(!(!(!(Lbenchr_0__out) && (Lbenchn13)) && !(Icontrollable_do_shift)) && !(!(!(!(!(!(!(!(!(!(!(Lbenchr_0__out) && (Lbenchn13)) && !(Ish_0_)) && !(((Lbenchr_15__out) && (Lbenchn13)) && (Ish_0_))) && !(Ish_1_)) && !(!(!(((Lbenchr_14__out) && (Lbenchn13)) && !(Ish_0_)) && !(((Lbenchr_13__out) && (Lbenchn13)) && (Ish_0_))) && (Ish_1_))) && !(Ish_2_)) && !(!(!(!(!(((Lbenchr_12__out) && (Lbenchn13)) && !(Ish_0_)) && !(((Lbenchr_11__out) && (Lbenchn13)) && (Ish_0_))) && !(Ish_1_)) && !(!(!(((Lbenchr_10__out) && (Lbenchn13)) && !(Ish_0_)) && !(((Lbenchr_9__out) && (Lbenchn13)) && (Ish_0_))) && (Ish_1_))) && (Ish_2_))) && !(Ish_3_)) && !(!(!(!(!(!(!(((Lbenchr_8__out) && (Lbenchn13)) && !(Ish_0_)) && !(((Lbenchr_7__out) && (Lbenchn13)) && (Ish_0_))) && !(Ish_1_)) && !(!(!(((Lbenchr_6__out) && (Lbenchn13)) && !(Ish_0_)) && !(((Lbenchr_5__out) && (Lbenchn13)) && (Ish_0_))) && (Ish_1_))) && !(Ish_2_)) && !(!(!(!(!(((Lbenchr_4__out) && (Lbenchn13)) && !(Ish_0_)) && !(((Lbenchr_3__out) && (Lbenchn13)) && (Ish_0_))) && !(Ish_1_)) && !(!(!(((Lbenchr_2__out) && (Lbenchn13)) && !(Ish_0_)) && !(((Lbenchr_1__out) && (Lbenchn13)) && (Ish_0_))) && (Ish_1_))) && (Ish_2_))) && (Ish_3_))) && (Icontrollable_do_shift))); }, + UpdatedLbenchn13 -> UpdatedLbenchr_0__out_becomes1 { guard Lbenchr_0__out == 0 && Lbenchr_0__out != !(!(!(!(Lbenchr_0__out) && (Lbenchn13)) && !(Icontrollable_do_shift)) && !(!(!(!(!(!(!(!(!(!(!(Lbenchr_0__out) && (Lbenchn13)) && !(Ish_0_)) && !(((Lbenchr_15__out) && (Lbenchn13)) && (Ish_0_))) && !(Ish_1_)) && !(!(!(((Lbenchr_14__out) && (Lbenchn13)) && !(Ish_0_)) && !(((Lbenchr_13__out) && (Lbenchn13)) && (Ish_0_))) && (Ish_1_))) && !(Ish_2_)) && !(!(!(!(!(((Lbenchr_12__out) && (Lbenchn13)) && !(Ish_0_)) && !(((Lbenchr_11__out) && (Lbenchn13)) && (Ish_0_))) && !(Ish_1_)) && !(!(!(((Lbenchr_10__out) && (Lbenchn13)) && !(Ish_0_)) && !(((Lbenchr_9__out) && (Lbenchn13)) && (Ish_0_))) && (Ish_1_))) && (Ish_2_))) && !(Ish_3_)) && !(!(!(!(!(!(!(((Lbenchr_8__out) && (Lbenchn13)) && !(Ish_0_)) && !(((Lbenchr_7__out) && (Lbenchn13)) && (Ish_0_))) && !(Ish_1_)) && !(!(!(((Lbenchr_6__out) && (Lbenchn13)) && !(Ish_0_)) && !(((Lbenchr_5__out) && (Lbenchn13)) && (Ish_0_))) && (Ish_1_))) && !(Ish_2_)) && !(!(!(!(!(((Lbenchr_4__out) && (Lbenchn13)) && !(Ish_0_)) && !(((Lbenchr_3__out) && (Lbenchn13)) && (Ish_0_))) && !(Ish_1_)) && !(!(!(((Lbenchr_2__out) && (Lbenchn13)) && !(Ish_0_)) && !(((Lbenchr_1__out) && (Lbenchn13)) && (Ish_0_))) && (Ish_1_))) && (Ish_2_))) && (Ish_3_))) && (Icontrollable_do_shift))) && x_14 < 2000; }, + UpdatedLbenchr_0__out_becomes1 -> UpdatedLbenchr_0__out { guard x_14 >= 2000; assign x_14:=0, Lbenchr_0__out := !(!(!(!(Lbenchr_0__out) && (Lbenchn13)) && !(Icontrollable_do_shift)) && !(!(!(!(!(!(!(!(!(!(!(Lbenchr_0__out) && (Lbenchn13)) && !(Ish_0_)) && !(((Lbenchr_15__out) && (Lbenchn13)) && (Ish_0_))) && !(Ish_1_)) && !(!(!(((Lbenchr_14__out) && (Lbenchn13)) && !(Ish_0_)) && !(((Lbenchr_13__out) && (Lbenchn13)) && (Ish_0_))) && (Ish_1_))) && !(Ish_2_)) && !(!(!(!(!(((Lbenchr_12__out) && (Lbenchn13)) && !(Ish_0_)) && !(((Lbenchr_11__out) && (Lbenchn13)) && (Ish_0_))) && !(Ish_1_)) && !(!(!(((Lbenchr_10__out) && (Lbenchn13)) && !(Ish_0_)) && !(((Lbenchr_9__out) && (Lbenchn13)) && (Ish_0_))) && (Ish_1_))) && (Ish_2_))) && !(Ish_3_)) && !(!(!(!(!(!(!(((Lbenchr_8__out) && (Lbenchn13)) && !(Ish_0_)) && !(((Lbenchr_7__out) && (Lbenchn13)) && (Ish_0_))) && !(Ish_1_)) && !(!(!(((Lbenchr_6__out) && (Lbenchn13)) && !(Ish_0_)) && !(((Lbenchr_5__out) && (Lbenchn13)) && (Ish_0_))) && (Ish_1_))) && !(Ish_2_)) && !(!(!(!(!(((Lbenchr_4__out) && (Lbenchn13)) && !(Ish_0_)) && !(((Lbenchr_3__out) && (Lbenchn13)) && (Ish_0_))) && !(Ish_1_)) && !(!(!(((Lbenchr_2__out) && (Lbenchn13)) && !(Ish_0_)) && !(((Lbenchr_1__out) && (Lbenchn13)) && (Ish_0_))) && (Ish_1_))) && (Ish_2_))) && (Ish_3_))) && (Icontrollable_do_shift))); }, + UpdatedLbenchr_0__out -> UpdatedLbenchr_1__out { guard Lbenchr_1__out == !(!(((Lbenchr_1__out) && (Lbenchn13)) && !(Icontrollable_do_shift)) && !(!(!(!(!(!(!(!(!(((Lbenchr_1__out) && (Lbenchn13)) && !(Ish_0_)) && !(!(!(Lbenchr_0__out) && (Lbenchn13)) && (Ish_0_))) && !(Ish_1_)) && !(!(!(((Lbenchr_15__out) && (Lbenchn13)) && !(Ish_0_)) && !(((Lbenchr_14__out) && (Lbenchn13)) && (Ish_0_))) && (Ish_1_))) && !(Ish_2_)) && !(!(!(!(!(((Lbenchr_13__out) && (Lbenchn13)) && !(Ish_0_)) && !(((Lbenchr_12__out) && (Lbenchn13)) && (Ish_0_))) && !(Ish_1_)) && !(!(!(((Lbenchr_11__out) && (Lbenchn13)) && !(Ish_0_)) && !(((Lbenchr_10__out) && (Lbenchn13)) && (Ish_0_))) && (Ish_1_))) && (Ish_2_))) && !(Ish_3_)) && !(!(!(!(!(!(!(((Lbenchr_9__out) && (Lbenchn13)) && !(Ish_0_)) && !(((Lbenchr_8__out) && (Lbenchn13)) && (Ish_0_))) && !(Ish_1_)) && !(!(!(((Lbenchr_7__out) && (Lbenchn13)) && !(Ish_0_)) && !(((Lbenchr_6__out) && (Lbenchn13)) && (Ish_0_))) && (Ish_1_))) && !(Ish_2_)) && !(!(!(!(!(((Lbenchr_5__out) && (Lbenchn13)) && !(Ish_0_)) && !(((Lbenchr_4__out) && (Lbenchn13)) && (Ish_0_))) && !(Ish_1_)) && !(!(!(((Lbenchr_3__out) && (Lbenchn13)) && !(Ish_0_)) && !(((Lbenchr_2__out) && (Lbenchn13)) && (Ish_0_))) && (Ish_1_))) && (Ish_2_))) && (Ish_3_))) && (Icontrollable_do_shift))); }, + UpdatedLbenchr_0__out -> UpdatedLbenchr_1__out { guard Lbenchr_1__out == 1 && Lbenchr_1__out != !(!(((Lbenchr_1__out) && (Lbenchn13)) && !(Icontrollable_do_shift)) && !(!(!(!(!(!(!(!(!(((Lbenchr_1__out) && (Lbenchn13)) && !(Ish_0_)) && !(!(!(Lbenchr_0__out) && (Lbenchn13)) && (Ish_0_))) && !(Ish_1_)) && !(!(!(((Lbenchr_15__out) && (Lbenchn13)) && !(Ish_0_)) && !(((Lbenchr_14__out) && (Lbenchn13)) && (Ish_0_))) && (Ish_1_))) && !(Ish_2_)) && !(!(!(!(!(((Lbenchr_13__out) && (Lbenchn13)) && !(Ish_0_)) && !(((Lbenchr_12__out) && (Lbenchn13)) && (Ish_0_))) && !(Ish_1_)) && !(!(!(((Lbenchr_11__out) && (Lbenchn13)) && !(Ish_0_)) && !(((Lbenchr_10__out) && (Lbenchn13)) && (Ish_0_))) && (Ish_1_))) && (Ish_2_))) && !(Ish_3_)) && !(!(!(!(!(!(!(((Lbenchr_9__out) && (Lbenchn13)) && !(Ish_0_)) && !(((Lbenchr_8__out) && (Lbenchn13)) && (Ish_0_))) && !(Ish_1_)) && !(!(!(((Lbenchr_7__out) && (Lbenchn13)) && !(Ish_0_)) && !(((Lbenchr_6__out) && (Lbenchn13)) && (Ish_0_))) && (Ish_1_))) && !(Ish_2_)) && !(!(!(!(!(((Lbenchr_5__out) && (Lbenchn13)) && !(Ish_0_)) && !(((Lbenchr_4__out) && (Lbenchn13)) && (Ish_0_))) && !(Ish_1_)) && !(!(!(((Lbenchr_3__out) && (Lbenchn13)) && !(Ish_0_)) && !(((Lbenchr_2__out) && (Lbenchn13)) && (Ish_0_))) && (Ish_1_))) && (Ish_2_))) && (Ish_3_))) && (Icontrollable_do_shift))) && x_16 >= 2000; }, + UpdatedLbenchr_0__out -> UpdatedLbenchr_1__out { guard Lbenchr_1__out == 0 && Lbenchr_1__out != !(!(((Lbenchr_1__out) && (Lbenchn13)) && !(Icontrollable_do_shift)) && !(!(!(!(!(!(!(!(!(((Lbenchr_1__out) && (Lbenchn13)) && !(Ish_0_)) && !(!(!(Lbenchr_0__out) && (Lbenchn13)) && (Ish_0_))) && !(Ish_1_)) && !(!(!(((Lbenchr_15__out) && (Lbenchn13)) && !(Ish_0_)) && !(((Lbenchr_14__out) && (Lbenchn13)) && (Ish_0_))) && (Ish_1_))) && !(Ish_2_)) && !(!(!(!(!(((Lbenchr_13__out) && (Lbenchn13)) && !(Ish_0_)) && !(((Lbenchr_12__out) && (Lbenchn13)) && (Ish_0_))) && !(Ish_1_)) && !(!(!(((Lbenchr_11__out) && (Lbenchn13)) && !(Ish_0_)) && !(((Lbenchr_10__out) && (Lbenchn13)) && (Ish_0_))) && (Ish_1_))) && (Ish_2_))) && !(Ish_3_)) && !(!(!(!(!(!(!(((Lbenchr_9__out) && (Lbenchn13)) && !(Ish_0_)) && !(((Lbenchr_8__out) && (Lbenchn13)) && (Ish_0_))) && !(Ish_1_)) && !(!(!(((Lbenchr_7__out) && (Lbenchn13)) && !(Ish_0_)) && !(((Lbenchr_6__out) && (Lbenchn13)) && (Ish_0_))) && (Ish_1_))) && !(Ish_2_)) && !(!(!(!(!(((Lbenchr_5__out) && (Lbenchn13)) && !(Ish_0_)) && !(((Lbenchr_4__out) && (Lbenchn13)) && (Ish_0_))) && !(Ish_1_)) && !(!(!(((Lbenchr_3__out) && (Lbenchn13)) && !(Ish_0_)) && !(((Lbenchr_2__out) && (Lbenchn13)) && (Ish_0_))) && (Ish_1_))) && (Ish_2_))) && (Ish_3_))) && (Icontrollable_do_shift))) && x_16 >= 3000; }, + UpdatedLbenchr_0__out -> UpdatedLbenchr_1__out_becomes0 { guard Lbenchr_1__out == 1 && Lbenchr_1__out != !(!(((Lbenchr_1__out) && (Lbenchn13)) && !(Icontrollable_do_shift)) && !(!(!(!(!(!(!(!(!(((Lbenchr_1__out) && (Lbenchn13)) && !(Ish_0_)) && !(!(!(Lbenchr_0__out) && (Lbenchn13)) && (Ish_0_))) && !(Ish_1_)) && !(!(!(((Lbenchr_15__out) && (Lbenchn13)) && !(Ish_0_)) && !(((Lbenchr_14__out) && (Lbenchn13)) && (Ish_0_))) && (Ish_1_))) && !(Ish_2_)) && !(!(!(!(!(((Lbenchr_13__out) && (Lbenchn13)) && !(Ish_0_)) && !(((Lbenchr_12__out) && (Lbenchn13)) && (Ish_0_))) && !(Ish_1_)) && !(!(!(((Lbenchr_11__out) && (Lbenchn13)) && !(Ish_0_)) && !(((Lbenchr_10__out) && (Lbenchn13)) && (Ish_0_))) && (Ish_1_))) && (Ish_2_))) && !(Ish_3_)) && !(!(!(!(!(!(!(((Lbenchr_9__out) && (Lbenchn13)) && !(Ish_0_)) && !(((Lbenchr_8__out) && (Lbenchn13)) && (Ish_0_))) && !(Ish_1_)) && !(!(!(((Lbenchr_7__out) && (Lbenchn13)) && !(Ish_0_)) && !(((Lbenchr_6__out) && (Lbenchn13)) && (Ish_0_))) && (Ish_1_))) && !(Ish_2_)) && !(!(!(!(!(((Lbenchr_5__out) && (Lbenchn13)) && !(Ish_0_)) && !(((Lbenchr_4__out) && (Lbenchn13)) && (Ish_0_))) && !(Ish_1_)) && !(!(!(((Lbenchr_3__out) && (Lbenchn13)) && !(Ish_0_)) && !(((Lbenchr_2__out) && (Lbenchn13)) && (Ish_0_))) && (Ish_1_))) && (Ish_2_))) && (Ish_3_))) && (Icontrollable_do_shift))) && x_16 < 2000; }, + UpdatedLbenchr_1__out_becomes0 -> UpdatedLbenchr_1__out { guard x_16 >= 2000; assign x_16:=0, Lbenchr_1__out := !(!(((Lbenchr_1__out) && (Lbenchn13)) && !(Icontrollable_do_shift)) && !(!(!(!(!(!(!(!(!(((Lbenchr_1__out) && (Lbenchn13)) && !(Ish_0_)) && !(!(!(Lbenchr_0__out) && (Lbenchn13)) && (Ish_0_))) && !(Ish_1_)) && !(!(!(((Lbenchr_15__out) && (Lbenchn13)) && !(Ish_0_)) && !(((Lbenchr_14__out) && (Lbenchn13)) && (Ish_0_))) && (Ish_1_))) && !(Ish_2_)) && !(!(!(!(!(((Lbenchr_13__out) && (Lbenchn13)) && !(Ish_0_)) && !(((Lbenchr_12__out) && (Lbenchn13)) && (Ish_0_))) && !(Ish_1_)) && !(!(!(((Lbenchr_11__out) && (Lbenchn13)) && !(Ish_0_)) && !(((Lbenchr_10__out) && (Lbenchn13)) && (Ish_0_))) && (Ish_1_))) && (Ish_2_))) && !(Ish_3_)) && !(!(!(!(!(!(!(((Lbenchr_9__out) && (Lbenchn13)) && !(Ish_0_)) && !(((Lbenchr_8__out) && (Lbenchn13)) && (Ish_0_))) && !(Ish_1_)) && !(!(!(((Lbenchr_7__out) && (Lbenchn13)) && !(Ish_0_)) && !(((Lbenchr_6__out) && (Lbenchn13)) && (Ish_0_))) && (Ish_1_))) && !(Ish_2_)) && !(!(!(!(!(((Lbenchr_5__out) && (Lbenchn13)) && !(Ish_0_)) && !(((Lbenchr_4__out) && (Lbenchn13)) && (Ish_0_))) && !(Ish_1_)) && !(!(!(((Lbenchr_3__out) && (Lbenchn13)) && !(Ish_0_)) && !(((Lbenchr_2__out) && (Lbenchn13)) && (Ish_0_))) && (Ish_1_))) && (Ish_2_))) && (Ish_3_))) && (Icontrollable_do_shift))); }, + UpdatedLbenchr_0__out -> UpdatedLbenchr_1__out_becomes1 { guard Lbenchr_1__out == 0 && Lbenchr_1__out != !(!(((Lbenchr_1__out) && (Lbenchn13)) && !(Icontrollable_do_shift)) && !(!(!(!(!(!(!(!(!(((Lbenchr_1__out) && (Lbenchn13)) && !(Ish_0_)) && !(!(!(Lbenchr_0__out) && (Lbenchn13)) && (Ish_0_))) && !(Ish_1_)) && !(!(!(((Lbenchr_15__out) && (Lbenchn13)) && !(Ish_0_)) && !(((Lbenchr_14__out) && (Lbenchn13)) && (Ish_0_))) && (Ish_1_))) && !(Ish_2_)) && !(!(!(!(!(((Lbenchr_13__out) && (Lbenchn13)) && !(Ish_0_)) && !(((Lbenchr_12__out) && (Lbenchn13)) && (Ish_0_))) && !(Ish_1_)) && !(!(!(((Lbenchr_11__out) && (Lbenchn13)) && !(Ish_0_)) && !(((Lbenchr_10__out) && (Lbenchn13)) && (Ish_0_))) && (Ish_1_))) && (Ish_2_))) && !(Ish_3_)) && !(!(!(!(!(!(!(((Lbenchr_9__out) && (Lbenchn13)) && !(Ish_0_)) && !(((Lbenchr_8__out) && (Lbenchn13)) && (Ish_0_))) && !(Ish_1_)) && !(!(!(((Lbenchr_7__out) && (Lbenchn13)) && !(Ish_0_)) && !(((Lbenchr_6__out) && (Lbenchn13)) && (Ish_0_))) && (Ish_1_))) && !(Ish_2_)) && !(!(!(!(!(((Lbenchr_5__out) && (Lbenchn13)) && !(Ish_0_)) && !(((Lbenchr_4__out) && (Lbenchn13)) && (Ish_0_))) && !(Ish_1_)) && !(!(!(((Lbenchr_3__out) && (Lbenchn13)) && !(Ish_0_)) && !(((Lbenchr_2__out) && (Lbenchn13)) && (Ish_0_))) && (Ish_1_))) && (Ish_2_))) && (Ish_3_))) && (Icontrollable_do_shift))) && x_16 < 3000; }, + UpdatedLbenchr_1__out_becomes1 -> UpdatedLbenchr_1__out { guard x_16 >= 3000; assign x_16:=0, Lbenchr_1__out := !(!(((Lbenchr_1__out) && (Lbenchn13)) && !(Icontrollable_do_shift)) && !(!(!(!(!(!(!(!(!(((Lbenchr_1__out) && (Lbenchn13)) && !(Ish_0_)) && !(!(!(Lbenchr_0__out) && (Lbenchn13)) && (Ish_0_))) && !(Ish_1_)) && !(!(!(((Lbenchr_15__out) && (Lbenchn13)) && !(Ish_0_)) && !(((Lbenchr_14__out) && (Lbenchn13)) && (Ish_0_))) && (Ish_1_))) && !(Ish_2_)) && !(!(!(!(!(((Lbenchr_13__out) && (Lbenchn13)) && !(Ish_0_)) && !(((Lbenchr_12__out) && (Lbenchn13)) && (Ish_0_))) && !(Ish_1_)) && !(!(!(((Lbenchr_11__out) && (Lbenchn13)) && !(Ish_0_)) && !(((Lbenchr_10__out) && (Lbenchn13)) && (Ish_0_))) && (Ish_1_))) && (Ish_2_))) && !(Ish_3_)) && !(!(!(!(!(!(!(((Lbenchr_9__out) && (Lbenchn13)) && !(Ish_0_)) && !(((Lbenchr_8__out) && (Lbenchn13)) && (Ish_0_))) && !(Ish_1_)) && !(!(!(((Lbenchr_7__out) && (Lbenchn13)) && !(Ish_0_)) && !(((Lbenchr_6__out) && (Lbenchn13)) && (Ish_0_))) && (Ish_1_))) && !(Ish_2_)) && !(!(!(!(!(((Lbenchr_5__out) && (Lbenchn13)) && !(Ish_0_)) && !(((Lbenchr_4__out) && (Lbenchn13)) && (Ish_0_))) && !(Ish_1_)) && !(!(!(((Lbenchr_3__out) && (Lbenchn13)) && !(Ish_0_)) && !(((Lbenchr_2__out) && (Lbenchn13)) && (Ish_0_))) && (Ish_1_))) && (Ish_2_))) && (Ish_3_))) && (Icontrollable_do_shift))); }, + UpdatedLbenchr_1__out -> UpdatedLbenchr_2__out { guard 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_1__out -> UpdatedLbenchr_2__out { guard Lbenchr_2__out == 1 && 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 >= 3000; }, + UpdatedLbenchr_1__out -> UpdatedLbenchr_2__out { 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_1__out -> UpdatedLbenchr_2__out_becomes0 { guard Lbenchr_2__out == 1 && 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 < 3000; }, + UpdatedLbenchr_2__out_becomes0 -> UpdatedLbenchr_2__out { guard x_18 >= 3000; 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_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 <= 1000; assign T:=0; }, + UpdatedLbenchr_2__out -> dead { guard T >1000; }; +} + +system Circuit; \ No newline at end of file diff --git a/subprojects/xta/xta-analysis/src/test/resources/property/bs16y.aag_4L_100.prop b/subprojects/xta/xta-analysis/src/test/resources/property/bs16y.aag_4L_100.prop new file mode 100644 index 0000000000..f29774a237 --- /dev/null +++ b/subprojects/xta/xta-analysis/src/test/resources/property/bs16y.aag_4L_100.prop @@ -0,0 +1,3 @@ +prop{ + E<> Circuit_dead +} \ No newline at end of file diff --git a/subprojects/xta/xta-analysis/src/test/resources/property/genbuf2b3unrealy.aag_5L_300.prop b/subprojects/xta/xta-analysis/src/test/resources/property/genbuf2b3unrealy.aag_5L_300.prop new file mode 100644 index 0000000000..f29774a237 --- /dev/null +++ b/subprojects/xta/xta-analysis/src/test/resources/property/genbuf2b3unrealy.aag_5L_300.prop @@ -0,0 +1,3 @@ +prop{ + E<> Circuit_dead +} \ No newline at end of file diff --git a/subprojects/xta/xta/src/main/java/hu/bme/mit/theta/xta/XtaProcess.java b/subprojects/xta/xta/src/main/java/hu/bme/mit/theta/xta/XtaProcess.java index 76275dcf26..0a852a392e 100644 --- a/subprojects/xta/xta/src/main/java/hu/bme/mit/theta/xta/XtaProcess.java +++ b/subprojects/xta/xta/src/main/java/hu/bme/mit/theta/xta/XtaProcess.java @@ -31,7 +31,6 @@ import java.util.*; import java.util.stream.Collectors; -import java.util.stream.Stream; import static com.google.common.base.Preconditions.checkArgument; import static com.google.common.base.Preconditions.checkNotNull; @@ -117,17 +116,18 @@ public Edge createEdge(final Loc source, final Loc target, final Collection var : system.getDataVars()) { //count : if we find both of the location bool variable we can break the cycle if (!target.equals(source) && count < 2) { - if (var.getName().contains(target.name)) { + if (var.getName().equals("__" + target.name)) { updates.add(AssignStmt.create(var, BoolLitExpr.of(true))); count++; } - if (var.getName().contains(source.name)) { + if (var.getName().equals("__" + source.name)) { updates.add(AssignStmt.create(var, BoolLitExpr.of(false))); count++; } } else break; } } + final Edge edge = new Edge(source, target, guards, sync, updates); source.outEdges.add(edge); target.inEdges.add(edge); @@ -301,6 +301,7 @@ public final class Edge { private final Optional sync; private final List updates; + private Edge(final Loc source, final Loc target, final Collection> guards, final Optional sync, final List updates) { this.source = checkNotNull(source); @@ -309,7 +310,29 @@ private Edge(final Loc source, final Loc target, final Collection this.sync = checkNotNull(sync); this.updates = createUpdates(updates); } + private Edge(final Loc source, final Loc target, final Collection guards, + final Optional sync, final Collection updates){ + this.source = checkNotNull(source); + this.target = checkNotNull(target); + this.guards = checkNotNull(guards); + this.sync = checkNotNull(sync); + checkNotNull(updates); + this.updates = updates.stream().toList(); + } + public Edge pruneClocksFromEdge(){ + final ImmutableList.Builder guardBuilder = ImmutableList.builder(); + final ImmutableList.Builder updateBuilder = ImmutableList.builder(); + for(Guard guard : guards){ + if(guard.isDataGuard()) + guardBuilder.add(guard); + } + for(Update update : updates){ + if(update.isDataUpdate()) + updateBuilder.add(update); + } + return new Edge(source, target, guardBuilder.build(), sync, updateBuilder.build()); + } public Loc getSource() { return source; }