From 842eada5d300a568234cdddeecc4e870769aba3f Mon Sep 17 00:00:00 2001
From: Dave Parker <dave.x.parker@gmail.com>
Date: Tue, 14 Dec 2010 22:39:14 +0000
Subject: [PATCH] Error message tweak.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@2329 bbc10eb1-c90d-0410-af57-cb519fbb1720
---
 prism/NOTES                            | 24 ++++++++++++++++++------
 prism/src/prism/StateModelChecker.java |  2 +-
 2 files changed, 19 insertions(+), 7 deletions(-)

diff --git a/prism/NOTES b/prism/NOTES
index 996b0182..9c7866bd 100644
--- a/prism/NOTES
+++ b/prism/NOTES
@@ -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
 
diff --git a/prism/src/prism/StateModelChecker.java b/prism/src/prism/StateModelChecker.java
index 2178863e..94cc7fee 100644
--- a/prism/src/prism/StateModelChecker.java
+++ b/prism/src/prism/StateModelChecker.java
@@ -1259,7 +1259,7 @@ public class StateModelChecker implements ModelChecker
 			mainLog.print("\nThere are " + states.sizeString() + " states with ");
 			mainLog.print(expr.getType() instanceof TypeDouble ? "(approximately) " : "" + "this value");
 			if (!verbose && (states.size() == -1 || states.size() > 10)) {
-				mainLog.print(".\nThe first 10 states are displayed below. To view them all, enable verbose mode or use filters.\n");
+				mainLog.print(".\nThe first 10 states are displayed below. To view them all, enable verbose mode or use a print filter.\n");
 				states.print(mainLog, 10);
 			} else {
 				mainLog.print(":\n");