diff --git a/prism/src/explicit/Model.java b/prism/src/explicit/Model.java index e467d18f..e80a1a7f 100644 --- a/prism/src/explicit/Model.java +++ b/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 decorators = new ArrayList(); 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)); diff --git a/prism/src/explicit/graphviz/ShowStatesDecorator.java b/prism/src/explicit/graphviz/ShowStatesDecorator.java index c24d25a6..10d8b48b 100644 --- a/prism/src/explicit/graphviz/ShowStatesDecorator.java +++ b/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 stateList; + /** Optionally, an observation map, i.e., the observable valuation information for each state index */ + private Function 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 stateList, Function 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; } }