From ed5919811ff6d3a7e5e18c0c1b896906dc90bc2e Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Thu, 16 Dec 2010 00:57:13 +0000 Subject: [PATCH] NOTES. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@2335 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/NOTES | 21 ++++++--------------- 1 file changed, 6 insertions(+), 15 deletions(-) diff --git a/prism/NOTES b/prism/NOTES index 9c7866bd..42b5ac74 100644 --- a/prism/NOTES +++ b/prism/NOTES @@ -6,40 +6,31 @@ Remove for beta distributions: TODO (before any release) ------------------------- - -DOC! - - -Documentation: - -* 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) +fix prob 1 for <=t ? + ======================================================= TODO (before public release) ---------------------------- Documentation: -* Fix links from tutorial to manual +* Fix links from tutorial to manual (and reread/tweak) * Add DTMC/MDP case to synchronisation section * New -exportprism/-exportprismconst/-nobuild switches * Check for existence of zero-reward loops * New -exporttarget switch +* Extra reach info switches? Filters, property semantics, etc. * Integer-valued props displayed as doubles when printed as vector * Intervals (e.g. for multiple initial states) plotted in graphs * Add "single" filter - throws error if filter states > 1? * Allow other filter types to be spec with {} notation? + and then in doc clarify P>=p[...{filter}] means & not print + (didn't print in 3.3 anyway, despite manual) Action labels: * Check status of export/import trans wrt actions (alll models)