From 23c02e6b0621d16d6b2908a206052c95e9bdbf6b Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Fri, 12 Oct 2018 14:24:50 +0200 Subject: [PATCH] explicit engine: support -exportrows --- prism/src/automata/LTSFromDA.java | 2 +- prism/src/explicit/DTMCExplicit.java | 9 ++++++- prism/src/explicit/LTSExplicit.java | 2 +- prism/src/explicit/MDPExplicit.java | 30 ++++++++++++++++++--- prism/src/explicit/Model.java | 12 +++++++-- prism/src/explicit/ModelExplicit.java | 2 +- prism/src/explicit/STPGAbstrSimple.java | 9 ++++++- prism/src/explicit/SubNondetModel.java | 2 +- prism/src/explicit/modelviews/DTMCView.java | 10 ++++++- prism/src/explicit/modelviews/MDPView.java | 8 +++++- prism/src/param/ParamModel.java | 2 +- prism/src/prism/Prism.java | 4 +-- prism/src/strat/MDStrategyArray.java | 4 ++- prism/src/strat/Strategy.java | 3 ++- 14 files changed, 80 insertions(+), 19 deletions(-) diff --git a/prism/src/automata/LTSFromDA.java b/prism/src/automata/LTSFromDA.java index 0a62288b..88993245 100644 --- a/prism/src/automata/LTSFromDA.java +++ b/prism/src/automata/LTSFromDA.java @@ -129,7 +129,7 @@ public class LTSFromDA extends ModelExplicit implements LTS } @Override - public void exportToPrismExplicitTra(PrismLog out) + public void exportToPrismExplicitTra(PrismLog out, int exportType) { throw new RuntimeException("Not implemented yet"); } diff --git a/prism/src/explicit/DTMCExplicit.java b/prism/src/explicit/DTMCExplicit.java index 79c8fed2..6c9d9c1e 100644 --- a/prism/src/explicit/DTMCExplicit.java +++ b/prism/src/explicit/DTMCExplicit.java @@ -55,8 +55,15 @@ public abstract class DTMCExplicit extends ModelExplicit implements DTMC } @Override - public void exportToPrismExplicitTra(PrismLog out) + public void exportToPrismExplicitTra(PrismLog out, int exportType) throws PrismException { + switch (exportType) { + case prism.Prism.EXPORT_PLAIN: + case prism.Prism.EXPORT_ROWS: + break; + default: + throw new PrismException("Unsupported export type"); + } int i; TreeMap> sorted; // Output transitions to .tra file diff --git a/prism/src/explicit/LTSExplicit.java b/prism/src/explicit/LTSExplicit.java index 16bdd3ad..baa02483 100644 --- a/prism/src/explicit/LTSExplicit.java +++ b/prism/src/explicit/LTSExplicit.java @@ -184,7 +184,7 @@ public class LTSExplicit extends ModelExplicit implements LTS } @Override - public void exportToPrismExplicitTra(PrismLog out) + public void exportToPrismExplicitTra(PrismLog out, int exportType) { throw new UnsupportedOperationException(); } diff --git a/prism/src/explicit/MDPExplicit.java b/prism/src/explicit/MDPExplicit.java index faf32d01..78de56f4 100644 --- a/prism/src/explicit/MDPExplicit.java +++ b/prism/src/explicit/MDPExplicit.java @@ -78,8 +78,20 @@ public abstract class MDPExplicit extends ModelExplicit implements MDP } @Override - public void exportToPrismExplicitTra(PrismLog out) + public void exportToPrismExplicitTra(PrismLog out, int exportType) throws PrismException { + boolean rows = false; + switch (exportType) + { + case prism.Prism.EXPORT_PLAIN: + break; + case prism.Prism.EXPORT_ROWS: + rows = true; + break; + default: + throw new PrismException("Unsupported export type"); + } + int i, j, numChoices; Object action; TreeMap sorted; @@ -96,11 +108,21 @@ public abstract class MDPExplicit extends ModelExplicit implements MDP 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())); + if (rows) { + out.print(i); + for (Map.Entry e : sorted.entrySet()) { + // Note use of PrismUtils.formatDouble to match PRISM-exported files + out.print(" " + PrismUtils.formatDouble(e.getValue()) + ":" + e.getKey()); + } action = getAction(i, j); out.print(action == null ? "\n" : (" " + action + "\n")); + } else { + 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(); } diff --git a/prism/src/explicit/Model.java b/prism/src/explicit/Model.java index e00a1cf1..1485733a 100644 --- a/prism/src/explicit/Model.java +++ b/prism/src/explicit/Model.java @@ -285,8 +285,16 @@ public interface Model /** * Export transition matrix to explicit format readable by PRISM (i.e. a .tra file). */ - public void exportToPrismExplicitTra(PrismLog log); - + public default void exportToPrismExplicitTra(PrismLog log) throws PrismException + { + exportToPrismExplicitTra(log, prism.Prism.EXPORT_PLAIN); + } + + /** + * Export transition matrix to explicit format readable by PRISM (i.e. a .tra file). + */ + public void exportToPrismExplicitTra(PrismLog log, int exportType) throws PrismException; + /** * Export to a dot file. * @param filename Name of file to export to diff --git a/prism/src/explicit/ModelExplicit.java b/prism/src/explicit/ModelExplicit.java index c042635d..bfae3c2b 100644 --- a/prism/src/explicit/ModelExplicit.java +++ b/prism/src/explicit/ModelExplicit.java @@ -387,7 +387,7 @@ public abstract class ModelExplicit implements Model } @Override - public abstract void exportToPrismExplicitTra(PrismLog out); + public abstract void exportToPrismExplicitTra(PrismLog out, int exportType) throws PrismException; @Override public abstract void exportToPrismLanguage(String filename) throws PrismException; diff --git a/prism/src/explicit/STPGAbstrSimple.java b/prism/src/explicit/STPGAbstrSimple.java index 02a23c96..d32f8f13 100644 --- a/prism/src/explicit/STPGAbstrSimple.java +++ b/prism/src/explicit/STPGAbstrSimple.java @@ -365,8 +365,15 @@ public class STPGAbstrSimple extends ModelExplicit implements STPG, NondetModelS } @Override - public void exportToPrismExplicitTra(PrismLog out) + public void exportToPrismExplicitTra(PrismLog out, int exportType) throws PrismException { + switch (exportType) { + case prism.Prism.EXPORT_ROWS: + break; + default: + throw new PrismException("Unsupported export type"); + } + int i, j, k; TreeMap sorted; // Output transitions to .tra file diff --git a/prism/src/explicit/SubNondetModel.java b/prism/src/explicit/SubNondetModel.java index 22774544..131a884c 100644 --- a/prism/src/explicit/SubNondetModel.java +++ b/prism/src/explicit/SubNondetModel.java @@ -245,7 +245,7 @@ public class SubNondetModel implements NondetModel } @Override - public void exportToPrismExplicitTra(PrismLog log) + public void exportToPrismExplicitTra(PrismLog log, int exportType) { throw new UnsupportedOperationException(); } diff --git a/prism/src/explicit/modelviews/DTMCView.java b/prism/src/explicit/modelviews/DTMCView.java index d65a96d9..c2186206 100644 --- a/prism/src/explicit/modelviews/DTMCView.java +++ b/prism/src/explicit/modelviews/DTMCView.java @@ -132,8 +132,16 @@ public abstract class DTMCView extends ModelView implements DTMC, Cloneable } @Override - public void exportToPrismExplicitTra(final PrismLog log) + public void exportToPrismExplicitTra(final PrismLog log, int exportType) throws PrismException { + switch (exportType) { + case prism.Prism.EXPORT_PLAIN: + case prism.Prism.EXPORT_ROWS: + break; + default: + throw new PrismException("Unsupported export type"); + } + // Output transitions to .tra file log.print(getNumStates() + " " + getNumTransitions() + "\n"); final TreeMap sorted = new TreeMap<>(); diff --git a/prism/src/explicit/modelviews/MDPView.java b/prism/src/explicit/modelviews/MDPView.java index f88eaf9b..1279c75f 100644 --- a/prism/src/explicit/modelviews/MDPView.java +++ b/prism/src/explicit/modelviews/MDPView.java @@ -120,8 +120,14 @@ public abstract class MDPView extends ModelView implements MDP, Cloneable } @Override - public void exportToPrismExplicitTra(final PrismLog out) + public void exportToPrismExplicitTra(final PrismLog out, int exportType) throws PrismException { + switch (exportType) { + case prism.Prism.EXPORT_PLAIN: + break; + default: + throw new PrismException("Unsupported export type"); + } final int numStates = getNumStates(); // Output transitions to .tra file out.print(numStates + " " + getNumChoices() + " " + getNumTransitions() + "\n"); diff --git a/prism/src/param/ParamModel.java b/prism/src/param/ParamModel.java index c2268b3b..e0b065f9 100644 --- a/prism/src/param/ParamModel.java +++ b/prism/src/param/ParamModel.java @@ -277,7 +277,7 @@ public final class ParamModel extends ModelExplicit implements MDPGeneric