Browse Source

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
master
Joachim Klein 9 years ago
parent
commit
456c7be353
  1. 3
      prism/src/prism/ECComputerDefault.java

3
prism/src/prism/ECComputerDefault.java

@ -118,8 +118,7 @@ public class ECComputerDefault extends ECComputer
} }
// Filter bad transitions // Filter bad transitions
JDD.Ref(stableSet);
JDDNode stableSetTrans = maxStableSetTrans(stableSet);
JDDNode stableSetTrans = getStableTransReln(stableSet.copy());
// Find the maximal SCCs in (stableSet, stableSetTrans) // Find the maximal SCCs in (stableSet, stableSetTrans)
sccComputer = SCCComputer.createSCCComputer(this, stableSet, stableSetTrans, allDDRowVars, allDDColVars); sccComputer = SCCComputer.createSCCComputer(this, stableSet, stableSetTrans, allDDRowVars, allDDColVars);

Loading…
Cancel
Save