s14h
/
prism-accumulation
1
0
Fork 0
Code Releases Activity
Browse Source

Explicit models: Move exportToDot methods to default implementations in interfaces.

accumulation-v4.7
Dave Parker 6 years ago
parent
4c6ce6f4d8
commit
d4cf7a59ee
11 changed files with 125 additions and 243 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 13
      prism/src/automata/LTSFromDA.java
  2. 21
      prism/src/explicit/DTMC.java
  3. 20
      prism/src/explicit/DTMCExplicit.java
  4. 21
      prism/src/explicit/LTS.java
  5. 19
      prism/src/explicit/LTSExplicit.java
  6. 77
      prism/src/explicit/MDP.java
  7. 80
      prism/src/explicit/MDPExplicit.java
  8. 3
      prism/src/explicit/Model.java
  9. 1
      prism/src/explicit/NondetModel.java
  10. 32
      prism/src/explicit/modelviews/DTMCView.java
  11. 81
      prism/src/explicit/modelviews/MDPView.java

13
prism/src/automata/LTSFromDA.java
View File

@ -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");
}
}

21
prism/src/explicit/DTMC.java
View File

@ -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<explicit.graphviz.Decorator> decorators)
{
Iterator<Map.Entry<Integer, Double>> iter = getTransitionsIterator(i);
while (iter.hasNext()) {
Map.Entry<Integer, Double> 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
/**

20
prism/src/explicit/DTMCExplicit.java
View File

@ -47,26 +47,6 @@ public abstract class DTMCExplicit extends ModelExplicit implements DTMC
{
// Accessors (for Model)
@Override
public void exportTransitionsToDotFile(int i, PrismLog out, Iterable<explicit.graphviz.Decorator> decorators)
{
Iterator<Map.Entry<Integer, Double>> iter = getTransitionsIterator(i);
while (iter.hasNext()) {
Map.Entry<Integer, Double> 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
{

21
prism/src/explicit/LTS.java
View File

@ -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<explicit.graphviz.Decorator> decorators)
{
for (Iterator<Integer> 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();
}
}

19
prism/src/explicit/LTSExplicit.java
View File

@ -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<explicit.graphviz.Decorator> decorators)
{
for (Iterator<Integer> 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
{

77
prism/src/explicit/MDP.java
View File

@ -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<Double>
}
}
@Override
default void exportTransitionsToDotFile(int i, PrismLog out, Iterable<explicit.graphviz.Decorator> 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<Map.Entry<Integer, Double>> iter = getTransitionsIterator(i, j);
while (iter.hasNext()) {
Map.Entry<Integer, Double> 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<Map.Entry<Integer, Double>> iter = getTransitionsIterator(i, j);
while (iter.hasNext()) {
Map.Entry<Integer, Double> e = iter.next();
out.print(nij + " -> " + e.getKey() + " [ label=\"" + e.getValue() + "\"" + style + " ];\n");
}
}
}
out.print("}\n");
}
// Accessors
/**

80
prism/src/explicit/MDPExplicit.java
View File

@ -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<explicit.graphviz.Decorator> 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<Map.Entry<Integer, Double>> iter = getTransitionsIterator(i, j);
while (iter.hasNext()) {
Map.Entry<Integer, Double> 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<Map.Entry<Integer, Double>> iter = getTransitionsIterator(i, j);
while (iter.hasNext()) {
Map.Entry<Integer, Double> e = iter.next();
out.print(nij + " -> " + e.getKey() + " [ label=\"" + e.getValue() + "\"" + style + " ];\n");
}
}
}
out.print("}\n");
}
@Override
public void exportToPrismLanguage(String filename) throws PrismException
{

3
prism/src/explicit/Model.java
View File

@ -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);
}

1
prism/src/explicit/NondetModel.java
View File

@ -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;

32
prism/src/explicit/modelviews/DTMCView.java
View File

@ -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<Entry<Integer, Double>> 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<explicit.graphviz.Decorator> decorators)
{
Iterator<Map.Entry<Integer, Double>> iter = getTransitionsIterator(i);
while (iter.hasNext()) {
Map.Entry<Integer, Double> 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());
}
}
}

81
prism/src/explicit/modelviews/MDPView.java
View File

@ -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<Entry<Integer, Double>> transitions = getTransitionsIterator(state, choice); transitions.hasNext();) {
Entry<Integer, Double> 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<explicit.graphviz.Decorator> 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<Map.Entry<Integer, Double>> iter = getTransitionsIterator(i, j);
while (iter.hasNext()) {
Map.Entry<Integer, Double> 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(";");
}
}
}
}
Write Preview
Loading…
Cancel
Save