From 21748bcaa4da9ba61b2d8ba1eecf403b4b05d82c Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Wed, 16 Apr 2014 10:25:57 +0000 Subject: [PATCH] Tidy up of export-to-Dot functionality, plus new "dot" option for exporting strategy (explicit engine only, currently). git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@8110 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/explicit/DTMCExplicit.java | 28 +-- prism/src/explicit/MDP.java | 6 - prism/src/explicit/MDPExplicit.java | 90 ++++---- prism/src/explicit/Model.java | 10 + prism/src/explicit/ModelExplicit.java | 28 +-- prism/src/explicit/NondetModel.java | 8 + prism/src/explicit/STPGAbstrSimple.java | 52 ++--- prism/src/explicit/SubNondetModel.java | 274 +++++++++++++++--------- prism/src/param/ParamModel.java | 12 ++ prism/src/prism/Prism.java | 14 +- prism/src/prism/PrismCL.java | 2 + prism/src/strat/MDStrategyArray.java | 6 + prism/src/strat/MDStrategyIV.java | 19 +- prism/src/strat/Strategy.java | 5 + 14 files changed, 329 insertions(+), 225 deletions(-) diff --git a/prism/src/explicit/DTMCExplicit.java b/prism/src/explicit/DTMCExplicit.java index f89509ef..5ecce327 100644 --- a/prism/src/explicit/DTMCExplicit.java +++ b/prism/src/explicit/DTMCExplicit.java @@ -96,27 +96,21 @@ public abstract class DTMCExplicit extends ModelExplicit implements DTMC } @Override - public void exportToDotFile(String filename, BitSet mark) throws PrismException + public void exportToDotFile(PrismLog out, BitSet mark) { int i; - try { - FileWriter out = new FileWriter(filename); - out.write("digraph " + getModelType() + " {\nsize=\"8,5\"\nnode [shape=box];\n"); - for (i = 0; i < numStates; i++) { - if (mark != null && mark.get(i)) - out.write(i + " [style=filled fillcolor=\"#cccccc\"]\n"); - Iterator> iter = getTransitionsIterator(i); - while (iter.hasNext()) { - Map.Entry e = iter.next(); - out.write(i + " -> " + e.getKey() + " [ label=\""); - out.write(e.getValue() + "\" ];\n"); - } + out.print("digraph " + getModelType() + " {\nsize=\"8,5\"\nnode [shape=box];\n"); + for (i = 0; i < numStates; i++) { + if (mark != null && mark.get(i)) + out.print(i + " [style=filled fillcolor=\"#cccccc\"]\n"); + Iterator> iter = getTransitionsIterator(i); + while (iter.hasNext()) { + Map.Entry e = iter.next(); + out.print(i + " -> " + e.getKey() + " [ label=\""); + out.print(e.getValue() + "\" ];\n"); } - out.write("}\n"); - out.close(); - } catch (IOException e) { - throw new PrismException("Could not write " + getModelType() + " to file \"" + filename + "\"" + e); } + out.print("}\n"); } @Override diff --git a/prism/src/explicit/MDP.java b/prism/src/explicit/MDP.java index 8835e3dd..fb8c98f6 100644 --- a/prism/src/explicit/MDP.java +++ b/prism/src/explicit/MDP.java @@ -31,7 +31,6 @@ import java.util.Iterator; import java.util.List; import java.util.Map.Entry; -import prism.PrismException; import explicit.rewards.MCRewards; import explicit.rewards.MDPRewards; @@ -277,9 +276,4 @@ public interface MDP extends NondetModel * @param dest Vector to write result to. */ public void mvMultRight(int[] states, int[] strat, double[] source, double[] dest); - - /** - * Export to a dot file, highlighting states in 'mark' and choices for a (memoryless) strategy. - */ - public void exportToDotFileWithStrat(String filename, BitSet mark, int strat[]) throws PrismException; } diff --git a/prism/src/explicit/MDPExplicit.java b/prism/src/explicit/MDPExplicit.java index 3b262c3d..d0ab45eb 100644 --- a/prism/src/explicit/MDPExplicit.java +++ b/prism/src/explicit/MDPExplicit.java @@ -108,75 +108,63 @@ public abstract class MDPExplicit extends ModelExplicit implements MDP } @Override - public void exportToDotFile(String filename, BitSet mark) throws PrismException + public void exportToDotFile(PrismLog out, BitSet mark) { int i, j, numChoices; String nij; Object action; - try { - FileWriter out = new FileWriter(filename); - out.write("digraph " + getModelType() + " {\nsize=\"8,5\"\nnode [shape=box];\n"); - for (i = 0; i < numStates; i++) { - if (mark != null && mark.get(i)) - out.write(i + " [style=filled fillcolor=\"#cccccc\"]\n"); - numChoices = getNumChoices(i); - for (j = 0; j < numChoices; j++) { - action = getAction(i, j); - nij = "n" + i + "_" + j; - out.write(i + " -> " + nij + " [ arrowhead=none,label=\"" + j); - if (action != null) - out.write(":" + action); - out.write("\" ];\n"); - out.write(nij + " [ shape=point,width=0.1,height=0.1,label=\"\" ];\n"); - Iterator> iter = getTransitionsIterator(i, j); - while (iter.hasNext()) { - Map.Entry e = iter.next(); - out.write(nij + " -> " + e.getKey() + " [ label=\"" + e.getValue() + "\" ];\n"); - } + out.print("digraph " + getModelType() + " {\nsize=\"8,5\"\nnode [shape=box];\n"); + for (i = 0; i < numStates; i++) { + if (mark != null && mark.get(i)) + out.print(i + " [style=filled fillcolor=\"#cccccc\"]\n"); + numChoices = getNumChoices(i); + for (j = 0; j < numChoices; j++) { + action = getAction(i, j); + nij = "n" + i + "_" + j; + out.print(i + " -> " + nij + " [ arrowhead=none,label=\"" + j); + if (action != null) + out.print(":" + action); + out.print("\" ];\n"); + out.print(nij + " [ shape=point,width=0.1,height=0.1,label=\"\" ];\n"); + Iterator> iter = getTransitionsIterator(i, j); + while (iter.hasNext()) { + Map.Entry e = iter.next(); + out.print(nij + " -> " + e.getKey() + " [ label=\"" + e.getValue() + "\" ];\n"); } } - out.write("}\n"); - out.close(); - } catch (IOException e) { - throw new PrismException("Could not write " + getModelType() + " to file \"" + filename + "\"" + e); } + out.print("}\n"); } @Override - public void exportToDotFileWithStrat(String filename, BitSet mark, int strat[]) throws PrismException + public void exportToDotFileWithStrat(PrismLog out, BitSet mark, int strat[]) { int i, j, numChoices; String nij; Object action; String style; - try { - FileWriter out = new FileWriter(filename); - out.write("digraph " + getModelType() + " {\nsize=\"8,5\"\nnode [shape=box];\n"); - for (i = 0; i < numStates; i++) { - if (mark != null && mark.get(i)) - out.write(i + " [style=filled fillcolor=\"#cccccc\"]\n"); - numChoices = getNumChoices(i); - for (j = 0; j < numChoices; j++) { - style = (strat[i] == j) ? ",color=\"#ff0000\",fontcolor=\"#ff0000\"" : ""; - action = getAction(i, j); - nij = "n" + i + "_" + j; - out.write(i + " -> " + nij + " [ arrowhead=none,label=\"" + j); - if (action != null) - out.write(":" + action); - out.write("\"" + style + " ];\n"); - out.write(nij + " [ shape=point,height=0.1,label=\"\"" + style + " ];\n"); - Iterator> iter = getTransitionsIterator(i, j); - while (iter.hasNext()) { - Map.Entry e = iter.next(); - out.write(nij + " -> " + e.getKey() + " [ label=\"" + e.getValue() + "\"" + style + " ];\n"); - } + out.print("digraph " + getModelType() + " {\nsize=\"8,5\"\nnode [shape=box];\n"); + for (i = 0; i < numStates; i++) { + if (mark != null && mark.get(i)) + out.print(i + " [style=filled fillcolor=\"#cccccc\"]\n"); + numChoices = getNumChoices(i); + for (j = 0; j < numChoices; j++) { + style = (strat[i] == j) ? ",color=\"#ff0000\",fontcolor=\"#ff0000\"" : ""; + action = getAction(i, j); + nij = "n" + i + "_" + j; + out.print(i + " -> " + nij + " [ arrowhead=none,label=\"" + j); + if (action != null) + out.print(":" + action); + out.print("\"" + style + " ];\n"); + out.print(nij + " [ shape=point,height=0.1,label=\"\"" + style + " ];\n"); + Iterator> iter = getTransitionsIterator(i, j); + while (iter.hasNext()) { + Map.Entry e = iter.next(); + out.print(nij + " -> " + e.getKey() + " [ label=\"" + e.getValue() + "\"" + style + " ];\n"); } } - out.write("}\n"); - out.close(); - } catch (IOException e) { - throw new PrismException("Could not write " + getModelType() + " to file \"" + filename + "\"" + e); } + out.print("}\n"); } @Override diff --git a/prism/src/explicit/Model.java b/prism/src/explicit/Model.java index 6567041f..4cebd024 100644 --- a/prism/src/explicit/Model.java +++ b/prism/src/explicit/Model.java @@ -203,6 +203,16 @@ public interface Model */ public void exportToDotFile(String filename, BitSet mark) throws PrismException; + /** + * Export to a dot file. + */ + public void exportToDotFile(PrismLog out); + + /** + * Export to a dot file, highlighting states in 'mark'. + */ + public void exportToDotFile(PrismLog out, BitSet mark); + /** * Export to a equivalent PRISM language model description. */ diff --git a/prism/src/explicit/ModelExplicit.java b/prism/src/explicit/ModelExplicit.java index 38db438f..3aaac05d 100644 --- a/prism/src/explicit/ModelExplicit.java +++ b/prism/src/explicit/ModelExplicit.java @@ -288,21 +288,13 @@ public abstract class ModelExplicit implements Model @Override public void exportToPrismExplicitTra(String filename) throws PrismException { - PrismLog tmpLog = new PrismFileLog(filename); - if (!tmpLog.ready()) { - throw new PrismException("Could not open file \"" + filename + "\" for output"); - } - exportToPrismExplicitTra(tmpLog); + exportToPrismExplicitTra(PrismFileLog.create(filename)); } @Override public void exportToPrismExplicitTra(File file) throws PrismException { - PrismLog tmpLog = new PrismFileLog(file.getPath()); - if (!tmpLog.ready()) { - throw new PrismException("Could not open file \"" + file + "\" for output"); - } - exportToPrismExplicitTra(new PrismFileLog(file.getPath())); + exportToPrismExplicitTra(PrismFileLog.create(file.getPath())); } @Override @@ -311,11 +303,23 @@ public abstract class ModelExplicit implements Model @Override public void exportToDotFile(String filename) throws PrismException { - exportToDotFile(filename, null); + exportToDotFile(PrismFileLog.create(filename), null); + } + + @Override + public void exportToDotFile(String filename, BitSet mark) throws PrismException + { + exportToDotFile(PrismFileLog.create(filename), mark); + } + + @Override + public void exportToDotFile(PrismLog out) + { + exportToDotFile(out, null); } @Override - public abstract void exportToDotFile(String filename, BitSet mark) throws PrismException; + public abstract void exportToDotFile(PrismLog out, BitSet mark); @Override public abstract void exportToPrismLanguage(String filename) throws PrismException; diff --git a/prism/src/explicit/NondetModel.java b/prism/src/explicit/NondetModel.java index ebe0b21d..02b1fbeb 100644 --- a/prism/src/explicit/NondetModel.java +++ b/prism/src/explicit/NondetModel.java @@ -30,6 +30,9 @@ import java.util.BitSet; import java.util.Iterator; import java.util.Map.Entry; +import prism.PrismException; +import prism.PrismLog; + import strat.MDStrategy; /** @@ -91,4 +94,9 @@ public interface NondetModel extends Model * @param strat (Memoryless) strategy to use */ public Model constructInducedModel(MDStrategy strat); + + /** + * Export to a dot file, highlighting states in 'mark' and choices for a (memoryless) strategy. + */ + public void exportToDotFileWithStrat(PrismLog out, BitSet mark, int strat[]); } \ No newline at end of file diff --git a/prism/src/explicit/STPGAbstrSimple.java b/prism/src/explicit/STPGAbstrSimple.java index cb7524c5..5752ab8d 100644 --- a/prism/src/explicit/STPGAbstrSimple.java +++ b/prism/src/explicit/STPGAbstrSimple.java @@ -394,41 +394,41 @@ public class STPGAbstrSimple extends ModelExplicit implements STPG, NondetModelS } @Override - public void exportToDotFile(String filename, BitSet mark) throws PrismException + public void exportToDotFile(PrismLog out, BitSet mark) { int i, j, k; String nij, nijk; - try { - FileWriter out = new FileWriter(filename); - out.write("digraph " + getModelType() + " {\nsize=\"8,5\"\nnode [shape=box];\n"); - for (i = 0; i < numStates; i++) { - if (mark != null && mark.get(i)) - out.write(i + " [style=filled fillcolor=\"#cccccc\"]\n"); - j = -1; - for (DistributionSet distrs : trans.get(i)) { - j++; - nij = "n" + i + "_" + j; - out.write(i + " -> " + nij + " [ arrowhead=none,label=\"" + j + "\" ];\n"); - out.write(nij + " [ shape=circle,width=0.1,height=0.1,label=\"\" ];\n"); - k = -1; - for (Distribution distr : distrs) { - k++; - nijk = "n" + i + "_" + j + "_" + k; - out.write(nij + " -> " + nijk + " [ arrowhead=none,label=\"" + k + "\" ];\n"); - out.write(nijk + " [ shape=point,label=\"\" ];\n"); - for (Map.Entry e : distr) { - out.write(nijk + " -> " + e.getKey() + " [ label=\"" + e.getValue() + "\" ];\n"); - } + out.print("digraph " + getModelType() + " {\nsize=\"8,5\"\nnode [shape=box];\n"); + for (i = 0; i < numStates; i++) { + if (mark != null && mark.get(i)) + out.print(i + " [style=filled fillcolor=\"#cccccc\"]\n"); + j = -1; + for (DistributionSet distrs : trans.get(i)) { + j++; + nij = "n" + i + "_" + j; + out.print(i + " -> " + nij + " [ arrowhead=none,label=\"" + j + "\" ];\n"); + out.print(nij + " [ shape=circle,width=0.1,height=0.1,label=\"\" ];\n"); + k = -1; + for (Distribution distr : distrs) { + k++; + nijk = "n" + i + "_" + j + "_" + k; + out.print(nij + " -> " + nijk + " [ arrowhead=none,label=\"" + k + "\" ];\n"); + out.print(nijk + " [ shape=point,label=\"\" ];\n"); + for (Map.Entry e : distr) { + out.print(nijk + " -> " + e.getKey() + " [ label=\"" + e.getValue() + "\" ];\n"); } } } - out.write("}\n"); - out.close(); - } catch (IOException e) { - throw new PrismException("Could not write " + getModelType() + " to file \"" + filename + "\"" + e); } + out.print("}\n"); } + @Override + public void exportToDotFileWithStrat(PrismLog out, BitSet mark, int strat[]) + { + throw new RuntimeException("Not yet supported"); + } + @Override public void exportToPrismLanguage(String filename) throws PrismException { diff --git a/prism/src/explicit/SubNondetModel.java b/prism/src/explicit/SubNondetModel.java index 42b14137..3ad3397a 100644 --- a/prism/src/explicit/SubNondetModel.java +++ b/prism/src/explicit/SubNondetModel.java @@ -44,113 +44,125 @@ import prism.PrismException; import prism.PrismLog; import strat.MDStrategy; -/* +/** * Class for creating a sub-model of any NondetModel, please note the translate* methods * used to translate between state ids for model and sub-model. Created sub-model will have new * state numbering from 0 to number of states in the sub model. - * */ - -public class SubNondetModel implements NondetModel { +public class SubNondetModel implements NondetModel +{ private NondetModel model = null; private BitSet states = null; - private Map actions = null; + private Map actions = null; private BitSet initialStates = null; private List statesList = null; - private Map stateLookupTable = new HashMap(); - private Map> actionLookupTable = new HashMap>(); - private Map inverseStateLookupTable = new HashMap(); - + private Map stateLookupTable = new HashMap(); + private Map> actionLookupTable = new HashMap>(); + private Map inverseStateLookupTable = new HashMap(); + private int numTransitions = 0; private int maxNumChoices = 0; private int numChoices = 0; - - public SubNondetModel(NondetModel model, BitSet states, Map actions, BitSet initialStates) { + + public SubNondetModel(NondetModel model, BitSet states, Map actions, BitSet initialStates) + { this.model = model; this.states = states; this.actions = actions; this.initialStates = initialStates; - + generateStatistics(); generateLookupTable(states, actions); } - + @Override - public ModelType getModelType() { + public ModelType getModelType() + { return model.getModelType(); } @Override - public int getNumStates() { + public int getNumStates() + { return states.cardinality(); } @Override - public int getNumInitialStates() { + public int getNumInitialStates() + { return initialStates.cardinality(); } @Override - public Iterable getInitialStates() { + public Iterable getInitialStates() + { List is = new ArrayList(); - for(int i=initialStates.nextSetBit(0); i>=0; i=initialStates.nextSetBit(i+1)) { + for (int i = initialStates.nextSetBit(0); i >= 0; i = initialStates.nextSetBit(i + 1)) { is.add(translateState(i)); } - + return is; } @Override - public int getFirstInitialState() { + public int getFirstInitialState() + { return translateState(initialStates.nextSetBit(0)); } @Override - public boolean isInitialState(int i) { + public boolean isInitialState(int i) + { return initialStates.get(translateState(i)); } @Override - public int getNumDeadlockStates() { + public int getNumDeadlockStates() + { throw new UnsupportedOperationException(); } @Override - public Iterable getDeadlockStates() { + public Iterable getDeadlockStates() + { throw new UnsupportedOperationException(); } @Override - public StateValues getDeadlockStatesList() { + public StateValues getDeadlockStatesList() + { throw new UnsupportedOperationException(); } @Override - public int getFirstDeadlockState() { + public int getFirstDeadlockState() + { throw new UnsupportedOperationException(); } @Override - public boolean isDeadlockState(int i) { + public boolean isDeadlockState(int i) + { throw new UnsupportedOperationException(); } @Override - - public List getStatesList() { + public List getStatesList() + { //We use lazy generation because in many cases the state list is not //needed - if(statesList == null) { + if (statesList == null) { statesList = generateSubStateList(states); } return statesList; } - - private List generateSubStateList(BitSet states) { + + private List generateSubStateList(BitSet states) + { List statesList = new ArrayList(); - for(int i=0;i getSuccessorsIterator(int s) { + public Iterator getSuccessorsIterator(int s) + { s = translateState(s); - + List succ = new ArrayList(); - for(int i=0;i> it = model.getTransitionsIterator(s,i); - while(it.hasNext()) { + for (int i = 0; i < model.getNumChoices(s); i++) { + if (actions.get(s).get(i)) { + Iterator> it = model.getTransitionsIterator(s, i); + while (it.hasNext()) { int succc = it.next().getKey(); succ.add(inverseTranslateState(succc)); } @@ -188,114 +204,148 @@ public class SubNondetModel implements NondetModel { } return succ.iterator(); } - @Override - public boolean isSuccessor(int s1, int s2) { + public boolean isSuccessor(int s1, int s2) + { s1 = translateState(s1); s2 = translateState(s2); return model.isSuccessor(s1, s2); } @Override - public boolean allSuccessorsInSet(int s, BitSet set) { + public boolean allSuccessorsInSet(int s, BitSet set) + { throw new UnsupportedOperationException(); } @Override - public boolean someSuccessorsInSet(int s, BitSet set) { + public boolean someSuccessorsInSet(int s, BitSet set) + { throw new UnsupportedOperationException(); } - + @Override - public void findDeadlocks(boolean fix) throws PrismException { + public void findDeadlocks(boolean fix) throws PrismException + { throw new UnsupportedOperationException(); } @Override - public void checkForDeadlocks() throws PrismException { + public void checkForDeadlocks() throws PrismException + { throw new UnsupportedOperationException(); } @Override - public void checkForDeadlocks(BitSet except) throws PrismException { + public void checkForDeadlocks(BitSet except) throws PrismException + { throw new UnsupportedOperationException(); } @Override - public void exportToPrismExplicit(String baseFilename) - throws PrismException { + public void exportToPrismExplicit(String baseFilename) throws PrismException + { throw new UnsupportedOperationException(); } @Override - public void exportToPrismExplicitTra(String filename) throws PrismException { + public void exportToPrismExplicitTra(String filename) throws PrismException + { throw new UnsupportedOperationException(); } @Override - public void exportToPrismExplicitTra(File file) throws PrismException { + public void exportToPrismExplicitTra(File file) throws PrismException + { throw new UnsupportedOperationException(); } @Override - public void exportToPrismExplicitTra(PrismLog log) { + public void exportToPrismExplicitTra(PrismLog log) + { throw new UnsupportedOperationException(); } @Override - public void exportToDotFile(String filename) throws PrismException { + public void exportToDotFile(String filename) throws PrismException + { throw new UnsupportedOperationException(); } @Override - public void exportToDotFile(String filename, BitSet mark) - throws PrismException { + public void exportToDotFile(String filename, BitSet mark) throws PrismException + { throw new UnsupportedOperationException(); } @Override - public void exportToPrismLanguage(String filename) throws PrismException { + public void exportToDotFile(PrismLog out) + { throw new UnsupportedOperationException(); } @Override - public void exportStates(int exportType, VarList varList, PrismLog log) - throws PrismException { + public void exportToDotFile(PrismLog out, BitSet mark) + { throw new UnsupportedOperationException(); } @Override - public String infoString() { + public void exportToDotFileWithStrat(PrismLog out, BitSet mark, int strat[]) + { + throw new UnsupportedOperationException(); + } + + @Override + public void exportToPrismLanguage(String filename) throws PrismException + { + throw new UnsupportedOperationException(); + } + + @Override + public void exportStates(int exportType, VarList varList, PrismLog log) throws PrismException + { + throw new UnsupportedOperationException(); + } + + @Override + public String infoString() + { throw new UnsupportedOperationException(); } @Override - public String infoStringTable() { + public String infoStringTable() + { throw new UnsupportedOperationException(); } @Override - public int getNumChoices(int s) { + public int getNumChoices(int s) + { s = translateState(s); return actions.get(s).cardinality(); } @Override - public int getMaxNumChoices() { + public int getMaxNumChoices() + { return maxNumChoices; } @Override - public int getNumChoices() { + public int getNumChoices() + { return numChoices; } @Override - public Object getAction(int s, int i) { + public Object getAction(int s, int i) + { s = translateState(s); i = translateAction(s, i); - + return model.getAction(s, i); } @@ -306,7 +356,8 @@ public class SubNondetModel implements NondetModel { } @Override - public boolean allSuccessorsInSet(int s, int i, BitSet set) { + public boolean allSuccessorsInSet(int s, int i, BitSet set) + { s = translateState(s); i = translateAction(s, i); set = translateSet(set); @@ -315,37 +366,41 @@ public class SubNondetModel implements NondetModel { } @Override - public boolean someSuccessorsInSet(int s, int i, BitSet set) { + public boolean someSuccessorsInSet(int s, int i, BitSet set) + { s = translateState(s); i = translateAction(s, i); set = translateSet(set); return model.someSuccessorsInSet(s, i, set); } - - private BitSet translateSet(BitSet set) { + + private BitSet translateSet(BitSet set) + { BitSet translatedBitSet = new BitSet(); - for (int i = set.nextSetBit(0); i >= 0; i = set.nextSetBit(i+1)) { - translatedBitSet.set(translateState(i)); - } - return translatedBitSet; + for (int i = set.nextSetBit(0); i >= 0; i = set.nextSetBit(i + 1)) { + translatedBitSet.set(translateState(i)); + } + return translatedBitSet; } - - private void generateStatistics() { - for(int i=0;i> it = model.getTransitionsIterator(state, i); - while(it.hasNext()) { + for (int i = 0; i < model.getNumChoices(state); i++) { + Iterator> it = model.getTransitionsIterator(state, i); + while (it.hasNext()) { it.next(); transitions += 1; } @@ -354,51 +409,56 @@ public class SubNondetModel implements NondetModel { } @Override - public Iterator> getTransitionsIterator(int s, int i) { + public Iterator> getTransitionsIterator(int s, int i) + { s = translateState(s); i = translateAction(s, i); - - Map distrs = new HashMap(); - Iterator> it = model.getTransitionsIterator(s, i); - while(it.hasNext()) { + + Map distrs = new HashMap(); + Iterator> it = model.getTransitionsIterator(s, i); + while (it.hasNext()) { Entry e = it.next(); int succ = inverseTranslateState(e.getKey()); distrs.put(succ, e.getValue()); } return distrs.entrySet().iterator(); } - + @Override public Model constructInducedModel(MDStrategy strat) { throw new RuntimeException("Not implemented"); } - - private void generateLookupTable(BitSet states, Map actions) { - for(int i=0;i < model.getNumStates();i++) { - if(states.get(i)) { + + private void generateLookupTable(BitSet states, Map actions) + { + for (int i = 0; i < model.getNumStates(); i++) { + if (states.get(i)) { inverseStateLookupTable.put(i, stateLookupTable.size()); - stateLookupTable.put(stateLookupTable.size(),i); - Map r = new HashMap(); - for(int j=0;j r = new HashMap(); + for (int j = 0; j < model.getNumChoices(i); j++) { + if (actions.get(i).get(j)) { + r.put(r.size(), j); } } - actionLookupTable.put(actionLookupTable.size(),r); + actionLookupTable.put(actionLookupTable.size(), r); } } } - - public int translateState(int s) { + + public int translateState(int s) + { return stateLookupTable.get(s); } - - private int inverseTranslateState(int s) { + + private int inverseTranslateState(int s) + { return inverseStateLookupTable.get(s); } - - public int translateAction(int s, int i) { + + public int translateAction(int s, int i) + { return actionLookupTable.get(s).get(i); } } diff --git a/prism/src/param/ParamModel.java b/prism/src/param/ParamModel.java index f5593ba0..5a9c7617 100644 --- a/prism/src/param/ParamModel.java +++ b/prism/src/param/ParamModel.java @@ -195,6 +195,18 @@ final class ParamModel extends ModelExplicit throw new UnsupportedOperationException(); } + @Override + public void exportToDotFile(PrismLog out) + { + throw new UnsupportedOperationException(); + } + + @Override + public void exportToDotFile(PrismLog out, BitSet mark) + { + throw new UnsupportedOperationException(); + } + @Override public void exportToPrismLanguage(String filename) throws PrismException { diff --git a/prism/src/prism/Prism.java b/prism/src/prism/Prism.java index 3737f0cb..5c5ae770 100644 --- a/prism/src/prism/Prism.java +++ b/prism/src/prism/Prism.java @@ -155,7 +155,7 @@ public class Prism extends PrismComponent implements PrismSettingsListener // Options for type of strategy export public enum StrategyExportType { - ACTIONS, INDICES, INDUCED_MODEL; + ACTIONS, INDICES, INDUCED_MODEL, DOT_FILE; public String description() { switch (this) { @@ -165,6 +165,8 @@ public class Prism extends PrismComponent implements PrismSettingsListener return "as indices"; case INDUCED_MODEL: return "as an induced model"; + case DOT_FILE: + return "as a dot file"; default: return this.toString(); } @@ -2158,7 +2160,9 @@ public class Prism extends PrismComponent implements PrismSettingsListener currentModelExpl.exportToPrismExplicitTra(tmpLog); break; case Prism.EXPORT_MATLAB: + throw new PrismException("Export not yet supported"); case Prism.EXPORT_DOT: + currentModelExpl.exportToDotFile(tmpLog); case Prism.EXPORT_MRMC: case Prism.EXPORT_ROWS: case Prism.EXPORT_DOT_STATES: @@ -2997,6 +3001,9 @@ public class Prism extends PrismComponent implements PrismSettingsListener case INDUCED_MODEL: strat.exportInducedModel(tmpLog); break; + case DOT_FILE: + strat.exportDotFile(tmpLog); + break; } if (file != null) tmpLog.close(); @@ -3475,10 +3482,7 @@ public class Prism extends PrismComponent implements PrismSettingsListener // create new file log or use main log PrismLog tmpLog; if (file != null) { - tmpLog = new PrismFileLog(file.getPath(), append); - if (!tmpLog.ready()) { - throw new PrismException("Could not open file \"" + file + "\" for output"); - } + tmpLog = PrismFileLog.create(file.getPath(), append); } else { tmpLog = mainLog; } diff --git a/prism/src/prism/PrismCL.java b/prism/src/prism/PrismCL.java index fdb1e198..ec5904c2 100644 --- a/prism/src/prism/PrismCL.java +++ b/prism/src/prism/PrismCL.java @@ -1825,6 +1825,8 @@ public class PrismCL implements PrismModelListener exportStratType = StrategyExportType.INDICES; else if (optVal.equals("induced")) exportStratType = StrategyExportType.INDUCED_MODEL; + else if (optVal.equals("dot")) + exportStratType = StrategyExportType.DOT_FILE; else throw new PrismException("Unknown value \"" + optVal + "\" provided for \"type\" option of -exportstrat"); } diff --git a/prism/src/strat/MDStrategyArray.java b/prism/src/strat/MDStrategyArray.java index 63270226..a7ae374a 100644 --- a/prism/src/strat/MDStrategyArray.java +++ b/prism/src/strat/MDStrategyArray.java @@ -103,6 +103,12 @@ public class MDStrategyArray extends MDStrategy dtmcInd.exportToPrismExplicitTra(out); } + @Override + public void exportDotFile(PrismLog out) + { + model.exportToDotFileWithStrat(out, null, choices); + } + @Override public void clear() { diff --git a/prism/src/strat/MDStrategyIV.java b/prism/src/strat/MDStrategyIV.java index d083de0f..9de9cc74 100644 --- a/prism/src/strat/MDStrategyIV.java +++ b/prism/src/strat/MDStrategyIV.java @@ -26,9 +26,12 @@ package strat; +import java.io.FileNotFoundException; import java.util.List; import prism.Model; +import prism.Prism; +import prism.PrismException; import prism.PrismLog; import dv.IntegerVector; @@ -42,7 +45,7 @@ public class MDStrategyIV extends MDStrategy // Other model info private int numStates; private List actions; - // Array storing MD strategy (action index for each state) + // Array storing MD strategy: *action* index (not choice index) for each state private IntegerVector iv; /** @@ -106,6 +109,20 @@ public class MDStrategyIV extends MDStrategy { // TODO } + + @Override + public void exportDotFile(PrismLog out) + { + try { + model.exportToFile(Prism.EXPORT_DOT, true, new java.io.File("a.dot")); + } catch (FileNotFoundException e) { + // TODO Auto-generated catch block + e.printStackTrace(); + } catch (PrismException e) { + // TODO Auto-generated catch block + e.printStackTrace(); + } + } @Override public void clear() diff --git a/prism/src/strat/Strategy.java b/prism/src/strat/Strategy.java index 9900f95b..3d5d3ed5 100644 --- a/prism/src/strat/Strategy.java +++ b/prism/src/strat/Strategy.java @@ -54,6 +54,11 @@ public interface Strategy */ public void exportInducedModel(PrismLog out); + /** + * Export the strategy to a dot file (of the model showing the strategy). + */ + public void exportDotFile(PrismLog out); + /** * Initialise the strategy, based on an initial model state. * @param s Initial state of the model