Some CTMDP examples.

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

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
+

prism/examples/ctmdp/Neu10.lab

@@ -0,0 +1,3 @@
+0="init" 1="deadlock" 2="target"
+0: 0
+2: 2

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;

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

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

prism/examples/ctmdp/jsp.csl

@@ -0,0 +1 @@
+"done"

prism/examples/ctmdp/jsp.lab

@@ -0,0 +1,3 @@
+0="init" 1="deadlock" 2="done"
+0: 0
+14: 2

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;

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