From 40ea6eeecd85085f54d992c48b97d6cd015842b3 Mon Sep 17 00:00:00 2001
From: sjunges <sebastian.junges@rwth-aachen.de>
Date: Wed, 12 Oct 2016 21:12:13 +0200
Subject: [PATCH] pctmc example

Former-commit-id: 22aa41bdd1a81d86e40327220dfd43d3c4b407e1 [formerly ea552f454c9d0cb586541ae70e2339faa97ba0f8]
Former-commit-id: 5231d96db57ed07ce82c515b8bddfc96c2901f72
---
 examples/pctmc/polling6.sm | 83 ++++++++++++++++++++++++++++++++++++++
 1 file changed, 83 insertions(+)
 create mode 100644 examples/pctmc/polling6.sm

diff --git a/examples/pctmc/polling6.sm b/examples/pctmc/polling6.sm
new file mode 100644
index 000000000..cb4faa90c
--- /dev/null
+++ b/examples/pctmc/polling6.sm
@@ -0,0 +1,83 @@
+// polling example [IT90]
+// gxn/dxp 26/01/00
+
+ctmc
+
+const int N=6;
+
+const double mu;
+const double gamma;
+
+//const double mu= 1;
+//const double gamma= 200;
+//const double lambda= mu/N;
+
+module server
+
+	s : [1..6]; // station
+	a : [0..1]; // action: 0=polling, 1=serving
+	
+	[loop1a] (s=1)&(a=0) -> gamma	: (s'=s+1);
+	[loop1b] (s=1)&(a=0) -> gamma	: (a'=1);
+	[serve1] (s=1)&(a=1) -> mu	: (s'=s+1)&(a'=0);
+	
+	[loop2a] (s=2)&(a=0) -> gamma	: (s'=s+1);
+	[loop2b] (s=2)&(a=0) -> gamma	: (a'=1);
+	[serve2] (s=2)&(a=1) -> mu	: (s'=s+1)&(a'=0);
+	
+	[loop3a] (s=3)&(a=0) -> gamma	: (s'=s+1);
+	[loop3b] (s=3)&(a=0) -> gamma	: (a'=1);
+	[serve3] (s=3)&(a=1) -> mu	: (s'=s+1)&(a'=0);
+	
+	[loop4a] (s=4)&(a=0) -> gamma	: (s'=s+1);
+	[loop4b] (s=4)&(a=0) -> gamma	: (a'=1);
+	[serve4] (s=4)&(a=1) -> mu	: (s'=s+1)&(a'=0);
+
+	[loop5a] (s=5)&(a=0) -> gamma	: (s'=s+1);
+	[loop5b] (s=5)&(a=0) -> gamma	: (a'=1);
+	[serve5] (s=5)&(a=1) -> mu	: (s'=s+1)&(a'=0);
+	
+	[loop6a] (s=6)&(a=0) -> gamma	: (s'=1);
+	[loop6b] (s=6)&(a=0) -> gamma	: (a'=1);
+	[serve6] (s=6)&(a=1) -> mu	: (s'=1)&(a'=0);
+	
+endmodule
+
+module station1
+
+	s1 : [0..1];
+	
+	[loop1a] (s1=0) -> 1 : (s1'=0);
+	[]       (s1=0) -> mu/N : (s1'=1);
+	[loop1b] (s1=1) -> 1 : (s1'=1);
+	[serve1] (s1=1) -> 1 : (s1'=0);
+	
+endmodule
+
+// construct further stations through renaming
+module station2 = station1 [s1=s2, loop1a=loop2a, loop1b=loop2b, serve1=serve2] endmodule
+module station3 = station1 [s1=s3, loop1a=loop3a, loop1b=loop3b, serve1=serve3] endmodule
+module station4 = station1 [s1=s4, loop1a=loop4a, loop1b=loop4b, serve1=serve4] endmodule
+module station5 = station1 [s1=s5, loop1a=loop5a, loop1b=loop5b, serve1=serve5] endmodule
+module station6 = station1 [s1=s6, loop1a=loop6a, loop1b=loop6b, serve1=serve6] endmodule
+
+// cumulative rewards
+
+//rewards "waiting" // expected time the station 1 is waiting to be served
+//	s1=1 & !(s=1 & a=1) : 1;
+//endrewards
+
+//rewards "served" // expected number of times station1 is served
+//	[serve1] true : 1;
+//endrewards
+
+init
+s = 1 &
+a = 0 &
+s1 = 0 &
+s2 = 0 &
+s3 = 0 &
+s4 = 0 &
+s5 = 0 &
+s6 = 0
+endinit