Notes.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@2139 bbc10eb1-c90d-0410-af57-cb519fbb1720

prism/CHANGELOG.txt

@@ -10,7 +10,7 @@ Ongoing changes:
 * New simulator
 * Adversary generation
 * Access to action labels. inclusion in export, etc.
-* Filters and propert semantics changes/additions
+* Filters and property semantics changes/additions
 
 Latest changes (reverse chronological):
 [correct wrt svn rev 1610]

prism/NOTES

@@ -1,6 +1,6 @@
 
 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)
+(there is a copy of this, e.g. to get working old simulator, in ~/prism-old)
 
 -----------------------------------------------------------------------
 
@@ -62,6 +62,13 @@ Other notes/ideas:
 -----------------------------------------------------------------------
 
 LTL...
+
+bug:
+
+prism ~/prism-examples/dice/dice.pm \
+-pctl '(s=0|s=1)=>P>=1 [ (P>=0.9 [ F<=1 s=3 ])=>(P>=0.5 [ F<=2 s=4 ]) ]'
+time-bounds should be ok in inner pctl but are not
+
 bscc stuff
 - regression testing on ltl stuff with 3 diff options
 

prism/README.txt

@@ -91,7 +91,7 @@ Contributions to the development of PRISM have also been gratefully received fro
  * Joachim Meyer-Kayser: Original implementation of the "Fox-Glynn" algorithm
  * Alistair John Strachan: Port to 64-bit architectures
  * Stephen Gilmore: Support for the stochastic process algebra PEPA
- * Paolo Ballarini & Kenneth Chan: Port of PRISM to Mac OS X
+ * Paolo Ballarini & Kenneth Chan: Port to Mac OS X
  * Rashid Mehmood: Improvements to low-level data structures and numerical solution algorithms
  * Alistair John Strachan, Mike Arthur and Zak Cohen: Integration of JFreeChart into PRISM
  * Carlos Bederian (working with Pedro D'Argenio): Addition of LTL model checking for MDPs to PRISM