diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/symbolic/fixpoint/GeneralizedSaturationProvider.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/symbolic/fixpoint/GeneralizedSaturationProvider.java index 6af29c08f8..088b1b5242 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/symbolic/fixpoint/GeneralizedSaturationProvider.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/symbolic/fixpoint/GeneralizedSaturationProvider.java @@ -112,17 +112,37 @@ private MddNode saturate( // indent++; final MddStateSpaceInfo stateSpaceInfo = new MddStateSpaceInfo(variable, n); - - IntObjMapView satTemplate = new IntObjMapViews.Transforming(n, - (node, key) -> node == null ? null : terminalZeroToNull(saturate(node, - d.getDiagonal(stateSpaceInfo).get(key), - variable.getLower().orElse(null), - cache.getLower() - )) - ); - - MddNode nsat = variable.checkInNode(MddStructuralTemplate.of(satTemplate)); - + +// +// IntObjMapView satTemplate = new IntObjMapViews.Transforming(n, +// (node, key) -> node == null ? null : terminalZeroToNull(saturate(node, +// d.getDiagonal(stateSpaceInfo).get(key), +// variable.getLower().orElse(null), +// cache.getLower() +// )) +// ); +// +// MddNode nsat = variable.checkInNode(MddStructuralTemplate.of(satTemplate)); + + + MddUnsafeTemplateBuilder templateBuilder = JavaMddFactory.getDefault().createUnsafeTemplateBuilder(); + + for (IntObjCursor cFrom = n.cursor(); cFrom.moveNext(); ){ + + MddNode s = saturate(cFrom.value(), + d.getDiagonal(stateSpaceInfo).get(cFrom.key()), + variable.getLower().orElse(null), + cache.getLower() + ); + + templateBuilder.set(cFrom.key(), + terminalZeroToNull(unionChildren(templateBuilder.get(cFrom.key()), s, variable)) + ); + + } + + MddNode nsat = variable.checkInNode(MddStructuralTemplate.of(templateBuilder.buildAndReset())); + boolean changed; do {