You can not select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
138 lines
4.8 KiB
138 lines
4.8 KiB
Remove for beta distributions:
|
|
------------------------------
|
|
* NOTES
|
|
|
|
=======================================================
|
|
|
|
TODO (before any release)
|
|
-------------------------
|
|
|
|
PTAs:
|
|
* GUI
|
|
* Tidy prism-examples/pta, incl. delete brp
|
|
* Clarify semantic/type checks (consistency with games/digital)
|
|
* Check guards/invariants for convexity (for now, neither can be non-convex, see below)
|
|
* Clarify time divergence issues
|
|
* non-zeno checks?
|
|
* 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)?
|
|
* Bug fix: action alphabet (syntactic) for sync lost in PTA object construction
|
|
|
|
=======================================================
|
|
|
|
TODO (before public release)
|
|
----------------------------
|
|
|
|
Filters, property semantics, etc.
|
|
* Integer-valued props displayed as doubles - need to give types to StateValues?
|
|
- lots of other places too e.g. GUI results)
|
|
* Intervals for multiple initial states
|
|
- Need classes for Result
|
|
- Graph plotting?
|
|
* Restructure Result class? e.g. separate bracketed comment? (done I think)
|
|
- Errors (Exceptions) formatted properly?
|
|
|
|
PTAs:
|
|
* 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?
|
|
|
|
DOC (before public release)
|
|
---------------------------
|
|
|
|
Filters:
|
|
* Filters - no longer allowed minmax (or encode as range?)
|
|
* P>=p[...{filter}] means & not print (didn't print in 3.3 anyway, despite manual)
|
|
|
|
PTAs:
|
|
* Where can clocks be used
|
|
- clock constraints (just (some) binops)
|
|
- in guards
|
|
- in invariants
|
|
- resets (normal updates, but to ints only)
|
|
- var decl.s
|
|
- generally must be convex (i.e. just conj of constraints) (can be relaxed a bit for digital clocks)
|
|
* Currently, modules cannot access non-local vars (and there are no globals)
|
|
(this is too restrictive, e.g. for message passing)
|
|
* Must have single initial state (is this true for digital clocks too?)
|
|
* Invariants must come straight after var decls
|
|
|
|
=======================================================
|
|
|
|
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)
|
|
* 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:
|
|
* Investigate efficiency wrt old simulator
|
|
* Add (back) support for full loop detection? (embedded into Path*?)
|
|
* Add (back) early manual termination of sampling (thru expt stop?)
|
|
* Random initial state
|
|
* Variable overflow etc.
|
|
* 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.)
|
|
|
|
Actions:
|
|
* 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)
|
|
|
|
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
|
|
|
|
Code tidy:
|
|
* remove colons from @params
|
|
|
|
DOC (some time)
|
|
---------------
|
|
|
|
Prism-multi:
|
|
* No state rewards
|