From ba6340e13bd0a761768aadfbdb6383bee6b6adae Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Tue, 7 Dec 2010 22:47:44 +0000 Subject: [PATCH] NOTES. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@2323 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/NOTES | 25 +++++++++++++++---------- 1 file changed, 15 insertions(+), 10 deletions(-) diff --git a/prism/NOTES b/prism/NOTES index b2a18fe9..996b0182 100644 --- a/prism/NOTES +++ b/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) =======================================================