diff --git a/prism/src/explicit/DTMCSimple.java b/prism/src/explicit/DTMCSimple.java index 3d5ecd89..900b02aa 100644 --- a/prism/src/explicit/DTMCSimple.java +++ b/prism/src/explicit/DTMCSimple.java @@ -238,13 +238,6 @@ public class DTMCSimple extends DTMCExplicit implements ModelSimple return (trans.get(s).containsOneOf(set)); } - @Override - public int getNumChoices(int s) - { - // Always 1 for a DTMC - return 1; - } - @Override public void findDeadlocks(boolean fix) throws PrismException { diff --git a/prism/src/explicit/Distribution.java b/prism/src/explicit/Distribution.java index 6cf983f0..be7c58f8 100644 --- a/prism/src/explicit/Distribution.java +++ b/prism/src/explicit/Distribution.java @@ -145,7 +145,7 @@ public class Distribution implements Iterable> } /** - * Returns true if all at least one index in the support of the distribution is in the set. + * Returns true if at least one index in the support of the distribution is in the set. */ public boolean containsOneOf(BitSet set) { diff --git a/prism/src/explicit/DistributionSet.java b/prism/src/explicit/DistributionSet.java index cf4ba487..55419f4b 100644 --- a/prism/src/explicit/DistributionSet.java +++ b/prism/src/explicit/DistributionSet.java @@ -37,7 +37,7 @@ import java.util.*; public class DistributionSet extends LinkedHashSet { private static final long serialVersionUID = 1L; - + public Object action; public DistributionSet(Object action) @@ -56,6 +56,32 @@ public class DistributionSet extends LinkedHashSet this.action = action; } + /** + * Returns true if all indices in the supports of all distributions are in the set. + */ + public boolean isSubsetOf(BitSet set) + { + for (Distribution itDist : this) { + if (!itDist.isSubsetOf(set)) { + return false; + } + } + return true; + } + + /** + * Returns true if at least one index in the support of some distribution is in the set. + */ + public boolean containsOneOf(BitSet set) + { + for (Distribution itDist : this) { + if (itDist.containsOneOf(set)) { + return true; + } + } + return false; + } + public String toString() { return (action == null ? "" : "\"" + action + "\":") + super.toString(); @@ -65,7 +91,7 @@ public class DistributionSet extends LinkedHashSet { return super.equals(o) && action == ((DistributionSet) o).action; } - + /** * Returns the index of the distribution {@code d}, i.e. the position in the order given by the iterator of this set * @param d the distribution to look up @@ -74,11 +100,9 @@ public class DistributionSet extends LinkedHashSet public int indexOf(Distribution d) { int i = -1; - for(Distribution itDist : this) - { + for (Distribution itDist : this) { i++; - if (itDist.equals(d)) - { + if (itDist.equals(d)) { return i; } } diff --git a/prism/src/explicit/MDP.java b/prism/src/explicit/MDP.java index 8aa1bb95..9d365b5e 100644 --- a/prism/src/explicit/MDP.java +++ b/prism/src/explicit/MDP.java @@ -37,23 +37,8 @@ import explicit.rewards.MDPRewards; /** * Interface for classes that provide (read) access to an explicit-state MDP. */ -public interface MDP extends Model +public interface MDP extends NondetModel { - /** - * Get the total number of choices (distributions) over all states. - */ - public int getNumChoices(); - - /** - * Get the maximum number of choices (distributions) in any state. - */ - public int getMaxNumChoices(); - - /** - * Get the action label (if any) for choice {@code i} of state {@code s}. - */ - public Object getAction(int s, int i); - /** * Get the number of transitions from choice {@code i} of state {@code s}. */ @@ -64,22 +49,6 @@ public interface MDP extends Model */ public Iterator> getTransitionsIterator(int s, int i); - /** - * 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 - * @param i Choice index - * @param set The set to test for inclusion - */ - public boolean allSuccessorsInSet(int s, int i, BitSet set); - - /** - * Check if some successor state from choice {@code i} of state {@code s} is in the set {@code set}. - * @param s The state to check - * @param i Choice index - * @param set The set to test for inclusion - */ - public boolean someSuccessorsInSet(int s, int i, BitSet set); - /** * Perform a single step of precomputation algorithm Prob0, i.e., for states i in {@code subset}, * set bit i of {@code result} iff, for all/some choices, diff --git a/prism/src/explicit/MDPModelChecker.java b/prism/src/explicit/MDPModelChecker.java index 68536479..32a7d257 100644 --- a/prism/src/explicit/MDPModelChecker.java +++ b/prism/src/explicit/MDPModelChecker.java @@ -435,7 +435,7 @@ public class MDPModelChecker extends ProbModelChecker // Store strategy if (genStrat) { - res.strat = new MDStrategyArray(strat); + res.strat = new MDStrategyArray(mdp, strat); } // Export adversary if (exportAdv) { diff --git a/prism/src/explicit/MDPSimple.java b/prism/src/explicit/MDPSimple.java index 36ed14c7..c657022a 100644 --- a/prism/src/explicit/MDPSimple.java +++ b/prism/src/explicit/MDPSimple.java @@ -49,7 +49,7 @@ import explicit.rewards.MDPRewards; * The model is, however, easy to manipulate. For a static model (i.e. one that does not change * after creation), consider MDPSparse, which is more efficient. */ -public class MDPSimple extends MDPExplicit implements ModelSimple +public class MDPSimple extends MDPExplicit implements NondetModelSimple { // Transition function (Steps) protected List> trans; @@ -482,12 +482,6 @@ public class MDPSimple extends MDPExplicit implements ModelSimple return false; } - @Override - public int getNumChoices(int s) - { - return trans.get(s).size(); - } - @Override public void findDeadlocks(boolean fix) throws PrismException { @@ -513,12 +507,12 @@ public class MDPSimple extends MDPExplicit implements ModelSimple } } - // Accessors (for MDP) - + // Accessors (for NondetModel) + @Override - public int getNumChoices() + public int getNumChoices(int s) { - return numDistrs; + return trans.get(s).size(); } @Override @@ -533,6 +527,12 @@ public class MDPSimple extends MDPExplicit implements ModelSimple return maxNumDistrs; } + @Override + public int getNumChoices() + { + return numDistrs; + } + @Override public Object getAction(int s, int i) { @@ -543,29 +543,31 @@ public class MDPSimple extends MDPExplicit implements ModelSimple } @Override - public int getNumTransitions(int s, int i) + public boolean allSuccessorsInSet(int s, int i, BitSet set) { - return trans.get(s).get(i).size(); + return trans.get(s).get(i).isSubsetOf(set); } - + @Override - public Iterator> getTransitionsIterator(int s, int i) + public boolean someSuccessorsInSet(int s, int i, BitSet set) { - return trans.get(s).get(i).iterator(); + return trans.get(s).get(i).containsOneOf(set); } + + // Accessors (for MDP) @Override - public boolean allSuccessorsInSet(int s, int i, BitSet set) + public int getNumTransitions(int s, int i) { - return trans.get(s).get(i).isSubsetOf(set); + return trans.get(s).get(i).size(); } - + @Override - public boolean someSuccessorsInSet(int s, int i, BitSet set) + public Iterator> getTransitionsIterator(int s, int i) { - return trans.get(s).get(i).containsOneOf(set); + return trans.get(s).get(i).iterator(); } - + @Override public void prob0step(BitSet subset, BitSet u, boolean forall, BitSet result) { diff --git a/prism/src/explicit/MDPSparse.java b/prism/src/explicit/MDPSparse.java index 54272520..53f3e020 100644 --- a/prism/src/explicit/MDPSparse.java +++ b/prism/src/explicit/MDPSparse.java @@ -453,12 +453,6 @@ public class MDPSparse extends MDPExplicit return false; } - @Override - public int getNumChoices(int s) - { - return rowStarts[s + 1] - rowStarts[s]; - } - @Override public void findDeadlocks(boolean fix) throws PrismException { @@ -482,12 +476,12 @@ public class MDPSparse extends MDPExplicit } } - // Accessors (for MDP) + // Accessors (for NondetModel) @Override - public int getNumChoices() + public int getNumChoices(int s) { - return numDistrs; + return rowStarts[s + 1] - rowStarts[s]; } @Override @@ -496,12 +490,52 @@ public class MDPSparse extends MDPExplicit return maxNumDistrs; } + @Override + public int getNumChoices() + { + return numDistrs; + } + @Override public Object getAction(int s, int i) { return actions == null ? null : actions[rowStarts[s] + i]; } + @Override + public boolean allSuccessorsInSet(int s, int i, BitSet set) + { + int j, k, l2, h2; + j = rowStarts[s] + i; + l2 = choiceStarts[j]; + h2 = choiceStarts[j + 1]; + for (k = l2; k < h2; k++) { + // Assume that only non-zero entries are stored + if (!set.get(cols[k])) { + return false; + } + } + return true; + } + + @Override + public boolean someSuccessorsInSet(int s, int i, BitSet set) + { + int j, k, l2, h2; + j = rowStarts[s] + i; + l2 = choiceStarts[j]; + h2 = choiceStarts[j + 1]; + for (k = l2; k < h2; k++) { + // Assume that only non-zero entries are stored + if (set.get(cols[k])) { + return true; + } + } + return false; + } + + // Accessors (for MDP) + @Override public int getNumTransitions(int s, int i) { @@ -562,38 +596,6 @@ public class MDPSparse extends MDPExplicit }; } - @Override - public boolean allSuccessorsInSet(int s, int i, BitSet set) - { - int j, k, l2, h2; - j = rowStarts[s] + i; - l2 = choiceStarts[j]; - h2 = choiceStarts[j + 1]; - for (k = l2; k < h2; k++) { - // Assume that only non-zero entries are stored - if (!set.get(cols[k])) { - return false; - } - } - return true; - } - - @Override - public boolean someSuccessorsInSet(int s, int i, BitSet set) - { - int j, k, l2, h2; - j = rowStarts[s] + i; - l2 = choiceStarts[j]; - h2 = choiceStarts[j + 1]; - for (k = l2; k < h2; k++) { - // Assume that only non-zero entries are stored - if (set.get(cols[k])) { - return true; - } - } - return false; - } - @Override public void prob0step(BitSet subset, BitSet u, boolean forall, BitSet result) { diff --git a/prism/src/explicit/Model.java b/prism/src/explicit/Model.java index d5e8f565..744216c3 100644 --- a/prism/src/explicit/Model.java +++ b/prism/src/explicit/Model.java @@ -147,11 +147,6 @@ public interface Model */ public boolean someSuccessorsInSet(int s, BitSet set); - /** - * Get the number of nondeterministic choices in state s. - */ - public int getNumChoices(int s); - /** * Find all deadlock states and store this information in the model. * If requested (if fix=true) and if needed (i.e. for DTMCs/CTMCs), diff --git a/prism/src/explicit/ModelExplicit.java b/prism/src/explicit/ModelExplicit.java index 160cd56e..7a9b6e5e 100644 --- a/prism/src/explicit/ModelExplicit.java +++ b/prism/src/explicit/ModelExplicit.java @@ -238,9 +238,6 @@ public abstract class ModelExplicit implements Model @Override public abstract boolean isSuccessor(int s1, int s2); - @Override - public abstract int getNumChoices(int s); - @Override public void checkForDeadlocks() throws PrismException { diff --git a/prism/src/explicit/NondetModel.java b/prism/src/explicit/NondetModel.java new file mode 100644 index 00000000..eb7a9354 --- /dev/null +++ b/prism/src/explicit/NondetModel.java @@ -0,0 +1,73 @@ +//============================================================================== +// +// Copyright (c) 2002- +// Authors: +// * Dave Parker (University of Birmingham/Oxford) +// +//------------------------------------------------------------------------------ +// +// This file is part of PRISM. +// +// PRISM is free software; you can redistribute it and/or modify +// it under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 2 of the License, or +// (at your option) any later version. +// +// PRISM is distributed in the hope that it will be useful, +// but WITHOUT ANY WARRANTY; without even the implied warranty of +// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +// GNU General Public License for more details. +// +// You should have received a copy of the GNU General Public License +// along with PRISM; if not, write to the Free Software Foundation, +// Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA +// +//============================================================================== + +package explicit; + +import java.util.BitSet; + +/** + * Interface for (abstract) classes that provide (read-only) access to an explicit-state model with nondeterminism. + */ +public interface NondetModel extends Model +{ + // Accessors + + /** + * Get the number of nondeterministic choices in state s. + */ + public int getNumChoices(int s); + + /** + * Get the maximum number of nondeterministic choices in any state. + */ + public int getMaxNumChoices(); + + /** + * Get the total number of nondeterministic choices over all states. + */ + public int getNumChoices(); + + /** + * Get the action label (if any) for choice {@code i} of state {@code s}. + */ + public Object getAction(int s, int i); + + /** + * 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 + * @param i Choice index + * @param set The set to test for inclusion + */ + public boolean allSuccessorsInSet(int s, int i, BitSet set); + + /** + * Check if some successor state from choice {@code i} of state {@code s} is in the set {@code set}. + * @param s The state to check + * @param i Choice index + * @param set The set to test for inclusion + */ + public boolean someSuccessorsInSet(int s, int i, BitSet set); +} \ No newline at end of file diff --git a/prism/src/explicit/NondetModelSimple.java b/prism/src/explicit/NondetModelSimple.java new file mode 100644 index 00000000..8864e9cc --- /dev/null +++ b/prism/src/explicit/NondetModelSimple.java @@ -0,0 +1,35 @@ +//============================================================================== +// +// Copyright (c) 2002- +// Authors: +// * Dave Parker (University of Birmingham/Oxford) +// +//------------------------------------------------------------------------------ +// +// This file is part of PRISM. +// +// PRISM is free software; you can redistribute it and/or modify +// it under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 2 of the License, or +// (at your option) any later version. +// +// PRISM is distributed in the hope that it will be useful, +// but WITHOUT ANY WARRANTY; without even the implied warranty of +// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +// GNU General Public License for more details. +// +// You should have received a copy of the GNU General Public License +// along with PRISM; if not, write to the Free Software Foundation, +// Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA +// +//============================================================================== + +package explicit; + +/** + * Interface for simple mutable explicit-state nondeterministic model representations + * (i.e. classes that implement both {@link explicit.NondetModel} and {@link explicit.ModelSimple}). + */ +public interface NondetModelSimple extends NondetModel, ModelSimple +{ +} \ No newline at end of file diff --git a/prism/src/explicit/QuantAbstractRefine.java b/prism/src/explicit/QuantAbstractRefine.java index 09a858be..8074bae0 100644 --- a/prism/src/explicit/QuantAbstractRefine.java +++ b/prism/src/explicit/QuantAbstractRefine.java @@ -116,7 +116,7 @@ public abstract class QuantAbstractRefine // Abstract model info (updated by subclasses) /** Abstract model */ - protected ModelSimple abstraction; + protected NondetModelSimple abstraction; /** BitSet of (abstract) target states for property to drive refinement */ protected BitSet target; diff --git a/prism/src/explicit/STPG.java b/prism/src/explicit/STPG.java index 0e6f1e6a..465fa5d5 100644 --- a/prism/src/explicit/STPG.java +++ b/prism/src/explicit/STPG.java @@ -49,18 +49,13 @@ import explicit.rewards.STPGRewards; * Use {@link #getNumNestedChoices(s, i)}, {@link #getNestedAction(s, i)} and {@link #getNestedTransitionsIterator(s, i, j)} * to access the information. */ -public interface STPG extends Model +public interface STPG extends NondetModel { /** * Get the player (1 or 2) for state {@code s}. */ public int getPlayer(int s); - /** - * Get the action label (if any) for choice {@code i} of state {@code s}. - */ - public Object getAction(int s, int i); - /** * Get the number of transitions from choice {@code i} of state {@code s}. */ diff --git a/prism/src/explicit/STPGAbstrSimple.java b/prism/src/explicit/STPGAbstrSimple.java index 44d34731..b8f4ad55 100644 --- a/prism/src/explicit/STPGAbstrSimple.java +++ b/prism/src/explicit/STPGAbstrSimple.java @@ -41,9 +41,11 @@ import prism.PrismUtils; * Simple explicit-state representation of a stochastic two-player game (STPG), * as used for abstraction of MDPs, i.e. with strict cycling between player 1, * player 2 and probabilistic states. Thus, we store this a set of sets of - * distributions for each state. + * distributions for each state. This means that the player 2 states are not true + * states, i.e. they don't count for statistics and player 1 states are treated + * as successors of each other. */ -public class STPGAbstrSimple extends ModelExplicit implements STPG, ModelSimple +public class STPGAbstrSimple extends ModelExplicit implements STPG, NondetModelSimple { // Transition function (Steps) protected List> trans; @@ -293,7 +295,7 @@ public class STPGAbstrSimple extends ModelExplicit implements STPG, ModelSimple } return succs.iterator(); } - + @Override public boolean isSuccessor(int s1, int s2) { @@ -330,12 +332,6 @@ public class STPGAbstrSimple extends ModelExplicit implements STPG, ModelSimple return false; } - @Override - public int getNumChoices(int s) - { - return trans.get(s).size(); - } - @Override public void findDeadlocks(boolean fix) throws PrismException { @@ -461,15 +457,26 @@ public class STPGAbstrSimple extends ModelExplicit implements STPG, ModelSimple return s; } - // Accessors (for STPG) + // Accessors (for NondetModel) @Override - public int getPlayer(int s) + public int getNumChoices(int s) { - // All states are player 1 - return 1; + return trans.get(s).size(); } - + + @Override + public int getMaxNumChoices() + { + return maxNumDistrSets; + } + + @Override + public int getNumChoices() + { + return numDistrSets; + } + @Override public Object getAction(int s, int i) { @@ -477,6 +484,27 @@ public class STPGAbstrSimple extends ModelExplicit implements STPG, ModelSimple return null; } + @Override + public boolean allSuccessorsInSet(int s, int i, BitSet set) + { + return trans.get(s).get(i).isSubsetOf(set); + } + + @Override + public boolean someSuccessorsInSet(int s, int i, BitSet set) + { + return trans.get(s).get(i).containsOneOf(set); + } + + // Accessors (for STPG) + + @Override + public int getPlayer(int s) + { + // All states are player 1 + return 1; + } + @Override public int getNumTransitions(int s, int i) { @@ -485,7 +513,7 @@ public class STPGAbstrSimple extends ModelExplicit implements STPG, ModelSimple } @Override - public Iterator> getTransitionsIterator(int s, int i) + public Iterator> getTransitionsIterator(int s, int i) { // All choices are nested return null; diff --git a/prism/src/param/ParamModel.java b/prism/src/param/ParamModel.java index 7ec85d08..17e44b0c 100644 --- a/prism/src/param/ParamModel.java +++ b/prism/src/param/ParamModel.java @@ -44,10 +44,9 @@ import explicit.ModelExplicit; * with and without nondeterminism, discrete- as well as continuous-time. * This turned out the be the most convenient way to implement model checking * for parametric models. - * - * @author Ernst Moritz Hahn (University of Oxford) */ -final class ParamModel extends ModelExplicit { +final class ParamModel extends ModelExplicit +{ /** total number of nondeterministic choices over all states */ private int numTotalChoices; /** total number of probabilistic transitions over all states */ @@ -68,7 +67,7 @@ final class ParamModel extends ModelExplicit { private ModelType modelType; /** function factory which manages functions used on transitions, etc. */ private FunctionFactory functionFactory; - + /** * Constructs a new parametric model. */ @@ -80,36 +79,49 @@ final class ParamModel extends ModelExplicit { initialStates = new LinkedList(); deadlocks = new TreeSet(); } - + /** * Sets the type of the model. * * @param modelType type the model shall have */ - void setModelType(ModelType modelType) { + void setModelType(ModelType modelType) + { this.modelType = modelType; } - + + // Accessors (for Model) + @Override - public ModelType getModelType() { + public ModelType getModelType() + { return modelType; } - + @Override - public Values getConstantValues() { + public Values getConstantValues() + { throw new UnsupportedOperationException(); } @Override - public int getNumTransitions() { + public int getNumTransitions() + { return numTotalTransitions; } @Override - public boolean isSuccessor(int from, int to) { - for (int choice = stateBegin(from); choice < stateEnd(from); choice++) { + public Iterator getSuccessorsIterator(int s) + { + throw new UnsupportedOperationException(); + } + + @Override + public boolean isSuccessor(int s1, int s2) + { + for (int choice = stateBegin(s1); choice < stateEnd(s1); choice++) { for (int succ = choiceBegin(choice); succ < choiceEnd(choice); succ++) { - if (succState(succ) == to) { + if (succState(succ) == s2) { return true; } } @@ -118,78 +130,80 @@ final class ParamModel extends ModelExplicit { } @Override - public boolean allSuccessorsInSet(int s, BitSet set) { + public boolean allSuccessorsInSet(int s, BitSet set) + { throw new UnsupportedOperationException(); } @Override - public boolean someSuccessorsInSet(int s, BitSet set) { + public boolean someSuccessorsInSet(int s, BitSet set) + { throw new UnsupportedOperationException(); } @Override - public int getNumChoices(int state) { - return stateEnd(state) - stateBegin(state); - } - - public int getNumTotalChoices() { - return numTotalChoices; - } - - @Override - public void checkForDeadlocks() throws PrismException { + public void findDeadlocks(boolean fix) throws PrismException + { throw new UnsupportedOperationException(); } @Override - public void findDeadlocks(boolean fix) throws PrismException { + public void checkForDeadlocks() throws PrismException + { throw new UnsupportedOperationException(); } @Override - public void checkForDeadlocks(BitSet except) throws PrismException { + public void checkForDeadlocks(BitSet except) throws PrismException + { throw new UnsupportedOperationException(); } @Override - public void exportToPrismExplicit(String baseFilename) - throws PrismException { + public void exportToPrismExplicit(String baseFilename) throws PrismException + { throw new UnsupportedOperationException(); } @Override - public void exportToPrismExplicitTra(String filename) throws PrismException { + public void exportToPrismExplicitTra(String filename) throws PrismException + { throw new UnsupportedOperationException(); } @Override - public void exportToPrismExplicitTra(File file) throws PrismException { + public void exportToPrismExplicitTra(File file) throws PrismException + { throw new UnsupportedOperationException(); } @Override - public void exportToPrismExplicitTra(PrismLog log) throws PrismException { + public void exportToPrismExplicitTra(PrismLog log) throws PrismException + { throw new UnsupportedOperationException(); } @Override - public void exportToDotFile(String filename) throws PrismException { + public void exportToDotFile(String filename) throws PrismException + { throw new UnsupportedOperationException(); } @Override - public void exportToDotFile(String filename, BitSet mark) - throws PrismException { + public void exportToDotFile(String filename, BitSet mark) throws PrismException + { throw new UnsupportedOperationException(); } @Override - public void exportToPrismLanguage(String filename) throws PrismException { + public void exportToPrismLanguage(String filename) throws PrismException + { throw new UnsupportedOperationException(); } @Override - public String infoString() { + public String infoString() + { throw new UnsupportedOperationException(); } @@ -202,6 +216,18 @@ final class ParamModel extends ModelExplicit { return s; } + // Other + + public int getNumChoices(int state) + { + return stateEnd(state) - stateBegin(state); + } + + public int getNumTotalChoices() + { + return numTotalChoices; + } + /** * Allocates memory for subsequent construction of model. * @@ -209,7 +235,8 @@ final class ParamModel extends ModelExplicit { * @param numTotalChoices total number of nondeterministic choices of the model * @param numTotalSuccessors total number of probabilistic transitions of the model */ - void reserveMem(int numStates, int numTotalChoices, int numTotalSuccessors) { + void reserveMem(int numStates, int numTotalChoices, int numTotalSuccessors) + { rows = new int[numStates + 1]; choices = new int[numTotalChoices + 1]; labels = new String[numTotalSuccessors]; @@ -217,7 +244,7 @@ final class ParamModel extends ModelExplicit { nonZeros = new Function[numTotalSuccessors]; sumRates = new Function[numTotalChoices]; } - + /** * Finish the current state. * Starting with the 0th state, this function shall be called once all @@ -227,7 +254,8 @@ final class ParamModel extends ModelExplicit { * called for each state of the method, even the last one, once all its * transitions have been added. */ - void finishState() { + void finishState() + { rows[numStates + 1] = numTotalChoices; numStates++; } @@ -240,7 +268,8 @@ final class ParamModel extends ModelExplicit { * one. Notice that DTMCs and CTMCs should only have a single * nondeterministic choice per state. */ - void finishChoice() { + void finishChoice() + { choices[numTotalChoices + 1] = numTotalTransitions; numTotalChoices++; } @@ -256,13 +285,14 @@ final class ParamModel extends ModelExplicit { * @param probFn with which probability it leads to this state * @param action action with which the choice is labelled */ - void addTransition(int toState, Function probFn, String action) { + void addTransition(int toState, Function probFn, String action) + { cols[numTotalTransitions] = toState; nonZeros[numTotalTransitions] = probFn; labels[numTotalTransitions] = action; numTotalTransitions++; } - + /** * Sets the total sum of leaving rate of the current nondeterministic choice. * For discrete-time models, this function shall always be called with @@ -274,7 +304,7 @@ final class ParamModel extends ModelExplicit { { sumRates[numTotalChoices] = leaving; } - + /** * Returns the number of the first nondeterministic choice of {@code state}. * @@ -296,7 +326,7 @@ final class ParamModel extends ModelExplicit { { return rows[state + 1]; } - + /** * Returns the first probabilistic branch of the given nondeterministic decision. * @@ -307,7 +337,7 @@ final class ParamModel extends ModelExplicit { { return choices[choice]; } - + /** * Returns the last probabilistic branch of the given nondeterministic decision plus one. * @@ -318,7 +348,7 @@ final class ParamModel extends ModelExplicit { { return choices[choice + 1]; } - + /** * Returns the successor state of the given probabilistic branch. * @@ -329,7 +359,7 @@ final class ParamModel extends ModelExplicit { { return cols[succNr]; } - + /** * Returns the probability of the given probabilistic branch * @@ -362,7 +392,7 @@ final class ParamModel extends ModelExplicit { { return sumRates[choice]; } - + /** * Instantiates the parametric model at a given point. * All transition probabilities, etc. will be evaluated and set as @@ -390,9 +420,10 @@ final class ParamModel extends ModelExplicit { return result; } - + @Override - public void buildFromPrismExplicit(String filename) throws PrismException { + public void buildFromPrismExplicit(String filename) throws PrismException + { throw new UnsupportedOperationException(); } @@ -405,20 +436,14 @@ final class ParamModel extends ModelExplicit { { this.functionFactory = functionFactory; } + /** * Returns the function factory used in this parametric model. * * @return function factory used in this parametric model - */ + */ FunctionFactory getFunctionFactory() { return functionFactory; } - - @Override - public Iterator getSuccessorsIterator(int s) - { - throw new UnsupportedOperationException(); - } - }