diff --git a/prism/NOTES b/prism/NOTES index 5a640a22..5b7c8ddd 100644 --- a/prism/NOTES +++ b/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 diff --git a/prism/NOTES-PTAS b/prism/NOTES-PTAS index 9ded8636..a9b2c9b7 100644 --- a/prism/NOTES-PTAS +++ b/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? diff --git a/prism/NOTES-SIM b/prism/NOTES-SIM index dcff3d48..a919cc01 100644 --- a/prism/NOTES-SIM +++ b/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?