Some CTMDP examples.

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

prism/examples/ctmdp/NOTES

@@ -1,3 +1,5 @@
+prism examples/ctmdp/Neu10.sm -noprobchecks -exporttrans examples/ctmdp/Neu10.tra -exportlabels examples/ctmdp/Neu10.lab
+
 java -cp classes explicit.CTMDPModelChecker examples/ctmdp/Neu10.{tra,lab} target 1 -max
 
 java -cp classes explicit.CTMDPModelChecker examples/ctmdp/jsp.{tra,lab} done 10 -max

prism/examples/ctmdp/Neu10.sm

@@ -1,7 +1,7 @@
 // Simple CTMP from Neuhausser thesis defence slides (2010)
 
 // For mac prob of reaching target within time bound 1,
-// exact answer is 1 + 19/24 e^−3 − 3/2 e^-1 = (approx.) 0.48759
+// exact answer is 1 + 19/24 e^-3 - 3/2 e^-1 = (approx.) 0.48759
 // discretisation (k = 4500, tau = 0.0002222...) gives 0.487552953296395
 
 mdp