Include observations in POMDP Dot model export.

prism/src/explicit/Model.java

@@ -39,6 +39,7 @@ import java.util.TreeMap;
 import java.util.function.IntPredicate;
 
 import common.IteratorTools;
+import explicit.graphviz.Decoration;
 import explicit.graphviz.Decorator;
 import parser.State;
 import parser.Values;
@@ -423,7 +424,11 @@ public interface Model
 	{
 		ArrayList<explicit.graphviz.Decorator> decorators = new ArrayList<explicit.graphviz.Decorator>();
 		if (showStates) {
-			decorators.add(new explicit.graphviz.ShowStatesDecorator(getStatesList()));
+			if (getModelType().partiallyObservable()) {
+				decorators.add(new explicit.graphviz.ShowStatesDecorator(getStatesList(), ((PartiallyObservableModel) this)::getObservationAsState));
+			} else {
+				decorators.add(new explicit.graphviz.ShowStatesDecorator(getStatesList()));
+			}
 		}
 		if (mark != null) {
 			decorators.add(new explicit.graphviz.MarkStateSetDecorator(mark));

prism/src/explicit/graphviz/ShowStatesDecorator.java

@@ -27,6 +27,7 @@
 package explicit.graphviz;
 
 import java.util.List;
+import java.util.function.Function;
 
 import parser.State;
 
@@ -38,6 +39,9 @@ public class ShowStatesDecorator implements Decorator
 	/** The state list, i.e., the variable valuation information for each state index */
 	private List<State> stateList;
 
+	/** Optionally, an observation map, i.e., the observable valuation information for each state index */
+	private Function<Integer, State> obsList;
+
 	/**
 	 * Constructor.
 	 * @param stateList the variable valuation information for each state index
@@ -47,10 +51,27 @@ public class ShowStatesDecorator implements Decorator
 		this.stateList = stateList;
 	}
 
+	/**
+	 * Constructor.
+	 * @param stateList the variable valuation information for each state index
+	 * @param obsList optionally, the observable valuation information for each state index
+	 */
+	public ShowStatesDecorator(List<State> stateList, Function<Integer, State> obsList)
+	{
+		this.stateList = stateList;
+		this.obsList = obsList;
+	}
+
 	/** Decorate state label by appending the variable information */
 	public Decoration decorateState(int state, Decoration d)
 	{
 		d.labelAddBelow(stateList.get(state).toString());
+		if (obsList != null) {
+			State o = obsList.apply(state);
+			if (o != null) {
+				d.labelAddBelow(o.toString());
+			}
+		}
 		return d;
 	}
 }