Browse Source

NOTES.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@2323 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Dave Parker 15 years ago
parent
commit
ba6340e13b
  1. 25
      prism/NOTES

25
prism/NOTES

@ -14,11 +14,19 @@ verbose has new behaviour now?! (wrt filters)
pta rewards with digital clocks (just F) - no clocks in rew strs though
filters: {} always range, even if single value (allow "single"?)
Documentation:
* 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 (before public release)
----------------------------
Documentation:
* Fix links from tutorial to manual
* Add DTMC/MDP case to synchronisation section
Filters, property semantics, etc.
* Integer-valued props displayed as doubles when printed as vector
* Intervals (e.g. for multiple initial states) plotted in graphs
@ -31,11 +39,6 @@ Action labels:
- also fix e.g. importtrans, prism-statra
* make action storage optional (when required e.g. for export) (especially for MCs)
Sim:
* Result object creation pushed into SimEngine
* tidy doSampling, looking at Vincent's code
* seed issues (Vlad)
PTAs:
* More tidying of PTA examples
- README files for other (non-firewire) examples
@ -58,12 +61,14 @@ PTAs:
* Bug fix: action alphabet (syntactic) for sync lost in PTA object construction
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)
TODO (before statmc release)
----------------------------
* Result object creation pushed into SimEngine
* tidy doSampling, looking at Vincent's code
* seed issues (Vlad)
=======================================================

Loading…
Cancel
Save