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.
68 lines
1.9 KiB
68 lines
1.9 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*
|
|
* TODO?
|
|
* examples/des
|
|
* examples/explicit
|
|
* src/explicit/PrismSTPGAsbtractRefine
|
|
|
|
-----------------------------------------------------------------------
|
|
|
|
See also:
|
|
* NOTES-PTAS
|
|
* NOTES-SIM
|
|
* NOTES-ABSTR
|
|
|
|
-----------------------------------------------------------------------
|
|
|
|
Filters, property semantics, etc.
|
|
|
|
TODO:
|
|
* 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?
|
|
|
|
Doc:
|
|
* Filters - no longer allowed minmax (or encode as range?)
|
|
* P>=p[...{filter}] means & not print (didn't print in 3.3 anyway, despite manual)
|
|
|
|
-----------------------------------------------------------------------
|
|
|
|
TODO:
|
|
|
|
- remove colons from @params
|
|
|
|
- fix adversary generation (de alfaro thesis)
|
|
- add adversary generation for other engines
|
|
- make action storage optional (when required e.g. for export) (especially for MCs)
|
|
- lp stuff - plugin support for eclipse/lpsolve (in prism-multi?)
|
|
- also look up lrs?
|
|
- finalise tra format with actions (needs to work with actions too)
|
|
- so also fix e.g. importtrans, prism-statra
|
|
|
|
-----------------------------------------------------------------------
|
|
|
|
Abstraction/refinement:
|
|
|
|
TODO:
|
|
* exp reach for games
|
|
|
|
Other notes/ideas:
|
|
* refine opt: don't add ubsets of player1 choices
|
|
|
|
-----------------------------------------------------------------------
|
|
|
|
LTL...
|
|
bscc stuff
|
|
- regression testing on ltl stuff with 3 diff options
|
|
|
|
|