From 521e8faae8a751f93e177097ab7c346f19c9be35 Mon Sep 17 00:00:00 2001 From: mondokm Date: Thu, 15 Feb 2024 17:43:24 +0100 Subject: [PATCH] Change to template-based iteration instead of transforming IntObjMapView --- .../GeneralizedSaturationProvider.java | 42 ++++++++++++++----- 1 file changed, 31 insertions(+), 11 deletions(-) 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 {