diff --git a/prism/src/automata/LTSFromDA.java b/prism/src/automata/LTSFromDA.java index 9b2d9f88..a1f423b4 100644 --- a/prism/src/automata/LTSFromDA.java +++ b/prism/src/automata/LTSFromDA.java @@ -28,14 +28,13 @@ package automata; import java.util.BitSet; -import prism.ModelType; -import prism.PrismException; -import prism.PrismLog; -import strat.MDStrategy; import explicit.LTS; import explicit.Model; import explicit.ModelExplicit; import explicit.SuccessorsIterator; +import prism.ModelType; +import prism.PrismException; +import strat.MDStrategy; /** * Class giving access to the labelled transition system (LTS) underlying a deterministic automaton (DA). @@ -206,10 +205,4 @@ public class LTSFromDA extends ModelExplicit implements LTS { throw new RuntimeException("Not implemented yet"); } - - @Override - public void exportToDotFileWithStrat(PrismLog out, BitSet mark, int[] strat) - { - throw new RuntimeException("Not implemented yet"); - } } diff --git a/prism/src/explicit/DTMC.java b/prism/src/explicit/DTMC.java index d7fc24db..427b708f 100644 --- a/prism/src/explicit/DTMC.java +++ b/prism/src/explicit/DTMC.java @@ -37,6 +37,7 @@ import prism.Pair; import prism.PrismException; import prism.PrismLog; import prism.PrismUtils; +import explicit.graphviz.Decorator; import explicit.rewards.MCRewards; /** @@ -80,6 +81,26 @@ public interface DTMC extends Model } } + @Override + default void exportTransitionsToDotFile(int i, PrismLog out, Iterable decorators) + { + Iterator> iter = getTransitionsIterator(i); + while (iter.hasNext()) { + Map.Entry e = iter.next(); + out.print(i + " -> " + e.getKey()); + + explicit.graphviz.Decoration d = new explicit.graphviz.Decoration(); + d.setLabel(e.getValue().toString()); + if (decorators != null) { + for (Decorator decorator : decorators) { + d = decorator.decorateProbability(i, e.getKey(), e.getValue(), d); + } + } + + out.println(d.toString()); + } + } + // Accessors /** diff --git a/prism/src/explicit/DTMCExplicit.java b/prism/src/explicit/DTMCExplicit.java index 83ecd994..5158e1e1 100644 --- a/prism/src/explicit/DTMCExplicit.java +++ b/prism/src/explicit/DTMCExplicit.java @@ -47,26 +47,6 @@ public abstract class DTMCExplicit extends ModelExplicit implements DTMC { // Accessors (for Model) - @Override - public void exportTransitionsToDotFile(int i, PrismLog out, Iterable decorators) - { - Iterator> iter = getTransitionsIterator(i); - while (iter.hasNext()) { - Map.Entry e = iter.next(); - out.print(i + " -> " + e.getKey()); - - explicit.graphviz.Decoration d = new explicit.graphviz.Decoration(); - d.setLabel(e.getValue().toString()); - if (decorators != null) { - for (Decorator decorator : decorators) { - d = decorator.decorateProbability(i, e.getKey(), e.getValue(), d); - } - } - - out.println(d.toString()); - } - } - @Override public void exportToPrismLanguage(String filename) throws PrismException { diff --git a/prism/src/explicit/LTS.java b/prism/src/explicit/LTS.java index 2f415085..353fcc2b 100644 --- a/prism/src/explicit/LTS.java +++ b/prism/src/explicit/LTS.java @@ -26,6 +26,9 @@ package explicit; +import java.util.BitSet; +import java.util.Iterator; + import prism.ModelType; import prism.PrismLog; @@ -47,4 +50,22 @@ public interface LTS extends NondetModel { throw new UnsupportedOperationException(); } + + @Override + default void exportTransitionsToDotFile(int s, PrismLog out, Iterable decorators) + { + for (Iterator it = getSuccessorsIterator(s); it.hasNext(); ) { + Integer successor = it.next(); + // we ignore decorators here + out.println(s + " -> " + successor + ";"); + } + } + + // Accessors (for NondetModel) - default implementations + + @Override + default void exportToDotFileWithStrat(PrismLog out, BitSet mark, int[] strat) + { + throw new UnsupportedOperationException(); + } } diff --git a/prism/src/explicit/LTSExplicit.java b/prism/src/explicit/LTSExplicit.java index b20a70d6..d16f6707 100644 --- a/prism/src/explicit/LTSExplicit.java +++ b/prism/src/explicit/LTSExplicit.java @@ -29,10 +29,8 @@ package explicit; import java.util.ArrayList; import java.util.BitSet; -import java.util.Iterator; import prism.PrismException; -import prism.PrismLog; import strat.MDStrategy; /** @@ -135,12 +133,6 @@ public class LTSExplicit extends ModelExplicit implements LTS throw new UnsupportedOperationException(); } - @Override - public void exportToDotFileWithStrat(PrismLog out, BitSet mark, int[] strat) - { - throw new UnsupportedOperationException(); - } - @Override public SuccessorsIterator getSuccessors(int s) { @@ -177,17 +169,6 @@ public class LTSExplicit extends ModelExplicit implements LTS throw new UnsupportedOperationException(); } - @Override - public void exportTransitionsToDotFile(int s, PrismLog out, Iterable decorators) - { - for (Iterator it = getSuccessorsIterator(s); it.hasNext(); ) { - Integer successor = it.next(); - - // we ignore decorators here - out.println(s + " -> " + successor + ";"); - } - } - @Override public void exportToPrismLanguage(String filename) throws PrismException { diff --git a/prism/src/explicit/MDP.java b/prism/src/explicit/MDP.java index 63e62ed9..cf622ebc 100644 --- a/prism/src/explicit/MDP.java +++ b/prism/src/explicit/MDP.java @@ -37,6 +37,7 @@ import java.util.TreeMap; import java.util.PrimitiveIterator.OfInt; import common.IterableStateSet; +import explicit.graphviz.Decorator; import explicit.rewards.MCRewards; import explicit.rewards.MDPRewards; import prism.ModelType; @@ -88,6 +89,82 @@ public interface MDP extends MDPGeneric } } + @Override + default void exportTransitionsToDotFile(int i, PrismLog out, Iterable decorators) + { + int j, numChoices; + String nij; + Object action; + numChoices = getNumChoices(i); + for (j = 0; j < numChoices; j++) { + action = getAction(i, j); + nij = "n" + i + "_" + j; + out.print(i + " -> " + nij + " "); + + explicit.graphviz.Decoration d = new explicit.graphviz.Decoration(); + d.attributes().put("arrowhead", "none"); + d.setLabel(j + (action != null ? ":" + action : "")); + + if (decorators != null) { + for (Decorator decorator : decorators) { + d = decorator.decorateTransition(i, j, d); + } + } + out.print(d); + out.println(";"); + + 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() + " "); + + d = new explicit.graphviz.Decoration(); + d.setLabel(e.getValue().toString()); + + if (decorators != null) { + for (Decorator decorator : decorators) { + d = decorator.decorateProbability(i, e.getKey(), j, e.getValue(), d); + } + } + + out.print(d); + out.println(";"); + } + } + } + + // Accessors (for NondetModel) - default implementations + + @Override + default void exportToDotFileWithStrat(PrismLog out, BitSet mark, int strat[]) + { + int numStates = getNumStates(); + out.print("digraph " + getModelType() + " {\nnode [shape=box];\n"); + for (int i = 0; i < numStates; i++) { + if (mark != null && mark.get(i)) + out.print(i + " [style=filled fillcolor=\"#cccccc\"]\n"); + int numChoices = getNumChoices(i); + for (int j = 0; j < numChoices; j++) { + String style = (strat[i] == j) ? ",color=\"#ff0000\",fontcolor=\"#ff0000\"" : ""; + Object action = getAction(i, j); + String 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.print("}\n"); + } + // Accessors /** diff --git a/prism/src/explicit/MDPExplicit.java b/prism/src/explicit/MDPExplicit.java index 8289f52f..df148da0 100644 --- a/prism/src/explicit/MDPExplicit.java +++ b/prism/src/explicit/MDPExplicit.java @@ -29,17 +29,14 @@ package explicit; import java.io.FileWriter; import java.io.IOException; -import java.util.BitSet; import java.util.HashSet; import java.util.Iterator; import java.util.Map; import java.util.TreeMap; import prism.PrismException; -import prism.PrismLog; import prism.PrismUtils; import strat.MDStrategy; -import explicit.graphviz.Decorator; /** * Base class for explicit-state representations of an MDP. @@ -70,83 +67,6 @@ public abstract class MDPExplicit extends ModelExplicit implements MDP return s; } - @Override - public void exportTransitionsToDotFile(int i, PrismLog out, Iterable decorators) - { - int j, numChoices; - String nij; - Object action; - numChoices = getNumChoices(i); - for (j = 0; j < numChoices; j++) { - action = getAction(i, j); - nij = "n" + i + "_" + j; - out.print(i + " -> " + nij + " "); - - explicit.graphviz.Decoration d = new explicit.graphviz.Decoration(); - d.attributes().put("arrowhead", "none"); - d.setLabel(j + (action != null ? ":" + action : "")); - - if (decorators != null) { - for (Decorator decorator : decorators) { - d = decorator.decorateTransition(i, j, d); - } - } - out.print(d); - out.println(";"); - - 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() + " "); - - d = new explicit.graphviz.Decoration(); - d.setLabel(e.getValue().toString()); - - if (decorators != null) { - for (Decorator decorator : decorators) { - d = decorator.decorateProbability(i, e.getKey(), j, e.getValue(), d); - } - } - - out.print(d); - out.println(";"); - } - } - } - - @Override - public void exportToDotFileWithStrat(PrismLog out, BitSet mark, int strat[]) - { - int i, j, numChoices; - String nij; - Object action; - String style; - out.print("digraph " + getModelType() + " {\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.print("}\n"); - } - @Override public void exportToPrismLanguage(String filename) throws PrismException { diff --git a/prism/src/explicit/Model.java b/prism/src/explicit/Model.java index 64e6f5e7..570920ff 100644 --- a/prism/src/explicit/Model.java +++ b/prism/src/explicit/Model.java @@ -387,7 +387,8 @@ public interface Model * @param out PrismLog to export to * @param mark States to highlight (ignored if null) */ - default void exportToDotFile(PrismLog out, BitSet mark) { + default void exportToDotFile(PrismLog out, BitSet mark) + { if (mark == null) { exportToDotFile(out); } diff --git a/prism/src/explicit/NondetModel.java b/prism/src/explicit/NondetModel.java index 014af246..ab730993 100644 --- a/prism/src/explicit/NondetModel.java +++ b/prism/src/explicit/NondetModel.java @@ -28,7 +28,6 @@ package explicit; import java.util.BitSet; import java.util.Iterator; -import java.util.PrimitiveIterator; import java.util.function.IntPredicate; import prism.PrismLog; diff --git a/prism/src/explicit/modelviews/DTMCView.java b/prism/src/explicit/modelviews/DTMCView.java index 86447bc3..e288f604 100644 --- a/prism/src/explicit/modelviews/DTMCView.java +++ b/prism/src/explicit/modelviews/DTMCView.java @@ -31,23 +31,19 @@ import java.io.FileWriter; import java.io.IOException; import java.util.AbstractMap; import java.util.Iterator; -import java.util.Map; import java.util.Map.Entry; import java.util.PrimitiveIterator; import java.util.TreeMap; import java.util.function.IntFunction; -import common.IteratorTools; import common.IterableStateSet; +import common.IteratorTools; import common.iterable.MappingIterator; import explicit.DTMC; import explicit.Distribution; import explicit.SuccessorsIterator; -import explicit.graphviz.Decorator; -import prism.ModelType; import prism.Pair; import prism.PrismException; -import prism.PrismLog; import prism.PrismUtils; /** @@ -189,30 +185,4 @@ public abstract class DTMCView extends ModelView implements DTMC, Cloneable final Iterator> transitions = getTransitionsIterator(state); return new MappingIterator.From<>(transitions, transition -> attachAction(transition, null)); } - - - //--- ModelView --- - - /** - * @see explicit.DTMCExplicit#exportTransitionsToDotFile(int, PrismLog) DTMCExplicit - **/ - @Override - public void exportTransitionsToDotFile(int i, PrismLog out, Iterable decorators) - { - Iterator> iter = getTransitionsIterator(i); - while (iter.hasNext()) { - Map.Entry e = iter.next(); - out.print(i + " -> " + e.getKey()); - - explicit.graphviz.Decoration d = new explicit.graphviz.Decoration(); - d.setLabel(e.getValue().toString()); - if (decorators != null) { - for (Decorator decorator : decorators) { - d = decorator.decorateProbability(i, e.getKey(), e.getValue(), d); - } - } - - out.println(d.toString()); - } - } } diff --git a/prism/src/explicit/modelviews/MDPView.java b/prism/src/explicit/modelviews/MDPView.java index 2fac3638..fe14399c 100644 --- a/prism/src/explicit/modelviews/MDPView.java +++ b/prism/src/explicit/modelviews/MDPView.java @@ -29,10 +29,8 @@ package explicit.modelviews; import java.io.FileWriter; import java.io.IOException; -import java.util.BitSet; import java.util.HashSet; import java.util.Iterator; -import java.util.Map; import java.util.Map.Entry; import java.util.PrimitiveIterator; import java.util.TreeMap; @@ -43,9 +41,7 @@ import explicit.Distribution; import explicit.MDP; import explicit.Model; import explicit.SuccessorsIterator; -import explicit.graphviz.Decorator; import prism.PrismException; -import prism.PrismLog; import prism.PrismUtils; import strat.MDStrategy; @@ -237,81 +233,4 @@ public abstract class MDPView extends ModelView implements MDP, Cloneable { return new DTMCFromMDPAndMDStrategy(this, strat); } - - @Override - public void exportToDotFileWithStrat(final PrismLog out, final BitSet mark, final int[] strat) - { - out.print("digraph " + getModelType() + " {\nnode [shape=box];\n"); - for (int state = 0, numStates = getNumStates(); state < numStates; state++) { - if (mark != null && mark.get(state)) - out.print(state + " [style=filled fillcolor=\"#cccccc\"]\n"); - for (int choice = 0, numChoices = getNumChoices(state); choice < numChoices; choice++) { - final String style = (strat[state] == choice) ? ",color=\"#ff0000\",fontcolor=\"#ff0000\"" : ""; - final Object action = getAction(state, choice); - final String nij = "n" + state + "_" + choice; - out.print(state + " -> " + nij + " [ arrowhead=none,label=\"" + choice); - if (action != null) { - out.print(":" + action); - } - out.print("\"" + style + " ];\n"); - out.print(nij + " [ shape=point,height=0.1,label=\"\"" + style + " ];\n"); - for (Iterator> transitions = getTransitionsIterator(state, choice); transitions.hasNext();) { - Entry trans = transitions.next(); - out.print(nij + " -> " + trans.getKey() + " [ label=\"" + trans.getValue() + "\"" + style + " ];\n"); - } - } - } - out.print("}\n"); - } - - //--- ModelView --- - - /** - * @see explicit.MDPExplicit#exportTransitionsToDotFile(int, PrismLog) MDPExplicit - **/ - @Override - public void exportTransitionsToDotFile(int i, PrismLog out, Iterable decorators) - { - int j, numChoices; - String nij; - Object action; - numChoices = getNumChoices(i); - for (j = 0; j < numChoices; j++) { - action = getAction(i, j); - nij = "n" + i + "_" + j; - out.print(i + " -> " + nij + " "); - - explicit.graphviz.Decoration d = new explicit.graphviz.Decoration(); - d.attributes().put("arrowhead", "none"); - d.setLabel(j + (action != null ? ":" + action : "")); - - if (decorators != null) { - for (Decorator decorator : decorators) { - d = decorator.decorateTransition(i, j, d); - } - } - out.print(d); - out.println(";"); - - 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() + " "); - - d = new explicit.graphviz.Decoration(); - d.setLabel(e.getValue().toString()); - - if (decorators != null) { - for (Decorator decorator : decorators) { - d = decorator.decorateProbability(i, e.getKey(), j, e.getValue(), d); - } - } - - out.print(d); - out.println(";"); - } - } - } }