From 5f58cddd4996bc0cd0a43c031335d3a20a5be0cb Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Wed, 7 Apr 2010 09:20:29 +0000 Subject: [PATCH] Some CTMDP examples. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@1838 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/examples/ctmdp/NOTES | 2 ++ prism/examples/ctmdp/Neu10.sm | 2 +- 2 files changed, 3 insertions(+), 1 deletion(-) diff --git a/prism/examples/ctmdp/NOTES b/prism/examples/ctmdp/NOTES index 77adbd53..62803015 100644 --- a/prism/examples/ctmdp/NOTES +++ b/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 diff --git a/prism/examples/ctmdp/Neu10.sm b/prism/examples/ctmdp/Neu10.sm index 26327080..9f6c1641 100644 --- a/prism/examples/ctmdp/Neu10.sm +++ b/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