diff --git a/prism/NOTES-PTAS b/prism/NOTES-PTAS
index d9e0d53e..021296b2 100644
--- a/prism/NOTES-PTAS
+++ b/prism/NOTES-PTAS
@@ -1,5 +1,6 @@
-Todo
-----
+
+TODO (before any release)
+-------------------------
 
 * GUI
 
@@ -51,7 +52,8 @@ Where can clocks be used
 * var decl.s
 * generally must be convex (i.e. just conj of constraints) (can be relaxed a bit for digital clocks)
 
-Modules cannot access non-local vars (is this too restrictive, e.g. for message passing?)
+Currently, modules cannot access non-local vars (and there are no globals)
+(this is too restrictive, e.g. for message passing)
 
 Must have single initial state (is this true for digital clocks too?)
 
diff --git a/prism/NOTES-SIM b/prism/NOTES-SIM
index 7ca4d080..3dfa9fae 100644
--- a/prism/NOTES-SIM
+++ b/prism/NOTES-SIM
@@ -2,6 +2,8 @@
 NOW/NEXT
 --------
 
+Updater, esp. local nodet
+
 DTMC with local nondet and actions (~/prism-models/dave-test.nm)
 
 GUI transition box: "true" updates don't display correctly
@@ -10,6 +12,9 @@ GUI transition box: "true" updates don't display correctly
 TODO (before any release)
 -------------------------
 
+* local nondet in Updater (and tidy that class)
+* ChoiceListFlexi TODOs
+
 
 TODO (later)
 ------------
@@ -27,6 +32,9 @@ TODO (later)
 
 * explicit build doesn't handle multiple initial states
 
+CODE:
+* Optimise Choices (ChoiceList/ChoiceSingleton/etc.)
+
 BUGS (later)
 ------------