model.prism (0.01 MB) property.props (0.01 MB) model.jani (0.07 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.
mdp const int WIDTH = 5; const int HEIGHT = 5; const int XINIT = 3; const int YINIT = 1; const int GOLD_TO_COLLECT=100; // Set to 0 to avoid unfolding const int GEM_TO_COLLECT=100; // Set to 0 to avoid unfolding const int B=1300; const double pAttack = 1/10; formula left_of_gold = x=2 & y=5; formula right_of_gold = x=4 & y=5; formula below_of_gold = (x=3 & y=4); formula above_of_gold = false; formula left_of_gem = (x=4 & y=4); formula right_of_gem = false; formula below_of_gem = (x=5 & y=3); formula above_of_gem = (x=5 & y=5); formula left_of_home = x=2 & y=1; formula right_of_home = x=4 & y=1; formula above_of_home = x=3 & y=2; formula below_of_home = false; formula left_of_enemy = (x=3 & y=5) | (x=2 & y=4); formula right_of_enemy = (x=5 & y=5) | (x=4 & y=4); formula above_of_enemy = x=3 & y=5; formula below_of_enemy = (x=3 & y=3) | (x=4 & y=4); module robot gold : bool init false; gem : bool init false; attacked : bool init false; x : [1..WIDTH] init XINIT; y : [1..HEIGHT] init YINIT; [right] !left_of_enemy & x(attacked'=false) & (x'=x+1) & (gold' = (gold & !left_of_home) | left_of_gold) & (gem' = (gem & !left_of_home) | left_of_gem); [left] !right_of_enemy & x>1 -> (attacked'=false) & (x'=x-1) & (gold' = (gold & !right_of_home) | right_of_gold) & (gem' = (gem & !right_of_home) | right_of_gem); [top] !below_of_enemy & y (attacked'=false) & (y'=y+1) & (gold' = (gold & !below_of_home) | below_of_gold) & (gem' = (gem & !below_of_home) | below_of_gem); [down] !above_of_enemy & y>1 -> (attacked'=false) & (y'=y-1) & (gold' = (gold & !above_of_home) | above_of_gold) & (gem' = (gem & !above_of_home) | above_of_gem); [right] left_of_enemy & x pAttack : (attacked'=true) & (x'=XINIT) & (y'=YINIT) & (gold'=false) & (gem'=false) + (1-pAttack) : (attacked'=false) & (x'=x+1) & (gold' = (gold & !left_of_home) | left_of_gold) & (gem' = (gem & !left_of_home) | left_of_gem); [left] right_of_enemy & x>1 -> pAttack : (attacked'=true) & (x'=XINIT) & (y'=YINIT) & (gold'=false) & (gem'=false) + (1-pAttack) : (attacked'=false) & (x'=x-1) & (gold' = (gold & !right_of_home) | right_of_gold) & (gem' = (gem & !right_of_home) | right_of_gem); [top] below_of_enemy & y pAttack : (attacked'=true) & (x'=XINIT) & (y'=YINIT) & (gold'=false) & (gem'=false) + (1-pAttack) : (attacked'=false) & (y'=y+1) & (gold' = (gold & !below_of_home) | below_of_gold) & (gem' = (gem & !below_of_home) | below_of_gem); [down] above_of_enemy & y>1 -> pAttack : (attacked'=true) & (x'=XINIT) & (y'=YINIT) & (gold'=false) & (gem'=false) + (1-pAttack) : (attacked'=false) & (y'=y-1) & (gold' = (gold & !above_of_home) | above_of_gold) & (gem' = (gem & !above_of_home) | above_of_gem); endmodule module goldcounter required_gold : [0..GOLD_TO_COLLECT] init GOLD_TO_COLLECT; [right] true -> (required_gold'=max(0, required_gold - (left_of_home & gold ? 1: 0))); [left] true -> (required_gold'=max(0, required_gold - (right_of_home & gold ? 1 : 0))); [top] true -> (required_gold'=max(0, required_gold - (below_of_home & gold ? 1 : 0))); [down] true -> (required_gold'=max(0, required_gold - (above_of_home & gold ? 1 : 0))); endmodule module gemcounter required_gem : [0..GEM_TO_COLLECT] init GEM_TO_COLLECT; [right] true -> (required_gem'=max(0, required_gem - (left_of_home & gem ? 1: 0))); [left] true -> (required_gem'=max(0, required_gem - (right_of_home & gem ? 1 : 0))); [top] true -> (required_gem'=max(0, required_gem - (below_of_home & gem ? 1 : 0))); [down] true -> (required_gem'=max(0, required_gem - (above_of_home & gem ? 1 : 0))); endmodule label "success" = required_gold=0 & required_gem=0;
"prgoldgem": Pmax=? [F<=1300 "success"];
{
"actions": [
{
"name": "down"
},
{
"name": "left"
},
{
"name": "right"
},
{
"name": "top"
}
],
"automata": [
{
"edges": [
{
"action": "down",
"destinations": [
{
"assignments": [
{
"comment": "gold <- ((gold & !(above_of_home)) | above_of_gold)",
"ref": "gold",
"value": {
"left": {
"left": "gold",
"op": "∧",
"right": {
"exp": {
"args": [],
"function": "above_of_home",
"op": "call"
},
"op": "¬"
}
},
"op": "∨",
"right": {
"args": [],
"function": "above_of_gold",
"op": "call"
}
}
},
{
"comment": "gem <- ((gem & !(above_of_home)) | above_of_gem)",
"ref": "gem",
"value": {
"left": {
"left": "gem",
"op": "∧",
"right": {
"exp": {
"args": [],
"function": "above_of_home",
"op": "call"
},
"op": "¬"
}
},
"op": "∨",
"right": {
"args": [],
"function": "above_of_gem",
"op": "call"
}
}
},
{
"comment": "attacked <- false",
"ref": "attacked",
"value": false
},
{
"comment": "y <- (y - 1)",
"ref": "y",
"value": {
"left": "y",
"op": "-",
"right": 1
}
}
],
"location": "l"
}
],
"guard": {
"comment": "(!(above_of_enemy) & (y > 1))",
"exp": {
"left": {
"exp": {
"args": [],
"function": "above_of_enemy",
"op": "call"
},
"op": "¬"
},
"op": "∧",
"right": {
"left": "y",
"op": ">",
"right": 1
}
}
},
"location": "l"
},
{
"action": "down",
"destinations": [
{
"assignments": [
{
"comment": "gold <- false",
"ref": "gold",
"value": false
},
{
"comment": "gem <- false",
"ref": "gem",
"value": false
},
{
"comment": "attacked <- true",
"ref": "attacked",
"value": true
},
{
"comment": "x <- 3",
"ref": "x",
"value": 3
},
{
"comment": "y <- 1",
"ref": "y",
"value": 1
}
],
"location": "l",
"probability": {
"comment": "(1 / 10)",
"exp": {
"left": 1,
"op": "/",
"right": 10
}
}
},
{
"assignments": [
{
"comment": "gold <- ((gold & !(above_of_home)) | above_of_gold)",
"ref": "gold",
"value": {
"left": {
"left": "gold",
"op": "∧",
"right": {
"exp": {
"args": [],
"function": "above_of_home",
"op": "call"
},
"op": "¬"
}
},
"op": "∨",
"right": {
"args": [],
"function": "above_of_gold",
"op": "call"
}
}
},
{
"comment": "gem <- ((gem & !(above_of_home)) | above_of_gem)",
"ref": "gem",
"value": {
"left": {
"left": "gem",
"op": "∧",
"right": {
"exp": {
"args": [],
"function": "above_of_home",
"op": "call"
},
"op": "¬"
}
},
"op": "∨",
"right": {
"args": [],
"function": "above_of_gem",
"op": "call"
}
}
},
{
"comment": "attacked <- false",
"ref": "attacked",
"value": false
},
{
"comment": "y <- (y - 1)",
"ref": "y",
"value": {
"left": "y",
"op": "-",
"right": 1
}
}
],
"location": "l",
"probability": {
"comment": "(1 - (1 / 10))",
"exp": {
"left": 1,
"op": "-",
"right": {
"left": 1,
"op": "/",
"right": 10
}
}
}
}
],
"guard": {
"comment": "(above_of_enemy & (y > 1))",
"exp": {
"left": {
"args": [],
"function": "above_of_enemy",
"op": "call"
},
"op": "∧",
"right": {
"left": "y",
"op": ">",
"right": 1
}
}
},
"location": "l"
},
{
"action": "left",
"destinations": [
{
"assignments": [
{
"comment": "gold <- ((gold & !(right_of_home)) | right_of_gold)",
"ref": "gold",
"value": {
"left": {
"left": "gold",
"op": "∧",
"right": {
"exp": {
"args": [],
"function": "right_of_home",
"op": "call"
},
"op": "¬"
}
},
"op": "∨",
"right": {
"args": [],
"function": "right_of_gold",
"op": "call"
}
}
},
{
"comment": "gem <- ((gem & !(right_of_home)) | right_of_gem)",
"ref": "gem",
"value": {
"left": {
"left": "gem",
"op": "∧",
"right": {
"exp": {
"args": [],
"function": "right_of_home",
"op": "call"
},
"op": "¬"
}
},
"op": "∨",
"right": {
"args": [],
"function": "right_of_gem",
"op": "call"
}
}
},
{
"comment": "attacked <- false",
"ref": "attacked",
"value": false
},
{
"comment": "x <- (x - 1)",
"ref": "x",
"value": {
"left": "x",
"op": "-",
"right": 1
}
}
],
"location": "l"
}
],
"guard": {
"comment": "(!(right_of_enemy) & (x > 1))",
"exp": {
"left": {
"exp": {
"args": [],
"function": "right_of_enemy",
"op": "call"
},
"op": "¬"
},
"op": "∧",
"right": {
"left": "x",
"op": ">",
"right": 1
}
}
},
"location": "l"
},
{
"action": "left",
"destinations": [
{
"assignments": [
{
"comment": "gold <- false",
"ref": "gold",
"value": false
},
{
"comment": "gem <- false",
"ref": "gem",
"value": false
},
{
"comment": "attacked <- true",
"ref": "attacked",
"value": true
},
{
"comment": "x <- 3",
"ref": "x",
"value": 3
},
{
"comment": "y <- 1",
"ref": "y",
"value": 1
}
],
"location": "l",
"probability": {
"comment": "(1 / 10)",
"exp": {
"left": 1,
"op": "/",
"right": 10
}
}
},
{
"assignments": [
{
"comment": "gold <- ((gold & !(right_of_home)) | right_of_gold)",
"ref": "gold",
"value": {
"left": {
"left": "gold",
"op": "∧",
"right": {
"exp": {
"args": [],
"function": "right_of_home",
"op": "call"
},
"op": "¬"
}
},
"op": "∨",
"right": {
"args": [],
"function": "right_of_gold",
"op": "call"
}
}
},
{
"comment": "gem <- ((gem & !(right_of_home)) | right_of_gem)",
"ref": "gem",
"value": {
"left": {
"left": "gem",
"op": "∧",
"right": {
"exp": {
"args": [],
"function": "right_of_home",
"op": "call"
},
"op": "¬"
}
},
"op": "∨",
"right": {
"args": [],
"function": "right_of_gem",
"op": "call"
}
}
},
{
"comment": "attacked <- false",
"ref": "attacked",
"value": false
},
{
"comment": "x <- (x - 1)",
"ref": "x",
"value": {
"left": "x",
"op": "-",
"right": 1
}
}
],
"location": "l",
"probability": {
"comment": "(1 - (1 / 10))",
"exp": {
"left": 1,
"op": "-",
"right": {
"left": 1,
"op": "/",
"right": 10
}
}
}
}
],
"guard": {
"comment": "(right_of_enemy & (x > 1))",
"exp": {
"left": {
"args": [],
"function": "right_of_enemy",
"op": "call"
},
"op": "∧",
"right": {
"left": "x",
"op": ">",
"right": 1
}
}
},
"location": "l"
},
{
"action": "right",
"destinations": [
{
"assignments": [
{
"comment": "gold <- ((gold & !(left_of_home)) | left_of_gold)",
"ref": "gold",
"value": {
"left": {
"left": "gold",
"op": "∧",
"right": {
"exp": {
"args": [],
"function": "left_of_home",
"op": "call"
},
"op": "¬"
}
},
"op": "∨",
"right": {
"args": [],
"function": "left_of_gold",
"op": "call"
}
}
},
{
"comment": "gem <- ((gem & !(left_of_home)) | left_of_gem)",
"ref": "gem",
"value": {
"left": {
"left": "gem",
"op": "∧",
"right": {
"exp": {
"args": [],
"function": "left_of_home",
"op": "call"
},
"op": "¬"
}
},
"op": "∨",
"right": {
"args": [],
"function": "left_of_gem",
"op": "call"
}
}
},
{
"comment": "attacked <- false",
"ref": "attacked",
"value": false
},
{
"comment": "x <- (x + 1)",
"ref": "x",
"value": {
"left": "x",
"op": "+",
"right": 1
}
}
],
"location": "l"
}
],
"guard": {
"comment": "(!(left_of_enemy) & (x < 5))",
"exp": {
"left": {
"exp": {
"args": [],
"function": "left_of_enemy",
"op": "call"
},
"op": "¬"
},
"op": "∧",
"right": {
"left": "x",
"op": "<",
"right": 5
}
}
},
"location": "l"
},
{
"action": "right",
"destinations": [
{
"assignments": [
{
"comment": "gold <- false",
"ref": "gold",
"value": false
},
{
"comment": "gem <- false",
"ref": "gem",
"value": false
},
{
"comment": "attacked <- true",
"ref": "attacked",
"value": true
},
{
"comment": "x <- 3",
"ref": "x",
"value": 3
},
{
"comment": "y <- 1",
"ref": "y",
"value": 1
}
],
"location": "l",
"probability": {
"comment": "(1 / 10)",
"exp": {
"left": 1,
"op": "/",
"right": 10
}
}
},
{
"assignments": [
{
"comment": "gold <- ((gold & !(left_of_home)) | left_of_gold)",
"ref": "gold",
"value": {
"left": {
"left": "gold",
"op": "∧",
"right": {
"exp": {
"args": [],
"function": "left_of_home",
"op": "call"
},
"op": "¬"
}
},
"op": "∨",
"right": {
"args": [],
"function": "left_of_gold",
"op": "call"
}
}
},
{
"comment": "gem <- ((gem & !(left_of_home)) | left_of_gem)",
"ref": "gem",
"value": {
"left": {
"left": "gem",
"op": "∧",
"right": {
"exp": {
"args": [],
"function": "left_of_home",
"op": "call"
},
"op": "¬"
}
},
"op": "∨",
"right": {
"args": [],
"function": "left_of_gem",
"op": "call"
}
}
},
{
"comment": "attacked <- false",
"ref": "attacked",
"value": false
},
{
"comment": "x <- (x + 1)",
"ref": "x",
"value": {
"left": "x",
"op": "+",
"right": 1
}
}
],
"location": "l",
"probability": {
"comment": "(1 - (1 / 10))",
"exp": {
"left": 1,
"op": "-",
"right": {
"left": 1,
"op": "/",
"right": 10
}
}
}
}
],
"guard": {
"comment": "(left_of_enemy & (x < 5))",
"exp": {
"left": {
"args": [],
"function": "left_of_enemy",
"op": "call"
},
"op": "∧",
"right": {
"left": "x",
"op": "<",
"right": 5
}
}
},
"location": "l"
},
{
"action": "top",
"destinations": [
{
"assignments": [
{
"comment": "gold <- ((gold & !(below_of_home)) | below_of_gold)",
"ref": "gold",
"value": {
"left": {
"left": "gold",
"op": "∧",
"right": {
"exp": {
"args": [],
"function": "below_of_home",
"op": "call"
},
"op": "¬"
}
},
"op": "∨",
"right": {
"args": [],
"function": "below_of_gold",
"op": "call"
}
}
},
{
"comment": "gem <- ((gem & !(below_of_home)) | below_of_gem)",
"ref": "gem",
"value": {
"left": {
"left": "gem",
"op": "∧",
"right": {
"exp": {
"args": [],
"function": "below_of_home",
"op": "call"
},
"op": "¬"
}
},
"op": "∨",
"right": {
"args": [],
"function": "below_of_gem",
"op": "call"
}
}
},
{
"comment": "attacked <- false",
"ref": "attacked",
"value": false
},
{
"comment": "y <- (y + 1)",
"ref": "y",
"value": {
"left": "y",
"op": "+",
"right": 1
}
}
],
"location": "l"
}
],
"guard": {
"comment": "(!(below_of_enemy) & (y < 5))",
"exp": {
"left": {
"exp": {
"args": [],
"function": "below_of_enemy",
"op": "call"
},
"op": "¬"
},
"op": "∧",
"right": {
"left": "y",
"op": "<",
"right": 5
}
}
},
"location": "l"
},
{
"action": "top",
"destinations": [
{
"assignments": [
{
"comment": "gold <- false",
"ref": "gold",
"value": false
},
{
"comment": "gem <- false",
"ref": "gem",
"value": false
},
{
"comment": "attacked <- true",
"ref": "attacked",
"value": true
},
{
"comment": "x <- 3",
"ref": "x",
"value": 3
},
{
"comment": "y <- 1",
"ref": "y",
"value": 1
}
],
"location": "l",
"probability": {
"comment": "(1 / 10)",
"exp": {
"left": 1,
"op": "/",
"right": 10
}
}
},
{
"assignments": [
{
"comment": "gold <- ((gold & !(below_of_home)) | below_of_gold)",
"ref": "gold",
"value": {
"left": {
"left": "gold",
"op": "∧",
"right": {
"exp": {
"args": [],
"function": "below_of_home",
"op": "call"
},
"op": "¬"
}
},
"op": "∨",
"right": {
"args": [],
"function": "below_of_gold",
"op": "call"
}
}
},
{
"comment": "gem <- ((gem & !(below_of_home)) | below_of_gem)",
"ref": "gem",
"value": {
"left": {
"left": "gem",
"op": "∧",
"right": {
"exp": {
"args": [],
"function": "below_of_home",
"op": "call"
},
"op": "¬"
}
},
"op": "∨",
"right": {
"args": [],
"function": "below_of_gem",
"op": "call"
}
}
},
{
"comment": "attacked <- false",
"ref": "attacked",
"value": false
},
{
"comment": "y <- (y + 1)",
"ref": "y",
"value": {
"left": "y",
"op": "+",
"right": 1
}
}
],
"location": "l",
"probability": {
"comment": "(1 - (1 / 10))",
"exp": {
"left": 1,
"op": "-",
"right": {
"left": 1,
"op": "/",
"right": 10
}
}
}
}
],
"guard": {
"comment": "(below_of_enemy & (y < 5))",
"exp": {
"left": {
"args": [],
"function": "below_of_enemy",
"op": "call"
},
"op": "∧",
"right": {
"left": "y",
"op": "<",
"right": 5
}
}
},
"location": "l"
}
],
"initial-locations": [
"l"
],
"locations": [
{
"name": "l",
"transient-values": [
{
"comment": "success <- ((required_gold = 0) & (required_gem = 0))",
"ref": "success",
"value": {
"left": {
"left": "required_gold",
"op": "=",
"right": 0
},
"op": "∧",
"right": {
"left": "required_gem",
"op": "=",
"right": 0
}
}
}
]
}
],
"name": "robot",
"variables": [
{
"initial-value": false,
"name": "attacked",
"type": "bool"
}
]
},
{
"edges": [
{
"action": "down",
"destinations": [
{
"assignments": [
{
"comment": "required_gold <- (max(0, (required_gold - ((above_of_home & gold) ? 1 : 0))))",
"ref": "required_gold",
"value": {
"left": 0,
"op": "max",
"right": {
"left": "required_gold",
"op": "-",
"right": {
"else": 0,
"if": {
"left": {
"args": [],
"function": "above_of_home",
"op": "call"
},
"op": "∧",
"right": "gold"
},
"op": "ite",
"then": 1
}
}
}
}
],
"location": "l"
}
],
"location": "l"
},
{
"action": "left",
"destinations": [
{
"assignments": [
{
"comment": "required_gold <- (max(0, (required_gold - ((right_of_home & gold) ? 1 : 0))))",
"ref": "required_gold",
"value": {
"left": 0,
"op": "max",
"right": {
"left": "required_gold",
"op": "-",
"right": {
"else": 0,
"if": {
"left": {
"args": [],
"function": "right_of_home",
"op": "call"
},
"op": "∧",
"right": "gold"
},
"op": "ite",
"then": 1
}
}
}
}
],
"location": "l"
}
],
"location": "l"
},
{
"action": "right",
"destinations": [
{
"assignments": [
{
"comment": "required_gold <- (max(0, (required_gold - ((left_of_home & gold) ? 1 : 0))))",
"ref": "required_gold",
"value": {
"left": 0,
"op": "max",
"right": {
"left": "required_gold",
"op": "-",
"right": {
"else": 0,
"if": {
"left": {
"args": [],
"function": "left_of_home",
"op": "call"
},
"op": "∧",
"right": "gold"
},
"op": "ite",
"then": 1
}
}
}
}
],
"location": "l"
}
],
"location": "l"
},
{
"action": "top",
"destinations": [
{
"assignments": [
{
"comment": "required_gold <- (max(0, (required_gold - ((below_of_home & gold) ? 1 : 0))))",
"ref": "required_gold",
"value": {
"left": 0,
"op": "max",
"right": {
"left": "required_gold",
"op": "-",
"right": {
"else": 0,
"if": {
"left": {
"args": [],
"function": "below_of_home",
"op": "call"
},
"op": "∧",
"right": "gold"
},
"op": "ite",
"then": 1
}
}
}
}
],
"location": "l"
}
],
"location": "l"
}
],
"initial-locations": [
"l"
],
"locations": [
{
"name": "l"
}
],
"name": "goldcounter",
"variables": []
},
{
"edges": [
{
"action": "down",
"destinations": [
{
"assignments": [
{
"comment": "required_gem <- (max(0, (required_gem - ((above_of_home & gem) ? 1 : 0))))",
"ref": "required_gem",
"value": {
"left": 0,
"op": "max",
"right": {
"left": "required_gem",
"op": "-",
"right": {
"else": 0,
"if": {
"left": {
"args": [],
"function": "above_of_home",
"op": "call"
},
"op": "∧",
"right": "gem"
},
"op": "ite",
"then": 1
}
}
}
}
],
"location": "l"
}
],
"location": "l"
},
{
"action": "left",
"destinations": [
{
"assignments": [
{
"comment": "required_gem <- (max(0, (required_gem - ((right_of_home & gem) ? 1 : 0))))",
"ref": "required_gem",
"value": {
"left": 0,
"op": "max",
"right": {
"left": "required_gem",
"op": "-",
"right": {
"else": 0,
"if": {
"left": {
"args": [],
"function": "right_of_home",
"op": "call"
},
"op": "∧",
"right": "gem"
},
"op": "ite",
"then": 1
}
}
}
}
],
"location": "l"
}
],
"location": "l"
},
{
"action": "right",
"destinations": [
{
"assignments": [
{
"comment": "required_gem <- (max(0, (required_gem - ((left_of_home & gem) ? 1 : 0))))",
"ref": "required_gem",
"value": {
"left": 0,
"op": "max",
"right": {
"left": "required_gem",
"op": "-",
"right": {
"else": 0,
"if": {
"left": {
"args": [],
"function": "left_of_home",
"op": "call"
},
"op": "∧",
"right": "gem"
},
"op": "ite",
"then": 1
}
}
}
}
],
"location": "l"
}
],
"location": "l"
},
{
"action": "top",
"destinations": [
{
"assignments": [
{
"comment": "required_gem <- (max(0, (required_gem - ((below_of_home & gem) ? 1 : 0))))",
"ref": "required_gem",
"value": {
"left": 0,
"op": "max",
"right": {
"left": "required_gem",
"op": "-",
"right": {
"else": 0,
"if": {
"left": {
"args": [],
"function": "below_of_home",
"op": "call"
},
"op": "∧",
"right": "gem"
},
"op": "ite",
"then": 1
}
}
}
}
],
"location": "l"
}
],
"location": "l"
}
],
"initial-locations": [
"l"
],
"locations": [
{
"name": "l"
}
],
"name": "gemcounter",
"variables": []
}
],
"constants": [
{
"name": "WIDTH",
"type": "int",
"value": 5
},
{
"name": "HEIGHT",
"type": "int",
"value": 5
},
{
"name": "XINIT",
"type": "int",
"value": 3
},
{
"name": "YINIT",
"type": "int",
"value": 1
},
{
"name": "GOLD_TO_COLLECT",
"type": "int",
"value": 100
},
{
"name": "GEM_TO_COLLECT",
"type": "int",
"value": 100
},
{
"name": "B",
"type": "int",
"value": 1300
},
{
"name": "pAttack",
"type": "real",
"value": {
"left": 1,
"op": "/",
"right": 10
}
}
],
"features": [
"derived-operators",
"functions"
],
"functions": [
{
"body": {
"left": {
"left": "x",
"op": "=",
"right": 4
},
"op": "∧",
"right": {
"left": "y",
"op": "=",
"right": 5
}
},
"name": "right_of_gold",
"parameters": [],
"type": "bool"
},
{
"body": {
"left": {
"left": "x",
"op": "=",
"right": 3
},
"op": "∧",
"right": {
"left": "y",
"op": "=",
"right": 4
}
},
"name": "below_of_gold",
"parameters": [],
"type": "bool"
},
{
"body": false,
"name": "above_of_gold",
"parameters": [],
"type": "bool"
},
{
"body": {
"left": {
"left": "x",
"op": "=",
"right": 5
},
"op": "∧",
"right": {
"left": "y",
"op": "=",
"right": 5
}
},
"name": "above_of_gem",
"parameters": [],
"type": "bool"
},
{
"body": {
"left": {
"left": "x",
"op": "=",
"right": 2
},
"op": "∧",
"right": {
"left": "y",
"op": "=",
"right": 5
}
},
"name": "left_of_gold",
"parameters": [],
"type": "bool"
},
{
"body": {
"left": {
"left": "x",
"op": "=",
"right": 4
},
"op": "∧",
"right": {
"left": "y",
"op": "=",
"right": 4
}
},
"name": "left_of_gem",
"parameters": [],
"type": "bool"
},
{
"body": false,
"name": "right_of_gem",
"parameters": [],
"type": "bool"
},
{
"body": {
"left": {
"left": "x",
"op": "=",
"right": 3
},
"op": "∧",
"right": {
"left": "y",
"op": "=",
"right": 5
}
},
"name": "above_of_enemy",
"parameters": [],
"type": "bool"
},
{
"body": {
"left": {
"left": "x",
"op": "=",
"right": 4
},
"op": "∧",
"right": {
"left": "y",
"op": "=",
"right": 1
}
},
"name": "right_of_home",
"parameters": [],
"type": "bool"
},
{
"body": {
"left": {
"left": "x",
"op": "=",
"right": 2
},
"op": "∧",
"right": {
"left": "y",
"op": "=",
"right": 1
}
},
"name": "left_of_home",
"parameters": [],
"type": "bool"
},
{
"body": {
"left": {
"left": {
"left": "x",
"op": "=",
"right": 3
},
"op": "∧",
"right": {
"left": "y",
"op": "=",
"right": 3
}
},
"op": "∨",
"right": {
"left": {
"left": "x",
"op": "=",
"right": 4
},
"op": "∧",
"right": {
"left": "y",
"op": "=",
"right": 4
}
}
},
"name": "below_of_enemy",
"parameters": [],
"type": "bool"
},
{
"body": {
"left": {
"left": {
"left": "x",
"op": "=",
"right": 5
},
"op": "∧",
"right": {
"left": "y",
"op": "=",
"right": 5
}
},
"op": "∨",
"right": {
"left": {
"left": "x",
"op": "=",
"right": 4
},
"op": "∧",
"right": {
"left": "y",
"op": "=",
"right": 4
}
}
},
"name": "right_of_enemy",
"parameters": [],
"type": "bool"
},
{
"body": {
"left": {
"left": "x",
"op": "=",
"right": 3
},
"op": "∧",
"right": {
"left": "y",
"op": "=",
"right": 2
}
},
"name": "above_of_home",
"parameters": [],
"type": "bool"
},
{
"body": {
"left": {
"left": "x",
"op": "=",
"right": 5
},
"op": "∧",
"right": {
"left": "y",
"op": "=",
"right": 3
}
},
"name": "below_of_gem",
"parameters": [],
"type": "bool"
},
{
"body": {
"left": {
"left": {
"left": "x",
"op": "=",
"right": 3
},
"op": "∧",
"right": {
"left": "y",
"op": "=",
"right": 5
}
},
"op": "∨",
"right": {
"left": {
"left": "x",
"op": "=",
"right": 2
},
"op": "∧",
"right": {
"left": "y",
"op": "=",
"right": 4
}
}
},
"name": "left_of_enemy",
"parameters": [],
"type": "bool"
},
{
"body": false,
"name": "below_of_home",
"parameters": [],
"type": "bool"
}
],
"jani-version": 1,
"name": "model",
"properties": [
{
"expression": {
"fun": "values",
"op": "filter",
"states": {
"op": "initial"
},
"values": {
"exp": {
"left": true,
"op": "U",
"right": "success",
"step-bounds": {
"upper": 1300,
"upper-exclusive": false
}
},
"op": "Pmax"
}
},
"name": "prgoldgem"
}
],
"restrict-initial": {
"exp": true
},
"system": {
"elements": [
{
"automaton": "robot"
},
{
"automaton": "goldcounter"
},
{
"automaton": "gemcounter"
}
],
"syncs": [
{
"result": "down",
"synchronise": [
"down",
"down",
"down"
]
},
{
"result": "left",
"synchronise": [
"left",
"left",
"left"
]
},
{
"result": "right",
"synchronise": [
"right",
"right",
"right"
]
},
{
"result": "top",
"synchronise": [
"top",
"top",
"top"
]
}
]
},
"type": "mdp",
"variables": [
{
"initial-value": false,
"name": "success",
"transient": true,
"type": "bool"
},
{
"initial-value": 3,
"name": "x",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 1,
"upper-bound": 5
}
},
{
"initial-value": 1,
"name": "y",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 1,
"upper-bound": 5
}
},
{
"initial-value": false,
"name": "gold",
"type": "bool"
},
{
"initial-value": false,
"name": "gem",
"type": "bool"
},
{
"initial-value": 100,
"name": "required_gold",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 100
}
},
{
"initial-value": 100,
"name": "required_gem",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 100
}
}
]
}