diff --git a/prism/src/explicit/CTMCSimple.java b/prism/src/explicit/CTMCSimple.java index 4112cb41..d08afef9 100644 --- a/prism/src/explicit/CTMCSimple.java +++ b/prism/src/explicit/CTMCSimple.java @@ -59,6 +59,17 @@ public class CTMCSimple extends DTMCSimple implements CTMC super(ctmc); } + /** + * Construct a CTMC from an existing one and a state index permutation, + * i.e. in which state index i becomes index permut[i]. + * Note: have to build new Distributions from scratch anyway to do this, + * so may as well provide this functionality as a constructor. + */ + public CTMCSimple(CTMCSimple ctmc, int permut[]) + { + super(ctmc, permut); + } + // Accessors (for CTMC) @Override diff --git a/prism/src/explicit/DTMCSimple.java b/prism/src/explicit/DTMCSimple.java index 06ea6ece..d9ecaccf 100644 --- a/prism/src/explicit/DTMCSimple.java +++ b/prism/src/explicit/DTMCSimple.java @@ -31,6 +31,7 @@ import java.io.*; import prism.ModelType; import prism.PrismException; +import prism.PrismUtils; /** * Simple explicit-state representation of a DTMC. @@ -83,6 +84,25 @@ public class DTMCSimple extends ModelSimple implements DTMC numTransitions = dtmc.numTransitions; } + /** + * Construct a DTMC from an existing one and a state index permutation, + * i.e. in which state index i becomes index permut[i]. + * Note: have to build new Distributions from scratch anyway to do this, + * so may as well provide this functionality as a constructor. + */ + public DTMCSimple(DTMCSimple dtmc, int permut[]) + { + this(dtmc.numStates); + for (int in : dtmc.getInitialStates()) { + addInitialState(permut[in]); + } + for (int i = 0; i < numStates; i++) { + trans.set(permut[i], new Distribution(dtmc.trans.get(i), permut)); + } + // TODO: permute rewards + numTransitions = dtmc.numTransitions; + } + // Mutators (for ModelSimple) @Override @@ -182,7 +202,18 @@ public class DTMCSimple extends ModelSimple implements DTMC numTransitions--; if (prob != 0.0) numTransitions++; - trans.get(i).set(j, prob); + distr.set(j, prob); + } + + /** + * Add to the probability for a transition. + */ + public void addToProbability(int i, int j, double prob) + { + if (!trans.get(i).add(j, prob)) { + if (prob != 0.0) + numTransitions++; + } } /** @@ -273,7 +304,26 @@ public class DTMCSimple extends ModelSimple implements DTMC @Override public void exportToPrismExplicit(String baseFilename) throws PrismException { - throw new PrismException("Export not yet supported"); + int i; + String filename = null; + FileWriter out; + try { + // Output transitions to .tra file + filename = baseFilename + ".tra"; + out = new FileWriter(filename); + out.write(numStates + " " + numTransitions + "\n"); + for (i = 0; i < numStates; i++) { + for (Map.Entry e : trans.get(i)) { + out.write(i + " " + e.getKey() + " " + PrismUtils.formatDouble(e.getValue()) + "\n"); + } + } + out.close(); + // Output transition rewards to .trew file + // TODO + out.close(); + } catch (IOException e) { + throw new PrismException("Could not export " + getModelType() + " to file \"" + filename + "\"" + e); + } } @Override diff --git a/prism/src/explicit/Distribution.java b/prism/src/explicit/Distribution.java index ad5365a8..048c148c 100644 --- a/prism/src/explicit/Distribution.java +++ b/prism/src/explicit/Distribution.java @@ -60,6 +60,22 @@ public class Distribution implements Iterable> } } + /** + * Construct a distribution from an existing one and a state index permutation, + * i.e. in which state index i becomes index permut[i]. + * Note: have to build the new distributions from scratch anyway to do this, + * so may as well provide this functionality as a constructor. + */ + public Distribution(Distribution distr, int permut[]) + { + this(); + Iterator> i = distr.iterator(); + while (i.hasNext()) { + Map.Entry e = i.next(); + add(permut[e.getKey()], e.getValue()); + } + } + /** * Clear all entries of the distribution. */ @@ -70,14 +86,19 @@ public class Distribution implements Iterable> /** * Add 'prob' to the probability for state 'j'. + * Return boolean indicating whether or not there was already + * non-zero probability for this state (i.e. false denotes new transition). */ - public void add(int j, double prob) + public boolean add(int j, double prob) { Double d = (Double) map.get(j); - if (d == null) + if (d == null) { map.put(j, prob); - else + return false; + } else { set(j, d + prob); + return true; + } } /** diff --git a/prism/src/explicit/IndexedSet.java b/prism/src/explicit/IndexedSet.java index 16b076be..e23530d0 100644 --- a/prism/src/explicit/IndexedSet.java +++ b/prism/src/explicit/IndexedSet.java @@ -34,12 +34,17 @@ import java.util.*; */ public class IndexedSet { - private HashMap set; + private Map set; private int indexOfLastAdd; public IndexedSet() { - set = new HashMap(); + this(false); + } + + public IndexedSet(boolean sorted) + { + set = sorted ? new TreeMap() : new HashMap(); indexOfLastAdd = -1; } @@ -105,6 +110,26 @@ public class IndexedSet } } + /** + * Build sort permutation. Assuming this was built as a sorted set, + * this returns a permutation (integer array) mapping current indices + * to new indices under the sorting order. + */ + public int[] buildSortingPermutation() + { + int i, n; + int perm[]; + + n = set.size(); + perm = new int[n]; + i = 0; + for (Map.Entry e : set.entrySet()) { + perm[e.getValue()] = i++; + } + + return perm; + } + @Override public String toString() { diff --git a/prism/src/explicit/MDPSimple.java b/prism/src/explicit/MDPSimple.java index cec8d599..43ae30da 100644 --- a/prism/src/explicit/MDPSimple.java +++ b/prism/src/explicit/MDPSimple.java @@ -414,7 +414,7 @@ public class MDPSimple extends ModelSimple implements MDP for (Distribution distr : trans.get(i)) { j++; for (Map.Entry e : distr) { - out.write(i + " " + j + " " + e.getKey() + " " + e.getValue() + "\n"); + out.write(i + " " + j + " " + e.getKey() + " " + PrismUtils.formatDouble(e.getValue()) + "\n"); } } } @@ -492,7 +492,7 @@ public class MDPSimple extends ModelSimple implements MDP } return true; } - + @Override public boolean someAllSuccessorsInSetForSomeChoices(int s, BitSet set1, BitSet set2) { diff --git a/prism/src/explicit/STPG.java b/prism/src/explicit/STPG.java index 2fd57f72..f89cd483 100644 --- a/prism/src/explicit/STPG.java +++ b/prism/src/explicit/STPG.java @@ -247,7 +247,7 @@ public class STPG extends ModelSimple { return trans.get(s); } - + /** * Get the ith choice (distribution set) for state s. */ @@ -255,7 +255,7 @@ public class STPG extends ModelSimple { return trans.get(s).get(i); } - + @Override public ModelType getModelType() { @@ -318,7 +318,7 @@ public class STPG extends ModelSimple { return numDistrSets; } - + /** * Get the total number of player 2 choices (distributions) over all states. */ @@ -326,7 +326,7 @@ public class STPG extends ModelSimple { return numDistrs; } - + /** * Get the total number of transitions in the model. */ @@ -334,7 +334,7 @@ public class STPG extends ModelSimple { return numTransitions; } - + /** * Get the maximum number of player 1 choices (distribution sets) in any state. */ @@ -343,7 +343,7 @@ public class STPG extends ModelSimple // TODO: Recompute if necessary return maxNumDistrSets; } - + /** * Get the maximum number of player 2 choices (distributions) in any state. */ @@ -352,7 +352,7 @@ public class STPG extends ModelSimple // TODO: Recompute if necessary return maxNumDistrs; } - + /** * Checks for deadlocks (states with no choices) and throws an exception if any exist. * States in 'except' (If non-null) are excluded from the check. @@ -595,7 +595,8 @@ public class STPG extends ModelSimple for (Distribution distr : distrs) { k++; for (Map.Entry e : distr) { - out.write(i + " " + j + " " + k + " " + e.getKey() + " " + e.getValue() + "\n"); + out.write(i + " " + j + " " + k + " " + e.getKey() + " " + + PrismUtils.formatDouble(e.getValue()) + "\n"); } } }