Skip to content

Commit e6752b2

Browse files
davexparkerdavexparker
committed
States/observations optional in Dot file export.
Use e.g. -exportmodel file.dot:states=false,obs=false
1 parent 85e88e1 commit e6752b2

6 files changed

Lines changed: 65 additions & 11 deletions

File tree

‎prism/src/explicit/graphviz/ShowStatesDecorator.java‎

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -65,7 +65,9 @@ public ShowStatesDecorator(List<State> stateList, Function<Integer, State> obsLi
6565
/** Decorate state label by appending the variable information */
6666
public Decoration decorateState(int state, Decoration d)
6767
{
68-
d.labelAddBelow(stateList.get(state).toString());
68+
if (stateList != null) {
69+
d.labelAddBelow(stateList.get(state).toString());
70+
}
6971
if (obsList != null) {
7072
State o = obsList.apply(state);
7173
if (o != null) {

‎prism/src/io/DotExporter.java‎

Lines changed: 8 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -83,12 +83,14 @@ public void exportModel(Model<Value> model, PrismLog out, Iterable<explicit.grap
8383
// Set up Dot Decoration
8484
explicit.graphviz.Decoration d = new explicit.graphviz.Decoration(defaults);
8585
d.setLabel(Integer.toString(s));
86-
if (modelExportOptions.getShowStates() && model.getStatesList() != null) {
87-
if (modelType.partiallyObservable()) {
88-
d = new explicit.graphviz.ShowStatesDecorator(model.getStatesList(), ((PartiallyObservableModel<Value>) model)::getObservationAsState).decorateState(s, d);
89-
} else {
90-
d = new explicit.graphviz.ShowStatesDecorator(model.getStatesList()).decorateState(s, d);
91-
}
86+
boolean showStates = modelExportOptions.getShowStates() && model.getStatesList() != null;
87+
boolean showObs = modelType.partiallyObservable() && modelExportOptions.getShowObservations();
88+
if (showStates && showObs) {
89+
d = new explicit.graphviz.ShowStatesDecorator(model.getStatesList(), ((PartiallyObservableModel<Value>) model)::getObservationAsState).decorateState(s, d);
90+
} else if (showStates) {
91+
d = new explicit.graphviz.ShowStatesDecorator(model.getStatesList()).decorateState(s, d);
92+
} else if (showObs) {
93+
d = new explicit.graphviz.ShowStatesDecorator(null, ((PartiallyObservableModel<Value>) model)::getObservationAsState).decorateState(s, d);
9294
}
9395
if (decorators != null) {
9496
for (Decorator decorator : decorators) {

‎prism/src/io/ModelExportOptions.java‎

Lines changed: 25 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -50,6 +50,11 @@ public class ModelExportOptions implements Cloneable
5050
*/
5151
private Optional<Boolean> showStates = Optional.empty();
5252

53+
/**
54+
* Whether to show full observation details
55+
*/
56+
private Optional<Boolean> showObservations = Optional.empty();
57+
5358
/**
5459
* Whether to show actions
5560
*/
@@ -119,6 +124,15 @@ public ModelExportOptions setShowStates(boolean showStates)
119124
return this;
120125
}
121126

127+
/**
128+
* Set whether to show full observation details.
129+
*/
130+
public ModelExportOptions setShowObservations(boolean showObservations)
131+
{
132+
this.showObservations = Optional.of(showObservations);
133+
return this;
134+
}
135+
122136
/**
123137
* Set whether to show actions.
124138
*/
@@ -160,6 +174,9 @@ public void apply(ModelExportOptions other)
160174
if (other.showStates.isPresent()) {
161175
setShowStates(other.getShowStates());
162176
}
177+
if (other.showObservations.isPresent()) {
178+
setShowObservations(other.getShowObservations());
179+
}
163180
if (other.showActions.isPresent()) {
164181
setShowActions(other.getShowActions());
165182
}
@@ -208,6 +225,14 @@ public boolean getShowStates()
208225
return showStates.orElse(true);
209226
}
210227

228+
/**
229+
* Whether to show full observation details.
230+
*/
231+
public boolean getShowObservations()
232+
{
233+
return showObservations.orElse(true);
234+
}
235+
211236
/**
212237
* Whether to show actions.
213238
*/

‎prism/src/io/ModelExportTask.java‎

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -244,7 +244,6 @@ public static ModelExportTask fromOptions(File file, ModelExportOptions exportOp
244244
break;
245245
case DOT:
246246
exportTask = new ModelExportTask(ModelExportEntity.MODEL, file);
247-
exportTask.getExportOptions().setShowStates(true);
248247
break;
249248
case DRN:
250249
exportTask = new ModelExportTask(ModelExportEntity.MODEL, file);

‎prism/src/prism/Prism.java‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -4656,10 +4656,12 @@ public static ModelExportOptions convertExportType(int exportType)
46564656
case Prism.EXPORT_DOT:
46574657
exportOptions.setFormat(ModelExportFormat.DOT);
46584658
exportOptions.setShowStates(false);
4659+
exportOptions.setShowObservations(false);
46594660
break;
46604661
case Prism.EXPORT_DOT_STATES:
46614662
exportOptions.setFormat(ModelExportFormat.DOT);
46624663
exportOptions.setShowStates(true);
4664+
exportOptions.setShowObservations(true);
46634665
break;
46644666
case Prism.EXPORT_ROWS:
46654667
exportOptions.setFormat(ModelExportFormat.EXPLICIT);

‎prism/src/prism/PrismCL.java‎

Lines changed: 27 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -849,7 +849,7 @@ private void doExports() throws PrismException
849849
try {
850850
File dotFile = File.createTempFile("prism-dot-", ".dot", null);
851851
File dotPdfFile = File.createTempFile("prism-dot-", ".dot.pdf", null);
852-
prism.exportBuiltModelTransitions(dotFile, new ModelExportOptions().setFormat(ModelExportFormat.DOT).setShowStates(true));
852+
prism.exportBuiltModelTransitions(dotFile, new ModelExportOptions().setFormat(ModelExportFormat.DOT).setShowStates(true).setShowObservations(true));
853853
(new ProcessBuilder(new String[]{ "dot", "-Tpdf", "-o", dotPdfFile.getPath(), dotFile.getPath()})).start().waitFor();
854854
(new ProcessBuilder(new String[]{ "open",dotPdfFile.getPath()})).start();
855855
}
@@ -1515,7 +1515,7 @@ else if (sw.equals("exportunordered") || sw.equals("unordered")) {
15151515
// export transition matrix graph to dot file
15161516
else if (sw.equals("exporttransdot")) {
15171517
if (i < args.length - 1) {
1518-
ModelExportOptions exportOptions = new ModelExportOptions().setFormat(ModelExportFormat.DOT).setShowStates(false);
1518+
ModelExportOptions exportOptions = new ModelExportOptions().setFormat(ModelExportFormat.DOT).setShowStates(false).setShowObservations(false);
15191519
modelExportTasks.add(new ModelExportTask(ModelExportTask.ModelExportEntity.MODEL, args[++i], exportOptions));
15201520
} else {
15211521
errorAndExit("No file specified for -" + sw + " switch");
@@ -1524,7 +1524,7 @@ else if (sw.equals("exporttransdot")) {
15241524
// export transition matrix graph to dot file (with states)
15251525
else if (sw.equals("exporttransdotstates")) {
15261526
if (i < args.length - 1) {
1527-
ModelExportOptions exportOptions = new ModelExportOptions().setFormat(ModelExportFormat.DOT).setShowStates(true);
1527+
ModelExportOptions exportOptions = new ModelExportOptions().setFormat(ModelExportFormat.DOT).setShowStates(true).setShowObservations(true);
15281528
modelExportTasks.add(new ModelExportTask(ModelExportTask.ModelExportEntity.MODEL, args[++i], exportOptions));
15291529
} else {
15301530
errorAndExit("No file specified for -" + sw + " switch");
@@ -2163,6 +2163,28 @@ else if (opt.equals("proplabels")) {
21632163
}
21642164
}
21652165
}
2166+
else if (opt.startsWith(sOpt = "states")) {
2167+
if (!opt.startsWith(sOpt + "="))
2168+
throw new PrismException("No value provided for \"" + sOpt + "\" option of -exportmodel");
2169+
String optVal = opt.substring(sOpt.length() + 1);
2170+
if (optVal.equals("true"))
2171+
exportOptions.setShowStates(true);
2172+
else if (optVal.equals("false"))
2173+
exportOptions.setShowStates(false);
2174+
else
2175+
throw new PrismException("Unknown value \"" + optVal + "\" provided for \"reach\" option of -exportstrat");
2176+
}
2177+
else if (opt.startsWith(sOpt = "obs")) {
2178+
if (!opt.startsWith(sOpt + "="))
2179+
throw new PrismException("No value provided for \"" + sOpt + "\" option of -exportmodel");
2180+
String optVal = opt.substring(sOpt.length() + 1);
2181+
if (optVal.equals("true"))
2182+
exportOptions.setShowObservations(true);
2183+
else if (optVal.equals("false"))
2184+
exportOptions.setShowObservations(false);
2185+
else
2186+
throw new PrismException("Unknown value \"" + optVal + "\" provided for \"reach\" option of -exportstrat");
2187+
}
21662188
else if (opt.startsWith(sOpt = "actions")) {
21672189
if (!opt.startsWith(sOpt + "="))
21682190
throw new PrismException("No value provided for \"" + sOpt + "\" option of -exportmodel");
@@ -2762,6 +2784,8 @@ else if (sw.equals("exportmodel")) {
27622784
mainLog.println(" * matlab - same as format=matlab");
27632785
mainLog.println(" * rows - export matrices with one row/distribution on each line");
27642786
mainLog.println(" * proplabels - export labels from a properties file into the same file, too");
2787+
mainLog.println(" * states (=true/false) - include state definitions");
2788+
mainLog.println(" * obs (=true/false) - include observation definitions");
27652789
mainLog.println(" * actions (=true/false) - show actions on choices/transitions");
27662790
mainLog.println(" * headers (=true/false) - include headers when exporting rewards");
27672791
mainLog.println(" * precision (=n) - export probabilities/rewards with n significant decimal places");

0 commit comments

Comments
 (0)