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