diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/symbolic/symbolicnode/expression/MddNodeNextStateDescriptor.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/symbolic/symbolicnode/expression/MddNodeNextStateDescriptor.java index 594c5fd348..6aa74fd0ef 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/symbolic/symbolicnode/expression/MddNodeNextStateDescriptor.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/symbolic/symbolicnode/expression/MddNodeNextStateDescriptor.java @@ -1,9 +1,11 @@ package hu.bme.mit.theta.analysis.algorithm.symbolic.symbolicnode.expression; +import hu.bme.mit.delta.collections.IntObjCursor; import hu.bme.mit.delta.collections.IntObjMapView; import hu.bme.mit.delta.collections.RecursiveIntObjCursor; import hu.bme.mit.delta.collections.impl.IntObjMapViews; import hu.bme.mit.delta.java.mdd.MddHandle; +import hu.bme.mit.delta.java.mdd.MddNode; import hu.bme.mit.theta.analysis.algorithm.symbolic.model.AbstractNextStateDescriptor; import hu.bme.mit.theta.analysis.algorithm.symbolic.model.StateSpaceInfo; @@ -43,16 +45,18 @@ public boolean evaluate() { @Override public IntObjMapView getDiagonal(StateSpaceInfo localStateSpace) { - return new IntObjMapViews.Transforming<>(node, (n, key) -> { + final MddNode constraint = localStateSpace.toStructuralRepresentation(); + return new ConstrainedIntObjMapView<>(new IntObjMapViews.Transforming<>(node, (n, key) -> { if(key == null) return AbstractNextStateDescriptor.terminalEmpty(); else return MddNodeNextStateDescriptor.of((MddHandle) n.get(key)); - }); + }), constraint); } @Override public IntObjMapView> getOffDiagonal(StateSpaceInfo localStateSpace) { + final MddNode constraint = localStateSpace.toStructuralRepresentation(); return new IntObjMapViews.Transforming<>(node, - outerNode -> new IntObjMapViews.Transforming<>(outerNode, n -> MddNodeNextStateDescriptor.of((MddHandle) n))); + outerNode -> new ConstrainedIntObjMapView<>(new IntObjMapViews.Transforming<>(outerNode, n -> MddNodeNextStateDescriptor.of((MddHandle) n)),constraint)); } @Override @@ -225,4 +229,25 @@ public Optional> split() { } } + + private class ConstrainedIntObjMapView extends IntObjMapViews.ForwardingBase implements IntObjMapView { + + private final IntObjMapView target; + private final IntObjMapView constraint; + + public ConstrainedIntObjMapView(IntObjMapView target, IntObjMapView constraint) { + this.target = target; + this.constraint = constraint; + } + + @Override + public IntObjMapView getForwardingTarget() { + return this.target; + } + + @Override + public IntObjCursor cursor() { + return target.cursor(constraint); + } + } }