Remove for beta distributions:
------------------------------
* NOTES

=======================================================

TODO (before any release)
-------------------------
  
* Adversary generation (e.g. -exportadv switch)

fix prob 1 for <=t ?

=======================================================

TODO (before public release)
----------------------------

Documentation:
* Fix links from tutorial to manual (and reread/tweak)
* Add DTMC/MDP case to synchronisation section
* New -exportprism/-exportprismconst/-nobuild switches
* Check for existence of zero-reward loops
* New -exporttarget switch
* Extra reach info switches?

Filters, property semantics, etc.
* Integer-valued props displayed as doubles when printed as vector
* Intervals (e.g. for multiple initial states) plotted in graphs
* 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:
* 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)

* Bug fix: action alphabet (syntactic) for sync lost in PTA object construction

=======================================================

TODO (before statmc release)
----------------------------

* Result object creation pushed into SimEngine
* tidy doSampling, looking at Vincent's code
* seed issues (Vlad)

=======================================================

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:
* On-the-fly global reachability to allow (for A-R engine):
  - access to other local and global vars
  - system endsystem?
 (then test on Arnd's BRP model + others)
* 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