diff --git a/prism/NOTES-PTAS b/prism/NOTES-PTAS
index 23bbab5f..d9e0d53e 100644
--- a/prism/NOTES-PTAS
+++ b/prism/NOTES-PTAS
@@ -14,6 +14,8 @@ Todo
 
 * BRP example
 
+* Clarify issue of PTAs accessing non-local vars (currently don't allow this because doesn't work with AR approach which converts to PTA objects first). But this rules out message passing.
+
 
 Bugs
 ----
@@ -49,5 +51,9 @@ 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?)
+
 Must have single initial state (is this true for digital clocks too?)
 
+Invariants must come straight after var decls
+
diff --git a/prism/NOTES-SIM b/prism/NOTES-SIM
index f57f3879..fac0de4a 100644
--- a/prism/NOTES-SIM
+++ b/prism/NOTES-SIM
@@ -6,7 +6,14 @@ but need to sort out loop detection first?
 embedded into Path*?
 
 
-TODO:
+TODO (before any release):
+
+* variable overflow?
+
+TODO (later):
+
+* random initial state
+
 
 add support "deadlock" and "init" (new EvaluationContext, model *and* state dependent)