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.
69 lines
1.8 KiB
69 lines
1.8 KiB
|
|
Last stable version of PRISM on svn (3.3 plus some fixes) is rev 1405
|
|
(there is a copy of this, e.g. to get working simulator, in ~/prism-old)
|
|
|
|
-----------------------------------------------------------------------
|
|
|
|
Stuff to remove when distributing early copies to people:
|
|
* NOTES*
|
|
* examples/des
|
|
* examples/explicit
|
|
* src/explicit/PrismSTPGAsbtractRefine
|
|
* {src,classes}/abstraction
|
|
|
|
-----------------------------------------------------------------------
|
|
|
|
See also:
|
|
* NOTES-PTAS
|
|
* NOTES-SIM
|
|
* NOTES-ABSTR
|
|
|
|
-----------------------------------------------------------------------
|
|
|
|
Fixes/tidying needed before release to Kim:
|
|
|
|
Processing TODOs:
|
|
Check STPGAR carefully (and then PTAAR subclass)
|
|
CTL stuff (even if only disable?) in NonProbMC
|
|
Tidy up, disable and/or remove PTA rewards stuff
|
|
|
|
disable simulator neatly?
|
|
|
|
and to Holger et al.:
|
|
|
|
CTMDP stuff
|
|
|
|
-----------------------------------------------------------------------
|
|
|
|
Filters, property semantics, etc.
|
|
|
|
TODO:
|
|
* Integer-valued props displayed as doubles - need to give types to StateProbs?
|
|
- 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?
|
|
|
|
Doc:
|
|
* Filters - no longer allowed minmax
|
|
* P>=p[...{filter}] means & not print
|
|
|
|
-----------------------------------------------------------------------
|
|
|
|
TODO:
|
|
|
|
- make adv gen switchable
|
|
- make action storage optional (when required)
|
|
- action storage for D/CTMCs
|
|
- lp stuff - plugin support for eclipse/lpsolve (in prism-multi?)
|
|
- also look up lrs?
|
|
|
|
-----------------------------------------------------------------------
|
|
|
|
LTL...
|
|
bscc stuff
|
|
- regression testing on ltl stuff with 3 diff options
|
|
|
|
|