model.prism (0.01 MB) property.props (0.01 MB) model.jani (0.01 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.
// Toy example on which standard value iteration yields wrong results // This model originates from Haddad, Monmege: Reachability in MDPs: Refining Convergence of Value Iteration dtmc const int N=100; const double p=0.7; const double q = 0.5; module main x : [0..2*N] init N; [] x=N -> p : (x'=N-1) + (1-p) : (x'=N+1); [] x>0 & xq : (x'=x-1) + (1-q) : (x'=N); [] x>N & x<2*N -> q : (x'=x+1) + (1-q) : (x'=N); [] x=0 | x=2*N -> 1 : true; endmodule label "Target" = x=0;
// Probability to reach the target state "target": P=? [F "Target"];
{
"actions": [],
"automata": [
{
"edges": [
{
"destinations": [
{
"assignments": [
{
"comment": "x <- 99",
"ref": "x",
"value": 99
}
],
"location": "l",
"probability": {
"comment": "7/10",
"exp": 0.7
}
},
{
"assignments": [
{
"comment": "x <- 101",
"ref": "x",
"value": 101
}
],
"location": "l",
"probability": {
"comment": "(1 - 7/10)",
"exp": 0.3
}
}
],
"guard": {
"comment": "(x = 100)",
"exp": {
"left": "x",
"op": "=",
"right": 100
}
},
"location": "l"
},
{
"destinations": [
{
"assignments": [
{
"comment": "x <- (x - 1)",
"ref": "x",
"value": {
"left": "x",
"op": "-",
"right": 1
}
}
],
"location": "l",
"probability": {
"comment": "1/2",
"exp": 0.5
}
},
{
"assignments": [
{
"comment": "x <- 100",
"ref": "x",
"value": 100
}
],
"location": "l",
"probability": {
"comment": "(1 - 1/2)",
"exp": 0.5
}
}
],
"guard": {
"comment": "((x > 0) & (x < 100))",
"exp": {
"left": {
"left": "x",
"op": ">",
"right": 0
},
"op": "∧",
"right": {
"left": "x",
"op": "<",
"right": 100
}
}
},
"location": "l"
},
{
"destinations": [
{
"assignments": [
{
"comment": "x <- (x + 1)",
"ref": "x",
"value": {
"left": "x",
"op": "+",
"right": 1
}
}
],
"location": "l",
"probability": {
"comment": "1/2",
"exp": 0.5
}
},
{
"assignments": [
{
"comment": "x <- 100",
"ref": "x",
"value": 100
}
],
"location": "l",
"probability": {
"comment": "(1 - 1/2)",
"exp": 0.5
}
}
],
"guard": {
"comment": "((x > 100) & (x < (2 * 100)))",
"exp": {
"left": {
"left": "x",
"op": ">",
"right": 100
},
"op": "∧",
"right": {
"left": "x",
"op": "<",
"right": 200
}
}
},
"location": "l"
},
{
"destinations": [
{
"location": "l"
}
],
"guard": {
"comment": "((x = 0) | (x = (2 * 100)))",
"exp": {
"left": {
"left": "x",
"op": "=",
"right": 0
},
"op": "∨",
"right": {
"left": "x",
"op": "=",
"right": 200
}
}
},
"location": "l"
}
],
"initial-locations": [
"l"
],
"locations": [
{
"name": "l",
"transient-values": [
{
"comment": "Target <- (x = 0)",
"ref": "Target",
"value": {
"left": "x",
"op": "=",
"right": 0
}
}
]
}
],
"name": "main",
"variables": []
}
],
"constants": [
{
"name": "N",
"type": "int",
"value": 100
},
{
"name": "p",
"type": "real",
"value": 0.7
},
{
"name": "q",
"type": "real",
"value": 0.5
}
],
"features": [
"derived-operators"
],
"jani-version": 1,
"name": "model",
"properties": [
{
"expression": {
"fun": "values",
"op": "filter",
"states": {
"op": "initial"
},
"values": {
"exp": {
"left": true,
"op": "U",
"right": "Target"
},
"op": "Pmin"
}
},
"name": "target"
}
],
"restrict-initial": {
"exp": true
},
"system": {
"elements": [
{
"automaton": "main"
}
]
},
"type": "dtmc",
"variables": [
{
"initial-value": false,
"name": "Target",
"transient": true,
"type": "bool"
},
{
"initial-value": 100,
"name": "x",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 200
}
}
]
}