NOTES.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@1990 bbc10eb1-c90d-0410-af57-cb519fbb1720

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?)
 

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)
 ------------