From ea9463344b847127f89f7fe4d160a0d13e14a0d1 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Fri, 5 Aug 2011 19:53:33 +0000 Subject: [PATCH] Update to (explicit) MDP interface. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3394 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/explicit/MDP.java | 12 ++++++------ prism/src/explicit/MDPSimple.java | 22 ++++++++++------------ prism/src/explicit/MDPSparse.java | 14 +++++++------- 3 files changed, 23 insertions(+), 25 deletions(-) diff --git a/prism/src/explicit/MDP.java b/prism/src/explicit/MDP.java index e38f7512..18fae9e1 100644 --- a/prism/src/explicit/MDP.java +++ b/prism/src/explicit/MDP.java @@ -37,19 +37,19 @@ import explicit.rewards.*; public interface MDP extends Model { /** - * Get the number of transitions from choice i of state s. + * Get the number of transitions from choice {@code i} of state {@code s}. */ - public double getNumTransitions(int s, int i); + public int getNumTransitions(int s, int i); /** - * Get an iterator over the transitions from choice i of state s. + * Get the action label (if any) for choice {@code i} of state {@code s}. */ - public Iterator> getTransitionsIterator(int s, int i); + public Object getAction(int s, int i); /** - * Get the action label (if any) for choice i of state s. + * Get an iterator over the transitions from choice {@code i} of state {@code s}. */ - public Object getAction(int s, int i); + public Iterator> getTransitionsIterator(int s, int i); /** * Perform a single step of precomputation algorithm Prob0, i.e., for states i in {@code subset}, diff --git a/prism/src/explicit/MDPSimple.java b/prism/src/explicit/MDPSimple.java index 027665a4..305bc911 100644 --- a/prism/src/explicit/MDPSimple.java +++ b/prism/src/explicit/MDPSimple.java @@ -598,11 +598,20 @@ public class MDPSimple extends ModelSimple implements MDP // Accessors (for MDP) @Override - public double getNumTransitions(int s, int i) + public int getNumTransitions(int s, int i) { return trans.get(s).get(i).size(); } + @Override + public Object getAction(int s, int i) + { + List list; + if (actions == null || (list = actions.get(s)) == null) + return null; + return list.get(i); + } + @Override public Iterator> getTransitionsIterator(int s, int i) { @@ -975,17 +984,6 @@ public class MDPSimple extends ModelSimple implements MDP return trans.get(s).get(i); } - /** - * Get the action (if any) for choice i of state s. - */ - public Object getAction(int s, int i) - { - List list; - if (actions == null || (list = actions.get(s)) == null) - return null; - return list.get(i); - } - /** * Get the total number of choices (distributions) over all states. */ diff --git a/prism/src/explicit/MDPSparse.java b/prism/src/explicit/MDPSparse.java index f6bd0cab..f61d797d 100644 --- a/prism/src/explicit/MDPSparse.java +++ b/prism/src/explicit/MDPSparse.java @@ -588,11 +588,17 @@ public class MDPSparse extends ModelSparse implements MDP // Accessors (for MDP) @Override - public double getNumTransitions(int s, int i) + public int getNumTransitions(int s, int i) { return choiceStarts[rowStarts[s] + i + 1] - choiceStarts[rowStarts[s] + i]; } + @Override + public Object getAction(int s, int i) + { + return actions == null ? null : actions[rowStarts[s] + i]; + } + @Override public Iterator> getTransitionsIterator(final int s, final int i) { @@ -647,12 +653,6 @@ public class MDPSparse extends ModelSparse implements MDP }; } - @Override - public Object getAction(int s, int i) - { - return actions == null ? null : actions[rowStarts[s] + i]; - } - @Override public void prob0step(BitSet subset, BitSet u, boolean forall, BitSet result) {