From ed9365f6a03e1a6f126804bdc3c88c20595000de Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Wed, 7 Apr 2010 09:16:52 +0000 Subject: [PATCH] Some CTMDP examples. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@1837 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/examples/ctmdp/NOTES | 4 +++ prism/examples/ctmdp/Neu10.lab | 3 ++ prism/examples/ctmdp/Neu10.sm | 20 ++++++++++++ prism/examples/ctmdp/Neu10.tra | 7 ++++ prism/examples/ctmdp/erlang.sm | 28 ++++++++++++++++ prism/examples/ctmdp/jsp.csl | 1 + prism/examples/ctmdp/jsp.lab | 3 ++ prism/examples/ctmdp/jsp.sm | 58 ++++++++++++++++++++++++++++++++++ prism/examples/ctmdp/jsp.tra | 42 ++++++++++++++++++++++++ 9 files changed, 166 insertions(+) create mode 100644 prism/examples/ctmdp/NOTES create mode 100644 prism/examples/ctmdp/Neu10.lab create mode 100644 prism/examples/ctmdp/Neu10.sm create mode 100644 prism/examples/ctmdp/Neu10.tra create mode 100644 prism/examples/ctmdp/erlang.sm create mode 100644 prism/examples/ctmdp/jsp.csl create mode 100644 prism/examples/ctmdp/jsp.lab create mode 100644 prism/examples/ctmdp/jsp.sm create mode 100644 prism/examples/ctmdp/jsp.tra diff --git a/prism/examples/ctmdp/NOTES b/prism/examples/ctmdp/NOTES new file mode 100644 index 00000000..77adbd53 --- /dev/null +++ b/prism/examples/ctmdp/NOTES @@ -0,0 +1,4 @@ +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.lab b/prism/examples/ctmdp/Neu10.lab new file mode 100644 index 00000000..140f2c5a --- /dev/null +++ b/prism/examples/ctmdp/Neu10.lab @@ -0,0 +1,3 @@ +0="init" 1="deadlock" 2="target" +0: 0 +2: 2 diff --git a/prism/examples/ctmdp/Neu10.sm b/prism/examples/ctmdp/Neu10.sm new file mode 100644 index 00000000..26327080 --- /dev/null +++ b/prism/examples/ctmdp/Neu10.sm @@ -0,0 +1,20 @@ +// 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 +// discretisation (k = 4500, tau = 0.0002222...) gives 0.487552953296395 + +mdp + +module M + + s : [0..3]; + + [a] s=0 -> 1 : (s'=2) + 2 : (s'=3); + [b] s=0 -> 3 : (s'=1); + [b] s=1 -> 1 : (s'=2); + [c] s>1 -> 1 : true; + +endmodule + +label "target" = s=2; diff --git a/prism/examples/ctmdp/Neu10.tra b/prism/examples/ctmdp/Neu10.tra new file mode 100644 index 00000000..22983c8e --- /dev/null +++ b/prism/examples/ctmdp/Neu10.tra @@ -0,0 +1,7 @@ +4 5 6 +0 0 1 3 b +0 1 2 1 a +0 1 3 2 a +1 0 2 1 b +2 0 2 1 c +3 0 3 1 c diff --git a/prism/examples/ctmdp/erlang.sm b/prism/examples/ctmdp/erlang.sm new file mode 100644 index 00000000..1840fa75 --- /dev/null +++ b/prism/examples/ctmdp/erlang.sm @@ -0,0 +1,28 @@ +imc + +const int k; +const double mean = 10; + +module erlang + + s : [0..5]; + i : [1..k+1]; + + [] s=0 -> 1 : (s'=1); + [a] s=1 -> 1 : (s'=1); + [] i < k -> k/mean : (i'=i+1); + [go] i = k -> k/mean : (i'=i+1); + +endmodule + +module main + + x : [0..1]; + + [go] x=0 -> (x'=1); + +endmodule + +rewards "time" +true : 1; +endrewards diff --git a/prism/examples/ctmdp/jsp.csl b/prism/examples/ctmdp/jsp.csl new file mode 100644 index 00000000..1c1e8c91 --- /dev/null +++ b/prism/examples/ctmdp/jsp.csl @@ -0,0 +1 @@ +"done" diff --git a/prism/examples/ctmdp/jsp.lab b/prism/examples/ctmdp/jsp.lab new file mode 100644 index 00000000..233d7f1d --- /dev/null +++ b/prism/examples/ctmdp/jsp.lab @@ -0,0 +1,3 @@ +0="init" 1="deadlock" 2="done" +0: 0 +14: 2 diff --git a/prism/examples/ctmdp/jsp.sm b/prism/examples/ctmdp/jsp.sm new file mode 100644 index 00000000..8055fe8f --- /dev/null +++ b/prism/examples/ctmdp/jsp.sm @@ -0,0 +1,58 @@ +mdp + +const double lambda1 = 0.25; +const double lambda2 = 0.33; +const double lambda3 = 1.25; +const double lambda4 = 1.50; + +formula todo = (job1<2?1:0) + (job2<2?1:0) + (job3<2?1:0) + (job4<2?1:0); + +module jsp + + job1 : [0..2] init 1; + job2 : [0..2] init 0; + job3 : [0..2] init 1; + job4 : [0..2] init 0; + + // 1&3 initially scheduled + // a_ij_kl: when i (k) finishes, schedule j (l) + [a_12_32] todo=4 & job1=1 & job3=1 -> lambda1 : (job1'=2)&(job2'=1) + lambda3 : (job3'=2)&(job2'=1); + [a_12_34] todo=4 & job1=1 & job3=1 -> lambda1 : (job1'=2)&(job2'=1) + lambda3 : (job3'=2)&(job4'=1); + [a_14_32] todo=4 & job1=1 & job3=1 -> lambda1 : (job1'=2)&(job4'=1) + lambda3 : (job3'=2)&(job2'=1); + [a_14_34] todo=4 & job1=1 & job3=1 -> lambda1 : (job1'=2)&(job4'=1) + lambda3 : (job3'=2)&(job4'=1); + + // 1&2 scheduled (3 done, 4 next) + [step2] todo=3 & job1=1 & job2=1 -> lambda1 : (job1'=2)&(job4'=1) + lambda2 : (job2'=2)&(job4'=1); + // 1&4 scheduled (3 done, 2 next) + [step2] todo=3 & job1=1 & job4=1 -> lambda1 : (job1'=2)&(job2'=1) + lambda4 : (job4'=2)&(job2'=1); + // 3&2 scheduled (1 done, 4 next) + [step2] todo=3 & job3=1 & job2=1 -> lambda3 : (job3'=2)&(job4'=1) + lambda2 : (job2'=2)&(job4'=1); + // 3&4 scheduled (1 done, 2 next) + [step2] todo=3 & job3=1 & job4=1 -> lambda3 : (job3'=2)&(job2'=1) + lambda4 : (job4'=2)&(job2'=1); + + // two scheduled + [step3] todo=2 & job1=1 & job2=1 -> lambda1 : (job1'=2) + lambda2 : (job2'=2); + [step3] todo=2 & job1=1 & job3=1 -> lambda1 : (job1'=2) + lambda3 : (job3'=2); + [step3] todo=2 & job1=1 & job4=1 -> lambda1 : (job1'=2) + lambda4 : (job4'=2); + [step3] todo=2 & job2=1 & job1=1 -> lambda2 : (job2'=2) + lambda1 : (job1'=2); + [step3] todo=2 & job2=1 & job3=1 -> lambda2 : (job2'=2) + lambda3 : (job3'=2); + [step3] todo=2 & job2=1 & job4=1 -> lambda2 : (job2'=2) + lambda4 : (job4'=2); + [step3] todo=2 & job3=1 & job1=1 -> lambda3 : (job3'=2) + lambda1 : (job1'=2); + [step3] todo=2 & job3=1 & job2=1 -> lambda3 : (job3'=2) + lambda2 : (job2'=2); + [step3] todo=2 & job3=1 & job4=1 -> lambda3 : (job3'=2) + lambda4 : (job4'=2); + [step3] todo=2 & job4=1 & job1=1 -> lambda4 : (job4'=2) + lambda1 : (job1'=2); + [step3] todo=2 & job4=1 & job2=1 -> lambda4 : (job4'=2) + lambda2 : (job2'=2); + [step3] todo=2 & job4=1 & job3=1 -> lambda4 : (job4'=2) + lambda3 : (job3'=2); + + // one scheduled + [step4] todo=1 & job1=1 -> lambda1 : (job1'=2); + [step4] todo=1 & job2=1 -> lambda1 : (job2'=2); + [step4] todo=1 & job3=1 -> lambda1 : (job3'=2); + [step4] todo=1 & job4=1 -> lambda1 : (job4'=2); + + // done + [done] todo=0 -> true; + +endmodule + +label "done" = todo=0; diff --git a/prism/examples/ctmdp/jsp.tra b/prism/examples/ctmdp/jsp.tra new file mode 100644 index 00000000..97ae218a --- /dev/null +++ b/prism/examples/ctmdp/jsp.tra @@ -0,0 +1,42 @@ +15 23 41 +0 0 1 1.25 a_14_34 +0 0 6 0.25 a_14_34 +0 1 2 1.25 a_14_32 +0 1 6 0.25 a_14_32 +0 2 1 1.25 a_12_34 +0 2 7 0.25 a_12_34 +0 3 2 1.25 a_12_32 +0 3 7 0.25 a_12_32 +1 0 3 1.5 step2 +1 0 9 0.25 step2 +2 0 4 0.33 step2 +2 0 9 0.25 step2 +3 0 5 0.33 step3 +3 0 10 0.25 step3 +3 1 5 0.33 step3 +3 1 10 0.25 step3 +4 0 5 1.5 step3 +4 0 13 0.25 step3 +4 1 5 1.5 step3 +4 1 13 0.25 step3 +5 0 14 0.25 step4 +6 0 8 1.5 step2 +6 0 9 1.25 step2 +7 0 9 1.25 step2 +7 0 11 0.33 step2 +8 0 10 1.25 step3 +8 0 12 0.33 step3 +8 1 10 1.25 step3 +8 1 12 0.33 step3 +9 0 10 1.5 step3 +9 0 13 0.33 step3 +9 1 10 1.5 step3 +9 1 13 0.33 step3 +10 0 14 0.25 step4 +11 0 12 1.5 step3 +11 0 13 1.25 step3 +11 1 12 1.5 step3 +11 1 13 1.25 step3 +12 0 14 0.25 step4 +13 0 14 0.25 step4 +14 0 14 1 done