model.prism (0.01 MB) property.props (0.01 MB) model.jani (0.06 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.
// herman's self stabilising algorithm [Her90] // gxn/dxp 13/07/02 // the procotol is synchronous with no nondeterminism (a DTMC) dtmc const double p = 0.5; // module for process 1 module process1 // Boolean variable for process 1 x1 : [0..1]; [step] (x1=x15) -> p : (x1'=0) + 1-p : (x1'=1); [step] !(x1=x15) -> (x1'=x15); endmodule // add further processes through renaming module process2 = process1 [ x1=x2, x15=x1 ] endmodule module process3 = process1 [ x1=x3, x15=x2 ] endmodule module process4 = process1 [ x1=x4, x15=x3 ] endmodule module process5 = process1 [ x1=x5, x15=x4 ] endmodule module process6 = process1 [ x1=x6, x15=x5 ] endmodule module process7 = process1 [ x1=x7, x15=x6 ] endmodule module process8 = process1 [ x1=x8, x15=x7 ] endmodule module process9 = process1 [ x1=x9, x15=x8 ] endmodule module process10 = process1 [ x1=x10, x15=x9 ] endmodule module process11 = process1 [ x1=x11, x15=x10 ] endmodule module process12 = process1 [ x1=x12, x15=x11 ] endmodule module process13 = process1 [ x1=x13, x15=x12 ] endmodule module process14 = process1 [ x1=x14, x15=x13 ] endmodule module process15 = process1 [ x1=x15, x15=x14 ] endmodule // cost - 1 in each state (expected number of steps) rewards "steps" true : 1; endrewards // set of initial states: all (i.e. any possible initial configuration of tokens) init true endinit // formula, for use in properties: number of tokens // (i.e. number of processes that have the same value as the process to their left) formula num_tokens = (x1=x2?1:0)+(x2=x3?1:0)+(x3=x4?1:0)+(x4=x5?1:0)+(x5=x6?1:0)+(x6=x7?1:0)+(x7=x8?1:0)+(x8=x9?1:0)+(x9=x10?1:0)+(x10=x11?1:0)+(x11=x12?1:0)+(x12=x13?1:0)+(x13=x14?1:0)+(x14=x15?1:0)+(x15=x1?1:0); // label - stable configurations (1 token) label "stable" = num_tokens=1;
// Expected number of steps until termination "steps": filter(max, R=? [ F "stable" ], "init");
{
"actions": [
{
"name": "step"
}
],
"automata": [
{
"edges": [
{
"action": "step",
"destinations": [
{
"assignments": [
{
"comment": "x1 <- 0",
"ref": "x1",
"value": 0
}
],
"location": "l",
"probability": {
"comment": "1/2",
"exp": 0.5
}
},
{
"assignments": [
{
"comment": "x1 <- 1",
"ref": "x1",
"value": 1
}
],
"location": "l",
"probability": {
"comment": "(1 - 1/2)",
"exp": 0.5
}
}
],
"guard": {
"comment": "(x1 = x15)",
"exp": {
"left": "x1",
"op": "=",
"right": "x15"
}
},
"location": "l"
},
{
"action": "step",
"destinations": [
{
"assignments": [
{
"comment": "x1 <- x15",
"ref": "x1",
"value": "x15"
}
],
"location": "l"
}
],
"guard": {
"comment": "!((x1 = x15))",
"exp": {
"exp": {
"left": "x1",
"op": "=",
"right": "x15"
},
"op": "¬"
}
},
"location": "l"
}
],
"initial-locations": [
"l"
],
"locations": [
{
"name": "l",
"transient-values": [
{
"comment": "stable <- (num_tokens(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15) = 1)",
"ref": "stable",
"value": {
"left": {
"args": [
"x1",
"x2",
"x3",
"x4",
"x5",
"x6",
"x7",
"x8",
"x9",
"x10",
"x11",
"x12",
"x13",
"x14",
"x15"
],
"function": "num_tokens",
"op": "call"
},
"op": "=",
"right": 1
}
},
{
"comment": "steps <- 1",
"ref": "steps",
"value": 1
}
]
}
],
"name": "process1",
"variables": []
},
{
"edges": [
{
"action": "step",
"destinations": [
{
"assignments": [
{
"comment": "x2 <- 0",
"ref": "x2",
"value": 0
}
],
"location": "l",
"probability": {
"comment": "1/2",
"exp": 0.5
}
},
{
"assignments": [
{
"comment": "x2 <- 1",
"ref": "x2",
"value": 1
}
],
"location": "l",
"probability": {
"comment": "(1 - 1/2)",
"exp": 0.5
}
}
],
"guard": {
"comment": "(x2 = x1)",
"exp": {
"left": "x2",
"op": "=",
"right": "x1"
}
},
"location": "l"
},
{
"action": "step",
"destinations": [
{
"assignments": [
{
"comment": "x2 <- x1",
"ref": "x2",
"value": "x1"
}
],
"location": "l"
}
],
"guard": {
"comment": "!((x2 = x1))",
"exp": {
"exp": {
"left": "x2",
"op": "=",
"right": "x1"
},
"op": "¬"
}
},
"location": "l"
}
],
"initial-locations": [
"l"
],
"locations": [
{
"name": "l"
}
],
"name": "process2",
"variables": []
},
{
"edges": [
{
"action": "step",
"destinations": [
{
"assignments": [
{
"comment": "x3 <- 0",
"ref": "x3",
"value": 0
}
],
"location": "l",
"probability": {
"comment": "1/2",
"exp": 0.5
}
},
{
"assignments": [
{
"comment": "x3 <- 1",
"ref": "x3",
"value": 1
}
],
"location": "l",
"probability": {
"comment": "(1 - 1/2)",
"exp": 0.5
}
}
],
"guard": {
"comment": "(x3 = x2)",
"exp": {
"left": "x3",
"op": "=",
"right": "x2"
}
},
"location": "l"
},
{
"action": "step",
"destinations": [
{
"assignments": [
{
"comment": "x3 <- x2",
"ref": "x3",
"value": "x2"
}
],
"location": "l"
}
],
"guard": {
"comment": "!((x3 = x2))",
"exp": {
"exp": {
"left": "x3",
"op": "=",
"right": "x2"
},
"op": "¬"
}
},
"location": "l"
}
],
"initial-locations": [
"l"
],
"locations": [
{
"name": "l"
}
],
"name": "process3",
"variables": []
},
{
"edges": [
{
"action": "step",
"destinations": [
{
"assignments": [
{
"comment": "x4 <- 0",
"ref": "x4",
"value": 0
}
],
"location": "l",
"probability": {
"comment": "1/2",
"exp": 0.5
}
},
{
"assignments": [
{
"comment": "x4 <- 1",
"ref": "x4",
"value": 1
}
],
"location": "l",
"probability": {
"comment": "(1 - 1/2)",
"exp": 0.5
}
}
],
"guard": {
"comment": "(x4 = x3)",
"exp": {
"left": "x4",
"op": "=",
"right": "x3"
}
},
"location": "l"
},
{
"action": "step",
"destinations": [
{
"assignments": [
{
"comment": "x4 <- x3",
"ref": "x4",
"value": "x3"
}
],
"location": "l"
}
],
"guard": {
"comment": "!((x4 = x3))",
"exp": {
"exp": {
"left": "x4",
"op": "=",
"right": "x3"
},
"op": "¬"
}
},
"location": "l"
}
],
"initial-locations": [
"l"
],
"locations": [
{
"name": "l"
}
],
"name": "process4",
"variables": []
},
{
"edges": [
{
"action": "step",
"destinations": [
{
"assignments": [
{
"comment": "x5 <- 0",
"ref": "x5",
"value": 0
}
],
"location": "l",
"probability": {
"comment": "1/2",
"exp": 0.5
}
},
{
"assignments": [
{
"comment": "x5 <- 1",
"ref": "x5",
"value": 1
}
],
"location": "l",
"probability": {
"comment": "(1 - 1/2)",
"exp": 0.5
}
}
],
"guard": {
"comment": "(x5 = x4)",
"exp": {
"left": "x5",
"op": "=",
"right": "x4"
}
},
"location": "l"
},
{
"action": "step",
"destinations": [
{
"assignments": [
{
"comment": "x5 <- x4",
"ref": "x5",
"value": "x4"
}
],
"location": "l"
}
],
"guard": {
"comment": "!((x5 = x4))",
"exp": {
"exp": {
"left": "x5",
"op": "=",
"right": "x4"
},
"op": "¬"
}
},
"location": "l"
}
],
"initial-locations": [
"l"
],
"locations": [
{
"name": "l"
}
],
"name": "process5",
"variables": []
},
{
"edges": [
{
"action": "step",
"destinations": [
{
"assignments": [
{
"comment": "x6 <- 0",
"ref": "x6",
"value": 0
}
],
"location": "l",
"probability": {
"comment": "1/2",
"exp": 0.5
}
},
{
"assignments": [
{
"comment": "x6 <- 1",
"ref": "x6",
"value": 1
}
],
"location": "l",
"probability": {
"comment": "(1 - 1/2)",
"exp": 0.5
}
}
],
"guard": {
"comment": "(x6 = x5)",
"exp": {
"left": "x6",
"op": "=",
"right": "x5"
}
},
"location": "l"
},
{
"action": "step",
"destinations": [
{
"assignments": [
{
"comment": "x6 <- x5",
"ref": "x6",
"value": "x5"
}
],
"location": "l"
}
],
"guard": {
"comment": "!((x6 = x5))",
"exp": {
"exp": {
"left": "x6",
"op": "=",
"right": "x5"
},
"op": "¬"
}
},
"location": "l"
}
],
"initial-locations": [
"l"
],
"locations": [
{
"name": "l"
}
],
"name": "process6",
"variables": []
},
{
"edges": [
{
"action": "step",
"destinations": [
{
"assignments": [
{
"comment": "x7 <- 0",
"ref": "x7",
"value": 0
}
],
"location": "l",
"probability": {
"comment": "1/2",
"exp": 0.5
}
},
{
"assignments": [
{
"comment": "x7 <- 1",
"ref": "x7",
"value": 1
}
],
"location": "l",
"probability": {
"comment": "(1 - 1/2)",
"exp": 0.5
}
}
],
"guard": {
"comment": "(x7 = x6)",
"exp": {
"left": "x7",
"op": "=",
"right": "x6"
}
},
"location": "l"
},
{
"action": "step",
"destinations": [
{
"assignments": [
{
"comment": "x7 <- x6",
"ref": "x7",
"value": "x6"
}
],
"location": "l"
}
],
"guard": {
"comment": "!((x7 = x6))",
"exp": {
"exp": {
"left": "x7",
"op": "=",
"right": "x6"
},
"op": "¬"
}
},
"location": "l"
}
],
"initial-locations": [
"l"
],
"locations": [
{
"name": "l"
}
],
"name": "process7",
"variables": []
},
{
"edges": [
{
"action": "step",
"destinations": [
{
"assignments": [
{
"comment": "x8 <- 0",
"ref": "x8",
"value": 0
}
],
"location": "l",
"probability": {
"comment": "1/2",
"exp": 0.5
}
},
{
"assignments": [
{
"comment": "x8 <- 1",
"ref": "x8",
"value": 1
}
],
"location": "l",
"probability": {
"comment": "(1 - 1/2)",
"exp": 0.5
}
}
],
"guard": {
"comment": "(x8 = x7)",
"exp": {
"left": "x8",
"op": "=",
"right": "x7"
}
},
"location": "l"
},
{
"action": "step",
"destinations": [
{
"assignments": [
{
"comment": "x8 <- x7",
"ref": "x8",
"value": "x7"
}
],
"location": "l"
}
],
"guard": {
"comment": "!((x8 = x7))",
"exp": {
"exp": {
"left": "x8",
"op": "=",
"right": "x7"
},
"op": "¬"
}
},
"location": "l"
}
],
"initial-locations": [
"l"
],
"locations": [
{
"name": "l"
}
],
"name": "process8",
"variables": []
},
{
"edges": [
{
"action": "step",
"destinations": [
{
"assignments": [
{
"comment": "x9 <- 0",
"ref": "x9",
"value": 0
}
],
"location": "l",
"probability": {
"comment": "1/2",
"exp": 0.5
}
},
{
"assignments": [
{
"comment": "x9 <- 1",
"ref": "x9",
"value": 1
}
],
"location": "l",
"probability": {
"comment": "(1 - 1/2)",
"exp": 0.5
}
}
],
"guard": {
"comment": "(x9 = x8)",
"exp": {
"left": "x9",
"op": "=",
"right": "x8"
}
},
"location": "l"
},
{
"action": "step",
"destinations": [
{
"assignments": [
{
"comment": "x9 <- x8",
"ref": "x9",
"value": "x8"
}
],
"location": "l"
}
],
"guard": {
"comment": "!((x9 = x8))",
"exp": {
"exp": {
"left": "x9",
"op": "=",
"right": "x8"
},
"op": "¬"
}
},
"location": "l"
}
],
"initial-locations": [
"l"
],
"locations": [
{
"name": "l"
}
],
"name": "process9",
"variables": []
},
{
"edges": [
{
"action": "step",
"destinations": [
{
"assignments": [
{
"comment": "x10 <- 0",
"ref": "x10",
"value": 0
}
],
"location": "l",
"probability": {
"comment": "1/2",
"exp": 0.5
}
},
{
"assignments": [
{
"comment": "x10 <- 1",
"ref": "x10",
"value": 1
}
],
"location": "l",
"probability": {
"comment": "(1 - 1/2)",
"exp": 0.5
}
}
],
"guard": {
"comment": "(x10 = x9)",
"exp": {
"left": "x10",
"op": "=",
"right": "x9"
}
},
"location": "l"
},
{
"action": "step",
"destinations": [
{
"assignments": [
{
"comment": "x10 <- x9",
"ref": "x10",
"value": "x9"
}
],
"location": "l"
}
],
"guard": {
"comment": "!((x10 = x9))",
"exp": {
"exp": {
"left": "x10",
"op": "=",
"right": "x9"
},
"op": "¬"
}
},
"location": "l"
}
],
"initial-locations": [
"l"
],
"locations": [
{
"name": "l"
}
],
"name": "process10",
"variables": []
},
{
"edges": [
{
"action": "step",
"destinations": [
{
"assignments": [
{
"comment": "x11 <- 0",
"ref": "x11",
"value": 0
}
],
"location": "l",
"probability": {
"comment": "1/2",
"exp": 0.5
}
},
{
"assignments": [
{
"comment": "x11 <- 1",
"ref": "x11",
"value": 1
}
],
"location": "l",
"probability": {
"comment": "(1 - 1/2)",
"exp": 0.5
}
}
],
"guard": {
"comment": "(x11 = x10)",
"exp": {
"left": "x11",
"op": "=",
"right": "x10"
}
},
"location": "l"
},
{
"action": "step",
"destinations": [
{
"assignments": [
{
"comment": "x11 <- x10",
"ref": "x11",
"value": "x10"
}
],
"location": "l"
}
],
"guard": {
"comment": "!((x11 = x10))",
"exp": {
"exp": {
"left": "x11",
"op": "=",
"right": "x10"
},
"op": "¬"
}
},
"location": "l"
}
],
"initial-locations": [
"l"
],
"locations": [
{
"name": "l"
}
],
"name": "process11",
"variables": []
},
{
"edges": [
{
"action": "step",
"destinations": [
{
"assignments": [
{
"comment": "x12 <- 0",
"ref": "x12",
"value": 0
}
],
"location": "l",
"probability": {
"comment": "1/2",
"exp": 0.5
}
},
{
"assignments": [
{
"comment": "x12 <- 1",
"ref": "x12",
"value": 1
}
],
"location": "l",
"probability": {
"comment": "(1 - 1/2)",
"exp": 0.5
}
}
],
"guard": {
"comment": "(x12 = x11)",
"exp": {
"left": "x12",
"op": "=",
"right": "x11"
}
},
"location": "l"
},
{
"action": "step",
"destinations": [
{
"assignments": [
{
"comment": "x12 <- x11",
"ref": "x12",
"value": "x11"
}
],
"location": "l"
}
],
"guard": {
"comment": "!((x12 = x11))",
"exp": {
"exp": {
"left": "x12",
"op": "=",
"right": "x11"
},
"op": "¬"
}
},
"location": "l"
}
],
"initial-locations": [
"l"
],
"locations": [
{
"name": "l"
}
],
"name": "process12",
"variables": []
},
{
"edges": [
{
"action": "step",
"destinations": [
{
"assignments": [
{
"comment": "x13 <- 0",
"ref": "x13",
"value": 0
}
],
"location": "l",
"probability": {
"comment": "1/2",
"exp": 0.5
}
},
{
"assignments": [
{
"comment": "x13 <- 1",
"ref": "x13",
"value": 1
}
],
"location": "l",
"probability": {
"comment": "(1 - 1/2)",
"exp": 0.5
}
}
],
"guard": {
"comment": "(x13 = x12)",
"exp": {
"left": "x13",
"op": "=",
"right": "x12"
}
},
"location": "l"
},
{
"action": "step",
"destinations": [
{
"assignments": [
{
"comment": "x13 <- x12",
"ref": "x13",
"value": "x12"
}
],
"location": "l"
}
],
"guard": {
"comment": "!((x13 = x12))",
"exp": {
"exp": {
"left": "x13",
"op": "=",
"right": "x12"
},
"op": "¬"
}
},
"location": "l"
}
],
"initial-locations": [
"l"
],
"locations": [
{
"name": "l"
}
],
"name": "process13",
"variables": []
},
{
"edges": [
{
"action": "step",
"destinations": [
{
"assignments": [
{
"comment": "x14 <- 0",
"ref": "x14",
"value": 0
}
],
"location": "l",
"probability": {
"comment": "1/2",
"exp": 0.5
}
},
{
"assignments": [
{
"comment": "x14 <- 1",
"ref": "x14",
"value": 1
}
],
"location": "l",
"probability": {
"comment": "(1 - 1/2)",
"exp": 0.5
}
}
],
"guard": {
"comment": "(x14 = x13)",
"exp": {
"left": "x14",
"op": "=",
"right": "x13"
}
},
"location": "l"
},
{
"action": "step",
"destinations": [
{
"assignments": [
{
"comment": "x14 <- x13",
"ref": "x14",
"value": "x13"
}
],
"location": "l"
}
],
"guard": {
"comment": "!((x14 = x13))",
"exp": {
"exp": {
"left": "x14",
"op": "=",
"right": "x13"
},
"op": "¬"
}
},
"location": "l"
}
],
"initial-locations": [
"l"
],
"locations": [
{
"name": "l"
}
],
"name": "process14",
"variables": []
},
{
"edges": [
{
"action": "step",
"destinations": [
{
"assignments": [
{
"comment": "x15 <- 0",
"ref": "x15",
"value": 0
}
],
"location": "l",
"probability": {
"comment": "1/2",
"exp": 0.5
}
},
{
"assignments": [
{
"comment": "x15 <- 1",
"ref": "x15",
"value": 1
}
],
"location": "l",
"probability": {
"comment": "(1 - 1/2)",
"exp": 0.5
}
}
],
"guard": {
"comment": "(x15 = x14)",
"exp": {
"left": "x15",
"op": "=",
"right": "x14"
}
},
"location": "l"
},
{
"action": "step",
"destinations": [
{
"assignments": [
{
"comment": "x15 <- x14",
"ref": "x15",
"value": "x14"
}
],
"location": "l"
}
],
"guard": {
"comment": "!((x15 = x14))",
"exp": {
"exp": {
"left": "x15",
"op": "=",
"right": "x14"
},
"op": "¬"
}
},
"location": "l"
}
],
"initial-locations": [
"l"
],
"locations": [
{
"name": "l"
}
],
"name": "process15",
"variables": []
}
],
"constants": [
{
"name": "p",
"type": "real",
"value": 0.5
}
],
"features": [
"derived-operators",
"functions",
"state-exit-rewards"
],
"functions": [
{
"body": {
"left": {
"left": {
"left": {
"left": {
"else": 0,
"if": {
"left": "num_tokens__param__x15",
"op": "=",
"right": "num_tokens__param__x1"
},
"op": "ite",
"then": 1
},
"op": "+",
"right": {
"else": 0,
"if": {
"left": "num_tokens__param__x2",
"op": "=",
"right": "num_tokens__param__x3"
},
"op": "ite",
"then": 1
}
},
"op": "+",
"right": {
"else": 0,
"if": {
"left": "num_tokens__param__x8",
"op": "=",
"right": "num_tokens__param__x9"
},
"op": "ite",
"then": 1
}
},
"op": "+",
"right": {
"left": {
"left": {
"else": 0,
"if": {
"left": "num_tokens__param__x12",
"op": "=",
"right": "num_tokens__param__x13"
},
"op": "ite",
"then": 1
},
"op": "+",
"right": {
"else": 0,
"if": {
"left": "num_tokens__param__x4",
"op": "=",
"right": "num_tokens__param__x5"
},
"op": "ite",
"then": 1
}
},
"op": "+",
"right": {
"left": {
"else": 0,
"if": {
"left": "num_tokens__param__x11",
"op": "=",
"right": "num_tokens__param__x12"
},
"op": "ite",
"then": 1
},
"op": "+",
"right": {
"else": 0,
"if": {
"left": "num_tokens__param__x5",
"op": "=",
"right": "num_tokens__param__x6"
},
"op": "ite",
"then": 1
}
}
}
},
"op": "+",
"right": {
"left": {
"left": {
"left": {
"else": 0,
"if": {
"left": "num_tokens__param__x14",
"op": "=",
"right": "num_tokens__param__x15"
},
"op": "ite",
"then": 1
},
"op": "+",
"right": {
"else": 0,
"if": {
"left": "num_tokens__param__x1",
"op": "=",
"right": "num_tokens__param__x2"
},
"op": "ite",
"then": 1
}
},
"op": "+",
"right": {
"left": {
"else": 0,
"if": {
"left": "num_tokens__param__x9",
"op": "=",
"right": "num_tokens__param__x10"
},
"op": "ite",
"then": 1
},
"op": "+",
"right": {
"else": 0,
"if": {
"left": "num_tokens__param__x7",
"op": "=",
"right": "num_tokens__param__x8"
},
"op": "ite",
"then": 1
}
}
},
"op": "+",
"right": {
"left": {
"left": {
"else": 0,
"if": {
"left": "num_tokens__param__x13",
"op": "=",
"right": "num_tokens__param__x14"
},
"op": "ite",
"then": 1
},
"op": "+",
"right": {
"else": 0,
"if": {
"left": "num_tokens__param__x3",
"op": "=",
"right": "num_tokens__param__x4"
},
"op": "ite",
"then": 1
}
},
"op": "+",
"right": {
"left": {
"else": 0,
"if": {
"left": "num_tokens__param__x10",
"op": "=",
"right": "num_tokens__param__x11"
},
"op": "ite",
"then": 1
},
"op": "+",
"right": {
"else": 0,
"if": {
"left": "num_tokens__param__x6",
"op": "=",
"right": "num_tokens__param__x7"
},
"op": "ite",
"then": 1
}
}
}
}
},
"name": "num_tokens",
"parameters": [
{
"name": "num_tokens__param__x1",
"type": "int"
},
{
"name": "num_tokens__param__x2",
"type": "int"
},
{
"name": "num_tokens__param__x3",
"type": "int"
},
{
"name": "num_tokens__param__x4",
"type": "int"
},
{
"name": "num_tokens__param__x5",
"type": "int"
},
{
"name": "num_tokens__param__x6",
"type": "int"
},
{
"name": "num_tokens__param__x7",
"type": "int"
},
{
"name": "num_tokens__param__x8",
"type": "int"
},
{
"name": "num_tokens__param__x9",
"type": "int"
},
{
"name": "num_tokens__param__x10",
"type": "int"
},
{
"name": "num_tokens__param__x11",
"type": "int"
},
{
"name": "num_tokens__param__x12",
"type": "int"
},
{
"name": "num_tokens__param__x13",
"type": "int"
},
{
"name": "num_tokens__param__x14",
"type": "int"
},
{
"name": "num_tokens__param__x15",
"type": "int"
}
],
"type": "int"
}
],
"jani-version": 1,
"name": "model",
"properties": [
{
"expression": {
"fun": "max",
"op": "filter",
"states": {
"op": "initial"
},
"values": {
"accumulate": [
"exit"
],
"exp": "steps",
"op": "Emin",
"reach": "stable"
}
},
"name": "steps"
}
],
"restrict-initial": {
"exp": true
},
"system": {
"elements": [
{
"automaton": "process1"
},
{
"automaton": "process2"
},
{
"automaton": "process3"
},
{
"automaton": "process4"
},
{
"automaton": "process5"
},
{
"automaton": "process6"
},
{
"automaton": "process7"
},
{
"automaton": "process8"
},
{
"automaton": "process9"
},
{
"automaton": "process10"
},
{
"automaton": "process11"
},
{
"automaton": "process12"
},
{
"automaton": "process13"
},
{
"automaton": "process14"
},
{
"automaton": "process15"
}
],
"syncs": [
{
"result": "step",
"synchronise": [
"step",
"step",
"step",
"step",
"step",
"step",
"step",
"step",
"step",
"step",
"step",
"step",
"step",
"step",
"step"
]
}
]
},
"type": "dtmc",
"variables": [
{
"initial-value": false,
"name": "stable",
"transient": true,
"type": "bool"
},
{
"initial-value": 0.0,
"name": "steps",
"transient": true,
"type": "real"
},
{
"name": "x1",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 1
}
},
{
"name": "x2",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 1
}
},
{
"name": "x3",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 1
}
},
{
"name": "x4",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 1
}
},
{
"name": "x5",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 1
}
},
{
"name": "x6",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 1
}
},
{
"name": "x7",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 1
}
},
{
"name": "x8",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 1
}
},
{
"name": "x9",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 1
}
},
{
"name": "x10",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 1
}
},
{
"name": "x11",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 1
}
},
{
"name": "x12",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 1
}
},
{
"name": "x13",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 1
}
},
{
"name": "x14",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 1
}
},
{
"name": "x15",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 1
}
}
]
}