From 0c08af644d78f528a8d0fe8631a461e80530c731 Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Fri, 21 Jul 2017 13:14:33 +0000 Subject: [PATCH] explicit.DTMCEmbeddedSimple: simplify getTransitionsIterator, provide forEachTransition specialization git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12093 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/explicit/DTMCEmbeddedSimple.java | 26 +++++++++++++--------- 1 file changed, 15 insertions(+), 11 deletions(-) diff --git a/prism/src/explicit/DTMCEmbeddedSimple.java b/prism/src/explicit/DTMCEmbeddedSimple.java index 48dd8e44..dd2ceb69 100644 --- a/prism/src/explicit/DTMCEmbeddedSimple.java +++ b/prism/src/explicit/DTMCEmbeddedSimple.java @@ -29,8 +29,6 @@ package explicit; import java.util.*; import java.util.Map.Entry; -import common.IterableStateSet; - import explicit.rewards.MCRewards; import parser.State; import parser.Values; @@ -216,9 +214,7 @@ public class DTMCEmbeddedSimple extends DTMCExplicit { if (exitRates[s] == 0) { // return prob-1 self-loop - Map m = new TreeMap(); - m.put(s, 1.0); - return m.entrySet().iterator(); + return Collections.singletonMap(s, 1.0).entrySet().iterator(); } else { final Iterator> ctmcIterator = ctmc.getTransitionsIterator(s); @@ -256,16 +252,24 @@ public class DTMCEmbeddedSimple extends DTMCExplicit } }; } - - @Override - public void remove() - { - throw new UnsupportedOperationException(); - } }; } } + @Override + public void forEachTransition(int s, TransitionConsumer c) + { + final double er = exitRates[s]; + if (er == 0) { + // exit rate = 0 -> prob 1 self loop + c.accept(s, s, 1.0); + } else { + ctmc.forEachTransition(s, (s_,t,rate) -> { + c.accept(s_, t, rate / er); + }); + } + } + public double mvMultSingle(int s, double vect[]) { int k;