From e5b7ad597ed0d29bea796c5c1b5ebde69fd178e5 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Thu, 4 Aug 2011 09:45:00 +0000 Subject: [PATCH] Expansion of transition-matrix-export functionality for explicit engine. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3357 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/explicit/DTMCEmbeddedSimple.java | 12 ++++ .../DTMCFromMDPMemorylessAdversary.java | 12 ++++ prism/src/explicit/DTMCSimple.java | 42 ++++-------- prism/src/explicit/DTMCUniformisedSimple.java | 12 ++++ prism/src/explicit/MDPSimple.java | 46 ++++++------- prism/src/explicit/MDPSparse.java | 34 ++++------ prism/src/explicit/Model.java | 14 +++- prism/src/explicit/ModelSimple.java | 18 ++++- prism/src/explicit/ModelSparse.java | 18 ++++- prism/src/explicit/PrismExplicit.java | 68 +++++++++++++++++++ prism/src/explicit/STPGAbstrSimple.java | 48 ++++++------- 11 files changed, 221 insertions(+), 103 deletions(-) diff --git a/prism/src/explicit/DTMCEmbeddedSimple.java b/prism/src/explicit/DTMCEmbeddedSimple.java index 046142c6..60f5fa9f 100644 --- a/prism/src/explicit/DTMCEmbeddedSimple.java +++ b/prism/src/explicit/DTMCEmbeddedSimple.java @@ -26,6 +26,7 @@ package explicit; +import java.io.File; import java.util.*; import java.util.Map.Entry; @@ -34,6 +35,7 @@ import parser.State; import parser.Values; import prism.ModelType; import prism.PrismException; +import prism.PrismLog; /** * Simple explicit-state representation of a DTMC, constructed (implicitly) as the embedded DTMC of a CTMC. @@ -167,6 +169,16 @@ public class DTMCEmbeddedSimple implements DTMC throw new PrismException("Export not yet supported"); } + public void exportToPrismExplicitTra(File file) throws PrismException + { + throw new PrismException("Export not yet supported"); + } + + public void exportToPrismExplicitTra(PrismLog out) throws PrismException + { + throw new PrismException("Export not yet supported"); + } + public void exportToDotFile(String filename) throws PrismException { throw new PrismException("Export not yet supported"); diff --git a/prism/src/explicit/DTMCFromMDPMemorylessAdversary.java b/prism/src/explicit/DTMCFromMDPMemorylessAdversary.java index a43d263a..c9bd23cc 100644 --- a/prism/src/explicit/DTMCFromMDPMemorylessAdversary.java +++ b/prism/src/explicit/DTMCFromMDPMemorylessAdversary.java @@ -26,6 +26,7 @@ package explicit; +import java.io.File; import java.util.*; import java.util.Map.Entry; @@ -34,6 +35,7 @@ import parser.State; import parser.Values; import prism.ModelType; import prism.PrismException; +import prism.PrismLog; /** * Explicit-state representation of a DTMC, constructed (implicitly) @@ -158,6 +160,16 @@ public class DTMCFromMDPMemorylessAdversary implements DTMC throw new PrismException("Export not yet supported"); } + public void exportToPrismExplicitTra(File file) throws PrismException + { + throw new PrismException("Export not yet supported"); + } + + public void exportToPrismExplicitTra(PrismLog out) throws PrismException + { + throw new PrismException("Export not yet supported"); + } + public void exportToDotFile(String filename) throws PrismException { throw new PrismException("Export not yet supported"); diff --git a/prism/src/explicit/DTMCSimple.java b/prism/src/explicit/DTMCSimple.java index 57598bee..560f2457 100644 --- a/prism/src/explicit/DTMCSimple.java +++ b/prism/src/explicit/DTMCSimple.java @@ -33,6 +33,7 @@ import java.io.*; import explicit.rewards.*; import prism.ModelType; import prism.PrismException; +import prism.PrismLog; import prism.PrismUtils; /** @@ -273,37 +274,24 @@ public class DTMCSimple extends ModelSimple implements DTMC } @Override - public void exportToPrismExplicit(String baseFilename) throws PrismException - { - exportToPrismExplicitTra(baseFilename + ".tra"); - } - - @Override - public void exportToPrismExplicitTra(String filename) throws PrismException + public void exportToPrismExplicitTra(PrismLog out) throws PrismException { int i; - FileWriter out; TreeMap sorted; - try { - // Output transitions to .tra file - out = new FileWriter(filename); - out.write(numStates + " " + numTransitions + "\n"); - sorted = new TreeMap(); - for (i = 0; i < numStates; i++) { - // Extract transitions and sort by destination state index (to match PRISM-exported files) - for (Map.Entry e : trans.get(i)) { - sorted.put(e.getKey(), e.getValue()); - } - // Print out (sorted) transitions - for (Map.Entry e : sorted.entrySet()) { - // Note use of PrismUtils.formatDouble to match PRISM-exported files - out.write(i + " " + e.getKey() + " " + PrismUtils.formatDouble(e.getValue()) + "\n"); - } - sorted.clear(); + // Output transitions to .tra file + out.print(numStates + " " + numTransitions + "\n"); + sorted = new TreeMap(); + for (i = 0; i < numStates; i++) { + // Extract transitions and sort by destination state index (to match PRISM-exported files) + for (Map.Entry e : trans.get(i)) { + sorted.put(e.getKey(), e.getValue()); } - out.close(); - } catch (IOException e) { - throw new PrismException("Could not export " + getModelType() + " to file \"" + filename + "\"" + e); + // Print out (sorted) transitions + for (Map.Entry e : sorted.entrySet()) { + // Note use of PrismUtils.formatDouble to match PRISM-exported files + out.print(i + " " + e.getKey() + " " + PrismUtils.formatDouble(e.getValue()) + "\n"); + } + sorted.clear(); } } diff --git a/prism/src/explicit/DTMCUniformisedSimple.java b/prism/src/explicit/DTMCUniformisedSimple.java index 072e4eb6..08e38fe3 100644 --- a/prism/src/explicit/DTMCUniformisedSimple.java +++ b/prism/src/explicit/DTMCUniformisedSimple.java @@ -26,6 +26,7 @@ package explicit; +import java.io.File; import java.util.*; import java.util.Map.Entry; @@ -34,6 +35,7 @@ import parser.State; import parser.Values; import prism.ModelType; import prism.PrismException; +import prism.PrismLog; /** * Simple explicit-state representation of a DTMC, constructed (implicitly) as the uniformised DTMC of a CTMC. @@ -176,6 +178,16 @@ public class DTMCUniformisedSimple implements DTMC throw new PrismException("Export not yet supported"); } + public void exportToPrismExplicitTra(File file) throws PrismException + { + throw new PrismException("Export not yet supported"); + } + + public void exportToPrismExplicitTra(PrismLog out) throws PrismException + { + throw new PrismException("Export not yet supported"); + } + public void exportToDotFile(String filename) throws PrismException { throw new PrismException("Export not yet supported"); diff --git a/prism/src/explicit/MDPSimple.java b/prism/src/explicit/MDPSimple.java index 23ea10d3..d676eab1 100644 --- a/prism/src/explicit/MDPSimple.java +++ b/prism/src/explicit/MDPSimple.java @@ -35,6 +35,7 @@ import explicit.rewards.MDPRewards; import explicit.rewards.MDPRewardsSimple; import prism.ModelType; import prism.PrismException; +import prism.PrismLog; import prism.PrismUtils; /** @@ -540,38 +541,31 @@ public class MDPSimple extends ModelSimple implements MDP } @Override - public void exportToPrismExplicitTra(String filename) throws PrismException + public void exportToPrismExplicitTra(PrismLog out) throws PrismException { int i, j; Object action; - FileWriter out; TreeMap sorted; - try { - // Output transitions to .tra file - out = new FileWriter(filename); - out.write(numStates + " " + numDistrs + " " + numTransitions + "\n"); - sorted = new TreeMap(); - for (i = 0; i < numStates; i++) { - j = -1; - for (Distribution distr : trans.get(i)) { - j++; - // Extract transitions and sort by destination state index (to match PRISM-exported files) - for (Map.Entry e : distr) { - sorted.put(e.getKey(), e.getValue()); - } - // Print out (sorted) transitions - for (Map.Entry e : sorted.entrySet()) { - // Note use of PrismUtils.formatDouble to match PRISM-exported files - out.write(i + " " + j + " " + e.getKey() + " " + PrismUtils.formatDouble(e.getValue())); - action = getAction(i, j); - out.write(action == null ? "\n" : (" " + action + "\n")); - } - sorted.clear(); + // Output transitions to .tra file + out.print(numStates + " " + numDistrs + " " + numTransitions + "\n"); + sorted = new TreeMap(); + for (i = 0; i < numStates; i++) { + j = -1; + for (Distribution distr : trans.get(i)) { + j++; + // Extract transitions and sort by destination state index (to match PRISM-exported files) + for (Map.Entry e : distr) { + sorted.put(e.getKey(), e.getValue()); } + // Print out (sorted) transitions + for (Map.Entry e : sorted.entrySet()) { + // Note use of PrismUtils.formatDouble to match PRISM-exported files + out.print(i + " " + j + " " + e.getKey() + " " + PrismUtils.formatDouble(e.getValue())); + action = getAction(i, j); + out.print(action == null ? "\n" : (" " + action + "\n")); + } + sorted.clear(); } - out.close(); - } catch (IOException e) { - throw new PrismException("Could not export " + getModelType() + " to file \"" + filename + "\"" + e); } } diff --git a/prism/src/explicit/MDPSparse.java b/prism/src/explicit/MDPSparse.java index 4b7f98d3..5559a717 100644 --- a/prism/src/explicit/MDPSparse.java +++ b/prism/src/explicit/MDPSparse.java @@ -35,6 +35,7 @@ import explicit.rewards.MDPRewards; import parser.State; import prism.ModelType; import prism.PrismException; +import prism.PrismLog; import prism.PrismUtils; /** @@ -466,33 +467,26 @@ public class MDPSparse extends ModelSparse implements MDP } @Override - public void exportToPrismExplicitTra(String filename) throws PrismException + public void exportToPrismExplicitTra(PrismLog out) throws PrismException { // Note: In PRISM .tra files, transitions are usually sorted by column index within choices // (to ensure this is the case, you may need to sort the model when constructing) int i, j, k, l1, h1, l2, h2; Object action; - FileWriter out; - try { - // Output transitions to .tra file - out = new FileWriter(filename); - out.write(numStates + " " + numDistrs + " " + numTransitions + "\n"); - for (i = 0; i < numStates; i++) { - l1 = rowStarts[i]; - h1 = rowStarts[i + 1]; - for (j = l1; j < h1; j++) { - l2 = choiceStarts[j]; - h2 = choiceStarts[j + 1]; - for (k = l2; k < h2; k++) { - out.write(i + " " + (j - l1) + " " + cols[k] + " " + PrismUtils.formatDouble(nonZeros[k])); - action = getAction(i, j - l1); - out.write(action == null ? "\n" : (" " + action + "\n")); - } + // Output transitions to .tra file + out.print(numStates + " " + numDistrs + " " + numTransitions + "\n"); + for (i = 0; i < numStates; i++) { + l1 = rowStarts[i]; + h1 = rowStarts[i + 1]; + for (j = l1; j < h1; j++) { + l2 = choiceStarts[j]; + h2 = choiceStarts[j + 1]; + for (k = l2; k < h2; k++) { + out.print(i + " " + (j - l1) + " " + cols[k] + " " + PrismUtils.formatDouble(nonZeros[k])); + action = getAction(i, j - l1); + out.print(action == null ? "\n" : (" " + action + "\n")); } } - out.close(); - } catch (IOException e) { - throw new PrismException("Could not export " + getModelType() + " to file \"" + filename + "\"" + e); } } diff --git a/prism/src/explicit/Model.java b/prism/src/explicit/Model.java index 5f8974c0..5abee032 100644 --- a/prism/src/explicit/Model.java +++ b/prism/src/explicit/Model.java @@ -26,12 +26,14 @@ package explicit; +import java.io.File; import java.util.*; import parser.State; import parser.Values; import prism.ModelType; import prism.PrismException; +import prism.PrismLog; /** * Interface for (abstract) classes that provide (read-only) access to an explicit-state model. @@ -144,8 +146,18 @@ public interface Model /** * Export transition matrix to explicit format readable by PRISM (i.e. a .tra file). */ - public void exportToPrismExplicitTra(String traFilename) throws PrismException; + public void exportToPrismExplicitTra(String filename) throws PrismException; + /** + * Export transition matrix to explicit format readable by PRISM (i.e. a .tra file). + */ + public void exportToPrismExplicitTra(File file) throws PrismException; + + /** + * Export transition matrix to explicit format readable by PRISM (i.e. a .tra file). + */ + public void exportToPrismExplicitTra(PrismLog log) throws PrismException; + /** * Export to a dot file. */ diff --git a/prism/src/explicit/ModelSimple.java b/prism/src/explicit/ModelSimple.java index 326719a1..8ab57c0c 100644 --- a/prism/src/explicit/ModelSimple.java +++ b/prism/src/explicit/ModelSimple.java @@ -26,12 +26,15 @@ package explicit; +import java.io.File; import java.util.*; import parser.State; import parser.Values; import prism.ModelType; import prism.PrismException; +import prism.PrismLog; +import prism.PrismFileLog; /** * Base class for simple explicit-state model representations. @@ -202,7 +205,20 @@ public abstract class ModelSimple implements Model exportToPrismExplicitTra(baseFilename + ".tra"); } - public abstract void exportToPrismExplicitTra(String filename) throws PrismException; + @Override + public void exportToPrismExplicitTra(String filename) throws PrismException + { + exportToPrismExplicitTra(new PrismFileLog(filename)); + } + + @Override + public void exportToPrismExplicitTra(File file) throws PrismException + { + exportToPrismExplicitTra(new PrismFileLog(file.getPath())); + } + + @Override + public abstract void exportToPrismExplicitTra(PrismLog out) throws PrismException; public void exportToDotFile(String filename) throws PrismException { diff --git a/prism/src/explicit/ModelSparse.java b/prism/src/explicit/ModelSparse.java index 859a270c..75d0901c 100644 --- a/prism/src/explicit/ModelSparse.java +++ b/prism/src/explicit/ModelSparse.java @@ -26,12 +26,15 @@ package explicit; +import java.io.File; import java.util.*; import parser.State; import parser.Values; import prism.ModelType; import prism.PrismException; +import prism.PrismFileLog; +import prism.PrismLog; /** * Base class sparse matrix-based (non-mutable) explicit-state model representations @@ -153,7 +156,20 @@ public abstract class ModelSparse implements Model exportToPrismExplicitTra(baseFilename + ".tra"); } - public abstract void exportToPrismExplicitTra(String filename) throws PrismException; + @Override + public void exportToPrismExplicitTra(String filename) throws PrismException + { + exportToPrismExplicitTra(new PrismFileLog(filename)); + } + + @Override + public void exportToPrismExplicitTra(File file) throws PrismException + { + exportToPrismExplicitTra(new PrismFileLog(file.getPath())); + } + + @Override + public abstract void exportToPrismExplicitTra(PrismLog log) throws PrismException; public void exportToDotFile(String filename) throws PrismException { diff --git a/prism/src/explicit/PrismExplicit.java b/prism/src/explicit/PrismExplicit.java index 5abeae01..4747ea39 100644 --- a/prism/src/explicit/PrismExplicit.java +++ b/prism/src/explicit/PrismExplicit.java @@ -86,6 +86,54 @@ public class PrismExplicit return modelExpl; } + /** + * Export a model's transition matrix to a file (or to the log) + * @param model The model + * @param ordered Ensure that (source) states are in ascending order? + * @param exportType Type of export; one of:
    + *
  • {@link #EXPORT_PLAIN} + *
  • {@link #EXPORT_MATLAB} + *
  • {@link #EXPORT_DOT} + *
  • {@link #EXPORT_MRMC} + *
  • {@link #EXPORT_MRMC} + *
  • {@link #EXPORT_DOT_STATES} + *
+ * @param file File to export to (if null, print to the log instead) + */ + public void exportTransToFile(Model model, boolean ordered, int exportType, File file) throws FileNotFoundException, PrismException + { + // can only do ordered version of export for explicit engine + if (!ordered) { + mainLog.println("\nWarning: Cannot export unordered transition matrix with the explicit engine; using ordered."); + ordered = true; + } + // print message + mainLog.print("\nExporting transition matrix "); + switch (exportType) { + case Prism.EXPORT_PLAIN: mainLog.print("in plain text format "); break; + case Prism.EXPORT_MATLAB: mainLog.print("in Matlab format "); break; + case Prism.EXPORT_DOT: mainLog.print("in Dot format "); break; + case Prism.EXPORT_MRMC: mainLog.print("in MRMC format "); break; + case Prism.EXPORT_ROWS: mainLog.print("in rows format "); break; + case Prism.EXPORT_DOT_STATES: mainLog.print("in Dot format (with states) "); break; + } + if (file != null) mainLog.println("to file \"" + file + "\"..."); else mainLog.println("below:"); + PrismLog tmpLog = getPrismLogForFile(file); + + // do export + switch (exportType) { + case Prism.EXPORT_PLAIN: + model.exportToPrismExplicitTra(tmpLog); + break; + case Prism.EXPORT_MATLAB: + case Prism.EXPORT_DOT: + case Prism.EXPORT_MRMC: + case Prism.EXPORT_ROWS: + case Prism.EXPORT_DOT_STATES: + throw new PrismException("Export not yet supported"); // TODO + } + } + /** * Perform model checking of a property on a model and return result. * @param model The model @@ -313,6 +361,26 @@ public class PrismExplicit if (fileOut != null) tmpLog.close(); } + /** + * Either create a new PrismFileLog for {@code file} or, + * if {@code file} is null, return {@code mainLog}. + * Throws a {@code PrismException} if there is a problem opening the file. + */ + private PrismLog getPrismLogForFile(File file) throws PrismException + { + // create new file log or use main log + PrismLog tmpLog; + if (file != null) { + tmpLog = new PrismFileLog(file.getPath()); + if (!tmpLog.ready()) { + throw new PrismException("Could not open file \"" + file + "\" for output"); + } + } else { + tmpLog = mainLog; + } + return tmpLog; + } + /** * Simple test program. */ diff --git a/prism/src/explicit/STPGAbstrSimple.java b/prism/src/explicit/STPGAbstrSimple.java index e734e3ef..d837e37c 100644 --- a/prism/src/explicit/STPGAbstrSimple.java +++ b/prism/src/explicit/STPGAbstrSimple.java @@ -33,6 +33,7 @@ import java.io.*; import explicit.rewards.STPGRewards; import prism.ModelType; import prism.PrismException; +import prism.PrismLog; import prism.PrismUtils; /** @@ -354,39 +355,32 @@ public class STPGAbstrSimple extends ModelSimple implements STPG } @Override - public void exportToPrismExplicitTra(String filename) throws PrismException + public void exportToPrismExplicitTra(PrismLog out) throws PrismException { int i, j, k; - FileWriter out; TreeMap sorted; - try { - // Output transitions to .tra file - out = new FileWriter(filename); - out.write(numStates + " " + numDistrSets + " " + numDistrs + " " + numTransitions + "\n"); - sorted = new TreeMap(); - for (i = 0; i < numStates; i++) { - j = -1; - for (DistributionSet distrs : trans.get(i)) { - j++; - k = -1; - for (Distribution distr : distrs) { - k++; - // Extract transitions and sort by destination state index (to match PRISM-exported files) - for (Map.Entry e : distr) { - sorted.put(e.getKey(), e.getValue()); - } - // Print out (sorted) transitions - for (Map.Entry e : distr) { - // Note use of PrismUtils.formatDouble to match PRISM-exported files - out.write(i + " " + j + " " + k + " " + e.getKey() + " " + PrismUtils.formatDouble(e.getValue()) + "\n"); - } - sorted.clear(); + // Output transitions to .tra file + out.print(numStates + " " + numDistrSets + " " + numDistrs + " " + numTransitions + "\n"); + sorted = new TreeMap(); + for (i = 0; i < numStates; i++) { + j = -1; + for (DistributionSet distrs : trans.get(i)) { + j++; + k = -1; + for (Distribution distr : distrs) { + k++; + // Extract transitions and sort by destination state index (to match PRISM-exported files) + for (Map.Entry e : distr) { + sorted.put(e.getKey(), e.getValue()); } + // Print out (sorted) transitions + for (Map.Entry e : distr) { + // Note use of PrismUtils.formatDouble to match PRISM-exported files + out.print(i + " " + j + " " + k + " " + e.getKey() + " " + PrismUtils.formatDouble(e.getValue()) + "\n"); + } + sorted.clear(); } } - out.close(); - } catch (IOException e) { - throw new PrismException("Could not export " + getModelType() + " to file \"" + filename + "\"" + e); } }