|
|
|
@ -9,14 +9,19 @@ TODO (before any release) |
|
|
|
|
|
|
|
DOC! |
|
|
|
|
|
|
|
timelock reported as deadlock for digital |
|
|
|
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) |
|
|
|
|
|
|
|
* PTA model checking |
|
|
|
- timelock reported as deadlock for digital |
|
|
|
- pta rewards with digital clocks (just F) - no clocks in rew strs though |
|
|
|
|
|
|
|
* Filters and property semantics changes/additions |
|
|
|
- filters: {} always range, even if single value (allow "single"?) |
|
|
|
- P>=p[...{filter}] means & not print (didn't print in 3.3 anyway, despite manual) |
|
|
|
- verbose has new behaviour now?! (wrt filters) |
|
|
|
|
|
|
|
* Adversary generation (e.g. -exportadv switch) |
|
|
|
|
|
|
|
======================================================= |
|
|
|
|
|
|
|
@ -26,6 +31,9 @@ TODO (before public release) |
|
|
|
Documentation: |
|
|
|
* Fix links from tutorial to manual |
|
|
|
* Add DTMC/MDP case to synchronisation section |
|
|
|
* New -exportprism/-exportprismconst/-nobuild switches |
|
|
|
* Check for existence of zero-reward loops |
|
|
|
* New -exporttarget switch |
|
|
|
|
|
|
|
Filters, property semantics, etc. |
|
|
|
* Integer-valued props displayed as doubles when printed as vector |
|
|
|
@ -123,6 +131,10 @@ Simulator: |
|
|
|
* Traviendo export? |
|
|
|
* Code: Optimise/tidy Choices (ChoiceList/ChoiceSingleton/etc.) |
|
|
|
|
|
|
|
Other: |
|
|
|
* Export tr/ss probs from GUI |
|
|
|
* Initial distr for steady-state |
|
|
|
|
|
|
|
Adversary generation: |
|
|
|
* Add adversary generation for other engines |
|
|
|
|
|
|
|
|