diff --git a/prism/NOTES-PTAS b/prism/NOTES-PTAS
index 6b0d94f6..4a583bcd 100644
--- a/prism/NOTES-PTAS
+++ b/prism/NOTES-PTAS
@@ -4,6 +4,8 @@ TODO (before any release)
 
 * GUI
 
+* Tidy prism-examples/pta, incl. delete brp
+
 * Clarify semantic/type checks (consistency with games/digital)
 
 * Check guards/invariants for convexity (for now, neither can be non-convex, see below)
diff --git a/prism/src/explicit/ConstructModel.java b/prism/src/explicit/ConstructModel.java
index ebfba5e3..681619eb 100644
--- a/prism/src/explicit/ConstructModel.java
+++ b/prism/src/explicit/ConstructModel.java
@@ -57,10 +57,10 @@ public class ConstructModel
 		modelType = modulesFile.getModelType();
 		this.initialState = initialState;
 
-		int i, j, nc, nt, src, dest;
 		IndexedSet<State> states;
 		LinkedList<State> explore;
 		State state, stateNew;
+		LabelList ll;
 
 		ModelSimple model = null;
 		DTMCSimple dtmc = null;
@@ -68,8 +68,26 @@ public class ConstructModel
 		MDPSimple mdp = null;
 		Distribution distr = null;
 
+		int i, j, k, nc, nt, nl, src, dest;
+		boolean progressDisplayed;
+		long timer, timerProgress;
+
+		// Starting reachability...
+		mainLog.println("\nExploring reachable state space...");
+		timer = timerProgress = System.currentTimeMillis();
+		progressDisplayed = false;
+
 		// Initialise simulator for this model
 		engine.createNewOnTheFlyPath(modulesFile);
+		
+		// Go through labels: create Bitsets and add to simulator
+		ll = modulesFile.getLabelList();
+		nl = ll.size();
+		ArrayList<BitSet> labels = new ArrayList<BitSet>(nl);
+		for (i = 0; i < nl; i++) {
+			engine.addLabel(ll.getLabel(i));
+			labels.add(new BitSet());
+		}
 
 		// Create a (simple, mutable) model of the appropriate type
 		switch (modelType) {
@@ -102,6 +120,12 @@ public class ConstructModel
 			// Use simulator to explore all choices/transitions from this state
 			engine.initialisePath(state);
 			nc = engine.getNumChoices();
+			// TODO: remove this deadlock check (nc=0) hack
+			for (k = 0; k < nl; k++) {
+				if (nc == 0 && engine.queryLabel(k)) {
+					labels.get(k).set(src);
+				}
+			}
 			for (i = 0; i < nc; i++) {
 				if (modelType == ModelType.MDP) {
 					distr = new Distribution();
@@ -135,14 +159,32 @@ public class ConstructModel
 					mdp.addChoice(src, distr);
 				}
 			}
+			// Print some progress info occasionally
+			if (System.currentTimeMillis() - timerProgress > 3000) {
+				if (!progressDisplayed) {
+					mainLog.print("Number of states so far:");
+					progressDisplayed = true;
+				}
+				mainLog.print(" " + (src + 1));
+				mainLog.flush();
+				timerProgress = System.currentTimeMillis();
+			}
 		}
 
+		// Tidy up progress display
+		if (progressDisplayed)
+			mainLog.println(" " + (src + 1));
+
+		// Reachability complete
+		mainLog.println("State exploration done in " + ((System.currentTimeMillis() - timer) / 1000.0) + " secs.");
+		mainLog.println("States: " + (src + 1));
+
 		//graph.states = states.toArrayList();
 
 		int permut[] = states.buildSortingPermutation();
-		mainLog.println(permut);
+		//mainLog.println(permut);
 
-		mainLog.println("Model: " + model);
+		//mainLog.println("Model: " + model);
 
 		switch (modelType) {
 		case DTMC:
@@ -156,14 +198,31 @@ public class ConstructModel
 			break;
 		}
 
-		mainLog.println(states.size() + " states: " + states);
-		mainLog.println("Model: " + model);
+		//mainLog.println(states.size() + " states: " + states);
+		//mainLog.println("Model: " + model);
 
 		BitSet deadlocks = model.findDeadlocks(true);
 		if (deadlocks.cardinality() > 0) {
 			mainLog.println("Adding self-loops in " + deadlocks.cardinality() + " states...");
 		}
 
+		// Model construction complete
+		timer = System.currentTimeMillis() - timer;
+		mainLog.println("Model construction done in " + (timer / 1000.0) + " secs.");
+		
+		// TODO: clean me up
+		for (i = 0; i < nl; i++) {
+			mainLog.println(labels.get(i));
+			/*ll.getLabel(i);
+			j = 0;
+			for (Map.Entry<State, Integer> e : states.getEntrySet()) {
+				mainLog.println(j + ":" + permut[j] + ":" + e.getValue() + " - ");
+				j++;
+			}*/
+		}
+		
+		//model.exportToPrismLanguage("ctmc.sm");
+		
 		return model;
 	}
 
diff --git a/prism/src/explicit/IndexedSet.java b/prism/src/explicit/IndexedSet.java
index e23530d0..5a67c1b4 100644
--- a/prism/src/explicit/IndexedSet.java
+++ b/prism/src/explicit/IndexedSet.java
@@ -84,6 +84,14 @@ public class IndexedSet<T>
 		return set.size();
 	}
 
+	/**
+	 * Get access to the underlying set of map entries. 
+	 */
+	public Set<Map.Entry<T, Integer>> getEntrySet()
+	{
+		return set.entrySet();
+	}
+	
 	/**
 	 * Create an ArrayList of the states, ordered by index.
 	 */
diff --git a/prism/src/sparse/PS_NondetUntil.cc b/prism/src/sparse/PS_NondetUntil.cc
index 1c1b0576..091ba1e6 100644
--- a/prism/src/sparse/PS_NondetUntil.cc
+++ b/prism/src/sparse/PS_NondetUntil.cc
@@ -319,7 +319,7 @@ jboolean min				// min or max probabilities (true = min, false = max)
 				// But only output a choice if it is in the adversary
 				if (j == adv[i]) {
 					for (k = l2; k < h2; k++) {
-						fprintf(fp_adv, "%d %d %g", i, cols[k], non_zeros[k]);
+						fprintf(fp_adv, "%d 0 %d %g", i, cols[k], non_zeros[k]);
 						if (actions != NULL) fprintf(fp_adv, " %s", actions[j]>0?action_names[actions[j]-1]:"");
 						fprintf(fp_adv, "\n");
 					}