From 1d2bb4a49dd905067299886175e34151837135b9 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Tue, 3 Jun 2014 09:47:06 +0000 Subject: [PATCH] Add option to show states in dot file exported for explicit models (plus some commenting). git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@8390 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/explicit/Model.java | 14 +++++++++ prism/src/explicit/ModelExplicit.java | 43 +++++++++++++++++--------- prism/src/explicit/SubNondetModel.java | 6 ++++ 3 files changed, 49 insertions(+), 14 deletions(-) diff --git a/prism/src/explicit/Model.java b/prism/src/explicit/Model.java index 4cebd024..6980bbb2 100644 --- a/prism/src/explicit/Model.java +++ b/prism/src/explicit/Model.java @@ -195,24 +195,38 @@ public interface Model /** * Export to a dot file. + * @param filename Name of file to export to */ public void exportToDotFile(String filename) throws PrismException; /** * Export to a dot file, highlighting states in 'mark'. + * @param filename Name of file to export to + * @param mark States to highlight (ignored if null) */ public void exportToDotFile(String filename, BitSet mark) throws PrismException; /** * Export to a dot file. + * @param out PrismLog to export to */ public void exportToDotFile(PrismLog out); /** * Export to a dot file, highlighting states in 'mark'. + * @param out PrismLog to export to + * @param mark States to highlight (ignored if null) */ public void exportToDotFile(PrismLog out, BitSet mark); + /** + * Export to a dot file, highlighting states in 'mark'. + * @param out PrismLog to export to + * @param mark States to highlight (ignored if null) + * @param showStates Show state info on nodes? + */ + public void exportToDotFile(PrismLog out, BitSet mark, boolean showStates); + /** * Export to a equivalent PRISM language model description. */ diff --git a/prism/src/explicit/ModelExplicit.java b/prism/src/explicit/ModelExplicit.java index e942d8f5..76ea8109 100644 --- a/prism/src/explicit/ModelExplicit.java +++ b/prism/src/explicit/ModelExplicit.java @@ -49,7 +49,7 @@ import prism.PrismLog; public abstract class ModelExplicit implements Model { // Basic model information - + /** Number of states */ protected int numStates; /** Which states are initial states */ @@ -57,9 +57,9 @@ public abstract class ModelExplicit implements Model /** States that are/were deadlocks. Where requested and where appropriate (DTMCs/MDPs), * these states may have been fixed at build time by adding self-loops. */ protected TreeSet deadlocks; - + // Additional, optional information associated with the model - + /** (Optionally) information about the states of this model, * i.e. the State object corresponding to each state index. */ protected List statesList; @@ -67,8 +67,8 @@ public abstract class ModelExplicit implements Model protected Values constantValues; /** (Optionally) some labels (atomic propositions) associated with the model, * represented as a String->BitSet mapping from their names to the states that satisfy them. */ - protected Map labels = new TreeMap(); - + protected Map labels = new TreeMap(); + // Mutators /** @@ -154,7 +154,7 @@ public abstract class ModelExplicit implements Model { this.statesList = statesList; } - + /** * Set the associated (read-only) constant values. */ @@ -214,7 +214,7 @@ public abstract class ModelExplicit implements Model { return deadlocks.size(); } - + @Override public Iterable getDeadlockStates() { @@ -228,7 +228,7 @@ public abstract class ModelExplicit implements Model for (int dl : deadlocks) { bs.set(dl); } - + return StateValues.createFromBitSet(bs, this); } @@ -243,7 +243,7 @@ public abstract class ModelExplicit implements Model { return deadlocks.contains(i); } - + @Override public List getStatesList() { @@ -261,7 +261,7 @@ public abstract class ModelExplicit implements Model { return labels.get(name); } - + @Override public abstract int getNumTransitions(); @@ -315,11 +315,17 @@ public abstract class ModelExplicit implements Model @Override public void exportToDotFile(PrismLog out) { - exportToDotFile(out, null); + exportToDotFile(out, null, false); } @Override public void exportToDotFile(PrismLog out, BitSet mark) + { + exportToDotFile(out, mark, false); + } + + @Override + public void exportToDotFile(PrismLog out, BitSet mark, boolean showStates) { int i; // Header @@ -331,6 +337,15 @@ public abstract class ModelExplicit implements Model // Transitions for state i exportTransitionsToDotFile(i, out); } + // Append state info (if required) + if (showStates) { + List states = getStatesList(); + if (states != null) { + for (i = 0; i < numStates; i++) { + out.print(i + " [label=\"" + i + "\\n" + states.get(i) + "\"]\n"); + } + } + } // Footer out.print("}\n"); } @@ -341,7 +356,7 @@ public abstract class ModelExplicit implements Model * @param out PrismLog for output */ protected abstract void exportTransitionsToDotFile(int i, PrismLog out); - + @Override public abstract void exportToPrismLanguage(String filename) throws PrismException; @@ -350,7 +365,7 @@ public abstract class ModelExplicit implements Model { if (statesList == null) return; - + // Print header: list of model vars if (exportType == Prism.EXPORT_MATLAB) log.print("% "); @@ -378,7 +393,7 @@ public abstract class ModelExplicit implements Model if (exportType == Prism.EXPORT_MATLAB) log.println("];"); } - + @Override public abstract String infoString(); diff --git a/prism/src/explicit/SubNondetModel.java b/prism/src/explicit/SubNondetModel.java index 3ad3397a..ade6b67b 100644 --- a/prism/src/explicit/SubNondetModel.java +++ b/prism/src/explicit/SubNondetModel.java @@ -291,6 +291,12 @@ public class SubNondetModel implements NondetModel throw new UnsupportedOperationException(); } + @Override + public void exportToDotFile(PrismLog out, BitSet mark, boolean showStates) + { + throw new UnsupportedOperationException(); + } + @Override public void exportToDotFileWithStrat(PrismLog out, BitSet mark, int strat[]) {