From 99d2139f557bd681ffca4c54c121c1f30cbd521a Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Tue, 12 Jun 2012 09:52:31 +0000 Subject: [PATCH] Add getSuccessorsIterator to explicit Model interface. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@5331 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/explicit/DTMCEmbeddedSimple.java | 12 ++++++++++++ .../explicit/DTMCFromMDPMemorylessAdversary.java | 5 +++++ prism/src/explicit/DTMCSimple.java | 6 ++++++ prism/src/explicit/DTMCUniformisedSimple.java | 6 ++++++ prism/src/explicit/Distribution.java | 8 ++++++++ prism/src/explicit/MDPSimple.java | 12 ++++++++++++ prism/src/explicit/MDPSparse.java | 14 ++++++++++++++ prism/src/explicit/Model.java | 6 ++++++ prism/src/explicit/STPGAbstrSimple.java | 14 ++++++++++++++ 9 files changed, 83 insertions(+) diff --git a/prism/src/explicit/DTMCEmbeddedSimple.java b/prism/src/explicit/DTMCEmbeddedSimple.java index c10fc071..3e466950 100644 --- a/prism/src/explicit/DTMCEmbeddedSimple.java +++ b/prism/src/explicit/DTMCEmbeddedSimple.java @@ -125,6 +125,18 @@ public class DTMCEmbeddedSimple extends DTMCExplicit return ctmc.getNumTransitions() + numExtraTransitions; } + @Override + public Iterator getSuccessorsIterator(final int s) + { + if (exitRates[s] == 0) { + List list = new ArrayList(1); + list.add(s); + return list.iterator(); + } else { + return ctmc.getSuccessorsIterator(s); + } + } + public boolean isSuccessor(int s1, int s2) { return exitRates[s1] == 0 ? (s1 == s2) : ctmc.isSuccessor(s1, s2); diff --git a/prism/src/explicit/DTMCFromMDPMemorylessAdversary.java b/prism/src/explicit/DTMCFromMDPMemorylessAdversary.java index 32fcc55d..a8996db5 100644 --- a/prism/src/explicit/DTMCFromMDPMemorylessAdversary.java +++ b/prism/src/explicit/DTMCFromMDPMemorylessAdversary.java @@ -117,6 +117,11 @@ public class DTMCFromMDPMemorylessAdversary extends DTMCExplicit throw new RuntimeException("Not implemented"); } + public Iterator getSuccessorsIterator(final int s) + { + throw new RuntimeException("Not implemented yet"); + } + public boolean isSuccessor(int s1, int s2) { throw new RuntimeException("Not implemented yet"); diff --git a/prism/src/explicit/DTMCSimple.java b/prism/src/explicit/DTMCSimple.java index f311fc7a..ec92d2b2 100644 --- a/prism/src/explicit/DTMCSimple.java +++ b/prism/src/explicit/DTMCSimple.java @@ -212,6 +212,12 @@ public class DTMCSimple extends DTMCExplicit implements ModelSimple return numTransitions; } + @Override + public Iterator getSuccessorsIterator(final int s) + { + return trans.get(s).getSupport().iterator(); + } + @Override public boolean isSuccessor(int s1, int s2) { diff --git a/prism/src/explicit/DTMCUniformisedSimple.java b/prism/src/explicit/DTMCUniformisedSimple.java index ed941e1c..b31d9177 100644 --- a/prism/src/explicit/DTMCUniformisedSimple.java +++ b/prism/src/explicit/DTMCUniformisedSimple.java @@ -134,6 +134,12 @@ public class DTMCUniformisedSimple extends DTMCExplicit return ctmc.getNumTransitions() + numExtraTransitions; } + public Iterator getSuccessorsIterator(final int s) + { + // TODO + throw new Error("Not yet supported"); + } + public boolean isSuccessor(int s1, int s2) { // TODO diff --git a/prism/src/explicit/Distribution.java b/prism/src/explicit/Distribution.java index dde467e2..6cf983f0 100644 --- a/prism/src/explicit/Distribution.java +++ b/prism/src/explicit/Distribution.java @@ -158,6 +158,14 @@ public class Distribution implements Iterable> return false; } + /** + * Get the support of the distribution. + */ + public Set getSupport() + { + return map.keySet(); + } + /** * Get an iterator over the entries of the map defining the distribution. */ diff --git a/prism/src/explicit/MDPSimple.java b/prism/src/explicit/MDPSimple.java index d1f10130..73d8c893 100644 --- a/prism/src/explicit/MDPSimple.java +++ b/prism/src/explicit/MDPSimple.java @@ -389,6 +389,18 @@ public class MDPSimple extends MDPExplicit implements ModelSimple return numTransitions; } + @Override + public Iterator getSuccessorsIterator(final int s) + { + // Need to build set to avoid duplicates + // So not necessarily the fastest method to access successors + HashSet succs = new HashSet(); + for (Distribution distr : trans.get(s)) { + succs.addAll(distr.getSupport()); + } + return succs.iterator(); + } + @Override public boolean isSuccessor(int s1, int s2) { diff --git a/prism/src/explicit/MDPSparse.java b/prism/src/explicit/MDPSparse.java index 2a00fa5f..a4be1293 100644 --- a/prism/src/explicit/MDPSparse.java +++ b/prism/src/explicit/MDPSparse.java @@ -371,6 +371,20 @@ public class MDPSparse extends MDPExplicit return numTransitions; } + @Override + public Iterator getSuccessorsIterator(final int s) + { + // Need to build set to avoid duplicates + // So not necessarily the fastest method to access successors + int start = choiceStarts[rowStarts[s]]; + int end = choiceStarts[rowStarts[s + 1]]; + HashSet succs = new HashSet(); + for (int i = start; i < end; i++) { + succs.add(cols[i]); + } + return succs.iterator(); + } + @Override public boolean isSuccessor(int s1, int s2) { diff --git a/prism/src/explicit/Model.java b/prism/src/explicit/Model.java index 29047e3c..bc713171 100644 --- a/prism/src/explicit/Model.java +++ b/prism/src/explicit/Model.java @@ -28,6 +28,7 @@ package explicit; import java.io.File; import java.util.*; +import java.util.Map.Entry; import parser.State; import parser.Values; @@ -121,6 +122,11 @@ public interface Model */ public int getNumTransitions(); + /** + * Get an iterator over the successors of state s. + */ + public Iterator getSuccessorsIterator(int s); + /** * Returns true if state s2 is a successor of state s1. */ diff --git a/prism/src/explicit/STPGAbstrSimple.java b/prism/src/explicit/STPGAbstrSimple.java index a6ea8332..44d34731 100644 --- a/prism/src/explicit/STPGAbstrSimple.java +++ b/prism/src/explicit/STPGAbstrSimple.java @@ -280,6 +280,20 @@ public class STPGAbstrSimple extends ModelExplicit implements STPG, ModelSimple return numTransitions; } + @Override + public Iterator getSuccessorsIterator(final int s) + { + // Need to build set to avoid duplicates + // So not necessarily the fastest method to access successors + HashSet succs = new HashSet(); + for (DistributionSet distrs : trans.get(s)) { + for (Distribution distr : distrs) { + succs.addAll(distr.getSupport()); + } + } + return succs.iterator(); + } + @Override public boolean isSuccessor(int s1, int s2) {