diff --git a/prism/NOTES b/prism/NOTES deleted file mode 100644 index ecbeb5fc..00000000 --- a/prism/NOTES +++ /dev/null @@ -1,207 +0,0 @@ -======================================================= -Remove for beta distributions: -======================================================= - -* NOTES - -======================================================= -TODO (before public release of 4.0) -======================================================= - -PRIORITY (next betas) --------- - -* Benchmarks - - Get tar files online (mv all files into "files" for easier tar-ing?) - - Check/tidy - - Links to e.g CTMCs props from below CTMCs table - - Links from each prop to corr model table? - - More labels - - ctmc steady-state split up? - - unique prop names across models? - -* Intervals (e.g. for multiple initial states) plotted in graphs - -* Stat m/c - - Tidy up other new sim options (simmanual, simvar, simmaxrwd) ? - - Add MDP warning - - Sort initial state in sim dialog? - tick box for default initial - is there a bug in this already? - ready for mult init states? - - Result object creation pushed into SimEngine? - Result objects returned from SimEngine + explanation strings - -* PTA fix: digital clocks just non-diagonal again for now -* PTA fix: convex, non-diagonal, etc. - (see DigitalClocks.java.patch) - cases to consider: - - implications in invariants - - Pmax=? [ F "end" & (x<=5) ] - - Then: test with formats09 script - - Then: respond to Nico B (when live) - -* Doc: Adversary generation (e.g. -exportadv switch) -* Doc: Sim switches -simmanual, -simvar and -simmaxrwd - - -THE REST (before 4.0) --------- - -Documentation: -* Fix links from tutorial to manual (and reread/tweak) -* New -exportprism/-exportprismconst/-nobuild switches -* New -exporttarget switch -* Extra reach info switches? -* Some pointers for where to start with PTAs, e.g. where examples are -* SimulatorEngine JavaDoc -* Update other-downloads.php - -Filters, property semantics, etc. -* Integer-valued props displayed as doubles when printed as vector -* Add "single" filter - throws error if filter states > 1? -* Allow other filter types to be spec with {} notation? - and then in doc clarify P>=p[...{filter}] means & not print - (didn't print in 3.3 anyway, despite manual) -* Some info lost with new filters: - old: Result (minimum probability): 0.0 - new: 0.0 (value in the initial state) - can we merge? - -Action labels: -* Check status of export/import trans wrt actions (alll models) -* Finalise tra format with actions (needs to work with MCs too) - - also fix e.g. importtrans, prism-statra -* make action storage optional (when required e.g. for export) (especially for MCs) - -PTAs: -* Find a way to make PTA and multi-obj report that result - is just for initial state; need re-think of filters? -* More tidying of PTA examples - - README files for other (non-firewire) examples - - comments in pctl files, missing ones into autos -* Clarify rewards support (digital clocks) -* More of PCTL - even just G, bounded (not =?), etc. -* Enforce well-formedness checks (i.e. guards/resets imply target invariants) - (as opposed to say supporting strong invariants, - where targets with false invariants cannot be entered) - - zone-based: check during reach using valids - (or just during FW reach?) (nb: need to split dpost to do check) - (see non-well-formed.nm/pctl for a test case) - (if can't do that, syntax check using sat) - - digital clocks: check invariants after transform/reach? - (might be like non-pta case: doing before reach causes false alarms?) -* Digital clocks time-bounded - - will need to make sure cmax is updated accordingly - (currently just from temporal operator time bound since no clocks in formula) - - also might need to access property constants (see TODO in DC.java) -* Allow constraints of the form x-y<=c -* Bug fix: action alphabet (syntactic) for sync lost in PTA object construction - -======================================================= -Post-4.0 fixes/adds (4.0.1 etc.) -======================================================= - -Integrate multi-objective? - -General: -* Error (at least warning) on Pmax=? [ target ] (i.e. no F) (all models) - -Documentation: -* Add DTMC/MDP case to synchronisation section -* Check for existence of zero-reward loops - -PTAs: -* On-the-fly global reachability to allow (for A-R engine): - - more scalable - - access to other local and global vars - - system endsystem? - (then test on Arnd's BRP model + Marco's + others) - -Simulator: -* New display progress meter for simulation? -* SimMethod deal with possibility of more iters than expected - - recalc some stats on computeMissingParameterAfterSim? - - max 100% for getProgress? - - search TODO -* make call to setExpression earlier for earlier detection of errors? - (would need to pass multiple sim methods to Prism) - (but: consts not def yet, e.g. might not know theta) -* merge APMC/etc. triple subclasses? -* store log for likelihood ratio? -* make percentage from getProgress more accurate, do mod 10 after -* do we stil need reset() in SimMethod? Don't delete, just check - -General: -* finish -explicitbuild (e.g. no labels, rewards), currently in -qar -* postpone reward struct constr until needed? - -======================================================= -======================================================= - -BUG (some time) ---------------- - -Simulator: -* approx mc of a property loses any current simulator path in gui. - is that ok? (seems to be buggy in 3.3.1 anyway) - -* prism ~/prism-examples/dice/dice.pm \ --pctl '(s=0|s=1)=>P>=1 [ (P>=0.9 [ F<=1 s=3 ])=>(P>=0.5 [ F<=2 s=4 ]) ]' -(time-bounds should be ok in inner pctl but are not) - -TODO (some time) ----------------- - -PTAs: -* Implement structurally non-zeno checks -* BRP example -* Translate non-convex guards to DNF and multiple transitions -* Investigate whether non-convex invariants can be supported (look at zone ops) -* Games: Optimise number of states in time-bounded PTAs - (extras added in old target states) using until in forwards reach? -* Fix: Creation of new names (adding extra _s) doesn't take into account prop file ot consts etc. -* Digital clocks: urgency? -* Digital clocks: optimisations? -* New version of valid2 (inv/g push outside) -* Combined complement + intersection (terminating early) for when dbm lists get big -* Are we ok to have non-diagonal c-closure algorithm? - (or is it ok if only use this on initial reach graph construction?) - -Simulator: -* Variable overflow etc. - - would make sense to check in Update.update() because want to know offending command - - but need access to VarList, which we don't have -* Investigate efficiency wrt old simulator -* Add (back) support for *full* loop detection? (not just *single* self-loops) -* Add (back) early manual termination of sampling (thru expt stop?) -* Random initial state -* Add support for "deadlock" and "init" (new EvaluationContext, model *and* state dependent) -* Seed issues (currently twice in one second = same seed) -* explicitbuildtest doesn't handle dupes in mdps (e.g. consensus) -* Explicit build doesn't handle multiple initial states -* GUI sim - add context menu to transition list with e.g. "show in model" -* Traviendo export? -* Code: Optimise/tidy Choices (ChoiceList/ChoiceSingleton/etc.) - -Other: -* Export tr/ss probs from GUI -* Initial distr for steady-state -* Finish CTL - -Adversary generation: -* Add adversary generation for other engines - -Abstraction/refinement: -* Exp reach for games -* Poss. refine opt: don't add ubsets of player1 choices - -BSCC stuff: -* regression testing + perf. on ltl stuff with 3 diff options - - -DOC (some time) ---------------- - -Prism-multi: -* No state rewards