Various additions/improvements to explicit code needed for model construction.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@1848 bbc10eb1-c90d-0410-af57-cb519fbb1720

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

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<Integer, Double> 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

prism/src/explicit/Distribution.java

@@ -60,6 +60,22 @@ public class Distribution implements Iterable<Entry<Integer,Double>>
 		}
 	}
 	
+	/**
+	 * 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<Entry<Integer,Double>> i = distr.iterator();
+		while (i.hasNext()) {
+			Map.Entry<Integer,Double> e = i.next();
+			add(permut[e.getKey()], e.getValue());
+		}
+	}
+	
 	/**
 	 * Clear all entries of the distribution.
 	 */
@@ -70,14 +86,19 @@ public class Distribution implements Iterable<Entry<Integer,Double>>
 	
 	/**
 	 * 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;
+		}
 	}
 
 	/**

prism/src/explicit/IndexedSet.java

@@ -34,12 +34,17 @@ import java.util.*;
  */
 public class IndexedSet<T>
 {
-	private HashMap<T, Integer> set;
+	private Map<T, Integer> set;
 	private int indexOfLastAdd;
 
 	public IndexedSet()
 	{
-		set = new HashMap<T, Integer>();
+		this(false);
+	}
+
+	public IndexedSet(boolean sorted)
+	{
+		set = sorted ? new TreeMap<T, Integer>() : new HashMap<T, Integer>();
 		indexOfLastAdd = -1;
 	}
 
@@ -105,6 +110,26 @@ public class IndexedSet<T>
 		}
 	}
 	
+	/**
+	 * 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<T, Integer> e : set.entrySet()) {
+			perm[e.getValue()] = i++;
+		}
+		
+		return perm;
+	}
+	
 	@Override
 	public String toString()
 	{

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<Integer, Double> 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)
 	{

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<Integer, Double> e : distr) {
-							out.write(i + " " + j + " " + k + " " + e.getKey() + " " + e.getValue() + "\n");
+							out.write(i + " " + j + " " + k + " " + e.getKey() + " "
+									+ PrismUtils.formatDouble(e.getValue()) + "\n");
 						}
 					}
 				}