Removed NOTES from svn (not incl. public release).

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@2769 bbc10eb1-c90d-0410-af57-cb519fbb1720
15 years ago · d6a3a5e357
1 changed files with 0 additions and 207 deletions
--- a/prism/NOTES
+++ b/prism/NOTES
@ -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 <n> and -simmaxrwd <x>
 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