NOTES.

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

prism/NOTES

@@ -10,7 +10,6 @@ Stuff to remove when distributing early copies to people:
 * examples/des
 * examples/explicit
 * src/explicit/PrismSTPGAsbtractRefine
-* {src,classes}/abstraction
 
 -----------------------------------------------------------------------
 
@@ -67,6 +66,16 @@ TODO:
 
 -----------------------------------------------------------------------
 
+Abstraction/refinement:
+
+TODO:
+* exp reach for games
+
+Other notes/ideas:
+* refine opt: don't add ubsets of player1 choices
+
+-----------------------------------------------------------------------
+
 LTL...
 bscc stuff
 - regression testing on ltl stuff with 3 diff options

prism/NOTES-PTAS

@@ -11,6 +11,11 @@ Todo
 
 * Sort VarList (two types - before and after constants evaluated). Need for simulator too.
 
+* Digital clocks: No time-bounded until yet
+* Digital clocks: Translation done sep for each property (e.g. for cmax)?
+
+* BRP example
+
 
 Maybe todo
 ----------
@@ -20,8 +25,6 @@ Maybe todo
 
 * Fix: Creation of new names (adding extra _s) doesn't take into account prop file ot consts etc.
 
-* Digital clocks: Translation done sep for each property (e.g. for cmax)?
-
 * Digital clocks: urgency?
 
 * Digital clocks: optimisations?

prism/NOTES-SIM

@@ -1,16 +1,30 @@
 
-Copied prism-arrays typing stuff
-Disabled .jj stuff so cannot actually create arrays
-Completed update of type system
+NOW/NEXT:
+
+
+work on Sampler classes
+need to get property constants sorted out
+should be specified when passed to sim engine, like for models
+but when are props passed to sim engine? diff for pathgen/sampling?
+what about experiments, e.g. F<=t for t=...?
+
+
+looping
 
-Moved simulator to simulator-old
-Started to build coarse Java-version of SimulatorEngine.
-Currently, just a few statements in automaticChoices...
 
 TODO:
 
+explicitbuildtest doesn't handle dupes in mdps (e.fg. consensus)
+
+explicit build doesn't handle multiple initial states
+
 seed issues (currently twice in one second = same seed)
 
+traviendo export?
+
+approx mc of a property loses any current simulator path in gui.
+is that ok? (seems to be buggy in 3.3.1 anyway)
+
 TEST CASES
 
 [t,t'] examples sent as MRMC bug fix?