Import and export improvements

prism-examples/pomdps/simple/guess-multi.prism

@@ -9,7 +9,7 @@ observables s, g endobservables
 
 module M
 
-	s : [0..2]; // state
+	s : [0..3]; // state
 	h : [0..3]; // hidden var
 	g : [0..N] init N; // num guesses left
 

prism-examples/pomdps/simple/guess.prism

@@ -6,7 +6,7 @@ observables s endobservables
 
 module M
 
-	s : [0..2]; // state
+	s : [0..3]; // state
 	h : [0..3]; // hidden var
 
 	// Assign hidden variable randomly

prism-tests/functionality/export/pomdp/maze.prism.tra

@@ -1,4 +1,5 @@
 12 21 30 8
+- - 0 - 0
 0 0 1 0.1 1
 0 0 2 0.1 2
 0 0 3 0.1 3

prism-tests/functionality/import/maze.lab

@@ -0,0 +1,2 @@
+0="init" 1="deadlock"
+0: 0

prism-tests/functionality/import/maze.obs

@@ -0,0 +1,9 @@
+(west,east,north,south,target)
+0:(false,false,false,false,false)
+1:(true,false,true,false,false)
+2:(false,false,true,true,false)
+3:(false,false,true,false,false)
+4:(false,true,true,false,false)
+5:(true,true,false,false,false)
+6:(true,true,false,true,false)
+7:(true,true,false,true,true)

prism-tests/functionality/import/maze.prism.importexport.auto

@@ -0,0 +1 @@
+-importmodel maze.all -exportmodel maze.all

prism-tests/functionality/import/maze.prism.orig

@@ -0,0 +1,84 @@
+// maze example (POMDP)
+// Littman, Cassandra and Kaelbling
+// Learning policies for partially observable environments: Scaling up  
+// Technical Report CS, Brown University
+// gxn 29/01/16
+
+// state space (value of variable "s")
+
+//  0  1  2  3  4
+//  5     6     7
+//  8     10    9
+
+// 10 is the target
+
+pomdp
+
+// can observe the walls and target
+observable "west" = s=0|s=5|s=6|s=7|s=8|s=9|s=10; // wall to the west
+observable "east" = s=4|s=5|s=6|s=7|s=8|s=9|s=10; // wall to the east
+observable "north" = s=0|s=1|s=2|s=3|s=4; // wall to the north
+observable "south" = s=1|s=3|s=8|s=9|s=10; // wall to the south
+observable "target" = s=10; //target
+
+module maze
+
+	s : [-1..10];
+
+	// initialisation
+	[] s=-1 -> 0.1 : (s'=0)
+			 + 0.1 : (s'=1)
+			 + 0.1 : (s'=2)
+			 + 0.1 : (s'=3)
+			 + 0.1 : (s'=4)
+			 + 0.1 : (s'=5)
+			 + 0.1 : (s'=6)
+			 + 0.1 : (s'=7)
+			 + 0.1 : (s'=8)
+			 + 0.1 : (s'=9);
+
+	// moving around the maze
+
+	[east] s=0 -> (s'=1);
+	[south] s=0 -> (s'=5);
+
+	[east] s=1 -> (s'=2);
+	[west] s=1 -> (s'=0);
+
+	[east] s=2 -> (s'=3);
+	[west] s=2 -> (s'=1);
+	[south] s=2 -> (s'=6);
+
+	[east] s=3 -> (s'=4);
+	[west] s=3 -> (s'=2);
+
+	[west] s=4 -> (s'=3);
+	[south] s=4 -> (s'=7);
+
+	[north] s=5 -> (s'=0);
+	[south] s=5 -> (s'=8);
+
+	[north] s=6 -> (s'=2);
+	[south] s=6 -> (s'=10);
+
+	[north] s=7 -> (s'=4);
+	[south] s=7 -> (s'=9);
+
+	[north] s=8 -> (s'=5);
+
+	[north] s=9 -> (s'=7);
+
+	// loop when we reach the target
+	[done] s=10 -> true;
+
+endmodule
+
+// reward structure (number of steps to reach the target)
+rewards
+
+	[east] true : 1;
+	[west] true : 1;
+	[north] true : 1;
+	[south] true : 1;
+
+endrewards

prism-tests/functionality/import/maze.srew

@@ -0,0 +1,3 @@
+# Reward structure
+# State rewards
+12 0

prism-tests/functionality/import/maze.sta

@@ -0,0 +1,13 @@
+(s)
+0:(-1)
+1:(0)
+2:(1)
+3:(2)
+4:(3)
+5:(4)
+6:(5)
+7:(6)
+8:(7)
+9:(8)
+10:(9)
+11:(10)

prism-tests/functionality/import/maze.tra

@@ -0,0 +1,32 @@
+12 21 30 8
+- - 0 - 0
+0 0 1 0.1 1
+0 0 2 0.1 2
+0 0 3 0.1 3
+0 0 4 0.1 2
+0 0 5 0.1 4
+0 0 6 0.1 5
+0 0 7 0.1 5
+0 0 8 0.1 5
+0 0 9 0.1 6
+0 0 10 0.1 6
+1 0 2 1 2 east
+1 1 6 1 5 south
+2 0 3 1 3 east
+2 1 1 1 1 west
+3 0 4 1 2 east
+3 1 7 1 5 south
+3 2 2 1 2 west
+4 0 5 1 4 east
+4 1 3 1 3 west
+5 0 8 1 5 south
+5 1 4 1 2 west
+6 0 9 1 6 south
+6 1 1 1 1 north
+7 0 11 1 7 south
+7 1 3 1 3 north
+8 0 10 1 6 south
+8 1 5 1 4 north
+9 0 6 1 5 north
+10 0 8 1 5 north
+11 0 11 1 7 done

prism-tests/functionality/import/maze.trew

@@ -0,0 +1,22 @@
+# Reward structure
+# Transition rewards
+12 21 19
+1 0 2 1
+1 1 6 1
+2 0 3 1
+2 1 1 1
+3 0 4 1
+3 1 7 1
+3 2 2 1
+4 0 5 1
+4 1 3 1
+5 0 8 1
+5 1 4 1
+6 0 9 1
+6 1 1 1
+7 0 11 1
+7 1 3 1
+8 0 10 1
+8 1 5 1
+9 0 6 1
+10 0 8 1

prism-tests/functionality/verify/pomdps/guess-multi.prism

@@ -4,7 +4,7 @@ const int N;
 
 module M
 
-	s : [0..2]; // state
+	s : [0..3]; // state
 	h : [0..3]; // hidden var
 	g : [0..N] init N; // num guesses left
 

prism-tests/functionality/verify/pomdps/guess.prism

@@ -4,7 +4,7 @@ const double p = 0.2;
 
 module M
 
-	s : [0..2]; // state
+	s : [0..3]; // state
 	h : [0..3]; // hidden var
 
 	[toss] s=0 -> 0.1:(s'=1)&(h'=1) + 0.3:(s'=1)&(h'=2) + 0.6:(s'=1)&(h'=3);

prism/src/explicit/ExplicitFiles2Model.java

@@ -112,6 +112,10 @@ public <Value> Model<Value> build(ExplicitModelImporter modelImporter, Evaluator
 			MDP<Value> mdp = isDbl ? (MDP<Value>) new MDPSparse() : new MDPSimple<>();
 			model = (ModelExplicit<Value>) mdp;
 			break;
+		case POMDP:
+			POMDP<Value> pomdp = new POMDPSimple<>();
+			model = (ModelExplicit<Value>) pomdp;
+			break;
 		case IDTMC:
 			IDTMCSimple<Value> idtmc = new IDTMCSimple<>();
 			model = (ModelExplicit<Value>) idtmc;
@@ -159,6 +163,9 @@ public <Value> Model<Value> build(ExplicitModelImporter modelImporter, Evaluator
 		}
 
 		loadStates(modelImporter, model);
+		if (model.getModelType().partiallyObservable()) {
+			loadObservationDefinitions(modelImporter, (POMDPSimple<Value>) model);
+		}
 
 		return model;
 	}
@@ -196,7 +203,28 @@ private void loadStates(ExplicitModelImporter modelImporter, ModelExplicit<?> mo
 		for (int i = 0; i < numStates; i++) {
 			statesList.add(new State(numVars));
 		}
-		modelImporter.extractStates((s, i, o) -> statesList.get(s).setValue(i, o));
+		modelImporter.extractStates((s, i, v) -> statesList.get(s).setValue(i, v));
 		model.setStatesList(statesList);
 	}
+
+	/**
+	 * Load the observation information, and store in model
+	 */
+	private void loadObservationDefinitions(ExplicitModelImporter modelImporter, POMDPSimple<?> model) throws PrismException
+	{
+		int numObservations = model.getNumObservations();
+		int numObservables = modelImporter.getModelInfo().getNumObservables();
+		List<State> observationsList = new ArrayList<>(numObservations);
+		for (int i = 0; i < numObservations; i++) {
+			observationsList.add(new State(numObservables));
+		}
+		modelImporter.extractObservationDefinitions((o, i, v) -> observationsList.get(o).setValue(i, v));
+		model.setObservationsList(observationsList);
+		List<State> statesList = model.getStatesList();
+		if (statesList != null) {
+			model.setUnobservationsList(new ArrayList<>(statesList));
+		} else {
+			throw new PrismException("Can't load observation definitions without a states list");
+		}
+	}
 }

prism/src/explicit/ObservationsSimple.java

@@ -83,16 +83,19 @@ public ObservationsSimple()
 	 */
 	public ObservationsSimple(int numStates)
 	{
-		this.numStates = numStates;
-		observationsList = new ArrayList<>();
-		unobservationsList = new ArrayList<>();
-		observationStates = new ArrayList<>();
-		observablesMap = new ArrayList<>();
-		unobservablesMap = new ArrayList<>();
-		for (int i = 0; i < numStates; i++) {
-			observablesMap.add(-1);
-			unobservablesMap.add(-1);
-		}
+		this();
+		addStates(numStates);
+	}
+
+	/**
+	 * Constructor: initialise storage for observable info when the model has
+	 * {@code numStates} states and {@code numObservations} observations.
+	 */
+	public ObservationsSimple(int numStates, int numObservations)
+	{
+		this();
+		addStates(numStates);
+		addObservations(numObservations);
 	}
 
 	/**
@@ -137,6 +140,17 @@ public ObservationsSimple(ObservationsSimple obs, int permut[])
 
 	// Mutators
 
+	/**
+	 * Initialise observation info for {@code numToAdd} new observations.
+	 */
+	public void addObservations(int numToAdd)
+	{
+		for (int i = 0; i < numToAdd; i++) {
+			observationsList.add(null);
+			observationStates.add(-1);
+		}
+	}
+
 	/**
 	 * Clear observation info for state {@code s}.
 	 */
@@ -212,7 +226,7 @@ public void setObservation(int s, State observ, State unobserv, List<String> obs
 			unobservIndex = unobservationsList.size() - 1;
 		}
 		// Assign the unobservation (index) to the state
-		unobservablesMap.set(s, unobservIndex);
+		setUnobservation(s, unobservIndex);
 	}
 
 	/**
@@ -243,6 +257,17 @@ protected void setObservation(int s, int o, NondetModel model) throws PrismExcep
 		}
 	}
 
+	/**
+	 * Assign unobservation with index u to state s.
+	 * (assumes unobservation has already been added to the list)
+	 * @param s State
+	 * @param u Unobservation
+	 */
+	protected void setUnobservation(int s, int u)
+	{
+		unobservablesMap.set(s, u);
+	}
+
 	/**
 	 * Set the observation for each state {@code s} to be {@code s}.
 	 */

prism/src/explicit/POMDPSimple.java

@@ -33,6 +33,7 @@
 import java.util.Map;
 
 import explicit.rewards.MDPRewards;
+import io.ExplicitModelImporter;
 import parser.State;
 import prism.PrismException;
 import prism.PrismUtils;
@@ -117,6 +118,17 @@ public void addStates(int numToAdd)
 		observations.addStates(numToAdd);
 	}
 
+	@Override
+	public void buildFromExplicitImport(ExplicitModelImporter modelImporter) throws PrismException
+	{
+		super.buildFromExplicitImport(modelImporter);
+		observations = new ObservationsSimple(modelImporter.getNumStates(), modelImporter.getNumObservations());
+		modelImporter.extractObservations(this::setObservation);
+		for (int s = 0; s < numStates; s++) {
+			observations.setUnobservation(s, s);
+		}
+	}
+
 	// Mutators (other)
 
 	/**

prism/src/explicit/graphviz/ShowStatesDecorator.java

@@ -65,7 +65,9 @@ public ShowStatesDecorator(List<State> stateList, Function<Integer, State> obsLi
 	/** Decorate state label by appending the variable information */
 	public Decoration decorateState(int state, Decoration d)
 	{
-		d.labelAddBelow(stateList.get(state).toString());
+		if (stateList != null) {
+			d.labelAddBelow(stateList.get(state).toString());
+		}
 		if (obsList != null) {
 			State o = obsList.apply(state);
 			if (o != null) {

prism/src/io/DotExporter.java

@@ -83,12 +83,14 @@ public void exportModel(Model<Value> model, PrismLog out, Iterable<explicit.grap
 			// Set up Dot Decoration
 			explicit.graphviz.Decoration d = new explicit.graphviz.Decoration(defaults);
 			d.setLabel(Integer.toString(s));
-			if (modelExportOptions.getShowStates() && model.getStatesList() != null) {
-				if (modelType.partiallyObservable()) {
-					d = new explicit.graphviz.ShowStatesDecorator(model.getStatesList(), ((PartiallyObservableModel<Value>) model)::getObservationAsState).decorateState(s, d);
-				} else {
-					d = new explicit.graphviz.ShowStatesDecorator(model.getStatesList()).decorateState(s, d);
-				}
+			boolean showStates = modelExportOptions.getShowStates() && model.getStatesList() != null;
+			boolean showObs = modelType.partiallyObservable() && modelExportOptions.getShowObservations();
+			if (showStates && showObs) {
+				d = new explicit.graphviz.ShowStatesDecorator(model.getStatesList(), ((PartiallyObservableModel<Value>) model)::getObservationAsState).decorateState(s, d);
+			} else if (showStates) {
+				d = new explicit.graphviz.ShowStatesDecorator(model.getStatesList()).decorateState(s, d);
+			} else if (showObs) {
+				d = new explicit.graphviz.ShowStatesDecorator(null, ((PartiallyObservableModel<Value>) model)::getObservationAsState).decorateState(s, d);
 			}
 			if (decorators != null) {
 				for (Decorator decorator : decorators) {