From f67c6976c20a3c62758309f09d21df65ffb9c7a1 Mon Sep 17 00:00:00 2001
From: Dave Parker <dave.x.parker@gmail.com>
Date: Mon, 25 Jan 2010 09:57:55 +0000
Subject: [PATCH] NOTES files.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@1713 bbc10eb1-c90d-0410-af57-cb519fbb1720
---
 prism/NOTES       | 68 ++++++++++++++++++++++++++++++++++++++---------
 prism/NOTES-ABSTR |  4 +++
 prism/NOTES-PTAS  | 37 +++++++++++++++-----------
 3 files changed, 80 insertions(+), 29 deletions(-)

diff --git a/prism/NOTES b/prism/NOTES
index 57e73a9c..77222600 100644
--- a/prism/NOTES
+++ b/prism/NOTES
@@ -1,27 +1,69 @@
 
------------------------------------------------------
+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)
 
-bin/ptamc examples/pta/simple/iandc.des sr 'z<6'
+-----------------------------------------------------------------------
 
-bin/ptamc examples/pta/simple/tcs.des l3 true
+Stuff to remove when distributing early copies to people:
+* NOTES*
+* examples/des
+* examples/explicit
+* src/explicit/PrismSTPGAsbtractRefine
+* {src,classes}/abstraction
 
-bin/ptamc examples/pta/simple/gethin1.des l2 true
+-----------------------------------------------------------------------
 
-bin/ptamc examples/pta/simple/gethin2.des l2 true
+See also:
+* NOTES-PTAS
+* NOTES-SIM
+* NOTES-ABSTR
 
-bin/ptamc examples/pta/simple/formats.des l3 true -refine=first -v 
+-----------------------------------------------------------------------
 
------------------------------------------------------
+Fixes/tidying needed before release to Kim:
 
-bin/mdpmc coin2_10.tra coin2_10.lab finished 
+Processing TODOs:
+Check STPGAR carefully (and then PTAAR subclass)
+CTL stuff (even if only disable?) in NonProbMC
+Tidy up, disable and/or remove PTA rewards stuff
 
------------------------------------------------------
+disable simulator neatly?
 
-bin/ptamc-prof ...
+and to Holger et al.:
 
-java -jar ~/usr/packages/jip-1.1.1/client/client.jar finish localhost 15599
+CTMDP stuff
 
-java -jar ~/usr/packages/jip-1.1.1/client/jipViewer.jar profile.xtx.xml 
+-----------------------------------------------------------------------
+
+Filters, property semantics, etc.
+
+TODO:
+* Integer-valued props displayed as doubles - need to give types to StateProbs?
+  - 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
+* P>=p[...{filter}] means & not print
+
+-----------------------------------------------------------------------
+
+TODO:
+
+- make adv gen switchable
+- make action storage optional (when required)
+- action storage for D/CTMCs
+- lp stuff - plugin support for eclipse/lpsolve (in prism-multi?)
+- also look up lrs?
+
+-----------------------------------------------------------------------
+
+LTL...
+bscc stuff
+- regression testing on ltl stuff with 3 diff options
 
------------------------------------------------------
 
diff --git a/prism/NOTES-ABSTR b/prism/NOTES-ABSTR
index 6a5c0f86..8deb3797 100644
--- a/prism/NOTES-ABSTR
+++ b/prism/NOTES-ABSTR
@@ -1,5 +1,9 @@
 TODO:
 
+* Get PrismSTPGAsbtractRefine working better on more examples
+* When PrismSTPGAsbtractRefine can reproduce QEST results, delete abstraction package
+
+
 exp reach for games
 remove src/abstraction dir
 
diff --git a/prism/NOTES-PTAS b/prism/NOTES-PTAS
index 22d81ea2..9ded8636 100644
--- a/prism/NOTES-PTAS
+++ b/prism/NOTES-PTAS
@@ -1,31 +1,36 @@
------------------------------------------------------
+Bugs
+----
 
-More Type checking, semantic checks ???
-Make sure checks match Digital clocks, Stochastic games
-Time divergence?
 
-Creation of new names (adding extra _s) doesn't take into account prop file ot consts etc.
+Todo
+----
 
-Sort VarList (two types - before and after constants evaluated). Need for simulator too.
+* Clarify semantic/type checks (consistency with games/digital)
 
+* Clarify time divergence issues
 
-Digital clocks
---------------
+* Sort VarList (two types - before and after constants evaluated). Need for simulator too.
 
-Translation done sep for erach property (e.g. for cmax)
 
-Debugging on case studies
-Optimisations?
-Urgency?
+Maybe todo
+----------
 
+* Games: Optimise number of states in time-bounded PTAs
+  (extras added in old target states) using until in forwards reach?
 
-Stochastic games
-----------------
+* Fix: Creation of new names (adding extra _s) doesn't take into account prop file ot consts etc.
 
-Optimise number of states in time-bounded PTAs (extras added in old target states) using until in forwards reach?
+* Digital clocks: Translation done sep for each property (e.g. for cmax)?
 
+* Digital clocks: urgency?
 
-* Email Holger/Arndt some models
+* Digital clocks: optimisations?
+
+
+Tidy
+----
+
+* Remove unneeded files from examples (prism-benchmark, rewards stuff)
 
 
 Documentation