From 456c7be353b7e3bad82510de32d8163b6d92e84d Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Thu, 13 Jul 2017 16:55:00 +0000 Subject: [PATCH] ECComputerDefault: switch from numeric to graph-based computation of transitions remaining in an EC Numeric computations (relying on sum of outgoing transitions > 1 - epsilon to detect choices that remain in the EC) are not precise, better to just do a graph-based computation. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12028 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/prism/ECComputerDefault.java | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/prism/src/prism/ECComputerDefault.java b/prism/src/prism/ECComputerDefault.java index 6fc0553d..583a14bd 100644 --- a/prism/src/prism/ECComputerDefault.java +++ b/prism/src/prism/ECComputerDefault.java @@ -118,8 +118,7 @@ public class ECComputerDefault extends ECComputer } // Filter bad transitions - JDD.Ref(stableSet); - JDDNode stableSetTrans = maxStableSetTrans(stableSet); + JDDNode stableSetTrans = getStableTransReln(stableSet.copy()); // Find the maximal SCCs in (stableSet, stableSetTrans) sccComputer = SCCComputer.createSCCComputer(this, stableSet, stableSetTrans, allDDRowVars, allDDColVars);