diff --git a/prism/src/automata/LTSFromDA.java b/prism/src/automata/LTSFromDA.java index 0a62288b..178033c0 100644 --- a/prism/src/automata/LTSFromDA.java +++ b/prism/src/automata/LTSFromDA.java @@ -110,6 +110,12 @@ public class LTSFromDA extends ModelExplicit implements LTS return num; } + @Override + public int getNumTransitions(int s) + { + return da.getNumEdges(s); + } + @Override public boolean isSuccessor(int s1, int s2) { diff --git a/prism/src/explicit/DTMC.java b/prism/src/explicit/DTMC.java index b936a9f8..4b58dde6 100644 --- a/prism/src/explicit/DTMC.java +++ b/prism/src/explicit/DTMC.java @@ -41,11 +41,6 @@ import explicit.rewards.MCRewards; */ public interface DTMC extends Model { - /** - * Get the number of transitions from state s. - */ - public int getNumTransitions(int s); - /** * Get an iterator over the transitions from state s. */ @@ -128,23 +123,6 @@ public interface DTMC extends Model return sum.sum; } - /** - * Get the number of transitions leaving a set of states. - *
- * Default implementation: Iterator over the states and sum the result of getNumTransitions(s). - * @param states The set of states, specified by a OfInt iterator - * @return the number of transitions - */ - public default long getNumTransitions(PrimitiveIterator.OfInt states) - { - long count = 0; - while (states.hasNext()) { - int s = states.nextInt(); - count += getNumTransitions(s); - } - return count; - } - /** * Perform a single step of precomputation algorithm Prob0 for a single state, * i.e., for the state {@code s} returns true iff there is a transition from diff --git a/prism/src/explicit/DTMCEmbeddedSimple.java b/prism/src/explicit/DTMCEmbeddedSimple.java index 717d6e92..fe079282 100644 --- a/prism/src/explicit/DTMCEmbeddedSimple.java +++ b/prism/src/explicit/DTMCEmbeddedSimple.java @@ -126,6 +126,15 @@ public class DTMCEmbeddedSimple extends DTMCExplicit return ctmc.getNumTransitions() + numExtraTransitions; } + public int getNumTransitions(int s) + { + if (exitRates[s] == 0) { + return 1; + } else { + return ctmc.getNumTransitions(s); + } + } + @Override public SuccessorsIterator getSuccessors(final int s) { @@ -201,15 +210,6 @@ public class DTMCEmbeddedSimple extends DTMCExplicit // Accessors (for DTMC) - public int getNumTransitions(int s) - { - if (exitRates[s] == 0) { - return 1; - } else { - return ctmc.getNumTransitions(s); - } - } - public Iterator> getTransitionsIterator(int s) { if (exitRates[s] == 0) { diff --git a/prism/src/explicit/DTMCFromMDPAndMDStrategy.java b/prism/src/explicit/DTMCFromMDPAndMDStrategy.java index fe9ca18e..75084191 100644 --- a/prism/src/explicit/DTMCFromMDPAndMDStrategy.java +++ b/prism/src/explicit/DTMCFromMDPAndMDStrategy.java @@ -112,13 +112,9 @@ public class DTMCFromMDPAndMDStrategy extends DTMCExplicit return mdp.getConstantValues(); } - public int getNumTransitions() + public int getNumTransitions(int s) { - int numTransitions = 0; - for (int s = 0; s < numStates; s++) - if (strat.isChoiceDefined(s)) - numTransitions += mdp.getNumTransitions(s, strat.getChoiceIndex(s)); - return numTransitions; + return strat.isChoiceDefined(s) ? mdp.getNumTransitions(s, strat.getChoiceIndex(s)) : 0; } public SuccessorsIterator getSuccessors(final int s) @@ -165,11 +161,6 @@ public class DTMCFromMDPAndMDStrategy extends DTMCExplicit // Accessors (for DTMC) - public int getNumTransitions(int s) - { - return strat.isChoiceDefined(s) ? mdp.getNumTransitions(s, strat.getChoiceIndex(s)) : 0; - } - public Iterator> getTransitionsIterator(int s) { if (strat.isChoiceDefined(s)) { diff --git a/prism/src/explicit/DTMCFromMDPMemorylessAdversary.java b/prism/src/explicit/DTMCFromMDPMemorylessAdversary.java index 6f24cab8..fd3fd51e 100644 --- a/prism/src/explicit/DTMCFromMDPMemorylessAdversary.java +++ b/prism/src/explicit/DTMCFromMDPMemorylessAdversary.java @@ -115,13 +115,9 @@ public class DTMCFromMDPMemorylessAdversary extends DTMCExplicit return mdp.getConstantValues(); } - public int getNumTransitions() + public int getNumTransitions(int s) { - int numTransitions = 0; - for (int s = 0; s < numStates; s++) - if (adv[s] >= 0) - numTransitions += mdp.getNumTransitions(s, adv[s]); - return numTransitions; + return adv[s] >= 0 ? mdp.getNumTransitions(s, adv[s]) : 0; } public SuccessorsIterator getSuccessors(final int s) @@ -168,12 +164,6 @@ public class DTMCFromMDPMemorylessAdversary extends DTMCExplicit // Accessors (for DTMC) - @Override - public int getNumTransitions(int s) - { - return adv[s] >= 0 ? mdp.getNumTransitions(s, adv[s]) : 0; - } - @Override public Iterator> getTransitionsIterator(int s) { diff --git a/prism/src/explicit/DTMCSimple.java b/prism/src/explicit/DTMCSimple.java index 7e1cdc46..4791d52d 100644 --- a/prism/src/explicit/DTMCSimple.java +++ b/prism/src/explicit/DTMCSimple.java @@ -205,6 +205,12 @@ public class DTMCSimple extends DTMCExplicit implements ModelSimple return numTransitions; } + @Override + public int getNumTransitions(int s) + { + return trans.get(s).size(); + } + /** Get an iterator over the successors of state s */ @Override public Iterator getSuccessorsIterator(final int s) @@ -259,12 +265,6 @@ public class DTMCSimple extends DTMCExplicit implements ModelSimple // Accessors (for DTMC) - @Override - public int getNumTransitions(int s) - { - return trans.get(s).size(); - } - @Override public Iterator> getTransitionsIterator(int s) { diff --git a/prism/src/explicit/DTMCSparse.java b/prism/src/explicit/DTMCSparse.java index a0f33456..c337d969 100644 --- a/prism/src/explicit/DTMCSparse.java +++ b/prism/src/explicit/DTMCSparse.java @@ -145,6 +145,12 @@ public class DTMCSparse extends DTMCExplicit return rows[numStates]; } + @Override + public int getNumTransitions(int state) + { + return rows[state + 1] - rows[state]; + } + @Override public OfInt getSuccessorsIterator(final int state) { @@ -235,12 +241,6 @@ public class DTMCSparse extends DTMCExplicit } } - @Override - public int getNumTransitions(int state) - { - return rows[state + 1] - rows[state]; - } - @Override public Iterator> getTransitionsIterator(final int state) { diff --git a/prism/src/explicit/DTMCUniformisedSimple.java b/prism/src/explicit/DTMCUniformisedSimple.java index 12770ec8..4cc7a9c0 100644 --- a/prism/src/explicit/DTMCUniformisedSimple.java +++ b/prism/src/explicit/DTMCUniformisedSimple.java @@ -164,6 +164,12 @@ public class DTMCUniformisedSimple extends DTMCExplicit return ctmc.getNumTransitions() + numExtraTransitions; } + public int getNumTransitions(int s) + { + // TODO + throw new RuntimeException("Not implemented yet"); + } + public SuccessorsIterator getSuccessors(final int s) { // TODO @@ -211,12 +217,6 @@ public class DTMCUniformisedSimple extends DTMCExplicit // Accessors (for DTMC) - public int getNumTransitions(int s) - { - // TODO - throw new RuntimeException("Not implemented yet"); - } - public Iterator> getTransitionsIterator(int s) { // TODO diff --git a/prism/src/explicit/LTSExplicit.java b/prism/src/explicit/LTSExplicit.java index 16bdd3ad..4b1958aa 100644 --- a/prism/src/explicit/LTSExplicit.java +++ b/prism/src/explicit/LTSExplicit.java @@ -109,11 +109,6 @@ public class LTSExplicit extends ModelExplicit implements LTS throw new IllegalArgumentException(); } - public int getNumTransitions(int s) - { - return getNumChoices(s); - } - @Override public boolean allSuccessorsInSet(int s, int i, BitSet set) { @@ -177,6 +172,12 @@ public class LTSExplicit extends ModelExplicit implements LTS return numTransitions; } + @Override + public int getNumTransitions(int s) + { + return getNumChoices(s); + } + @Override public void checkForDeadlocks(BitSet except) throws PrismException { diff --git a/prism/src/explicit/MDPSimple.java b/prism/src/explicit/MDPSimple.java index c803a343..e76f3bfb 100644 --- a/prism/src/explicit/MDPSimple.java +++ b/prism/src/explicit/MDPSimple.java @@ -470,6 +470,17 @@ public class MDPSimple extends MDPExplicit implements NondetModelSimple return numTransitions; } + @Override + public int getNumTransitions(int s) + { + int numTransitions = 0; + int numChoices = getNumChoices(s); + for (int j = 0; j < numChoices; j++) { + numTransitions += trans.get(s).get(j).size(); + } + return numTransitions; + } + @Override public void findDeadlocks(boolean fix) throws PrismException { diff --git a/prism/src/explicit/MDPSparse.java b/prism/src/explicit/MDPSparse.java index 4180d0df..3f0b513e 100644 --- a/prism/src/explicit/MDPSparse.java +++ b/prism/src/explicit/MDPSparse.java @@ -478,6 +478,12 @@ public class MDPSparse extends MDPExplicit return numTransitions; } + @Override + public int getNumTransitions(int s) + { + return choiceStarts[rowStarts[s + 1]] - choiceStarts[rowStarts[s]]; + } + private SuccessorsIterator colsIterator(int start, int end, boolean distinct) { return new SuccessorsIterator() { diff --git a/prism/src/explicit/Model.java b/prism/src/explicit/Model.java index 48514ae2..d363f2ce 100644 --- a/prism/src/explicit/Model.java +++ b/prism/src/explicit/Model.java @@ -32,9 +32,11 @@ import java.util.BitSet; import java.util.Collections; import java.util.Iterator; import java.util.List; +import java.util.PrimitiveIterator; import java.util.Set; import java.util.function.IntPredicate; +import common.IteratorTools; import explicit.graphviz.Decorator; import parser.State; import parser.Values; @@ -145,7 +147,40 @@ public interface Model /** * Get the total number of transitions in the model. */ - public int getNumTransitions(); + public default int getNumTransitions() + { + int numStates = getNumStates(); + int numTransitions = 0; + for (int s = 0; s < numStates; s++) { + numTransitions += getNumTransitions(s); + } + return numTransitions; + } + + /** + * Get the number of transitions from state s. + */ + public default int getNumTransitions(int s) + { + return IteratorTools.count(getSuccessorsIterator(s)); + } + + /** + * Get the number of transitions leaving a set of states. + *
+ * Default implementation: Iterator over the states and sum the result of getNumTransitions(s). + * @param states The set of states, specified by an OfInt iterator + * @return the number of transitions + */ + public default long getNumTransitions(PrimitiveIterator.OfInt states) + { + long count = 0; + while (states.hasNext()) { + int s = states.nextInt(); + count += getNumTransitions(s); + } + return count; + } /** * Get an iterator over the successors of state s. diff --git a/prism/src/explicit/ModelExplicit.java b/prism/src/explicit/ModelExplicit.java index c042635d..b498a38f 100644 --- a/prism/src/explicit/ModelExplicit.java +++ b/prism/src/explicit/ModelExplicit.java @@ -352,9 +352,6 @@ public abstract class ModelExplicit implements Model return labels.keySet(); } - @Override - public abstract int getNumTransitions(); - @Override public void checkForDeadlocks() throws PrismException { diff --git a/prism/src/explicit/NondetModel.java b/prism/src/explicit/NondetModel.java index 3c91ed2c..014af246 100644 --- a/prism/src/explicit/NondetModel.java +++ b/prism/src/explicit/NondetModel.java @@ -71,26 +71,6 @@ public interface NondetModel extends Model */ public int getNumTransitions(int s, int i); - /** - * Get the number of transitions leaving a set of states. - *
- * Default implementation: Iterate over the states s and choices i - * and sum the result of getNumTransitions(s,i). - * @param states The set of states, specified by a OfInt iterator - * @return the number of transitions - */ - public default long getNumTransitions(PrimitiveIterator.OfInt states) - { - long count = 0; - while (states.hasNext()) { - int s = states.nextInt(); - for (int choice = 0, numChoices = getNumChoices(s); choice < numChoices; choice++) { - count += getNumTransitions(s, choice); - } - } - return count; - } - /** * Check if all the successor states from choice {@code i} of state {@code s} are in the set {@code set}. * @param s The state to check diff --git a/prism/src/explicit/modelviews/DTMCView.java b/prism/src/explicit/modelviews/DTMCView.java index d65a96d9..563cdcd8 100644 --- a/prism/src/explicit/modelviews/DTMCView.java +++ b/prism/src/explicit/modelviews/DTMCView.java @@ -111,13 +111,9 @@ public abstract class DTMCView extends ModelView implements DTMC, Cloneable } @Override - public int getNumTransitions() + public int getNumTransitions(final int s) { - int numTransitions = 0; - for (int state = 0, numStates = getNumStates(); state < numStates; state++) { - numTransitions += getNumTransitions(state); - } - return numTransitions; + return IteratorTools.count(getTransitionsIterator(s)); } @Override @@ -207,12 +203,6 @@ public abstract class DTMCView extends ModelView implements DTMC, Cloneable //--- DTMC --- - @Override - public int getNumTransitions(final int state) - { - return IteratorTools.count(getTransitionsIterator(state)); - } - public static Entry> attachAction(final Entry transition, final Object action) { final Integer state = transition.getKey(); diff --git a/prism/src/explicit/modelviews/MDPView.java b/prism/src/explicit/modelviews/MDPView.java index 563006d2..f5295447 100644 --- a/prism/src/explicit/modelviews/MDPView.java +++ b/prism/src/explicit/modelviews/MDPView.java @@ -109,12 +109,11 @@ public abstract class MDPView extends ModelView implements MDP, Cloneable } @Override - public int getNumTransitions() + public int getNumTransitions(int s) { int numTransitions = 0; - for (int state = 0, numStates = getNumStates(); state < numStates; state++) { - for (int choice = 0, numChoices = getNumChoices(state); choice < numChoices; choice++) - numTransitions += getNumTransitions(state, choice); + for (int j = 0, numChoices = getNumChoices(s); j < numChoices; j++) { + numTransitions += getNumTransitions(s, j); } return numTransitions; }