model.prism (0.01 MB) property.props (0.01 MB) model.jani (0.22 MB)
Taken from QVBS (January 2026). The given benchmark (including parameter instantiation and property) has been considered in QComp 2019 and QComp 2020. Original Prism model and property files have been adapted for compatibility and simplicity: - Constants: All open constants are now explicitly set within model.prism (no need to set them via command line) - Properties: The properties only refer to labels and rewards as defined in the model.prism file. No variables or constants are used in the property. - Formulas: some PRISM formula declarations have been renamed so that their identify does not crash with a label.
// polling example [IT90] // gxn/dxp 26/01/00 ctmc const int N = 18; const double T=16; const double mu = 1; const double gamma = 200; const double lambda = mu/N; module server s : [1..18]; // 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'=s+1); [loop6b] (s=6)&(a=0) -> gamma : (a'=1); [serve6] (s=6)&(a=1) -> mu : (s'=s+1)&(a'=0); [loop7a] (s=7)&(a=0) -> gamma : (s'=s+1); [loop7b] (s=7)&(a=0) -> gamma : (a'=1); [serve7] (s=7)&(a=1) -> mu : (s'=s+1)&(a'=0); [loop8a] (s=8)&(a=0) -> gamma : (s'=s+1); [loop8b] (s=8)&(a=0) -> gamma : (a'=1); [serve8] (s=8)&(a=1) -> mu : (s'=s+1)&(a'=0); [loop9a] (s=9)&(a=0) -> gamma : (s'=s+1); [loop9b] (s=9)&(a=0) -> gamma : (a'=1); [serve9] (s=9)&(a=1) -> mu : (s'=s+1)&(a'=0); [loop10a] (s=10)&(a=0) -> gamma : (s'=s+1); [loop10b] (s=10)&(a=0) -> gamma : (a'=1); [serve10] (s=10)&(a=1) -> mu : (s'=s+1)&(a'=0); [loop11a] (s=11)&(a=0) -> gamma : (s'=s+1); [loop11b] (s=11)&(a=0) -> gamma : (a'=1); [serve11] (s=11)&(a=1) -> mu : (s'=s+1)&(a'=0); [loop12a] (s=12)&(a=0) -> gamma : (s'=s+1); [loop12b] (s=12)&(a=0) -> gamma : (a'=1); [serve12] (s=12)&(a=1) -> mu : (s'=s+1)&(a'=0); [loop13a] (s=13)&(a=0) -> gamma : (s'=s+1); [loop13b] (s=13)&(a=0) -> gamma : (a'=1); [serve13] (s=13)&(a=1) -> mu : (s'=s+1)&(a'=0); [loop14a] (s=14)&(a=0) -> gamma : (s'=s+1); [loop14b] (s=14)&(a=0) -> gamma : (a'=1); [serve14] (s=14)&(a=1) -> mu : (s'=s+1)&(a'=0); [loop15a] (s=15)&(a=0) -> gamma : (s'=s+1); [loop15b] (s=15)&(a=0) -> gamma : (a'=1); [serve15] (s=15)&(a=1) -> mu : (s'=s+1)&(a'=0); [loop16a] (s=16)&(a=0) -> gamma : (s'=s+1); [loop16b] (s=16)&(a=0) -> gamma : (a'=1); [serve16] (s=16)&(a=1) -> mu : (s'=s+1)&(a'=0); [loop17a] (s=17)&(a=0) -> gamma : (s'=s+1); [loop17b] (s=17)&(a=0) -> gamma : (a'=1); [serve17] (s=17)&(a=1) -> mu : (s'=s+1)&(a'=0); [loop18a] (s=18)&(a=0) -> gamma : (s'=1); [loop18b] (s=18)&(a=0) -> gamma : (a'=1); [serve18] (s=18)&(a=1) -> mu : (s'=1)&(a'=0); endmodule module station1 s1 : [0..1]; // state of station: 0=empty, 1=full [loop1a] (s1=0) -> 1 : (s1'=0); [] (s1=0) -> lambda : (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 module station7 = station1 [ s1=s7, loop1a=loop7a, loop1b=loop7b, serve1=serve7 ] endmodule module station8 = station1 [ s1=s8, loop1a=loop8a, loop1b=loop8b, serve1=serve8 ] endmodule module station9 = station1 [ s1=s9, loop1a=loop9a, loop1b=loop9b, serve1=serve9 ] endmodule module station10 = station1 [ s1=s10, loop1a=loop10a, loop1b=loop10b, serve1=serve10 ] endmodule module station11 = station1 [ s1=s11, loop1a=loop11a, loop1b=loop11b, serve1=serve11 ] endmodule module station12 = station1 [ s1=s12, loop1a=loop12a, loop1b=loop12b, serve1=serve12 ] endmodule module station13 = station1 [ s1=s13, loop1a=loop13a, loop1b=loop13b, serve1=serve13 ] endmodule module station14 = station1 [ s1=s14, loop1a=loop14a, loop1b=loop14b, serve1=serve14 ] endmodule module station15 = station1 [ s1=s15, loop1a=loop15a, loop1b=loop15b, serve1=serve15 ] endmodule module station16 = station1 [ s1=s16, loop1a=loop16a, loop1b=loop16b, serve1=serve16 ] endmodule module station17 = station1 [ s1=s17, loop1a=loop17a, loop1b=loop17b, serve1=serve17 ] endmodule module station18 = station1 [ s1=s18, loop1a=loop18a, loop1b=loop18b, serve1=serve18 ] endmodule label "serve_s2" = (s=2 & a=1); label "serve_s1" = (s=1 & a=1);
"s1_before_s2": P=? [ !"serve_s2" U "serve_s1" ];
{
"actions": [
{
"name": "loop10a"
},
{
"name": "loop10b"
},
{
"name": "loop11a"
},
{
"name": "loop11b"
},
{
"name": "loop12a"
},
{
"name": "loop12b"
},
{
"name": "loop13a"
},
{
"name": "loop13b"
},
{
"name": "loop14a"
},
{
"name": "loop14b"
},
{
"name": "loop15a"
},
{
"name": "loop15b"
},
{
"name": "loop16a"
},
{
"name": "loop16b"
},
{
"name": "loop17a"
},
{
"name": "loop17b"
},
{
"name": "loop18a"
},
{
"name": "loop18b"
},
{
"name": "loop1a"
},
{
"name": "loop1b"
},
{
"name": "loop2a"
},
{
"name": "loop2b"
},
{
"name": "loop3a"
},
{
"name": "loop3b"
},
{
"name": "loop4a"
},
{
"name": "loop4b"
},
{
"name": "loop5a"
},
{
"name": "loop5b"
},
{
"name": "loop6a"
},
{
"name": "loop6b"
},
{
"name": "loop7a"
},
{
"name": "loop7b"
},
{
"name": "loop8a"
},
{
"name": "loop8b"
},
{
"name": "loop9a"
},
{
"name": "loop9b"
},
{
"name": "serve1"
},
{
"name": "serve10"
},
{
"name": "serve11"
},
{
"name": "serve12"
},
{
"name": "serve13"
},
{
"name": "serve14"
},
{
"name": "serve15"
},
{
"name": "serve16"
},
{
"name": "serve17"
},
{
"name": "serve18"
},
{
"name": "serve2"
},
{
"name": "serve3"
},
{
"name": "serve4"
},
{
"name": "serve5"
},
{
"name": "serve6"
},
{
"name": "serve7"
},
{
"name": "serve8"
},
{
"name": "serve9"
}
],
"automata": [
{
"edges": [
{
"action": "loop10a",
"destinations": [
{
"assignments": [
{
"comment": "s <- (s + 1)",
"ref": "s",
"value": {
"left": "s",
"op": "+",
"right": 1
}
}
],
"location": "l",
"probability": {
"comment": "(200 / 200)",
"exp": 1.0
}
}
],
"guard": {
"comment": "((s = 10) & (a = 0))",
"exp": {
"left": {
"left": "s",
"op": "=",
"right": 10
},
"op": "∧",
"right": {
"left": "a",
"op": "=",
"right": 0
}
}
},
"location": "l",
"rate": {
"comment": "200",
"exp": 200
}
},
{
"action": "loop10b",
"destinations": [
{
"assignments": [
{
"comment": "a <- 1",
"ref": "a",
"value": 1
}
],
"location": "l",
"probability": {
"comment": "(200 / 200)",
"exp": 1.0
}
}
],
"guard": {
"comment": "((s = 10) & (a = 0))",
"exp": {
"left": {
"left": "s",
"op": "=",
"right": 10
},
"op": "∧",
"right": {
"left": "a",
"op": "=",
"right": 0
}
}
},
"location": "l",
"rate": {
"comment": "200",
"exp": 200
}
},
{
"action": "loop11a",
"destinations": [
{
"assignments": [
{
"comment": "s <- (s + 1)",
"ref": "s",
"value": {
"left": "s",
"op": "+",
"right": 1
}
}
],
"location": "l",
"probability": {
"comment": "(200 / 200)",
"exp": 1.0
}
}
],
"guard": {
"comment": "((s = 11) & (a = 0))",
"exp": {
"left": {
"left": "s",
"op": "=",
"right": 11
},
"op": "∧",
"right": {
"left": "a",
"op": "=",
"right": 0
}
}
},
"location": "l",
"rate": {
"comment": "200",
"exp": 200
}
},
{
"action": "loop11b",
"destinations": [
{
"assignments": [
{
"comment": "a <- 1",
"ref": "a",
"value": 1
}
],
"location": "l",
"probability": {
"comment": "(200 / 200)",
"exp": 1.0
}
}
],
"guard": {
"comment": "((s = 11) & (a = 0))",
"exp": {
"left": {
"left": "s",
"op": "=",
"right": 11
},
"op": "∧",
"right": {
"left": "a",
"op": "=",
"right": 0
}
}
},
"location": "l",
"rate": {
"comment": "200",
"exp": 200
}
},
{
"action": "loop12a",
"destinations": [
{
"assignments": [
{
"comment": "s <- (s + 1)",
"ref": "s",
"value": {
"left": "s",
"op": "+",
"right": 1
}
}
],
"location": "l",
"probability": {
"comment": "(200 / 200)",
"exp": 1.0
}
}
],
"guard": {
"comment": "((s = 12) & (a = 0))",
"exp": {
"left": {
"left": "s",
"op": "=",
"right": 12
},
"op": "∧",
"right": {
"left": "a",
"op": "=",
"right": 0
}
}
},
"location": "l",
"rate": {
"comment": "200",
"exp": 200
}
},
{
"action": "loop12b",
"destinations": [
{
"assignments": [
{
"comment": "a <- 1",
"ref": "a",
"value": 1
}
],
"location": "l",
"probability": {
"comment": "(200 / 200)",
"exp": 1.0
}
}
],
"guard": {
"comment": "((s = 12) & (a = 0))",
"exp": {
"left": {
"left": "s",
"op": "=",
"right": 12
},
"op": "∧",
"right": {
"left": "a",
"op": "=",
"right": 0
}
}
},
"location": "l",
"rate": {
"comment": "200",
"exp": 200
}
},
{
"action": "loop13a",
"destinations": [
{
"assignments": [
{
"comment": "s <- (s + 1)",
"ref": "s",
"value": {
"left": "s",
"op": "+",
"right": 1
}
}
],
"location": "l",
"probability": {
"comment": "(200 / 200)",
"exp": 1.0
}
}
],
"guard": {
"comment": "((s = 13) & (a = 0))",
"exp": {
"left": {
"left": "s",
"op": "=",
"right": 13
},
"op": "∧",
"right": {
"left": "a",
"op": "=",
"right": 0
}
}
},
"location": "l",
"rate": {
"comment": "200",
"exp": 200
}
},
{
"action": "loop13b",
"destinations": [
{
"assignments": [
{
"comment": "a <- 1",
"ref": "a",
"value": 1
}
],
"location": "l",
"probability": {
"comment": "(200 / 200)",
"exp": 1.0
}
}
],
"guard": {
"comment": "((s = 13) & (a = 0))",
"exp": {
"left": {
"left": "s",
"op": "=",
"right": 13
},
"op": "∧",
"right": {
"left": "a",
"op": "=",
"right": 0
}
}
},
"location": "l",
"rate": {
"comment": "200",
"exp": 200
}
},
{
"action": "loop14a",
"destinations": [
{
"assignments": [
{
"comment": "s <- (s + 1)",
"ref": "s",
"value": {
"left": "s",
"op": "+",
"right": 1
}
}
],
"location": "l",
"probability": {
"comment": "(200 / 200)",
"exp": 1.0
}
}
],
"guard": {
"comment": "((s = 14) & (a = 0))",
"exp": {
"left": {
"left": "s",
"op": "=",
"right": 14
},
"op": "∧",
"right": {
"left": "a",
"op": "=",
"right": 0
}
}
},
"location": "l",
"rate": {
"comment": "200",
"exp": 200
}
},
{
"action": "loop14b",
"destinations": [
{
"assignments": [
{
"comment": "a <- 1",
"ref": "a",
"value": 1
}
],
"location": "l",
"probability": {
"comment": "(200 / 200)",
"exp": 1.0
}
}
],
"guard": {
"comment": "((s = 14) & (a = 0))",
"exp": {
"left": {
"left": "s",
"op": "=",
"right": 14
},
"op": "∧",
"right": {
"left": "a",
"op": "=",
"right": 0
}
}
},
"location": "l",
"rate": {
"comment": "200",
"exp": 200
}
},
{
"action": "loop15a",
"destinations": [
{
"assignments": [
{
"comment": "s <- (s + 1)",
"ref": "s",
"value": {
"left": "s",
"op": "+",
"right": 1
}
}
],
"location": "l",
"probability": {
"comment": "(200 / 200)",
"exp": 1.0
}
}
],
"guard": {
"comment": "((s = 15) & (a = 0))",
"exp": {
"left": {
"left": "s",
"op": "=",
"right": 15
},
"op": "∧",
"right": {
"left": "a",
"op": "=",
"right": 0
}
}
},
"location": "l",
"rate": {
"comment": "200",
"exp": 200
}
},
{
"action": "loop15b",
"destinations": [
{
"assignments": [
{
"comment": "a <- 1",
"ref": "a",
"value": 1
}
],
"location": "l",
"probability": {
"comment": "(200 / 200)",
"exp": 1.0
}
}
],
"guard": {
"comment": "((s = 15) & (a = 0))",
"exp": {
"left": {
"left": "s",
"op": "=",
"right": 15
},
"op": "∧",
"right": {
"left": "a",
"op": "=",
"right": 0
}
}
},
"location": "l",
"rate": {
"comment": "200",
"exp": 200
}
},
{
"action": "loop16a",
"destinations": [
{
"assignments": [
{
"comment": "s <- (s + 1)",
"ref": "s",
"value": {
"left": "s",
"op": "+",
"right": 1
}
}
],
"location": "l",
"probability": {
"comment": "(200 / 200)",
"exp": 1.0
}
}
],
"guard": {
"comment": "((s = 16) & (a = 0))",
"exp": {
"left": {
"left": "s",
"op": "=",
"right": 16
},
"op": "∧",
"right": {
"left": "a",
"op": "=",
"right": 0
}
}
},
"location": "l",
"rate": {
"comment": "200",
"exp": 200
}
},
{
"action": "loop16b",
"destinations": [
{
"assignments": [
{
"comment": "a <- 1",
"ref": "a",
"value": 1
}
],
"location": "l",
"probability": {
"comment": "(200 / 200)",
"exp": 1.0
}
}
],
"guard": {
"comment": "((s = 16) & (a = 0))",
"exp": {
"left": {
"left": "s",
"op": "=",
"right": 16
},
"op": "∧",
"right": {
"left": "a",
"op": "=",
"right": 0
}
}
},
"location": "l",
"rate": {
"comment": "200",
"exp": 200
}
},
{
"action": "loop17a",
"destinations": [
{
"assignments": [
{
"comment": "s <- (s + 1)",
"ref": "s",
"value": {
"left": "s",
"op": "+",
"right": 1
}
}
],
"location": "l",
"probability": {
"comment": "(200 / 200)",
"exp": 1.0
}
}
],
"guard": {
"comment": "((s = 17) & (a = 0))",
"exp": {
"left": {
"left": "s",
"op": "=",
"right": 17
},
"op": "∧",
"right": {
"left": "a",
"op": "=",
"right": 0
}
}
},
"location": "l",
"rate": {
"comment": "200",
"exp": 200
}
},
{
"action": "loop17b",
"destinations": [
{
"assignments": [
{
"comment": "a <- 1",
"ref": "a",
"value": 1
}
],
"location": "l",
"probability": {
"comment": "(200 / 200)",
"exp": 1.0
}
}
],
"guard": {
"comment": "((s = 17) & (a = 0))",
"exp": {
"left": {
"left": "s",
"op": "=",
"right": 17
},
"op": "∧",
"right": {
"left": "a",
"op": "=",
"right": 0
}
}
},
"location": "l",
"rate": {
"comment": "200",
"exp": 200
}
},
{
"action": "loop18a",
"destinations": [
{
"assignments": [
{
"comment": "s <- 1",
"ref": "s",
"value": 1
}
],
"location": "l",
"probability": {
"comment": "(200 / 200)",
"exp": 1.0
}
}
],
"guard": {
"comment": "((s = 18) & (a = 0))",
"exp": {
"left": {
"left": "s",
"op": "=",
"right": 18
},
"op": "∧",
"right": {
"left": "a",
"op": "=",
"right": 0
}
}
},
"location": "l",
"rate": {
"comment": "200",
"exp": 200
}
},
{
"action": "loop18b",
"destinations": [
{
"assignments": [
{
"comment": "a <- 1",
"ref": "a",
"value": 1
}
],
"location": "l",
"probability": {
"comment": "(200 / 200)",
"exp": 1.0
}
}
],
"guard": {
"comment": "((s = 18) & (a = 0))",
"exp": {
"left": {
"left": "s",
"op": "=",
"right": 18
},
"op": "∧",
"right": {
"left": "a",
"op": "=",
"right": 0
}
}
},
"location": "l",
"rate": {
"comment": "200",
"exp": 200
}
},
{
"action": "loop1a",
"destinations": [
{
"assignments": [
{
"comment": "s <- (s + 1)",
"ref": "s",
"value": {
"left": "s",
"op": "+",
"right": 1
}
}
],
"location": "l",
"probability": {
"comment": "(200 / 200)",
"exp": 1.0
}
}
],
"guard": {
"comment": "((s = 1) & (a = 0))",
"exp": {
"left": {
"left": "s",
"op": "=",
"right": 1
},
"op": "∧",
"right": {
"left": "a",
"op": "=",
"right": 0
}
}
},
"location": "l",
"rate": {
"comment": "200",
"exp": 200
}
},
{
"action": "loop1b",
"destinations": [
{
"assignments": [
{
"comment": "a <- 1",
"ref": "a",
"value": 1
}
],
"location": "l",
"probability": {
"comment": "(200 / 200)",
"exp": 1.0
}
}
],
"guard": {
"comment": "((s = 1) & (a = 0))",
"exp": {
"left": {
"left": "s",
"op": "=",
"right": 1
},
"op": "∧",
"right": {
"left": "a",
"op": "=",
"right": 0
}
}
},
"location": "l",
"rate": {
"comment": "200",
"exp": 200
}
},
{
"action": "loop2a",
"destinations": [
{
"assignments": [
{
"comment": "s <- (s + 1)",
"ref": "s",
"value": {
"left": "s",
"op": "+",
"right": 1
}
}
],
"location": "l",
"probability": {
"comment": "(200 / 200)",
"exp": 1.0
}
}
],
"guard": {
"comment": "((s = 2) & (a = 0))",
"exp": {
"left": {
"left": "s",
"op": "=",
"right": 2
},
"op": "∧",
"right": {
"left": "a",
"op": "=",
"right": 0
}
}
},
"location": "l",
"rate": {
"comment": "200",
"exp": 200
}
},
{
"action": "loop2b",
"destinations": [
{
"assignments": [
{
"comment": "a <- 1",
"ref": "a",
"value": 1
}
],
"location": "l",
"probability": {
"comment": "(200 / 200)",
"exp": 1.0
}
}
],
"guard": {
"comment": "((s = 2) & (a = 0))",
"exp": {
"left": {
"left": "s",
"op": "=",
"right": 2
},
"op": "∧",
"right": {
"left": "a",
"op": "=",
"right": 0
}
}
},
"location": "l",
"rate": {
"comment": "200",
"exp": 200
}
},
{
"action": "loop3a",
"destinations": [
{
"assignments": [
{
"comment": "s <- (s + 1)",
"ref": "s",
"value": {
"left": "s",
"op": "+",
"right": 1
}
}
],
"location": "l",
"probability": {
"comment": "(200 / 200)",
"exp": 1.0
}
}
],
"guard": {
"comment": "((s = 3) & (a = 0))",
"exp": {
"left": {
"left": "s",
"op": "=",
"right": 3
},
"op": "∧",
"right": {
"left": "a",
"op": "=",
"right": 0
}
}
},
"location": "l",
"rate": {
"comment": "200",
"exp": 200
}
},
{
"action": "loop3b",
"destinations": [
{
"assignments": [
{
"comment": "a <- 1",
"ref": "a",
"value": 1
}
],
"location": "l",
"probability": {
"comment": "(200 / 200)",
"exp": 1.0
}
}
],
"guard": {
"comment": "((s = 3) & (a = 0))",
"exp": {
"left": {
"left": "s",
"op": "=",
"right": 3
},
"op": "∧",
"right": {
"left": "a",
"op": "=",
"right": 0
}
}
},
"location": "l",
"rate": {
"comment": "200",
"exp": 200
}
},
{
"action": "loop4a",
"destinations": [
{
"assignments": [
{
"comment": "s <- (s + 1)",
"ref": "s",
"value": {
"left": "s",
"op": "+",
"right": 1
}
}
],
"location": "l",
"probability": {
"comment": "(200 / 200)",
"exp": 1.0
}
}
],
"guard": {
"comment": "((s = 4) & (a = 0))",
"exp": {
"left": {
"left": "s",
"op": "=",
"right": 4
},
"op": "∧",
"right": {
"left": "a",
"op": "=",
"right": 0
}
}
},
"location": "l",
"rate": {
"comment": "200",
"exp": 200
}
},
{
"action": "loop4b",
"destinations": [
{
"assignments": [
{
"comment": "a <- 1",
"ref": "a",
"value": 1
}
],
"location": "l",
"probability": {
"comment": "(200 / 200)",
"exp": 1.0
}
}
],
"guard": {
"comment": "((s = 4) & (a = 0))",
"exp": {
"left": {
"left": "s",
"op": "=",
"right": 4
},
"op": "∧",
"right": {
"left": "a",
"op": "=",
"right": 0
}
}
},
"location": "l",
"rate": {
"comment": "200",
"exp": 200
}
},
{
"action": "loop5a",
"destinations": [
{
"assignments": [
{
"comment": "s <- (s + 1)",
"ref": "s",
"value": {
"left": "s",
"op": "+",
"right": 1
}
}
],
"location": "l",
"probability": {
"comment": "(200 / 200)",
"exp": 1.0
}
}
],
"guard": {
"comment": "((s = 5) & (a = 0))",
"exp": {
"left": {
"left": "s",
"op": "=",
"right": 5
},
"op": "∧",
"right": {
"left": "a",
"op": "=",
"right": 0
}
}
},
"location": "l",
"rate": {
"comment": "200",
"exp": 200
}
},
{
"action": "loop5b",
"destinations": [
{
"assignments": [
{
"comment": "a <- 1",
"ref": "a",
"value": 1
}
],
"location": "l",
"probability": {
"comment": "(200 / 200)",
"exp": 1.0
}
}
],
"guard": {
"comment": "((s = 5) & (a = 0))",
"exp": {
"left": {
"left": "s",
"op": "=",
"right": 5
},
"op": "∧",
"right": {
"left": "a",
"op": "=",
"right": 0
}
}
},
"location": "l",
"rate": {
"comment": "200",
"exp": 200
}
},
{
"action": "loop6a",
"destinations": [
{
"assignments": [
{
"comment": "s <- (s + 1)",
"ref": "s",
"value": {
"left": "s",
"op": "+",
"right": 1
}
}
],
"location": "l",
"probability": {
"comment": "(200 / 200)",
"exp": 1.0
}
}
],
"guard": {
"comment": "((s = 6) & (a = 0))",
"exp": {
"left": {
"left": "s",
"op": "=",
"right": 6
},
"op": "∧",
"right": {
"left": "a",
"op": "=",
"right": 0
}
}
},
"location": "l",
"rate": {
"comment": "200",
"exp": 200
}
},
{
"action": "loop6b",
"destinations": [
{
"assignments": [
{
"comment": "a <- 1",
"ref": "a",
"value": 1
}
],
"location": "l",
"probability": {
"comment": "(200 / 200)",
"exp": 1.0
}
}
],
"guard": {
"comment": "((s = 6) & (a = 0))",
"exp": {
"left": {
"left": "s",
"op": "=",
"right": 6
},
"op": "∧",
"right": {
"left": "a",
"op": "=",
"right": 0
}
}
},
"location": "l",
"rate": {
"comment": "200",
"exp": 200
}
},
{
"action": "loop7a",
"destinations": [
{
"assignments": [
{
"comment": "s <- (s + 1)",
"ref": "s",
"value": {
"left": "s",
"op": "+",
"right": 1
}
}
],
"location": "l",
"probability": {
"comment": "(200 / 200)",
"exp": 1.0
}
}
],
"guard": {
"comment": "((s = 7) & (a = 0))",
"exp": {
"left": {
"left": "s",
"op": "=",
"right": 7
},
"op": "∧",
"right": {
"left": "a",
"op": "=",
"right": 0
}
}
},
"location": "l",
"rate": {
"comment": "200",
"exp": 200
}
},
{
"action": "loop7b",
"destinations": [
{
"assignments": [
{
"comment": "a <- 1",
"ref": "a",
"value": 1
}
],
"location": "l",
"probability": {
"comment": "(200 / 200)",
"exp": 1.0
}
}
],
"guard": {
"comment": "((s = 7) & (a = 0))",
"exp": {
"left": {
"left": "s",
"op": "=",
"right": 7
},
"op": "∧",
"right": {
"left": "a",
"op": "=",
"right": 0
}
}
},
"location": "l",
"rate": {
"comment": "200",
"exp": 200
}
},
{
"action": "loop8a",
"destinations": [
{
"assignments": [
{
"comment": "s <- (s + 1)",
"ref": "s",
"value": {
"left": "s",
"op": "+",
"right": 1
}
}
],
"location": "l",
"probability": {
"comment": "(200 / 200)",
"exp": 1.0
}
}
],
"guard": {
"comment": "((s = 8) & (a = 0))",
"exp": {
"left": {
"left": "s",
"op": "=",
"right": 8
},
"op": "∧",
"right": {
"left": "a",
"op": "=",
"right": 0
}
}
},
"location": "l",
"rate": {
"comment": "200",
"exp": 200
}
},
{
"action": "loop8b",
"destinations": [
{
"assignments": [
{
"comment": "a <- 1",
"ref": "a",
"value": 1
}
],
"location": "l",
"probability": {
"comment": "(200 / 200)",
"exp": 1.0
}
}
],
"guard": {
"comment": "((s = 8) & (a = 0))",
"exp": {
"left": {
"left": "s",
"op": "=",
"right": 8
},
"op": "∧",
"right": {
"left": "a",
"op": "=",
"right": 0
}
}
},
"location": "l",
"rate": {
"comment": "200",
"exp": 200
}
},
{
"action": "loop9a",
"destinations": [
{
"assignments": [
{
"comment": "s <- (s + 1)",
"ref": "s",
"value": {
"left": "s",
"op": "+",
"right": 1
}
}
],
"location": "l",
"probability": {
"comment": "(200 / 200)",
"exp": 1.0
}
}
],
"guard": {
"comment": "((s = 9) & (a = 0))",
"exp": {
"left": {
"left": "s",
"op": "=",
"right": 9
},
"op": "∧",
"right": {
"left": "a",
"op": "=",
"right": 0
}
}
},
"location": "l",
"rate": {
"comment": "200",
"exp": 200
}
},
{
"action": "loop9b",
"destinations": [
{
"assignments": [
{
"comment": "a <- 1",
"ref": "a",
"value": 1
}
],
"location": "l",
"probability": {
"comment": "(200 / 200)",
"exp": 1.0
}
}
],
"guard": {
"comment": "((s = 9) & (a = 0))",
"exp": {
"left": {
"left": "s",
"op": "=",
"right": 9
},
"op": "∧",
"right": {
"left": "a",
"op": "=",
"right": 0
}
}
},
"location": "l",
"rate": {
"comment": "200",
"exp": 200
}
},
{
"action": "serve1",
"destinations": [
{
"assignments": [
{
"comment": "s <- (s + 1)",
"ref": "s",
"value": {
"left": "s",
"op": "+",
"right": 1
}
},
{
"comment": "a <- 0",
"ref": "a",
"value": 0
}
],
"location": "l",
"probability": {
"comment": "(1 / 1)",
"exp": 1.0
}
}
],
"guard": {
"comment": "((s = 1) & (a = 1))",
"exp": {
"left": {
"left": "s",
"op": "=",
"right": 1
},
"op": "∧",
"right": {
"left": "a",
"op": "=",
"right": 1
}
}
},
"location": "l",
"rate": {
"comment": "1",
"exp": 1
}
},
{
"action": "serve10",
"destinations": [
{
"assignments": [
{
"comment": "s <- (s + 1)",
"ref": "s",
"value": {
"left": "s",
"op": "+",
"right": 1
}
},
{
"comment": "a <- 0",
"ref": "a",
"value": 0
}
],
"location": "l",
"probability": {
"comment": "(1 / 1)",
"exp": 1.0
}
}
],
"guard": {
"comment": "((s = 10) & (a = 1))",
"exp": {
"left": {
"left": "s",
"op": "=",
"right": 10
},
"op": "∧",
"right": {
"left": "a",
"op": "=",
"right": 1
}
}
},
"location": "l",
"rate": {
"comment": "1",
"exp": 1
}
},
{
"action": "serve11",
"destinations": [
{
"assignments": [
{
"comment": "s <- (s + 1)",
"ref": "s",
"value": {
"left": "s",
"op": "+",
"right": 1
}
},
{
"comment": "a <- 0",
"ref": "a",
"value": 0
}
],
"location": "l",
"probability": {
"comment": "(1 / 1)",
"exp": 1.0
}
}
],
"guard": {
"comment": "((s = 11) & (a = 1))",
"exp": {
"left": {
"left": "s",
"op": "=",
"right": 11
},
"op": "∧",
"right": {
"left": "a",
"op": "=",
"right": 1
}
}
},
"location": "l",
"rate": {
"comment": "1",
"exp": 1
}
},
{
"action": "serve12",
"destinations": [
{
"assignments": [
{
"comment": "s <- (s + 1)",
"ref": "s",
"value": {
"left": "s",
"op": "+",
"right": 1
}
},
{
"comment": "a <- 0",
"ref": "a",
"value": 0
}
],
"location": "l",
"probability": {
"comment": "(1 / 1)",
"exp": 1.0
}
}
],
"guard": {
"comment": "((s = 12) & (a = 1))",
"exp": {
"left": {
"left": "s",
"op": "=",
"right": 12
},
"op": "∧",
"right": {
"left": "a",
"op": "=",
"right": 1
}
}
},
"location": "l",
"rate": {
"comment": "1",
"exp": 1
}
},
{
"action": "serve13",
"destinations": [
{
"assignments": [
{
"comment": "s <- (s + 1)",
"ref": "s",
"value": {
"left": "s",
"op": "+",
"right": 1
}
},
{
"comment": "a <- 0",
"ref": "a",
"value": 0
}
],
"location": "l",
"probability": {
"comment": "(1 / 1)",
"exp": 1.0
}
}
],
"guard": {
"comment": "((s = 13) & (a = 1))",
"exp": {
"left": {
"left": "s",
"op": "=",
"right": 13
},
"op": "∧",
"right": {
"left": "a",
"op": "=",
"right": 1
}
}
},
"location": "l",
"rate": {
"comment": "1",
"exp": 1
}
},
{
"action": "serve14",
"destinations": [
{
"assignments": [
{
"comment": "s <- (s + 1)",
"ref": "s",
"value": {
"left": "s",
"op": "+",
"right": 1
}
},
{
"comment": "a <- 0",
"ref": "a",
"value": 0
}
],
"location": "l",
"probability": {
"comment": "(1 / 1)",
"exp": 1.0
}
}
],
"guard": {
"comment": "((s = 14) & (a = 1))",
"exp": {
"left": {
"left": "s",
"op": "=",
"right": 14
},
"op": "∧",
"right": {
"left": "a",
"op": "=",
"right": 1
}
}
},
"location": "l",
"rate": {
"comment": "1",
"exp": 1
}
},
{
"action": "serve15",
"destinations": [
{
"assignments": [
{
"comment": "s <- (s + 1)",
"ref": "s",
"value": {
"left": "s",
"op": "+",
"right": 1
}
},
{
"comment": "a <- 0",
"ref": "a",
"value": 0
}
],
"location": "l",
"probability": {
"comment": "(1 / 1)",
"exp": 1.0
}
}
],
"guard": {
"comment": "((s = 15) & (a = 1))",
"exp": {
"left": {
"left": "s",
"op": "=",
"right": 15
},
"op": "∧",
"right": {
"left": "a",
"op": "=",
"right": 1
}
}
},
"location": "l",
"rate": {
"comment": "1",
"exp": 1
}
},
{
"action": "serve16",
"destinations": [
{
"assignments": [
{
"comment": "s <- (s + 1)",
"ref": "s",
"value": {
"left": "s",
"op": "+",
"right": 1
}
},
{
"comment": "a <- 0",
"ref": "a",
"value": 0
}
],
"location": "l",
"probability": {
"comment": "(1 / 1)",
"exp": 1.0
}
}
],
"guard": {
"comment": "((s = 16) & (a = 1))",
"exp": {
"left": {
"left": "s",
"op": "=",
"right": 16
},
"op": "∧",
"right": {
"left": "a",
"op": "=",
"right": 1
}
}
},
"location": "l",
"rate": {
"comment": "1",
"exp": 1
}
},
{
"action": "serve17",
"destinations": [
{
"assignments": [
{
"comment": "s <- (s + 1)",
"ref": "s",
"value": {
"left": "s",
"op": "+",
"right": 1
}
},
{
"comment": "a <- 0",
"ref": "a",
"value": 0
}
],
"location": "l",
"probability": {
"comment": "(1 / 1)",
"exp": 1.0
}
}
],
"guard": {
"comment": "((s = 17) & (a = 1))",
"exp": {
"left": {
"left": "s",
"op": "=",
"right": 17
},
"op": "∧",
"right": {
"left": "a",
"op": "=",
"right": 1
}
}
},
"location": "l",
"rate": {
"comment": "1",
"exp": 1
}
},
{
"action": "serve18",
"destinations": [
{
"assignments": [
{
"comment": "s <- 1",
"ref": "s",
"value": 1
},
{
"comment": "a <- 0",
"ref": "a",
"value": 0
}
],
"location": "l",
"probability": {
"comment": "(1 / 1)",
"exp": 1.0
}
}
],
"guard": {
"comment": "((s = 18) & (a = 1))",
"exp": {
"left": {
"left": "s",
"op": "=",
"right": 18
},
"op": "∧",
"right": {
"left": "a",
"op": "=",
"right": 1
}
}
},
"location": "l",
"rate": {
"comment": "1",
"exp": 1
}
},
{
"action": "serve2",
"destinations": [
{
"assignments": [
{
"comment": "s <- (s + 1)",
"ref": "s",
"value": {
"left": "s",
"op": "+",
"right": 1
}
},
{
"comment": "a <- 0",
"ref": "a",
"value": 0
}
],
"location": "l",
"probability": {
"comment": "(1 / 1)",
"exp": 1.0
}
}
],
"guard": {
"comment": "((s = 2) & (a = 1))",
"exp": {
"left": {
"left": "s",
"op": "=",
"right": 2
},
"op": "∧",
"right": {
"left": "a",
"op": "=",
"right": 1
}
}
},
"location": "l",
"rate": {
"comment": "1",
"exp": 1
}
},
{
"action": "serve3",
"destinations": [
{
"assignments": [
{
"comment": "s <- (s + 1)",
"ref": "s",
"value": {
"left": "s",
"op": "+",
"right": 1
}
},
{
"comment": "a <- 0",
"ref": "a",
"value": 0
}
],
"location": "l",
"probability": {
"comment": "(1 / 1)",
"exp": 1.0
}
}
],
"guard": {
"comment": "((s = 3) & (a = 1))",
"exp": {
"left": {
"left": "s",
"op": "=",
"right": 3
},
"op": "∧",
"right": {
"left": "a",
"op": "=",
"right": 1
}
}
},
"location": "l",
"rate": {
"comment": "1",
"exp": 1
}
},
{
"action": "serve4",
"destinations": [
{
"assignments": [
{
"comment": "s <- (s + 1)",
"ref": "s",
"value": {
"left": "s",
"op": "+",
"right": 1
}
},
{
"comment": "a <- 0",
"ref": "a",
"value": 0
}
],
"location": "l",
"probability": {
"comment": "(1 / 1)",
"exp": 1.0
}
}
],
"guard": {
"comment": "((s = 4) & (a = 1))",
"exp": {
"left": {
"left": "s",
"op": "=",
"right": 4
},
"op": "∧",
"right": {
"left": "a",
"op": "=",
"right": 1
}
}
},
"location": "l",
"rate": {
"comment": "1",
"exp": 1
}
},
{
"action": "serve5",
"destinations": [
{
"assignments": [
{
"comment": "s <- (s + 1)",
"ref": "s",
"value": {
"left": "s",
"op": "+",
"right": 1
}
},
{
"comment": "a <- 0",
"ref": "a",
"value": 0
}
],
"location": "l",
"probability": {
"comment": "(1 / 1)",
"exp": 1.0
}
}
],
"guard": {
"comment": "((s = 5) & (a = 1))",
"exp": {
"left": {
"left": "s",
"op": "=",
"right": 5
},
"op": "∧",
"right": {
"left": "a",
"op": "=",
"right": 1
}
}
},
"location": "l",
"rate": {
"comment": "1",
"exp": 1
}
},
{
"action": "serve6",
"destinations": [
{
"assignments": [
{
"comment": "s <- (s + 1)",
"ref": "s",
"value": {
"left": "s",
"op": "+",
"right": 1
}
},
{
"comment": "a <- 0",
"ref": "a",
"value": 0
}
],
"location": "l",
"probability": {
"comment": "(1 / 1)",
"exp": 1.0
}
}
],
"guard": {
"comment": "((s = 6) & (a = 1))",
"exp": {
"left": {
"left": "s",
"op": "=",
"right": 6
},
"op": "∧",
"right": {
"left": "a",
"op": "=",
"right": 1
}
}
},
"location": "l",
"rate": {
"comment": "1",
"exp": 1
}
},
{
"action": "serve7",
"destinations": [
{
"assignments": [
{
"comment": "s <- (s + 1)",
"ref": "s",
"value": {
"left": "s",
"op": "+",
"right": 1
}
},
{
"comment": "a <- 0",
"ref": "a",
"value": 0
}
],
"location": "l",
"probability": {
"comment": "(1 / 1)",
"exp": 1.0
}
}
],
"guard": {
"comment": "((s = 7) & (a = 1))",
"exp": {
"left": {
"left": "s",
"op": "=",
"right": 7
},
"op": "∧",
"right": {
"left": "a",
"op": "=",
"right": 1
}
}
},
"location": "l",
"rate": {
"comment": "1",
"exp": 1
}
},
{
"action": "serve8",
"destinations": [
{
"assignments": [
{
"comment": "s <- (s + 1)",
"ref": "s",
"value": {
"left": "s",
"op": "+",
"right": 1
}
},
{
"comment": "a <- 0",
"ref": "a",
"value": 0
}
],
"location": "l",
"probability": {
"comment": "(1 / 1)",
"exp": 1.0
}
}
],
"guard": {
"comment": "((s = 8) & (a = 1))",
"exp": {
"left": {
"left": "s",
"op": "=",
"right": 8
},
"op": "∧",
"right": {
"left": "a",
"op": "=",
"right": 1
}
}
},
"location": "l",
"rate": {
"comment": "1",
"exp": 1
}
},
{
"action": "serve9",
"destinations": [
{
"assignments": [
{
"comment": "s <- (s + 1)",
"ref": "s",
"value": {
"left": "s",
"op": "+",
"right": 1
}
},
{
"comment": "a <- 0",
"ref": "a",
"value": 0
}
],
"location": "l",
"probability": {
"comment": "(1 / 1)",
"exp": 1.0
}
}
],
"guard": {
"comment": "((s = 9) & (a = 1))",
"exp": {
"left": {
"left": "s",
"op": "=",
"right": 9
},
"op": "∧",
"right": {
"left": "a",
"op": "=",
"right": 1
}
}
},
"location": "l",
"rate": {
"comment": "1",
"exp": 1
}
}
],
"initial-locations": [
"l"
],
"locations": [
{
"name": "l",
"transient-values": [
{
"comment": "serve_s2 <- ((s = 2) & (a = 1))",
"ref": "serve_s2",
"value": {
"left": {
"left": "s",
"op": "=",
"right": 2
},
"op": "∧",
"right": {
"left": "a",
"op": "=",
"right": 1
}
}
},
{
"comment": "serve_s1 <- ((s = 1) & (a = 1))",
"ref": "serve_s1",
"value": {
"left": {
"left": "s",
"op": "=",
"right": 1
},
"op": "∧",
"right": {
"left": "a",
"op": "=",
"right": 1
}
}
}
]
}
],
"name": "server",
"variables": []
},
{
"edges": [
{
"destinations": [
{
"assignments": [
{
"comment": "s1 <- 1",
"ref": "s1",
"value": 1
}
],
"location": "l",
"probability": {
"comment": "((1 / 18) / (1 / 18))",
"exp": 1.0
}
}
],
"guard": {
"comment": "(s1 = 0)",
"exp": {
"left": "s1",
"op": "=",
"right": 0
}
},
"location": "l",
"rate": {
"comment": "(1 / 18)",
"exp": {
"left": 1.0,
"op": "/",
"right": 18.0
}
}
},
{
"action": "loop1a",
"destinations": [
{
"assignments": [
{
"comment": "s1 <- 0",
"ref": "s1",
"value": 0
}
],
"location": "l",
"probability": {
"comment": "(1 / 1)",
"exp": 1
}
}
],
"guard": {
"comment": "(s1 = 0)",
"exp": {
"left": "s1",
"op": "=",
"right": 0
}
},
"location": "l",
"rate": {
"comment": "1",
"exp": 1
}
},
{
"action": "loop1b",
"destinations": [
{
"assignments": [
{
"comment": "s1 <- 1",
"ref": "s1",
"value": 1
}
],
"location": "l",
"probability": {
"comment": "(1 / 1)",
"exp": 1
}
}
],
"guard": {
"comment": "(s1 = 1)",
"exp": {
"left": "s1",
"op": "=",
"right": 1
}
},
"location": "l",
"rate": {
"comment": "1",
"exp": 1
}
},
{
"action": "serve1",
"destinations": [
{
"assignments": [
{
"comment": "s1 <- 0",
"ref": "s1",
"value": 0
}
],
"location": "l",
"probability": {
"comment": "(1 / 1)",
"exp": 1
}
}
],
"guard": {
"comment": "(s1 = 1)",
"exp": {
"left": "s1",
"op": "=",
"right": 1
}
},
"location": "l",
"rate": {
"comment": "1",
"exp": 1
}
}
],
"initial-locations": [
"l"
],
"locations": [
{
"name": "l"
}
],
"name": "station1",
"variables": [
{
"initial-value": 0,
"name": "s1",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 1
}
}
]
},
{
"edges": [
{
"destinations": [
{
"assignments": [
{
"comment": "s2 <- 1",
"ref": "s2",
"value": 1
}
],
"location": "l",
"probability": {
"comment": "((1 / 18) / (1 / 18))",
"exp": 1.0
}
}
],
"guard": {
"comment": "(s2 = 0)",
"exp": {
"left": "s2",
"op": "=",
"right": 0
}
},
"location": "l",
"rate": {
"comment": "(1 / 18)",
"exp": {
"left": 1.0,
"op": "/",
"right": 18.0
}
}
},
{
"action": "loop2a",
"destinations": [
{
"assignments": [
{
"comment": "s2 <- 0",
"ref": "s2",
"value": 0
}
],
"location": "l",
"probability": {
"comment": "(1 / 1)",
"exp": 1
}
}
],
"guard": {
"comment": "(s2 = 0)",
"exp": {
"left": "s2",
"op": "=",
"right": 0
}
},
"location": "l",
"rate": {
"comment": "1",
"exp": 1
}
},
{
"action": "loop2b",
"destinations": [
{
"assignments": [
{
"comment": "s2 <- 1",
"ref": "s2",
"value": 1
}
],
"location": "l",
"probability": {
"comment": "(1 / 1)",
"exp": 1
}
}
],
"guard": {
"comment": "(s2 = 1)",
"exp": {
"left": "s2",
"op": "=",
"right": 1
}
},
"location": "l",
"rate": {
"comment": "1",
"exp": 1
}
},
{
"action": "serve2",
"destinations": [
{
"assignments": [
{
"comment": "s2 <- 0",
"ref": "s2",
"value": 0
}
],
"location": "l",
"probability": {
"comment": "(1 / 1)",
"exp": 1
}
}
],
"guard": {
"comment": "(s2 = 1)",
"exp": {
"left": "s2",
"op": "=",
"right": 1
}
},
"location": "l",
"rate": {
"comment": "1",
"exp": 1
}
}
],
"initial-locations": [
"l"
],
"locations": [
{
"name": "l"
}
],
"name": "station2",
"variables": [
{
"initial-value": 0,
"name": "s2",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 1
}
}
]
},
{
"edges": [
{
"destinations": [
{
"assignments": [
{
"comment": "s3 <- 1",
"ref": "s3",
"value": 1
}
],
"location": "l",
"probability": {
"comment": "((1 / 18) / (1 / 18))",
"exp": 1.0
}
}
],
"guard": {
"comment": "(s3 = 0)",
"exp": {
"left": "s3",
"op": "=",
"right": 0
}
},
"location": "l",
"rate": {
"comment": "(1 / 18)",
"exp": {
"left": 1.0,
"op": "/",
"right": 18.0
}
}
},
{
"action": "loop3a",
"destinations": [
{
"assignments": [
{
"comment": "s3 <- 0",
"ref": "s3",
"value": 0
}
],
"location": "l",
"probability": {
"comment": "(1 / 1)",
"exp": 1
}
}
],
"guard": {
"comment": "(s3 = 0)",
"exp": {
"left": "s3",
"op": "=",
"right": 0
}
},
"location": "l",
"rate": {
"comment": "1",
"exp": 1
}
},
{
"action": "loop3b",
"destinations": [
{
"assignments": [
{
"comment": "s3 <- 1",
"ref": "s3",
"value": 1
}
],
"location": "l",
"probability": {
"comment": "(1 / 1)",
"exp": 1
}
}
],
"guard": {
"comment": "(s3 = 1)",
"exp": {
"left": "s3",
"op": "=",
"right": 1
}
},
"location": "l",
"rate": {
"comment": "1",
"exp": 1
}
},
{
"action": "serve3",
"destinations": [
{
"assignments": [
{
"comment": "s3 <- 0",
"ref": "s3",
"value": 0
}
],
"location": "l",
"probability": {
"comment": "(1 / 1)",
"exp": 1
}
}
],
"guard": {
"comment": "(s3 = 1)",
"exp": {
"left": "s3",
"op": "=",
"right": 1
}
},
"location": "l",
"rate": {
"comment": "1",
"exp": 1
}
}
],
"initial-locations": [
"l"
],
"locations": [
{
"name": "l"
}
],
"name": "station3",
"variables": [
{
"initial-value": 0,
"name": "s3",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 1
}
}
]
},
{
"edges": [
{
"destinations": [
{
"assignments": [
{
"comment": "s4 <- 1",
"ref": "s4",
"value": 1
}
],
"location": "l",
"probability": {
"comment": "((1 / 18) / (1 / 18))",
"exp": 1.0
}
}
],
"guard": {
"comment": "(s4 = 0)",
"exp": {
"left": "s4",
"op": "=",
"right": 0
}
},
"location": "l",
"rate": {
"comment": "(1 / 18)",
"exp": {
"left": 1.0,
"op": "/",
"right": 18.0
}
}
},
{
"action": "loop4a",
"destinations": [
{
"assignments": [
{
"comment": "s4 <- 0",
"ref": "s4",
"value": 0
}
],
"location": "l",
"probability": {
"comment": "(1 / 1)",
"exp": 1
}
}
],
"guard": {
"comment": "(s4 = 0)",
"exp": {
"left": "s4",
"op": "=",
"right": 0
}
},
"location": "l",
"rate": {
"comment": "1",
"exp": 1
}
},
{
"action": "loop4b",
"destinations": [
{
"assignments": [
{
"comment": "s4 <- 1",
"ref": "s4",
"value": 1
}
],
"location": "l",
"probability": {
"comment": "(1 / 1)",
"exp": 1
}
}
],
"guard": {
"comment": "(s4 = 1)",
"exp": {
"left": "s4",
"op": "=",
"right": 1
}
},
"location": "l",
"rate": {
"comment": "1",
"exp": 1
}
},
{
"action": "serve4",
"destinations": [
{
"assignments": [
{
"comment": "s4 <- 0",
"ref": "s4",
"value": 0
}
],
"location": "l",
"probability": {
"comment": "(1 / 1)",
"exp": 1
}
}
],
"guard": {
"comment": "(s4 = 1)",
"exp": {
"left": "s4",
"op": "=",
"right": 1
}
},
"location": "l",
"rate": {
"comment": "1",
"exp": 1
}
}
],
"initial-locations": [
"l"
],
"locations": [
{
"name": "l"
}
],
"name": "station4",
"variables": [
{
"initial-value": 0,
"name": "s4",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 1
}
}
]
},
{
"edges": [
{
"destinations": [
{
"assignments": [
{
"comment": "s5 <- 1",
"ref": "s5",
"value": 1
}
],
"location": "l",
"probability": {
"comment": "((1 / 18) / (1 / 18))",
"exp": 1.0
}
}
],
"guard": {
"comment": "(s5 = 0)",
"exp": {
"left": "s5",
"op": "=",
"right": 0
}
},
"location": "l",
"rate": {
"comment": "(1 / 18)",
"exp": {
"left": 1.0,
"op": "/",
"right": 18.0
}
}
},
{
"action": "loop5a",
"destinations": [
{
"assignments": [
{
"comment": "s5 <- 0",
"ref": "s5",
"value": 0
}
],
"location": "l",
"probability": {
"comment": "(1 / 1)",
"exp": 1
}
}
],
"guard": {
"comment": "(s5 = 0)",
"exp": {
"left": "s5",
"op": "=",
"right": 0
}
},
"location": "l",
"rate": {
"comment": "1",
"exp": 1
}
},
{
"action": "loop5b",
"destinations": [
{
"assignments": [
{
"comment": "s5 <- 1",
"ref": "s5",
"value": 1
}
],
"location": "l",
"probability": {
"comment": "(1 / 1)",
"exp": 1
}
}
],
"guard": {
"comment": "(s5 = 1)",
"exp": {
"left": "s5",
"op": "=",
"right": 1
}
},
"location": "l",
"rate": {
"comment": "1",
"exp": 1
}
},
{
"action": "serve5",
"destinations": [
{
"assignments": [
{
"comment": "s5 <- 0",
"ref": "s5",
"value": 0
}
],
"location": "l",
"probability": {
"comment": "(1 / 1)",
"exp": 1
}
}
],
"guard": {
"comment": "(s5 = 1)",
"exp": {
"left": "s5",
"op": "=",
"right": 1
}
},
"location": "l",
"rate": {
"comment": "1",
"exp": 1
}
}
],
"initial-locations": [
"l"
],
"locations": [
{
"name": "l"
}
],
"name": "station5",
"variables": [
{
"initial-value": 0,
"name": "s5",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 1
}
}
]
},
{
"edges": [
{
"destinations": [
{
"assignments": [
{
"comment": "s6 <- 1",
"ref": "s6",
"value": 1
}
],
"location": "l",
"probability": {
"comment": "((1 / 18) / (1 / 18))",
"exp": 1.0
}
}
],
"guard": {
"comment": "(s6 = 0)",
"exp": {
"left": "s6",
"op": "=",
"right": 0
}
},
"location": "l",
"rate": {
"comment": "(1 / 18)",
"exp": {
"left": 1.0,
"op": "/",
"right": 18.0
}
}
},
{
"action": "loop6a",
"destinations": [
{
"assignments": [
{
"comment": "s6 <- 0",
"ref": "s6",
"value": 0
}
],
"location": "l",
"probability": {
"comment": "(1 / 1)",
"exp": 1
}
}
],
"guard": {
"comment": "(s6 = 0)",
"exp": {
"left": "s6",
"op": "=",
"right": 0
}
},
"location": "l",
"rate": {
"comment": "1",
"exp": 1
}
},
{
"action": "loop6b",
"destinations": [
{
"assignments": [
{
"comment": "s6 <- 1",
"ref": "s6",
"value": 1
}
],
"location": "l",
"probability": {
"comment": "(1 / 1)",
"exp": 1
}
}
],
"guard": {
"comment": "(s6 = 1)",
"exp": {
"left": "s6",
"op": "=",
"right": 1
}
},
"location": "l",
"rate": {
"comment": "1",
"exp": 1
}
},
{
"action": "serve6",
"destinations": [
{
"assignments": [
{
"comment": "s6 <- 0",
"ref": "s6",
"value": 0
}
],
"location": "l",
"probability": {
"comment": "(1 / 1)",
"exp": 1
}
}
],
"guard": {
"comment": "(s6 = 1)",
"exp": {
"left": "s6",
"op": "=",
"right": 1
}
},
"location": "l",
"rate": {
"comment": "1",
"exp": 1
}
}
],
"initial-locations": [
"l"
],
"locations": [
{
"name": "l"
}
],
"name": "station6",
"variables": [
{
"initial-value": 0,
"name": "s6",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 1
}
}
]
},
{
"edges": [
{
"destinations": [
{
"assignments": [
{
"comment": "s7 <- 1",
"ref": "s7",
"value": 1
}
],
"location": "l",
"probability": {
"comment": "((1 / 18) / (1 / 18))",
"exp": 1.0
}
}
],
"guard": {
"comment": "(s7 = 0)",
"exp": {
"left": "s7",
"op": "=",
"right": 0
}
},
"location": "l",
"rate": {
"comment": "(1 / 18)",
"exp": {
"left": 1.0,
"op": "/",
"right": 18.0
}
}
},
{
"action": "loop7a",
"destinations": [
{
"assignments": [
{
"comment": "s7 <- 0",
"ref": "s7",
"value": 0
}
],
"location": "l",
"probability": {
"comment": "(1 / 1)",
"exp": 1
}
}
],
"guard": {
"comment": "(s7 = 0)",
"exp": {
"left": "s7",
"op": "=",
"right": 0
}
},
"location": "l",
"rate": {
"comment": "1",
"exp": 1
}
},
{
"action": "loop7b",
"destinations": [
{
"assignments": [
{
"comment": "s7 <- 1",
"ref": "s7",
"value": 1
}
],
"location": "l",
"probability": {
"comment": "(1 / 1)",
"exp": 1
}
}
],
"guard": {
"comment": "(s7 = 1)",
"exp": {
"left": "s7",
"op": "=",
"right": 1
}
},
"location": "l",
"rate": {
"comment": "1",
"exp": 1
}
},
{
"action": "serve7",
"destinations": [
{
"assignments": [
{
"comment": "s7 <- 0",
"ref": "s7",
"value": 0
}
],
"location": "l",
"probability": {
"comment": "(1 / 1)",
"exp": 1
}
}
],
"guard": {
"comment": "(s7 = 1)",
"exp": {
"left": "s7",
"op": "=",
"right": 1
}
},
"location": "l",
"rate": {
"comment": "1",
"exp": 1
}
}
],
"initial-locations": [
"l"
],
"locations": [
{
"name": "l"
}
],
"name": "station7",
"variables": [
{
"initial-value": 0,
"name": "s7",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 1
}
}
]
},
{
"edges": [
{
"destinations": [
{
"assignments": [
{
"comment": "s8 <- 1",
"ref": "s8",
"value": 1
}
],
"location": "l",
"probability": {
"comment": "((1 / 18) / (1 / 18))",
"exp": 1.0
}
}
],
"guard": {
"comment": "(s8 = 0)",
"exp": {
"left": "s8",
"op": "=",
"right": 0
}
},
"location": "l",
"rate": {
"comment": "(1 / 18)",
"exp": {
"left": 1.0,
"op": "/",
"right": 18.0
}
}
},
{
"action": "loop8a",
"destinations": [
{
"assignments": [
{
"comment": "s8 <- 0",
"ref": "s8",
"value": 0
}
],
"location": "l",
"probability": {
"comment": "(1 / 1)",
"exp": 1
}
}
],
"guard": {
"comment": "(s8 = 0)",
"exp": {
"left": "s8",
"op": "=",
"right": 0
}
},
"location": "l",
"rate": {
"comment": "1",
"exp": 1
}
},
{
"action": "loop8b",
"destinations": [
{
"assignments": [
{
"comment": "s8 <- 1",
"ref": "s8",
"value": 1
}
],
"location": "l",
"probability": {
"comment": "(1 / 1)",
"exp": 1
}
}
],
"guard": {
"comment": "(s8 = 1)",
"exp": {
"left": "s8",
"op": "=",
"right": 1
}
},
"location": "l",
"rate": {
"comment": "1",
"exp": 1
}
},
{
"action": "serve8",
"destinations": [
{
"assignments": [
{
"comment": "s8 <- 0",
"ref": "s8",
"value": 0
}
],
"location": "l",
"probability": {
"comment": "(1 / 1)",
"exp": 1
}
}
],
"guard": {
"comment": "(s8 = 1)",
"exp": {
"left": "s8",
"op": "=",
"right": 1
}
},
"location": "l",
"rate": {
"comment": "1",
"exp": 1
}
}
],
"initial-locations": [
"l"
],
"locations": [
{
"name": "l"
}
],
"name": "station8",
"variables": [
{
"initial-value": 0,
"name": "s8",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 1
}
}
]
},
{
"edges": [
{
"destinations": [
{
"assignments": [
{
"comment": "s9 <- 1",
"ref": "s9",
"value": 1
}
],
"location": "l",
"probability": {
"comment": "((1 / 18) / (1 / 18))",
"exp": 1.0
}
}
],
"guard": {
"comment": "(s9 = 0)",
"exp": {
"left": "s9",
"op": "=",
"right": 0
}
},
"location": "l",
"rate": {
"comment": "(1 / 18)",
"exp": {
"left": 1.0,
"op": "/",
"right": 18.0
}
}
},
{
"action": "loop9a",
"destinations": [
{
"assignments": [
{
"comment": "s9 <- 0",
"ref": "s9",
"value": 0
}
],
"location": "l",
"probability": {
"comment": "(1 / 1)",
"exp": 1
}
}
],
"guard": {
"comment": "(s9 = 0)",
"exp": {
"left": "s9",
"op": "=",
"right": 0
}
},
"location": "l",
"rate": {
"comment": "1",
"exp": 1
}
},
{
"action": "loop9b",
"destinations": [
{
"assignments": [
{
"comment": "s9 <- 1",
"ref": "s9",
"value": 1
}
],
"location": "l",
"probability": {
"comment": "(1 / 1)",
"exp": 1
}
}
],
"guard": {
"comment": "(s9 = 1)",
"exp": {
"left": "s9",
"op": "=",
"right": 1
}
},
"location": "l",
"rate": {
"comment": "1",
"exp": 1
}
},
{
"action": "serve9",
"destinations": [
{
"assignments": [
{
"comment": "s9 <- 0",
"ref": "s9",
"value": 0
}
],
"location": "l",
"probability": {
"comment": "(1 / 1)",
"exp": 1
}
}
],
"guard": {
"comment": "(s9 = 1)",
"exp": {
"left": "s9",
"op": "=",
"right": 1
}
},
"location": "l",
"rate": {
"comment": "1",
"exp": 1
}
}
],
"initial-locations": [
"l"
],
"locations": [
{
"name": "l"
}
],
"name": "station9",
"variables": [
{
"initial-value": 0,
"name": "s9",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 1
}
}
]
},
{
"edges": [
{
"destinations": [
{
"assignments": [
{
"comment": "s10 <- 1",
"ref": "s10",
"value": 1
}
],
"location": "l",
"probability": {
"comment": "((1 / 18) / (1 / 18))",
"exp": 1.0
}
}
],
"guard": {
"comment": "(s10 = 0)",
"exp": {
"left": "s10",
"op": "=",
"right": 0
}
},
"location": "l",
"rate": {
"comment": "(1 / 18)",
"exp": {
"left": 1.0,
"op": "/",
"right": 18.0
}
}
},
{
"action": "loop10a",
"destinations": [
{
"assignments": [
{
"comment": "s10 <- 0",
"ref": "s10",
"value": 0
}
],
"location": "l",
"probability": {
"comment": "(1 / 1)",
"exp": 1
}
}
],
"guard": {
"comment": "(s10 = 0)",
"exp": {
"left": "s10",
"op": "=",
"right": 0
}
},
"location": "l",
"rate": {
"comment": "1",
"exp": 1
}
},
{
"action": "loop10b",
"destinations": [
{
"assignments": [
{
"comment": "s10 <- 1",
"ref": "s10",
"value": 1
}
],
"location": "l",
"probability": {
"comment": "(1 / 1)",
"exp": 1
}
}
],
"guard": {
"comment": "(s10 = 1)",
"exp": {
"left": "s10",
"op": "=",
"right": 1
}
},
"location": "l",
"rate": {
"comment": "1",
"exp": 1
}
},
{
"action": "serve10",
"destinations": [
{
"assignments": [
{
"comment": "s10 <- 0",
"ref": "s10",
"value": 0
}
],
"location": "l",
"probability": {
"comment": "(1 / 1)",
"exp": 1
}
}
],
"guard": {
"comment": "(s10 = 1)",
"exp": {
"left": "s10",
"op": "=",
"right": 1
}
},
"location": "l",
"rate": {
"comment": "1",
"exp": 1
}
}
],
"initial-locations": [
"l"
],
"locations": [
{
"name": "l"
}
],
"name": "station10",
"variables": [
{
"initial-value": 0,
"name": "s10",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 1
}
}
]
},
{
"edges": [
{
"destinations": [
{
"assignments": [
{
"comment": "s11 <- 1",
"ref": "s11",
"value": 1
}
],
"location": "l",
"probability": {
"comment": "((1 / 18) / (1 / 18))",
"exp": 1.0
}
}
],
"guard": {
"comment": "(s11 = 0)",
"exp": {
"left": "s11",
"op": "=",
"right": 0
}
},
"location": "l",
"rate": {
"comment": "(1 / 18)",
"exp": {
"left": 1.0,
"op": "/",
"right": 18.0
}
}
},
{
"action": "loop11a",
"destinations": [
{
"assignments": [
{
"comment": "s11 <- 0",
"ref": "s11",
"value": 0
}
],
"location": "l",
"probability": {
"comment": "(1 / 1)",
"exp": 1
}
}
],
"guard": {
"comment": "(s11 = 0)",
"exp": {
"left": "s11",
"op": "=",
"right": 0
}
},
"location": "l",
"rate": {
"comment": "1",
"exp": 1
}
},
{
"action": "loop11b",
"destinations": [
{
"assignments": [
{
"comment": "s11 <- 1",
"ref": "s11",
"value": 1
}
],
"location": "l",
"probability": {
"comment": "(1 / 1)",
"exp": 1
}
}
],
"guard": {
"comment": "(s11 = 1)",
"exp": {
"left": "s11",
"op": "=",
"right": 1
}
},
"location": "l",
"rate": {
"comment": "1",
"exp": 1
}
},
{
"action": "serve11",
"destinations": [
{
"assignments": [
{
"comment": "s11 <- 0",
"ref": "s11",
"value": 0
}
],
"location": "l",
"probability": {
"comment": "(1 / 1)",
"exp": 1
}
}
],
"guard": {
"comment": "(s11 = 1)",
"exp": {
"left": "s11",
"op": "=",
"right": 1
}
},
"location": "l",
"rate": {
"comment": "1",
"exp": 1
}
}
],
"initial-locations": [
"l"
],
"locations": [
{
"name": "l"
}
],
"name": "station11",
"variables": [
{
"initial-value": 0,
"name": "s11",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 1
}
}
]
},
{
"edges": [
{
"destinations": [
{
"assignments": [
{
"comment": "s12 <- 1",
"ref": "s12",
"value": 1
}
],
"location": "l",
"probability": {
"comment": "((1 / 18) / (1 / 18))",
"exp": 1.0
}
}
],
"guard": {
"comment": "(s12 = 0)",
"exp": {
"left": "s12",
"op": "=",
"right": 0
}
},
"location": "l",
"rate": {
"comment": "(1 / 18)",
"exp": {
"left": 1.0,
"op": "/",
"right": 18.0
}
}
},
{
"action": "loop12a",
"destinations": [
{
"assignments": [
{
"comment": "s12 <- 0",
"ref": "s12",
"value": 0
}
],
"location": "l",
"probability": {
"comment": "(1 / 1)",
"exp": 1
}
}
],
"guard": {
"comment": "(s12 = 0)",
"exp": {
"left": "s12",
"op": "=",
"right": 0
}
},
"location": "l",
"rate": {
"comment": "1",
"exp": 1
}
},
{
"action": "loop12b",
"destinations": [
{
"assignments": [
{
"comment": "s12 <- 1",
"ref": "s12",
"value": 1
}
],
"location": "l",
"probability": {
"comment": "(1 / 1)",
"exp": 1
}
}
],
"guard": {
"comment": "(s12 = 1)",
"exp": {
"left": "s12",
"op": "=",
"right": 1
}
},
"location": "l",
"rate": {
"comment": "1",
"exp": 1
}
},
{
"action": "serve12",
"destinations": [
{
"assignments": [
{
"comment": "s12 <- 0",
"ref": "s12",
"value": 0
}
],
"location": "l",
"probability": {
"comment": "(1 / 1)",
"exp": 1
}
}
],
"guard": {
"comment": "(s12 = 1)",
"exp": {
"left": "s12",
"op": "=",
"right": 1
}
},
"location": "l",
"rate": {
"comment": "1",
"exp": 1
}
}
],
"initial-locations": [
"l"
],
"locations": [
{
"name": "l"
}
],
"name": "station12",
"variables": [
{
"initial-value": 0,
"name": "s12",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 1
}
}
]
},
{
"edges": [
{
"destinations": [
{
"assignments": [
{
"comment": "s13 <- 1",
"ref": "s13",
"value": 1
}
],
"location": "l",
"probability": {
"comment": "((1 / 18) / (1 / 18))",
"exp": 1.0
}
}
],
"guard": {
"comment": "(s13 = 0)",
"exp": {
"left": "s13",
"op": "=",
"right": 0
}
},
"location": "l",
"rate": {
"comment": "(1 / 18)",
"exp": {
"left": 1.0,
"op": "/",
"right": 18.0
}
}
},
{
"action": "loop13a",
"destinations": [
{
"assignments": [
{
"comment": "s13 <- 0",
"ref": "s13",
"value": 0
}
],
"location": "l",
"probability": {
"comment": "(1 / 1)",
"exp": 1
}
}
],
"guard": {
"comment": "(s13 = 0)",
"exp": {
"left": "s13",
"op": "=",
"right": 0
}
},
"location": "l",
"rate": {
"comment": "1",
"exp": 1
}
},
{
"action": "loop13b",
"destinations": [
{
"assignments": [
{
"comment": "s13 <- 1",
"ref": "s13",
"value": 1
}
],
"location": "l",
"probability": {
"comment": "(1 / 1)",
"exp": 1
}
}
],
"guard": {
"comment": "(s13 = 1)",
"exp": {
"left": "s13",
"op": "=",
"right": 1
}
},
"location": "l",
"rate": {
"comment": "1",
"exp": 1
}
},
{
"action": "serve13",
"destinations": [
{
"assignments": [
{
"comment": "s13 <- 0",
"ref": "s13",
"value": 0
}
],
"location": "l",
"probability": {
"comment": "(1 / 1)",
"exp": 1
}
}
],
"guard": {
"comment": "(s13 = 1)",
"exp": {
"left": "s13",
"op": "=",
"right": 1
}
},
"location": "l",
"rate": {
"comment": "1",
"exp": 1
}
}
],
"initial-locations": [
"l"
],
"locations": [
{
"name": "l"
}
],
"name": "station13",
"variables": [
{
"initial-value": 0,
"name": "s13",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 1
}
}
]
},
{
"edges": [
{
"destinations": [
{
"assignments": [
{
"comment": "s14 <- 1",
"ref": "s14",
"value": 1
}
],
"location": "l",
"probability": {
"comment": "((1 / 18) / (1 / 18))",
"exp": 1.0
}
}
],
"guard": {
"comment": "(s14 = 0)",
"exp": {
"left": "s14",
"op": "=",
"right": 0
}
},
"location": "l",
"rate": {
"comment": "(1 / 18)",
"exp": {
"left": 1.0,
"op": "/",
"right": 18.0
}
}
},
{
"action": "loop14a",
"destinations": [
{
"assignments": [
{
"comment": "s14 <- 0",
"ref": "s14",
"value": 0
}
],
"location": "l",
"probability": {
"comment": "(1 / 1)",
"exp": 1
}
}
],
"guard": {
"comment": "(s14 = 0)",
"exp": {
"left": "s14",
"op": "=",
"right": 0
}
},
"location": "l",
"rate": {
"comment": "1",
"exp": 1
}
},
{
"action": "loop14b",
"destinations": [
{
"assignments": [
{
"comment": "s14 <- 1",
"ref": "s14",
"value": 1
}
],
"location": "l",
"probability": {
"comment": "(1 / 1)",
"exp": 1
}
}
],
"guard": {
"comment": "(s14 = 1)",
"exp": {
"left": "s14",
"op": "=",
"right": 1
}
},
"location": "l",
"rate": {
"comment": "1",
"exp": 1
}
},
{
"action": "serve14",
"destinations": [
{
"assignments": [
{
"comment": "s14 <- 0",
"ref": "s14",
"value": 0
}
],
"location": "l",
"probability": {
"comment": "(1 / 1)",
"exp": 1
}
}
],
"guard": {
"comment": "(s14 = 1)",
"exp": {
"left": "s14",
"op": "=",
"right": 1
}
},
"location": "l",
"rate": {
"comment": "1",
"exp": 1
}
}
],
"initial-locations": [
"l"
],
"locations": [
{
"name": "l"
}
],
"name": "station14",
"variables": [
{
"initial-value": 0,
"name": "s14",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 1
}
}
]
},
{
"edges": [
{
"destinations": [
{
"assignments": [
{
"comment": "s15 <- 1",
"ref": "s15",
"value": 1
}
],
"location": "l",
"probability": {
"comment": "((1 / 18) / (1 / 18))",
"exp": 1.0
}
}
],
"guard": {
"comment": "(s15 = 0)",
"exp": {
"left": "s15",
"op": "=",
"right": 0
}
},
"location": "l",
"rate": {
"comment": "(1 / 18)",
"exp": {
"left": 1.0,
"op": "/",
"right": 18.0
}
}
},
{
"action": "loop15a",
"destinations": [
{
"assignments": [
{
"comment": "s15 <- 0",
"ref": "s15",
"value": 0
}
],
"location": "l",
"probability": {
"comment": "(1 / 1)",
"exp": 1
}
}
],
"guard": {
"comment": "(s15 = 0)",
"exp": {
"left": "s15",
"op": "=",
"right": 0
}
},
"location": "l",
"rate": {
"comment": "1",
"exp": 1
}
},
{
"action": "loop15b",
"destinations": [
{
"assignments": [
{
"comment": "s15 <- 1",
"ref": "s15",
"value": 1
}
],
"location": "l",
"probability": {
"comment": "(1 / 1)",
"exp": 1
}
}
],
"guard": {
"comment": "(s15 = 1)",
"exp": {
"left": "s15",
"op": "=",
"right": 1
}
},
"location": "l",
"rate": {
"comment": "1",
"exp": 1
}
},
{
"action": "serve15",
"destinations": [
{
"assignments": [
{
"comment": "s15 <- 0",
"ref": "s15",
"value": 0
}
],
"location": "l",
"probability": {
"comment": "(1 / 1)",
"exp": 1
}
}
],
"guard": {
"comment": "(s15 = 1)",
"exp": {
"left": "s15",
"op": "=",
"right": 1
}
},
"location": "l",
"rate": {
"comment": "1",
"exp": 1
}
}
],
"initial-locations": [
"l"
],
"locations": [
{
"name": "l"
}
],
"name": "station15",
"variables": [
{
"initial-value": 0,
"name": "s15",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 1
}
}
]
},
{
"edges": [
{
"destinations": [
{
"assignments": [
{
"comment": "s16 <- 1",
"ref": "s16",
"value": 1
}
],
"location": "l",
"probability": {
"comment": "((1 / 18) / (1 / 18))",
"exp": 1.0
}
}
],
"guard": {
"comment": "(s16 = 0)",
"exp": {
"left": "s16",
"op": "=",
"right": 0
}
},
"location": "l",
"rate": {
"comment": "(1 / 18)",
"exp": {
"left": 1.0,
"op": "/",
"right": 18.0
}
}
},
{
"action": "loop16a",
"destinations": [
{
"assignments": [
{
"comment": "s16 <- 0",
"ref": "s16",
"value": 0
}
],
"location": "l",
"probability": {
"comment": "(1 / 1)",
"exp": 1
}
}
],
"guard": {
"comment": "(s16 = 0)",
"exp": {
"left": "s16",
"op": "=",
"right": 0
}
},
"location": "l",
"rate": {
"comment": "1",
"exp": 1
}
},
{
"action": "loop16b",
"destinations": [
{
"assignments": [
{
"comment": "s16 <- 1",
"ref": "s16",
"value": 1
}
],
"location": "l",
"probability": {
"comment": "(1 / 1)",
"exp": 1
}
}
],
"guard": {
"comment": "(s16 = 1)",
"exp": {
"left": "s16",
"op": "=",
"right": 1
}
},
"location": "l",
"rate": {
"comment": "1",
"exp": 1
}
},
{
"action": "serve16",
"destinations": [
{
"assignments": [
{
"comment": "s16 <- 0",
"ref": "s16",
"value": 0
}
],
"location": "l",
"probability": {
"comment": "(1 / 1)",
"exp": 1
}
}
],
"guard": {
"comment": "(s16 = 1)",
"exp": {
"left": "s16",
"op": "=",
"right": 1
}
},
"location": "l",
"rate": {
"comment": "1",
"exp": 1
}
}
],
"initial-locations": [
"l"
],
"locations": [
{
"name": "l"
}
],
"name": "station16",
"variables": [
{
"initial-value": 0,
"name": "s16",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 1
}
}
]
},
{
"edges": [
{
"destinations": [
{
"assignments": [
{
"comment": "s17 <- 1",
"ref": "s17",
"value": 1
}
],
"location": "l",
"probability": {
"comment": "((1 / 18) / (1 / 18))",
"exp": 1.0
}
}
],
"guard": {
"comment": "(s17 = 0)",
"exp": {
"left": "s17",
"op": "=",
"right": 0
}
},
"location": "l",
"rate": {
"comment": "(1 / 18)",
"exp": {
"left": 1.0,
"op": "/",
"right": 18.0
}
}
},
{
"action": "loop17a",
"destinations": [
{
"assignments": [
{
"comment": "s17 <- 0",
"ref": "s17",
"value": 0
}
],
"location": "l",
"probability": {
"comment": "(1 / 1)",
"exp": 1
}
}
],
"guard": {
"comment": "(s17 = 0)",
"exp": {
"left": "s17",
"op": "=",
"right": 0
}
},
"location": "l",
"rate": {
"comment": "1",
"exp": 1
}
},
{
"action": "loop17b",
"destinations": [
{
"assignments": [
{
"comment": "s17 <- 1",
"ref": "s17",
"value": 1
}
],
"location": "l",
"probability": {
"comment": "(1 / 1)",
"exp": 1
}
}
],
"guard": {
"comment": "(s17 = 1)",
"exp": {
"left": "s17",
"op": "=",
"right": 1
}
},
"location": "l",
"rate": {
"comment": "1",
"exp": 1
}
},
{
"action": "serve17",
"destinations": [
{
"assignments": [
{
"comment": "s17 <- 0",
"ref": "s17",
"value": 0
}
],
"location": "l",
"probability": {
"comment": "(1 / 1)",
"exp": 1
}
}
],
"guard": {
"comment": "(s17 = 1)",
"exp": {
"left": "s17",
"op": "=",
"right": 1
}
},
"location": "l",
"rate": {
"comment": "1",
"exp": 1
}
}
],
"initial-locations": [
"l"
],
"locations": [
{
"name": "l"
}
],
"name": "station17",
"variables": [
{
"initial-value": 0,
"name": "s17",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 1
}
}
]
},
{
"edges": [
{
"destinations": [
{
"assignments": [
{
"comment": "s18 <- 1",
"ref": "s18",
"value": 1
}
],
"location": "l",
"probability": {
"comment": "((1 / 18) / (1 / 18))",
"exp": 1.0
}
}
],
"guard": {
"comment": "(s18 = 0)",
"exp": {
"left": "s18",
"op": "=",
"right": 0
}
},
"location": "l",
"rate": {
"comment": "(1 / 18)",
"exp": {
"left": 1.0,
"op": "/",
"right": 18.0
}
}
},
{
"action": "loop18a",
"destinations": [
{
"assignments": [
{
"comment": "s18 <- 0",
"ref": "s18",
"value": 0
}
],
"location": "l",
"probability": {
"comment": "(1 / 1)",
"exp": 1
}
}
],
"guard": {
"comment": "(s18 = 0)",
"exp": {
"left": "s18",
"op": "=",
"right": 0
}
},
"location": "l",
"rate": {
"comment": "1",
"exp": 1
}
},
{
"action": "loop18b",
"destinations": [
{
"assignments": [
{
"comment": "s18 <- 1",
"ref": "s18",
"value": 1
}
],
"location": "l",
"probability": {
"comment": "(1 / 1)",
"exp": 1
}
}
],
"guard": {
"comment": "(s18 = 1)",
"exp": {
"left": "s18",
"op": "=",
"right": 1
}
},
"location": "l",
"rate": {
"comment": "1",
"exp": 1
}
},
{
"action": "serve18",
"destinations": [
{
"assignments": [
{
"comment": "s18 <- 0",
"ref": "s18",
"value": 0
}
],
"location": "l",
"probability": {
"comment": "(1 / 1)",
"exp": 1
}
}
],
"guard": {
"comment": "(s18 = 1)",
"exp": {
"left": "s18",
"op": "=",
"right": 1
}
},
"location": "l",
"rate": {
"comment": "1",
"exp": 1
}
}
],
"initial-locations": [
"l"
],
"locations": [
{
"name": "l"
}
],
"name": "station18",
"variables": [
{
"initial-value": 0,
"name": "s18",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 1
}
}
]
}
],
"constants": [
{
"name": "N",
"type": "int",
"value": 18
},
{
"name": "T",
"type": "real",
"value": 16
},
{
"name": "mu",
"type": "real",
"value": 1
},
{
"name": "gamma",
"type": "real",
"value": 200
},
{
"name": "lambda",
"type": "real",
"value": {
"left": 1.0,
"op": "/",
"right": 18.0
}
}
],
"features": [
"derived-operators"
],
"jani-version": 1,
"name": "model",
"properties": [
{
"expression": {
"fun": "values",
"op": "filter",
"states": {
"op": "initial"
},
"values": {
"exp": {
"left": {
"exp": "serve_s2",
"op": "¬"
},
"op": "U",
"right": "serve_s1"
},
"op": "Pmin"
}
},
"name": "s1_before_s2"
}
],
"restrict-initial": {
"exp": true
},
"system": {
"elements": [
{
"automaton": "server"
},
{
"automaton": "station1"
},
{
"automaton": "station2"
},
{
"automaton": "station3"
},
{
"automaton": "station4"
},
{
"automaton": "station5"
},
{
"automaton": "station6"
},
{
"automaton": "station7"
},
{
"automaton": "station8"
},
{
"automaton": "station9"
},
{
"automaton": "station10"
},
{
"automaton": "station11"
},
{
"automaton": "station12"
},
{
"automaton": "station13"
},
{
"automaton": "station14"
},
{
"automaton": "station15"
},
{
"automaton": "station16"
},
{
"automaton": "station17"
},
{
"automaton": "station18"
}
],
"syncs": [
{
"result": "loop10a",
"synchronise": [
"loop10a",
null,
null,
null,
null,
null,
null,
null,
null,
null,
"loop10a",
null,
null,
null,
null,
null,
null,
null,
null
]
},
{
"result": "loop10b",
"synchronise": [
"loop10b",
null,
null,
null,
null,
null,
null,
null,
null,
null,
"loop10b",
null,
null,
null,
null,
null,
null,
null,
null
]
},
{
"result": "loop11a",
"synchronise": [
"loop11a",
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
"loop11a",
null,
null,
null,
null,
null,
null,
null
]
},
{
"result": "loop11b",
"synchronise": [
"loop11b",
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
"loop11b",
null,
null,
null,
null,
null,
null,
null
]
},
{
"result": "loop12a",
"synchronise": [
"loop12a",
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
"loop12a",
null,
null,
null,
null,
null,
null
]
},
{
"result": "loop12b",
"synchronise": [
"loop12b",
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
"loop12b",
null,
null,
null,
null,
null,
null
]
},
{
"result": "loop13a",
"synchronise": [
"loop13a",
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
"loop13a",
null,
null,
null,
null,
null
]
},
{
"result": "loop13b",
"synchronise": [
"loop13b",
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
"loop13b",
null,
null,
null,
null,
null
]
},
{
"result": "loop14a",
"synchronise": [
"loop14a",
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
"loop14a",
null,
null,
null,
null
]
},
{
"result": "loop14b",
"synchronise": [
"loop14b",
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
"loop14b",
null,
null,
null,
null
]
},
{
"result": "loop15a",
"synchronise": [
"loop15a",
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
"loop15a",
null,
null,
null
]
},
{
"result": "loop15b",
"synchronise": [
"loop15b",
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
"loop15b",
null,
null,
null
]
},
{
"result": "loop16a",
"synchronise": [
"loop16a",
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
"loop16a",
null,
null
]
},
{
"result": "loop16b",
"synchronise": [
"loop16b",
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
"loop16b",
null,
null
]
},
{
"result": "loop17a",
"synchronise": [
"loop17a",
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
"loop17a",
null
]
},
{
"result": "loop17b",
"synchronise": [
"loop17b",
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
"loop17b",
null
]
},
{
"result": "loop18a",
"synchronise": [
"loop18a",
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
"loop18a"
]
},
{
"result": "loop18b",
"synchronise": [
"loop18b",
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
"loop18b"
]
},
{
"result": "loop1a",
"synchronise": [
"loop1a",
"loop1a",
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null
]
},
{
"result": "loop1b",
"synchronise": [
"loop1b",
"loop1b",
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null
]
},
{
"result": "loop2a",
"synchronise": [
"loop2a",
null,
"loop2a",
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null
]
},
{
"result": "loop2b",
"synchronise": [
"loop2b",
null,
"loop2b",
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null
]
},
{
"result": "loop3a",
"synchronise": [
"loop3a",
null,
null,
"loop3a",
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null
]
},
{
"result": "loop3b",
"synchronise": [
"loop3b",
null,
null,
"loop3b",
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null
]
},
{
"result": "loop4a",
"synchronise": [
"loop4a",
null,
null,
null,
"loop4a",
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null
]
},
{
"result": "loop4b",
"synchronise": [
"loop4b",
null,
null,
null,
"loop4b",
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null
]
},
{
"result": "loop5a",
"synchronise": [
"loop5a",
null,
null,
null,
null,
"loop5a",
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null
]
},
{
"result": "loop5b",
"synchronise": [
"loop5b",
null,
null,
null,
null,
"loop5b",
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null
]
},
{
"result": "loop6a",
"synchronise": [
"loop6a",
null,
null,
null,
null,
null,
"loop6a",
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null
]
},
{
"result": "loop6b",
"synchronise": [
"loop6b",
null,
null,
null,
null,
null,
"loop6b",
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null
]
},
{
"result": "loop7a",
"synchronise": [
"loop7a",
null,
null,
null,
null,
null,
null,
"loop7a",
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null
]
},
{
"result": "loop7b",
"synchronise": [
"loop7b",
null,
null,
null,
null,
null,
null,
"loop7b",
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null
]
},
{
"result": "loop8a",
"synchronise": [
"loop8a",
null,
null,
null,
null,
null,
null,
null,
"loop8a",
null,
null,
null,
null,
null,
null,
null,
null,
null,
null
]
},
{
"result": "loop8b",
"synchronise": [
"loop8b",
null,
null,
null,
null,
null,
null,
null,
"loop8b",
null,
null,
null,
null,
null,
null,
null,
null,
null,
null
]
},
{
"result": "loop9a",
"synchronise": [
"loop9a",
null,
null,
null,
null,
null,
null,
null,
null,
"loop9a",
null,
null,
null,
null,
null,
null,
null,
null,
null
]
},
{
"result": "loop9b",
"synchronise": [
"loop9b",
null,
null,
null,
null,
null,
null,
null,
null,
"loop9b",
null,
null,
null,
null,
null,
null,
null,
null,
null
]
},
{
"result": "serve1",
"synchronise": [
"serve1",
"serve1",
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null
]
},
{
"result": "serve10",
"synchronise": [
"serve10",
null,
null,
null,
null,
null,
null,
null,
null,
null,
"serve10",
null,
null,
null,
null,
null,
null,
null,
null
]
},
{
"result": "serve11",
"synchronise": [
"serve11",
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
"serve11",
null,
null,
null,
null,
null,
null,
null
]
},
{
"result": "serve12",
"synchronise": [
"serve12",
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
"serve12",
null,
null,
null,
null,
null,
null
]
},
{
"result": "serve13",
"synchronise": [
"serve13",
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
"serve13",
null,
null,
null,
null,
null
]
},
{
"result": "serve14",
"synchronise": [
"serve14",
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
"serve14",
null,
null,
null,
null
]
},
{
"result": "serve15",
"synchronise": [
"serve15",
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
"serve15",
null,
null,
null
]
},
{
"result": "serve16",
"synchronise": [
"serve16",
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
"serve16",
null,
null
]
},
{
"result": "serve17",
"synchronise": [
"serve17",
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
"serve17",
null
]
},
{
"result": "serve18",
"synchronise": [
"serve18",
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
"serve18"
]
},
{
"result": "serve2",
"synchronise": [
"serve2",
null,
"serve2",
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null
]
},
{
"result": "serve3",
"synchronise": [
"serve3",
null,
null,
"serve3",
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null
]
},
{
"result": "serve4",
"synchronise": [
"serve4",
null,
null,
null,
"serve4",
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null
]
},
{
"result": "serve5",
"synchronise": [
"serve5",
null,
null,
null,
null,
"serve5",
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null
]
},
{
"result": "serve6",
"synchronise": [
"serve6",
null,
null,
null,
null,
null,
"serve6",
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null
]
},
{
"result": "serve7",
"synchronise": [
"serve7",
null,
null,
null,
null,
null,
null,
"serve7",
null,
null,
null,
null,
null,
null,
null,
null,
null,
null,
null
]
},
{
"result": "serve8",
"synchronise": [
"serve8",
null,
null,
null,
null,
null,
null,
null,
"serve8",
null,
null,
null,
null,
null,
null,
null,
null,
null,
null
]
},
{
"result": "serve9",
"synchronise": [
"serve9",
null,
null,
null,
null,
null,
null,
null,
null,
"serve9",
null,
null,
null,
null,
null,
null,
null,
null,
null
]
}
]
},
"type": "ctmc",
"variables": [
{
"initial-value": false,
"name": "serve_s2",
"transient": true,
"type": "bool"
},
{
"initial-value": false,
"name": "serve_s1",
"transient": true,
"type": "bool"
},
{
"initial-value": 1,
"name": "s",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 1,
"upper-bound": 18
}
},
{
"initial-value": 0,
"name": "a",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 1
}
}
]
}