prism-accumulation/prism/NOTES

=======================================================
Remove for beta distributions:
=======================================================

* NOTES

=======================================================
TODO (before public release of 4.0)
=======================================================

PRIORITY (first beta, w/ CAV paper)
--------

* JAVADOC
  - links on front page?


PRIORITY (next betas)
--------

* Benchmarks
  - Get tar files online
  - 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) ?
  - 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: 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

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)

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