From 6ee3395544920af667342c981b8397dbb6145fc5 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Thu, 28 May 2020 16:55:03 +0100 Subject: [PATCH] Explicit models: Move exportToPrismLanguage methods to default implementations in interfaces. --- prism/src/automata/LTSFromDA.java | 6 --- prism/src/explicit/DTMC.java | 35 ++++++++++++++ prism/src/explicit/DTMCExplicit.java | 50 ------------------- prism/src/explicit/LTS.java | 7 +++ prism/src/explicit/LTSExplicit.java | 7 --- prism/src/explicit/MDP.java | 42 ++++++++++++++++ prism/src/explicit/MDPExplicit.java | 53 --------------------- prism/src/explicit/ModelExplicit.java | 3 -- prism/src/explicit/STPG.java | 7 +++ prism/src/explicit/STPGAbstrSimple.java | 7 --- prism/src/explicit/STPGExplicit.java | 10 +++- prism/src/explicit/modelviews/DTMCView.java | 38 --------------- prism/src/explicit/modelviews/MDPView.java | 43 ----------------- 13 files changed, 100 insertions(+), 208 deletions(-) diff --git a/prism/src/automata/LTSFromDA.java b/prism/src/automata/LTSFromDA.java index a1f423b4..c453e8fc 100644 --- a/prism/src/automata/LTSFromDA.java +++ b/prism/src/automata/LTSFromDA.java @@ -133,12 +133,6 @@ public class LTSFromDA extends ModelExplicit implements LTS throw new RuntimeException("Not implemented yet"); } - @Override - public void exportToPrismLanguage(String filename) throws PrismException - { - throw new RuntimeException("Not implemented yet"); - } - // Methods to implement NondetModel @Override diff --git a/prism/src/explicit/DTMC.java b/prism/src/explicit/DTMC.java index 427b708f..9742e02a 100644 --- a/prism/src/explicit/DTMC.java +++ b/prism/src/explicit/DTMC.java @@ -26,6 +26,8 @@ package explicit; +import java.io.FileWriter; +import java.io.IOException; import java.util.*; import java.util.Map.Entry; import java.util.PrimitiveIterator.OfInt; @@ -101,6 +103,39 @@ public interface DTMC extends Model } } + @Override + default void exportToPrismLanguage(final String filename) throws PrismException + { + try (FileWriter out = new FileWriter(filename)) { + out.write(getModelType().keyword() + "\n"); + out.write("module M\nx : [0.." + (getNumStates() - 1) + "];\n"); + final TreeMap sorted = new TreeMap(); + for (int state = 0, max = getNumStates(); state < max; state++) { + // Extract transitions and sort by destination state index (to match PRISM-exported files) + for (Iterator> transitions = getTransitionsIterator(state); transitions.hasNext();) { + final Entry transition = transitions.next(); + sorted.put(transition.getKey(), transition.getValue()); + } + // Print out (sorted) transitions + out.write("[]x=" + state + "->"); + boolean first = true; + for (Entry transition : sorted.entrySet()) { + if (first) + first = false; + else + out.write("+"); + // Note use of PrismUtils.formatDouble to match PRISM-exported files + out.write(PrismUtils.formatDouble(transition.getValue()) + ":(x'=" + transition.getKey() + ")"); + } + out.write(";\n"); + sorted.clear(); + } + out.write("endmodule\n"); + } catch (IOException e) { + throw new PrismException("Could not export " + getModelType() + " to file \"" + filename + "\"" + e); + } + } + // Accessors /** diff --git a/prism/src/explicit/DTMCExplicit.java b/prism/src/explicit/DTMCExplicit.java index 5158e1e1..64bd1cdd 100644 --- a/prism/src/explicit/DTMCExplicit.java +++ b/prism/src/explicit/DTMCExplicit.java @@ -26,68 +26,18 @@ package explicit; -import java.io.FileWriter; -import java.io.IOException; import java.util.AbstractMap; import java.util.Iterator; import java.util.Map; -import java.util.TreeMap; import java.util.Map.Entry; -import explicit.graphviz.Decorator; import prism.Pair; -import prism.PrismException; -import prism.PrismLog; -import prism.PrismUtils; /** * Base class for explicit-state representations of a DTMC. */ public abstract class DTMCExplicit extends ModelExplicit implements DTMC { - // Accessors (for Model) - - @Override - public void exportToPrismLanguage(String filename) throws PrismException - { - int i; - boolean first; - FileWriter out; - TreeMap sorted; - try { - // Output transitions to PRISM language file - out = new FileWriter(filename); - out.write(getModelType().keyword() + "\n"); - out.write("module M\nx : [0.." + (numStates - 1) + "];\n"); - sorted = new TreeMap(); - for (i = 0; i < numStates; i++) { - // Extract transitions and sort by destination state index (to match PRISM-exported files) - Iterator> iter = getTransitionsIterator(i); - while (iter.hasNext()) { - Map.Entry e = iter.next(); - sorted.put(e.getKey(), e.getValue()); - } - // Print out (sorted) transitions - out.write("[]x=" + i + "->"); - first = true; - for (Map.Entry e : sorted.entrySet()) { - if (first) - first = false; - else - out.write("+"); - // Note use of PrismUtils.formatDouble to match PRISM-exported files - out.write(PrismUtils.formatDouble(e.getValue()) + ":(x'=" + e.getKey() + ")"); - } - out.write(";\n"); - sorted.clear(); - } - out.write("endmodule\n"); - out.close(); - } catch (IOException e) { - throw new PrismException("Could not export " + getModelType() + " to file \"" + filename + "\"" + e); - } - } - // Accessors (for DTMC) @Override diff --git a/prism/src/explicit/LTS.java b/prism/src/explicit/LTS.java index 353fcc2b..dd10a085 100644 --- a/prism/src/explicit/LTS.java +++ b/prism/src/explicit/LTS.java @@ -30,6 +30,7 @@ import java.util.BitSet; import java.util.Iterator; import prism.ModelType; +import prism.PrismException; import prism.PrismLog; /** @@ -61,6 +62,12 @@ public interface LTS extends NondetModel } } + @Override + default void exportToPrismLanguage(String filename) throws PrismException + { + throw new UnsupportedOperationException(); + } + // Accessors (for NondetModel) - default implementations @Override diff --git a/prism/src/explicit/LTSExplicit.java b/prism/src/explicit/LTSExplicit.java index d16f6707..de14a261 100644 --- a/prism/src/explicit/LTSExplicit.java +++ b/prism/src/explicit/LTSExplicit.java @@ -168,11 +168,4 @@ public class LTSExplicit extends ModelExplicit implements LTS { throw new UnsupportedOperationException(); } - - @Override - public void exportToPrismLanguage(String filename) throws PrismException - { - throw new UnsupportedOperationException(); - } - } diff --git a/prism/src/explicit/MDP.java b/prism/src/explicit/MDP.java index cf622ebc..30a4d525 100644 --- a/prism/src/explicit/MDP.java +++ b/prism/src/explicit/MDP.java @@ -26,6 +26,8 @@ package explicit; +import java.io.FileWriter; +import java.io.IOException; import java.util.ArrayList; import java.util.BitSet; import java.util.Iterator; @@ -41,6 +43,7 @@ import explicit.graphviz.Decorator; import explicit.rewards.MCRewards; import explicit.rewards.MDPRewards; import prism.ModelType; +import prism.PrismException; import prism.PrismLog; import prism.PrismUtils; @@ -135,6 +138,45 @@ public interface MDP extends MDPGeneric } } + @Override + default void exportToPrismLanguage(final String filename) throws PrismException + { + try (FileWriter out = new FileWriter(filename)) { + // Output transitions to PRISM language file + out.write(getModelType().keyword() + "\n"); + final int numStates = getNumStates(); + out.write("module M\nx : [0.." + (numStates - 1) + "];\n"); + final TreeMap sorted = new TreeMap(); + for (int state = 0; state < numStates; state++) { + for (int choice = 0, numChoices = getNumChoices(state); choice < numChoices; choice++) { + // Extract transitions and sort by destination state index (to match PRISM-exported files) + for (Iterator> transitions = getTransitionsIterator(state, choice); transitions.hasNext();) { + final Entry trans = transitions.next(); + sorted.put(trans.getKey(), trans.getValue()); + } + // Print out (sorted) transitions + final Object action = getAction(state, choice); + out.write(action != null ? ("[" + action + "]") : "[]"); + out.write("x=" + state + "->"); + boolean first = true; + for (Entry e : sorted.entrySet()) { + if (first) + first = false; + else + out.write("+"); + // Note use of PrismUtils.formatDouble to match PRISM-exported files + out.write(PrismUtils.formatDouble(e.getValue()) + ":(x'=" + e.getKey() + ")"); + } + out.write(";\n"); + sorted.clear(); + } + } + out.write("endmodule\n"); + } catch (IOException e) { + throw new PrismException("Could not export " + getModelType() + " to file \"" + filename + "\"" + e); + } + } + // Accessors (for NondetModel) - default implementations @Override diff --git a/prism/src/explicit/MDPExplicit.java b/prism/src/explicit/MDPExplicit.java index df148da0..bd3140af 100644 --- a/prism/src/explicit/MDPExplicit.java +++ b/prism/src/explicit/MDPExplicit.java @@ -27,14 +27,8 @@ package explicit; -import java.io.FileWriter; -import java.io.IOException; import java.util.HashSet; -import java.util.Iterator; -import java.util.Map; -import java.util.TreeMap; -import prism.PrismException; import prism.PrismUtils; import strat.MDStrategy; @@ -67,53 +61,6 @@ public abstract class MDPExplicit extends ModelExplicit implements MDP return s; } - @Override - public void exportToPrismLanguage(String filename) throws PrismException - { - int i, j, numChoices; - boolean first; - FileWriter out; - TreeMap sorted; - Object action; - try { - // Output transitions to PRISM language file - out = new FileWriter(filename); - out.write(getModelType().keyword() + "\n"); - out.write("module M\nx : [0.." + (numStates - 1) + "];\n"); - sorted = new TreeMap(); - for (i = 0; i < numStates; i++) { - numChoices = getNumChoices(i); - for (j = 0; j < numChoices; j++) { - // Extract transitions and sort by destination state index (to match PRISM-exported files) - Iterator> iter = getTransitionsIterator(i, j); - while (iter.hasNext()) { - Map.Entry e = iter.next(); - sorted.put(e.getKey(), e.getValue()); - } - // Print out (sorted) transitions - action = getAction(i, j); - out.write(action != null ? ("[" + action + "]") : "[]"); - out.write("x=" + i + "->"); - first = true; - for (Map.Entry e : sorted.entrySet()) { - if (first) - first = false; - else - out.write("+"); - // Note use of PrismUtils.formatDouble to match PRISM-exported files - out.write(PrismUtils.formatDouble(e.getValue()) + ":(x'=" + e.getKey() + ")"); - } - out.write(";\n"); - sorted.clear(); - } - } - out.write("endmodule\n"); - out.close(); - } catch (IOException e) { - throw new PrismException("Could not export " + getModelType() + " to file \"" + filename + "\"" + e); - } - } - // Accessors (for NondetModel) @Override diff --git a/prism/src/explicit/ModelExplicit.java b/prism/src/explicit/ModelExplicit.java index c1ac8269..95e183f4 100644 --- a/prism/src/explicit/ModelExplicit.java +++ b/prism/src/explicit/ModelExplicit.java @@ -355,9 +355,6 @@ public abstract class ModelExplicit implements Model @Override public abstract void checkForDeadlocks(BitSet except) throws PrismException; - @Override - public abstract void exportToPrismLanguage(String filename) throws PrismException; - @Override public void exportStates(int exportType, VarList varList, PrismLog log) throws PrismException { diff --git a/prism/src/explicit/STPG.java b/prism/src/explicit/STPG.java index df064d1f..7dd61e82 100644 --- a/prism/src/explicit/STPG.java +++ b/prism/src/explicit/STPG.java @@ -35,6 +35,7 @@ import java.util.Map.Entry; import explicit.rewards.STPGRewards; import prism.ModelType; +import prism.PrismException; import prism.PrismLog; import prism.PrismUtils; @@ -95,6 +96,12 @@ public interface STPG extends NondetModel } } + @Override + default void exportToPrismLanguage(final String filename) throws PrismException + { + throw new UnsupportedOperationException(); + } + // Accessors /** diff --git a/prism/src/explicit/STPGAbstrSimple.java b/prism/src/explicit/STPGAbstrSimple.java index 12662319..c7877832 100644 --- a/prism/src/explicit/STPGAbstrSimple.java +++ b/prism/src/explicit/STPGAbstrSimple.java @@ -35,7 +35,6 @@ import common.IterableStateSet; import explicit.rewards.STPGRewards; import prism.PrismException; -import prism.PrismNotSupportedException; import prism.PrismLog; import prism.PrismUtils; import strat.MDStrategy; @@ -390,12 +389,6 @@ public class STPGAbstrSimple extends ModelExplicit implements STPG, NondetModelS throw new RuntimeException("Not yet supported"); } - @Override - public void exportToPrismLanguage(String filename) throws PrismException - { - throw new PrismNotSupportedException("Export to STPG PRISM models not supported"); - } - @Override public String infoString() { diff --git a/prism/src/explicit/STPGExplicit.java b/prism/src/explicit/STPGExplicit.java index d7b6c870..fc95ad6d 100644 --- a/prism/src/explicit/STPGExplicit.java +++ b/prism/src/explicit/STPGExplicit.java @@ -36,6 +36,7 @@ import java.util.Map.Entry; import explicit.rewards.MDPRewards; import explicit.rewards.STPGRewards; import prism.ModelType; +import prism.PrismException; import prism.PrismLog; /** @@ -43,7 +44,7 @@ import prism.PrismLog; */ public class STPGExplicit extends MDPSimple implements STPG { - /** Which player owns each state, i.e. stateOwners[i] is owned by player i (1 or 2) */ + /** Which player owns each state,fl i.e. stateOwners[i] is owned by player i (1 or 2) */ protected List stateOwners; // Constructors @@ -163,6 +164,13 @@ public class STPGExplicit extends MDPSimple implements STPG STPG.super.exportToPrismExplicitTra(out); } + @Override + public void exportToPrismLanguage(final String filename) throws PrismException + { + // Resolve conflict: STPG interface does not (currently) extend MDP + STPG.super.exportToPrismLanguage(filename); + } + // Accessors (for STPG) @Override diff --git a/prism/src/explicit/modelviews/DTMCView.java b/prism/src/explicit/modelviews/DTMCView.java index e288f604..63a95e6f 100644 --- a/prism/src/explicit/modelviews/DTMCView.java +++ b/prism/src/explicit/modelviews/DTMCView.java @@ -27,13 +27,10 @@ package explicit.modelviews; -import java.io.FileWriter; -import java.io.IOException; import java.util.AbstractMap; import java.util.Iterator; import java.util.Map.Entry; import java.util.PrimitiveIterator; -import java.util.TreeMap; import java.util.function.IntFunction; import common.IterableStateSet; @@ -43,8 +40,6 @@ import explicit.DTMC; import explicit.Distribution; import explicit.SuccessorsIterator; import prism.Pair; -import prism.PrismException; -import prism.PrismUtils; /** * Base class for a DTMC view, i.e., a virtual DTMC that is obtained @@ -117,39 +112,6 @@ public abstract class DTMCView extends ModelView implements DTMC, Cloneable }, true); } - @Override - public void exportToPrismLanguage(final String filename) throws PrismException - { - try (FileWriter out = new FileWriter(filename)) { - out.write(getModelType().keyword() + "\n"); - out.write("module M\nx : [0.." + (getNumStates() - 1) + "];\n"); - final TreeMap sorted = new TreeMap(); - for (int state = 0, max = getNumStates(); state < max; state++) { - // Extract transitions and sort by destination state index (to match PRISM-exported files) - for (Iterator> transitions = getTransitionsIterator(state); transitions.hasNext();) { - final Entry transition = transitions.next(); - sorted.put(transition.getKey(), transition.getValue()); - } - // Print out (sorted) transitions - out.write("[]x=" + state + "->"); - boolean first = true; - for (Entry transition : sorted.entrySet()) { - if (first) - first = false; - else - out.write("+"); - // Note use of PrismUtils.formatDouble to match PRISM-exported files - out.write(PrismUtils.formatDouble(transition.getValue()) + ":(x'=" + transition.getKey() + ")"); - } - out.write(";\n"); - sorted.clear(); - } - out.write("endmodule\n"); - } catch (IOException e) { - throw new PrismException("Could not export " + getModelType() + " to file \"" + filename + "\"" + e); - } - } - @Override public String infoString() { diff --git a/prism/src/explicit/modelviews/MDPView.java b/prism/src/explicit/modelviews/MDPView.java index fe14399c..184d39f3 100644 --- a/prism/src/explicit/modelviews/MDPView.java +++ b/prism/src/explicit/modelviews/MDPView.java @@ -27,13 +27,10 @@ package explicit.modelviews; -import java.io.FileWriter; -import java.io.IOException; import java.util.HashSet; import java.util.Iterator; import java.util.Map.Entry; import java.util.PrimitiveIterator; -import java.util.TreeMap; import common.IteratorTools; import explicit.DTMCFromMDPAndMDStrategy; @@ -41,7 +38,6 @@ import explicit.Distribution; import explicit.MDP; import explicit.Model; import explicit.SuccessorsIterator; -import prism.PrismException; import prism.PrismUtils; import strat.MDStrategy; @@ -107,45 +103,6 @@ public abstract class MDPView extends ModelView implements MDP, Cloneable return numTransitions; } - @Override - public void exportToPrismLanguage(final String filename) throws PrismException - { - try (FileWriter out = new FileWriter(filename)) { - // Output transitions to PRISM language file - out.write(getModelType().keyword() + "\n"); - final int numStates = getNumStates(); - out.write("module M\nx : [0.." + (numStates - 1) + "];\n"); - final TreeMap sorted = new TreeMap(); - for (int state = 0; state < numStates; state++) { - for (int choice = 0, numChoices = getNumChoices(state); choice < numChoices; choice++) { - // Extract transitions and sort by destination state index (to match PRISM-exported files) - for (Iterator> transitions = getTransitionsIterator(state, choice); transitions.hasNext();) { - final Entry trans = transitions.next(); - sorted.put(trans.getKey(), trans.getValue()); - } - // Print out (sorted) transitions - final Object action = getAction(state, choice); - out.write(action != null ? ("[" + action + "]") : "[]"); - out.write("x=" + state + "->"); - boolean first = true; - for (Entry e : sorted.entrySet()) { - if (first) - first = false; - else - out.write("+"); - // Note use of PrismUtils.formatDouble to match PRISM-exported files - out.write(PrismUtils.formatDouble(e.getValue()) + ":(x'=" + e.getKey() + ")"); - } - out.write(";\n"); - sorted.clear(); - } - } - out.write("endmodule\n"); - } catch (IOException e) { - throw new PrismException("Could not export " + getModelType() + " to file \"" + filename + "\"" + e); - } - } - @Override public String infoString() {