model.prism (0.01 MB) property.props (0.01 MB) model.jani (0.21 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 B=11; formula localFailure = loc_1=crit&t_1=0&failure_1; formula noLocalFailure = !((loc_1=crit&t_1=0&failure_1)); formula process_1_finishes = (loc_1=crit&t_1=0); formula process_2_finishes = (loc_2=crit&t_2=0); formula process_3_finishes = (loc_3=crit&t_3=0); formula process_4_finishes = (loc_4=crit&t_4=0); formula process_5_finishes = (loc_5=crit&t_5=0); label "emptyBattery" = ((battery_load=0)); const int energy_capacity = 250; const int t_max = 9; const int undef = 0; const int ncrit = 2; const int wait = 0; const int crit = 1; const int none = 0; const int process_1 = 1; const int process_2 = 2; const int process_3 = 3; const int process_4 = 4; const int process_5 = 5; const int m_1 = 1; const int m_2 = 1; const int m_3 = 2; const int m_4 = 1; const int m_5 = 1; const int boost_multiplicator = 3; module Battery battery_load : [0..energy_capacity] init energy_capacity; [tick] loc_1=ncrit -> (battery_load'=max(0, battery_load-2*m_1)); [tick] loc_1=wait -> (battery_load'=max(0, battery_load-1*m_1)); [tick] loc_1=crit&user_1=process_1&boost_1=0 -> (battery_load'=max(0, battery_load-3*m_1)); [tick] loc_1=crit&user_1=process_1&boost_1=1 -> (battery_load'=max(0, battery_load-3*m_1*boost_multiplicator)); endmodule module Process_1 failure_1 : bool init false; loc_1 : [0..2] init ncrit; t_1 : [0..t_max] init 0; [tick] loc_1=ncrit&t_1!=0 -> (t_1'=t_1-1); [tick] loc_1=ncrit&t_1=0 -> 2/3 : (t_1'=9) & (loc_1'=wait) + 1/3 : (t_1'=7) & (loc_1'=wait); [tick] loc_1=wait&user_1!=process_1 -> (t_1'=max(0, t_1-1)); [tick] loc_1=wait&user_1=process_1 -> 1/3 : (loc_1'=crit) & (t_1'=2) & (failure_1'=(2<(boost_1+1)*t_1) ? false : true) + 2/3 : (loc_1'=crit) & (t_1'=3) & (failure_1'=(3<(boost_1+1)*t_1) ? false : true); [tick] loc_1=crit&t_1>0 -> (t_1'=max(t_1-(boost_1+1), 0)); [tick] loc_1=crit&t_1=0 -> 2/3 : (loc_1'=ncrit) & (t_1'=4) & (failure_1'=false) + 1/3 : (loc_1'=ncrit) & (t_1'=5) & (failure_1'=false); endmodule module Process_2 t_2 : [0..t_max] init 0; loc_2 : [0..2] init ncrit; [tick] loc_2=ncrit&t_2!=0 -> (t_2'=t_2-1); [tick] loc_2=ncrit&t_2=0 -> (loc_2'=wait); [tick] loc_2=wait&user_1!=process_2 -> (t_2'=max(0, t_2-1)); [tick] loc_2=wait&user_1=process_2 -> 1/3 : (loc_2'=crit) & (t_2'=2) + 2/3 : (loc_2'=crit) & (t_2'=3); [tick] loc_2=crit&t_2>0 -> (t_2'=max(t_2-(boost_1+1), 0)); [tick] loc_2=crit&t_2=0 -> 2/3 : (loc_2'=ncrit) & (t_2'=4) + 1/3 : (loc_2'=ncrit) & (t_2'=5); endmodule module Resources boost_1 : [0..1] init 0; user_1 : [0..5] init none; [tick] user_1=none&loc_1=wait -> (user_1'=process_1); [tick] user_1=none&loc_1=wait -> (user_1'=process_1) & (boost_1'=1); [tick] user_1=process_1&!(((loc_1=crit&t_1=0))) -> true; [tick] user_1=process_1&(((loc_1=crit&t_1=0)))&loc_1!=wait&loc_2!=wait&loc_3!=wait&loc_4!=wait&loc_5!=wait -> (user_1'=none) & (boost_1'=0); [tick] user_1=process_1&(((loc_1=crit&t_1=0)))&loc_2=wait -> (user_1'=process_2) & (boost_1'=1); [tick] user_1=process_1&(((loc_1=crit&t_1=0)))&loc_2=wait -> (user_1'=process_2) & (boost_1'=0); [tick] user_1=process_1&(((loc_1=crit&t_1=0)))&loc_3=wait -> (user_1'=process_3) & (boost_1'=1); [tick] user_1=process_1&(((loc_1=crit&t_1=0)))&loc_3=wait -> (user_1'=process_3) & (boost_1'=0); [tick] user_1=process_1&(((loc_1=crit&t_1=0)))&loc_4=wait -> (user_1'=process_4) & (boost_1'=1); [tick] user_1=process_1&(((loc_1=crit&t_1=0)))&loc_4=wait -> (user_1'=process_4) & (boost_1'=0); [tick] user_1=process_1&(((loc_1=crit&t_1=0)))&loc_5=wait -> (user_1'=process_5) & (boost_1'=1); [tick] user_1=process_1&(((loc_1=crit&t_1=0)))&loc_5=wait -> (user_1'=process_5) & (boost_1'=0); [tick] user_1=none&loc_2=wait -> (user_1'=process_2); [tick] user_1=none&loc_2=wait -> (user_1'=process_2) & (boost_1'=1); [tick] user_1=process_2&!(((loc_2=crit&t_2=0))) -> true; [tick] user_1=process_2&(((loc_2=crit&t_2=0)))&loc_1!=wait&loc_2!=wait&loc_3!=wait&loc_4!=wait&loc_5!=wait -> (user_1'=none) & (boost_1'=0); [tick] user_1=process_2&(((loc_2=crit&t_2=0)))&loc_1=wait -> (user_1'=process_1) & (boost_1'=1); [tick] user_1=process_2&(((loc_2=crit&t_2=0)))&loc_1=wait -> (user_1'=process_1) & (boost_1'=0); [tick] user_1=process_2&(((loc_2=crit&t_2=0)))&loc_3=wait -> (user_1'=process_3) & (boost_1'=1); [tick] user_1=process_2&(((loc_2=crit&t_2=0)))&loc_3=wait -> (user_1'=process_3) & (boost_1'=0); [tick] user_1=process_2&(((loc_2=crit&t_2=0)))&loc_4=wait -> (user_1'=process_4) & (boost_1'=1); [tick] user_1=process_2&(((loc_2=crit&t_2=0)))&loc_4=wait -> (user_1'=process_4) & (boost_1'=0); [tick] user_1=process_2&(((loc_2=crit&t_2=0)))&loc_5=wait -> (user_1'=process_5) & (boost_1'=1); [tick] user_1=process_2&(((loc_2=crit&t_2=0)))&loc_5=wait -> (user_1'=process_5) & (boost_1'=0); [tick] user_1=none&loc_3=wait -> (user_1'=process_3); [tick] user_1=none&loc_3=wait -> (user_1'=process_3) & (boost_1'=1); [tick] user_1=process_3&!(((loc_3=crit&t_3=0))) -> true; [tick] user_1=process_3&(((loc_3=crit&t_3=0)))&loc_1!=wait&loc_2!=wait&loc_3!=wait&loc_4!=wait&loc_5!=wait -> (user_1'=none) & (boost_1'=0); [tick] user_1=process_3&(((loc_3=crit&t_3=0)))&loc_1=wait -> (user_1'=process_1) & (boost_1'=1); [tick] user_1=process_3&(((loc_3=crit&t_3=0)))&loc_1=wait -> (user_1'=process_1) & (boost_1'=0); [tick] user_1=process_3&(((loc_3=crit&t_3=0)))&loc_2=wait -> (user_1'=process_2) & (boost_1'=1); [tick] user_1=process_3&(((loc_3=crit&t_3=0)))&loc_2=wait -> (user_1'=process_2) & (boost_1'=0); [tick] user_1=process_3&(((loc_3=crit&t_3=0)))&loc_4=wait -> (user_1'=process_4) & (boost_1'=1); [tick] user_1=process_3&(((loc_3=crit&t_3=0)))&loc_4=wait -> (user_1'=process_4) & (boost_1'=0); [tick] user_1=process_3&(((loc_3=crit&t_3=0)))&loc_5=wait -> (user_1'=process_5) & (boost_1'=1); [tick] user_1=process_3&(((loc_3=crit&t_3=0)))&loc_5=wait -> (user_1'=process_5) & (boost_1'=0); [tick] user_1=none&loc_4=wait -> (user_1'=process_4); [tick] user_1=none&loc_4=wait -> (user_1'=process_4) & (boost_1'=1); [tick] user_1=process_4&!(((loc_4=crit&t_4=0))) -> true; [tick] user_1=process_4&(((loc_4=crit&t_4=0)))&loc_1!=wait&loc_2!=wait&loc_3!=wait&loc_4!=wait&loc_5!=wait -> (user_1'=none) & (boost_1'=0); [tick] user_1=process_4&(((loc_4=crit&t_4=0)))&loc_1=wait -> (user_1'=process_1) & (boost_1'=1); [tick] user_1=process_4&(((loc_4=crit&t_4=0)))&loc_1=wait -> (user_1'=process_1) & (boost_1'=0); [tick] user_1=process_4&(((loc_4=crit&t_4=0)))&loc_2=wait -> (user_1'=process_2) & (boost_1'=1); [tick] user_1=process_4&(((loc_4=crit&t_4=0)))&loc_2=wait -> (user_1'=process_2) & (boost_1'=0); [tick] user_1=process_4&(((loc_4=crit&t_4=0)))&loc_3=wait -> (user_1'=process_3) & (boost_1'=1); [tick] user_1=process_4&(((loc_4=crit&t_4=0)))&loc_3=wait -> (user_1'=process_3) & (boost_1'=0); [tick] user_1=process_4&(((loc_4=crit&t_4=0)))&loc_5=wait -> (user_1'=process_5) & (boost_1'=1); [tick] user_1=process_4&(((loc_4=crit&t_4=0)))&loc_5=wait -> (user_1'=process_5) & (boost_1'=0); [tick] user_1=none&loc_5=wait -> (user_1'=process_5); [tick] user_1=none&loc_5=wait -> (user_1'=process_5) & (boost_1'=1); [tick] user_1=process_5&!(((loc_5=crit&t_5=0))) -> true; [tick] user_1=process_5&(((loc_5=crit&t_5=0)))&loc_1!=wait&loc_2!=wait&loc_3!=wait&loc_4!=wait&loc_5!=wait -> (user_1'=none) & (boost_1'=0); [tick] user_1=process_5&(((loc_5=crit&t_5=0)))&loc_1=wait -> (user_1'=process_1) & (boost_1'=1); [tick] user_1=process_5&(((loc_5=crit&t_5=0)))&loc_1=wait -> (user_1'=process_1) & (boost_1'=0); [tick] user_1=process_5&(((loc_5=crit&t_5=0)))&loc_2=wait -> (user_1'=process_2) & (boost_1'=1); [tick] user_1=process_5&(((loc_5=crit&t_5=0)))&loc_2=wait -> (user_1'=process_2) & (boost_1'=0); [tick] user_1=process_5&(((loc_5=crit&t_5=0)))&loc_3=wait -> (user_1'=process_3) & (boost_1'=1); [tick] user_1=process_5&(((loc_5=crit&t_5=0)))&loc_3=wait -> (user_1'=process_3) & (boost_1'=0); [tick] user_1=process_5&(((loc_5=crit&t_5=0)))&loc_4=wait -> (user_1'=process_4) & (boost_1'=1); [tick] user_1=process_5&(((loc_5=crit&t_5=0)))&loc_4=wait -> (user_1'=process_4) & (boost_1'=0); [tick] user_1=none&loc_1!=wait&loc_2!=wait&loc_3!=wait&loc_4!=wait&loc_5!=wait -> true; endmodule module Process_3 t_3 : [0..t_max] init 0; loc_3 : [0..2] init ncrit; [tick] loc_3=ncrit&t_3!=0 -> (t_3'=t_3-1); [tick] loc_3=ncrit&t_3=0 -> (loc_3'=wait); [tick] loc_3=wait&user_1!=process_3 -> (t_3'=max(0, t_3-1)); [tick] loc_3=wait&user_1=process_3 -> 1/3 : (loc_3'=crit) & (t_3'=2) + 2/3 : (loc_3'=crit) & (t_3'=3); [tick] loc_3=crit&t_3>0 -> (t_3'=max(t_3-(boost_1+1), 0)); [tick] loc_3=crit&t_3=0 -> 2/3 : (loc_3'=ncrit) & (t_3'=4) + 1/3 : (loc_3'=ncrit) & (t_3'=5); endmodule module Process_5 loc_5 : [0..2] init ncrit; t_5 : [0..t_max] init 0; [tick] loc_5=ncrit&t_5!=0 -> (t_5'=t_5-1); [tick] loc_5=ncrit&t_5=0 -> (loc_5'=wait); [tick] loc_5=wait&user_1!=process_5 -> (t_5'=max(0, t_5-1)); [tick] loc_5=wait&user_1=process_5 -> 1/3 : (loc_5'=crit) & (t_5'=2) + 2/3 : (loc_5'=crit) & (t_5'=3); [tick] loc_5=crit&t_5>0 -> (t_5'=max(t_5-(boost_1+1), 0)); [tick] loc_5=crit&t_5=0 -> 2/3 : (loc_5'=ncrit) & (t_5'=4) + 1/3 : (loc_5'=ncrit) & (t_5'=5); endmodule module Process_4 t_4 : [0..t_max] init 0; loc_4 : [0..2] init ncrit; [tick] loc_4=ncrit&t_4!=0 -> (t_4'=t_4-1); [tick] loc_4=ncrit&t_4=0 -> (loc_4'=wait); [tick] loc_4=wait&user_1!=process_4 -> (t_4'=max(0, t_4-1)); [tick] loc_4=wait&user_1=process_4 -> 1/3 : (loc_4'=crit) & (t_4'=2) + 2/3 : (loc_4'=crit) & (t_4'=3); [tick] loc_4=crit&t_4>0 -> (t_4'=max(t_4-(boost_1+1), 0)); [tick] loc_4=crit&t_4=0 -> 2/3 : (loc_4'=ncrit) & (t_4'=4) + 1/3 : (loc_4'=ncrit) & (t_4'=5); endmodule rewards "utilityLocal" [tick] loc_1=crit&t_1=0&!failure_1&!((battery_load=0)) : 1; endrewards
"ExpUtil": R{"utilityLocal"}max=? [ F "emptyBattery" ];
{
"actions": [
{
"name": "tick"
}
],
"automata": [
{
"edges": [
{
"action": "tick",
"destinations": [
{
"assignments": [
{
"comment": "battery_load <- (max(0, (battery_load - 2)))",
"ref": "battery_load",
"value": {
"left": 0,
"op": "max",
"right": {
"left": "battery_load",
"op": "-",
"right": 2
}
}
},
{
"comment": "utilityLocal <- (((((loc_1 = 1) & (t_1 = 0)) & !(failure_1)) & !((battery_load = 0))) ? 1 : 0)",
"ref": "utilityLocal",
"value": {
"else": 0.0,
"if": {
"left": {
"left": {
"exp": {
"left": "battery_load",
"op": "=",
"right": 0
},
"op": "¬"
},
"op": "∧",
"right": {
"left": "t_1",
"op": "=",
"right": 0
}
},
"op": "∧",
"right": {
"left": {
"exp": "failure_1",
"op": "¬"
},
"op": "∧",
"right": {
"left": "loc_1",
"op": "=",
"right": 1
}
}
},
"op": "ite",
"then": 1
}
}
],
"location": "l"
}
],
"guard": {
"comment": "(loc_1 = 2)",
"exp": {
"left": "loc_1",
"op": "=",
"right": 2
}
},
"location": "l"
},
{
"action": "tick",
"destinations": [
{
"assignments": [
{
"comment": "battery_load <- (max(0, (battery_load - 1)))",
"ref": "battery_load",
"value": {
"left": 0,
"op": "max",
"right": {
"left": "battery_load",
"op": "-",
"right": 1
}
}
},
{
"comment": "utilityLocal <- (((((loc_1 = 1) & (t_1 = 0)) & !(failure_1)) & !((battery_load = 0))) ? 1 : 0)",
"ref": "utilityLocal",
"value": {
"else": 0.0,
"if": {
"left": {
"left": {
"exp": {
"left": "battery_load",
"op": "=",
"right": 0
},
"op": "¬"
},
"op": "∧",
"right": {
"left": "t_1",
"op": "=",
"right": 0
}
},
"op": "∧",
"right": {
"left": {
"exp": "failure_1",
"op": "¬"
},
"op": "∧",
"right": {
"left": "loc_1",
"op": "=",
"right": 1
}
}
},
"op": "ite",
"then": 1
}
}
],
"location": "l"
}
],
"guard": {
"comment": "(loc_1 = 0)",
"exp": {
"left": "loc_1",
"op": "=",
"right": 0
}
},
"location": "l"
},
{
"action": "tick",
"destinations": [
{
"assignments": [
{
"comment": "battery_load <- (max(0, (battery_load - 3)))",
"ref": "battery_load",
"value": {
"left": 0,
"op": "max",
"right": {
"left": "battery_load",
"op": "-",
"right": 3
}
}
},
{
"comment": "utilityLocal <- (((((loc_1 = 1) & (t_1 = 0)) & !(failure_1)) & !((battery_load = 0))) ? 1 : 0)",
"ref": "utilityLocal",
"value": {
"else": 0.0,
"if": {
"left": {
"left": {
"exp": {
"left": "battery_load",
"op": "=",
"right": 0
},
"op": "¬"
},
"op": "∧",
"right": {
"left": "t_1",
"op": "=",
"right": 0
}
},
"op": "∧",
"right": {
"left": {
"exp": "failure_1",
"op": "¬"
},
"op": "∧",
"right": {
"left": "loc_1",
"op": "=",
"right": 1
}
}
},
"op": "ite",
"then": 1
}
}
],
"location": "l"
}
],
"guard": {
"comment": "(((loc_1 = 1) & (user_1 = 1)) & (boost_1 = 0))",
"exp": {
"left": {
"left": {
"left": "loc_1",
"op": "=",
"right": 1
},
"op": "∧",
"right": {
"left": "user_1",
"op": "=",
"right": 1
}
},
"op": "∧",
"right": {
"left": "boost_1",
"op": "=",
"right": 0
}
}
},
"location": "l"
},
{
"action": "tick",
"destinations": [
{
"assignments": [
{
"comment": "battery_load <- (max(0, (battery_load - 9)))",
"ref": "battery_load",
"value": {
"left": 0,
"op": "max",
"right": {
"left": "battery_load",
"op": "-",
"right": 9
}
}
},
{
"comment": "utilityLocal <- (((((loc_1 = 1) & (t_1 = 0)) & !(failure_1)) & !((battery_load = 0))) ? 1 : 0)",
"ref": "utilityLocal",
"value": {
"else": 0.0,
"if": {
"left": {
"left": {
"exp": {
"left": "battery_load",
"op": "=",
"right": 0
},
"op": "¬"
},
"op": "∧",
"right": {
"left": "t_1",
"op": "=",
"right": 0
}
},
"op": "∧",
"right": {
"left": {
"exp": "failure_1",
"op": "¬"
},
"op": "∧",
"right": {
"left": "loc_1",
"op": "=",
"right": 1
}
}
},
"op": "ite",
"then": 1
}
}
],
"location": "l"
}
],
"guard": {
"comment": "(((loc_1 = 1) & (user_1 = 1)) & (boost_1 = 1))",
"exp": {
"left": {
"left": {
"left": "loc_1",
"op": "=",
"right": 1
},
"op": "∧",
"right": {
"left": "user_1",
"op": "=",
"right": 1
}
},
"op": "∧",
"right": {
"left": "boost_1",
"op": "=",
"right": 1
}
}
},
"location": "l"
}
],
"initial-locations": [
"l"
],
"locations": [
{
"name": "l",
"transient-values": [
{
"comment": "emptyBattery <- (battery_load = 0)",
"ref": "emptyBattery",
"value": {
"left": "battery_load",
"op": "=",
"right": 0
}
}
]
}
],
"name": "Battery",
"variables": []
},
{
"edges": [
{
"action": "tick",
"destinations": [
{
"assignments": [
{
"comment": "t_1 <- (t_1 - 1)",
"ref": "t_1",
"value": {
"left": "t_1",
"op": "-",
"right": 1
}
}
],
"location": "l"
}
],
"guard": {
"comment": "((loc_1 = 2) & (t_1 != 0))",
"exp": {
"left": {
"left": "loc_1",
"op": "=",
"right": 2
},
"op": "∧",
"right": {
"left": "t_1",
"op": "≠",
"right": 0
}
}
},
"location": "l"
},
{
"action": "tick",
"destinations": [
{
"assignments": [
{
"comment": "loc_1 <- 0",
"ref": "loc_1",
"value": 0
},
{
"comment": "t_1 <- 9",
"ref": "t_1",
"value": 9
}
],
"location": "l",
"probability": {
"comment": "(2 / 3)",
"exp": {
"left": 2,
"op": "/",
"right": 3
}
}
},
{
"assignments": [
{
"comment": "loc_1 <- 0",
"ref": "loc_1",
"value": 0
},
{
"comment": "t_1 <- 7",
"ref": "t_1",
"value": 7
}
],
"location": "l",
"probability": {
"comment": "(1 / 3)",
"exp": {
"left": 1,
"op": "/",
"right": 3
}
}
}
],
"guard": {
"comment": "((loc_1 = 2) & (t_1 = 0))",
"exp": {
"left": {
"left": "loc_1",
"op": "=",
"right": 2
},
"op": "∧",
"right": {
"left": "t_1",
"op": "=",
"right": 0
}
}
},
"location": "l"
},
{
"action": "tick",
"destinations": [
{
"assignments": [
{
"comment": "t_1 <- (max(0, (t_1 - 1)))",
"ref": "t_1",
"value": {
"left": 0,
"op": "max",
"right": {
"left": "t_1",
"op": "-",
"right": 1
}
}
}
],
"location": "l"
}
],
"guard": {
"comment": "((loc_1 = 0) & (user_1 != 1))",
"exp": {
"left": {
"left": "loc_1",
"op": "=",
"right": 0
},
"op": "∧",
"right": {
"left": "user_1",
"op": "≠",
"right": 1
}
}
},
"location": "l"
},
{
"action": "tick",
"destinations": [
{
"assignments": [
{
"comment": "failure_1 <- ((2 < ((boost_1 + 1) * t_1)) ? false : true)",
"ref": "failure_1",
"value": {
"else": true,
"if": {
"left": 2,
"op": "<",
"right": {
"left": {
"left": "boost_1",
"op": "+",
"right": 1
},
"op": "*",
"right": "t_1"
}
},
"op": "ite",
"then": false
}
},
{
"comment": "loc_1 <- 1",
"ref": "loc_1",
"value": 1
},
{
"comment": "t_1 <- 2",
"ref": "t_1",
"value": 2
}
],
"location": "l",
"probability": {
"comment": "(1 / 3)",
"exp": {
"left": 1,
"op": "/",
"right": 3
}
}
},
{
"assignments": [
{
"comment": "failure_1 <- ((3 < ((boost_1 + 1) * t_1)) ? false : true)",
"ref": "failure_1",
"value": {
"else": true,
"if": {
"left": 3,
"op": "<",
"right": {
"left": {
"left": "boost_1",
"op": "+",
"right": 1
},
"op": "*",
"right": "t_1"
}
},
"op": "ite",
"then": false
}
},
{
"comment": "loc_1 <- 1",
"ref": "loc_1",
"value": 1
},
{
"comment": "t_1 <- 3",
"ref": "t_1",
"value": 3
}
],
"location": "l",
"probability": {
"comment": "(2 / 3)",
"exp": {
"left": 2,
"op": "/",
"right": 3
}
}
}
],
"guard": {
"comment": "((loc_1 = 0) & (user_1 = 1))",
"exp": {
"left": {
"left": "loc_1",
"op": "=",
"right": 0
},
"op": "∧",
"right": {
"left": "user_1",
"op": "=",
"right": 1
}
}
},
"location": "l"
},
{
"action": "tick",
"destinations": [
{
"assignments": [
{
"comment": "t_1 <- (max((t_1 - (boost_1 + 1)), 0))",
"ref": "t_1",
"value": {
"left": {
"left": "t_1",
"op": "-",
"right": {
"left": "boost_1",
"op": "+",
"right": 1
}
},
"op": "max",
"right": 0
}
}
],
"location": "l"
}
],
"guard": {
"comment": "((loc_1 = 1) & (t_1 > 0))",
"exp": {
"left": {
"left": "loc_1",
"op": "=",
"right": 1
},
"op": "∧",
"right": {
"left": "t_1",
"op": ">",
"right": 0
}
}
},
"location": "l"
},
{
"action": "tick",
"destinations": [
{
"assignments": [
{
"comment": "failure_1 <- false",
"ref": "failure_1",
"value": false
},
{
"comment": "loc_1 <- 2",
"ref": "loc_1",
"value": 2
},
{
"comment": "t_1 <- 4",
"ref": "t_1",
"value": 4
}
],
"location": "l",
"probability": {
"comment": "(2 / 3)",
"exp": {
"left": 2,
"op": "/",
"right": 3
}
}
},
{
"assignments": [
{
"comment": "failure_1 <- false",
"ref": "failure_1",
"value": false
},
{
"comment": "loc_1 <- 2",
"ref": "loc_1",
"value": 2
},
{
"comment": "t_1 <- 5",
"ref": "t_1",
"value": 5
}
],
"location": "l",
"probability": {
"comment": "(1 / 3)",
"exp": {
"left": 1,
"op": "/",
"right": 3
}
}
}
],
"guard": {
"comment": "((loc_1 = 1) & (t_1 = 0))",
"exp": {
"left": {
"left": "loc_1",
"op": "=",
"right": 1
},
"op": "∧",
"right": {
"left": "t_1",
"op": "=",
"right": 0
}
}
},
"location": "l"
}
],
"initial-locations": [
"l"
],
"locations": [
{
"name": "l"
}
],
"name": "Process_1",
"variables": []
},
{
"edges": [
{
"action": "tick",
"destinations": [
{
"assignments": [
{
"comment": "t_2 <- (t_2 - 1)",
"ref": "t_2",
"value": {
"left": "t_2",
"op": "-",
"right": 1
}
}
],
"location": "l"
}
],
"guard": {
"comment": "((loc_2 = 2) & (t_2 != 0))",
"exp": {
"left": {
"left": "loc_2",
"op": "=",
"right": 2
},
"op": "∧",
"right": {
"left": "t_2",
"op": "≠",
"right": 0
}
}
},
"location": "l"
},
{
"action": "tick",
"destinations": [
{
"assignments": [
{
"comment": "loc_2 <- 0",
"ref": "loc_2",
"value": 0
}
],
"location": "l"
}
],
"guard": {
"comment": "((loc_2 = 2) & (t_2 = 0))",
"exp": {
"left": {
"left": "loc_2",
"op": "=",
"right": 2
},
"op": "∧",
"right": {
"left": "t_2",
"op": "=",
"right": 0
}
}
},
"location": "l"
},
{
"action": "tick",
"destinations": [
{
"assignments": [
{
"comment": "t_2 <- (max(0, (t_2 - 1)))",
"ref": "t_2",
"value": {
"left": 0,
"op": "max",
"right": {
"left": "t_2",
"op": "-",
"right": 1
}
}
}
],
"location": "l"
}
],
"guard": {
"comment": "((loc_2 = 0) & (user_1 != 2))",
"exp": {
"left": {
"left": "loc_2",
"op": "=",
"right": 0
},
"op": "∧",
"right": {
"left": "user_1",
"op": "≠",
"right": 2
}
}
},
"location": "l"
},
{
"action": "tick",
"destinations": [
{
"assignments": [
{
"comment": "t_2 <- 2",
"ref": "t_2",
"value": 2
},
{
"comment": "loc_2 <- 1",
"ref": "loc_2",
"value": 1
}
],
"location": "l",
"probability": {
"comment": "(1 / 3)",
"exp": {
"left": 1,
"op": "/",
"right": 3
}
}
},
{
"assignments": [
{
"comment": "t_2 <- 3",
"ref": "t_2",
"value": 3
},
{
"comment": "loc_2 <- 1",
"ref": "loc_2",
"value": 1
}
],
"location": "l",
"probability": {
"comment": "(2 / 3)",
"exp": {
"left": 2,
"op": "/",
"right": 3
}
}
}
],
"guard": {
"comment": "((loc_2 = 0) & (user_1 = 2))",
"exp": {
"left": {
"left": "loc_2",
"op": "=",
"right": 0
},
"op": "∧",
"right": {
"left": "user_1",
"op": "=",
"right": 2
}
}
},
"location": "l"
},
{
"action": "tick",
"destinations": [
{
"assignments": [
{
"comment": "t_2 <- (max((t_2 - (boost_1 + 1)), 0))",
"ref": "t_2",
"value": {
"left": {
"left": "t_2",
"op": "-",
"right": {
"left": "boost_1",
"op": "+",
"right": 1
}
},
"op": "max",
"right": 0
}
}
],
"location": "l"
}
],
"guard": {
"comment": "((loc_2 = 1) & (t_2 > 0))",
"exp": {
"left": {
"left": "loc_2",
"op": "=",
"right": 1
},
"op": "∧",
"right": {
"left": "t_2",
"op": ">",
"right": 0
}
}
},
"location": "l"
},
{
"action": "tick",
"destinations": [
{
"assignments": [
{
"comment": "t_2 <- 4",
"ref": "t_2",
"value": 4
},
{
"comment": "loc_2 <- 2",
"ref": "loc_2",
"value": 2
}
],
"location": "l",
"probability": {
"comment": "(2 / 3)",
"exp": {
"left": 2,
"op": "/",
"right": 3
}
}
},
{
"assignments": [
{
"comment": "t_2 <- 5",
"ref": "t_2",
"value": 5
},
{
"comment": "loc_2 <- 2",
"ref": "loc_2",
"value": 2
}
],
"location": "l",
"probability": {
"comment": "(1 / 3)",
"exp": {
"left": 1,
"op": "/",
"right": 3
}
}
}
],
"guard": {
"comment": "((loc_2 = 1) & (t_2 = 0))",
"exp": {
"left": {
"left": "loc_2",
"op": "=",
"right": 1
},
"op": "∧",
"right": {
"left": "t_2",
"op": "=",
"right": 0
}
}
},
"location": "l"
}
],
"initial-locations": [
"l"
],
"locations": [
{
"name": "l"
}
],
"name": "Process_2",
"variables": []
},
{
"edges": [
{
"action": "tick",
"destinations": [
{
"assignments": [
{
"comment": "user_1 <- 1",
"ref": "user_1",
"value": 1
}
],
"location": "l"
}
],
"guard": {
"comment": "((user_1 = 0) & (loc_1 = 0))",
"exp": {
"left": {
"left": "user_1",
"op": "=",
"right": 0
},
"op": "∧",
"right": {
"left": "loc_1",
"op": "=",
"right": 0
}
}
},
"location": "l"
},
{
"action": "tick",
"destinations": [
{
"assignments": [
{
"comment": "boost_1 <- 1",
"ref": "boost_1",
"value": 1
},
{
"comment": "user_1 <- 1",
"ref": "user_1",
"value": 1
}
],
"location": "l"
}
],
"guard": {
"comment": "((user_1 = 0) & (loc_1 = 0))",
"exp": {
"left": {
"left": "user_1",
"op": "=",
"right": 0
},
"op": "∧",
"right": {
"left": "loc_1",
"op": "=",
"right": 0
}
}
},
"location": "l"
},
{
"action": "tick",
"destinations": [
{
"location": "l"
}
],
"guard": {
"comment": "((user_1 = 1) & !(((loc_1 = 1) & (t_1 = 0))))",
"exp": {
"left": {
"left": "user_1",
"op": "=",
"right": 1
},
"op": "∧",
"right": {
"exp": {
"left": {
"left": "loc_1",
"op": "=",
"right": 1
},
"op": "∧",
"right": {
"left": "t_1",
"op": "=",
"right": 0
}
},
"op": "¬"
}
}
},
"location": "l"
},
{
"action": "tick",
"destinations": [
{
"assignments": [
{
"comment": "boost_1 <- 0",
"ref": "boost_1",
"value": 0
},
{
"comment": "user_1 <- 0",
"ref": "user_1",
"value": 0
}
],
"location": "l"
}
],
"guard": {
"comment": "(((((((user_1 = 1) & ((loc_1 = 1) & (t_1 = 0))) & (loc_1 != 0)) & (loc_2 != 0)) & (loc_3 != 0)) & (loc_4 != 0)) & (loc_5 != 0))",
"exp": {
"left": {
"left": {
"left": {
"left": "loc_5",
"op": "≠",
"right": 0
},
"op": "∧",
"right": {
"left": "t_1",
"op": "=",
"right": 0
}
},
"op": "∧",
"right": {
"left": {
"left": "loc_2",
"op": "≠",
"right": 0
},
"op": "∧",
"right": {
"left": "loc_1",
"op": "≠",
"right": 0
}
}
},
"op": "∧",
"right": {
"left": {
"left": {
"left": "loc_4",
"op": "≠",
"right": 0
},
"op": "∧",
"right": {
"left": "loc_1",
"op": "=",
"right": 1
}
},
"op": "∧",
"right": {
"left": {
"left": "loc_3",
"op": "≠",
"right": 0
},
"op": "∧",
"right": {
"left": "user_1",
"op": "=",
"right": 1
}
}
}
}
},
"location": "l"
},
{
"action": "tick",
"destinations": [
{
"assignments": [
{
"comment": "boost_1 <- 1",
"ref": "boost_1",
"value": 1
},
{
"comment": "user_1 <- 2",
"ref": "user_1",
"value": 2
}
],
"location": "l"
}
],
"guard": {
"comment": "(((user_1 = 1) & ((loc_1 = 1) & (t_1 = 0))) & (loc_2 = 0))",
"exp": {
"left": {
"left": {
"left": "loc_2",
"op": "=",
"right": 0
},
"op": "∧",
"right": {
"left": "t_1",
"op": "=",
"right": 0
}
},
"op": "∧",
"right": {
"left": {
"left": "user_1",
"op": "=",
"right": 1
},
"op": "∧",
"right": {
"left": "loc_1",
"op": "=",
"right": 1
}
}
}
},
"location": "l"
},
{
"action": "tick",
"destinations": [
{
"assignments": [
{
"comment": "boost_1 <- 0",
"ref": "boost_1",
"value": 0
},
{
"comment": "user_1 <- 2",
"ref": "user_1",
"value": 2
}
],
"location": "l"
}
],
"guard": {
"comment": "(((user_1 = 1) & ((loc_1 = 1) & (t_1 = 0))) & (loc_2 = 0))",
"exp": {
"left": {
"left": {
"left": "loc_2",
"op": "=",
"right": 0
},
"op": "∧",
"right": {
"left": "t_1",
"op": "=",
"right": 0
}
},
"op": "∧",
"right": {
"left": {
"left": "user_1",
"op": "=",
"right": 1
},
"op": "∧",
"right": {
"left": "loc_1",
"op": "=",
"right": 1
}
}
}
},
"location": "l"
},
{
"action": "tick",
"destinations": [
{
"assignments": [
{
"comment": "boost_1 <- 1",
"ref": "boost_1",
"value": 1
},
{
"comment": "user_1 <- 3",
"ref": "user_1",
"value": 3
}
],
"location": "l"
}
],
"guard": {
"comment": "(((user_1 = 1) & ((loc_1 = 1) & (t_1 = 0))) & (loc_3 = 0))",
"exp": {
"left": {
"left": {
"left": "loc_3",
"op": "=",
"right": 0
},
"op": "∧",
"right": {
"left": "t_1",
"op": "=",
"right": 0
}
},
"op": "∧",
"right": {
"left": {
"left": "user_1",
"op": "=",
"right": 1
},
"op": "∧",
"right": {
"left": "loc_1",
"op": "=",
"right": 1
}
}
}
},
"location": "l"
},
{
"action": "tick",
"destinations": [
{
"assignments": [
{
"comment": "boost_1 <- 0",
"ref": "boost_1",
"value": 0
},
{
"comment": "user_1 <- 3",
"ref": "user_1",
"value": 3
}
],
"location": "l"
}
],
"guard": {
"comment": "(((user_1 = 1) & ((loc_1 = 1) & (t_1 = 0))) & (loc_3 = 0))",
"exp": {
"left": {
"left": {
"left": "loc_3",
"op": "=",
"right": 0
},
"op": "∧",
"right": {
"left": "t_1",
"op": "=",
"right": 0
}
},
"op": "∧",
"right": {
"left": {
"left": "user_1",
"op": "=",
"right": 1
},
"op": "∧",
"right": {
"left": "loc_1",
"op": "=",
"right": 1
}
}
}
},
"location": "l"
},
{
"action": "tick",
"destinations": [
{
"assignments": [
{
"comment": "boost_1 <- 1",
"ref": "boost_1",
"value": 1
},
{
"comment": "user_1 <- 4",
"ref": "user_1",
"value": 4
}
],
"location": "l"
}
],
"guard": {
"comment": "(((user_1 = 1) & ((loc_1 = 1) & (t_1 = 0))) & (loc_4 = 0))",
"exp": {
"left": {
"left": {
"left": "loc_4",
"op": "=",
"right": 0
},
"op": "∧",
"right": {
"left": "t_1",
"op": "=",
"right": 0
}
},
"op": "∧",
"right": {
"left": {
"left": "user_1",
"op": "=",
"right": 1
},
"op": "∧",
"right": {
"left": "loc_1",
"op": "=",
"right": 1
}
}
}
},
"location": "l"
},
{
"action": "tick",
"destinations": [
{
"assignments": [
{
"comment": "boost_1 <- 0",
"ref": "boost_1",
"value": 0
},
{
"comment": "user_1 <- 4",
"ref": "user_1",
"value": 4
}
],
"location": "l"
}
],
"guard": {
"comment": "(((user_1 = 1) & ((loc_1 = 1) & (t_1 = 0))) & (loc_4 = 0))",
"exp": {
"left": {
"left": {
"left": "loc_4",
"op": "=",
"right": 0
},
"op": "∧",
"right": {
"left": "t_1",
"op": "=",
"right": 0
}
},
"op": "∧",
"right": {
"left": {
"left": "user_1",
"op": "=",
"right": 1
},
"op": "∧",
"right": {
"left": "loc_1",
"op": "=",
"right": 1
}
}
}
},
"location": "l"
},
{
"action": "tick",
"destinations": [
{
"assignments": [
{
"comment": "boost_1 <- 1",
"ref": "boost_1",
"value": 1
},
{
"comment": "user_1 <- 5",
"ref": "user_1",
"value": 5
}
],
"location": "l"
}
],
"guard": {
"comment": "(((user_1 = 1) & ((loc_1 = 1) & (t_1 = 0))) & (loc_5 = 0))",
"exp": {
"left": {
"left": {
"left": "loc_5",
"op": "=",
"right": 0
},
"op": "∧",
"right": {
"left": "t_1",
"op": "=",
"right": 0
}
},
"op": "∧",
"right": {
"left": {
"left": "user_1",
"op": "=",
"right": 1
},
"op": "∧",
"right": {
"left": "loc_1",
"op": "=",
"right": 1
}
}
}
},
"location": "l"
},
{
"action": "tick",
"destinations": [
{
"assignments": [
{
"comment": "boost_1 <- 0",
"ref": "boost_1",
"value": 0
},
{
"comment": "user_1 <- 5",
"ref": "user_1",
"value": 5
}
],
"location": "l"
}
],
"guard": {
"comment": "(((user_1 = 1) & ((loc_1 = 1) & (t_1 = 0))) & (loc_5 = 0))",
"exp": {
"left": {
"left": {
"left": "loc_5",
"op": "=",
"right": 0
},
"op": "∧",
"right": {
"left": "t_1",
"op": "=",
"right": 0
}
},
"op": "∧",
"right": {
"left": {
"left": "user_1",
"op": "=",
"right": 1
},
"op": "∧",
"right": {
"left": "loc_1",
"op": "=",
"right": 1
}
}
}
},
"location": "l"
},
{
"action": "tick",
"destinations": [
{
"assignments": [
{
"comment": "user_1 <- 2",
"ref": "user_1",
"value": 2
}
],
"location": "l"
}
],
"guard": {
"comment": "((user_1 = 0) & (loc_2 = 0))",
"exp": {
"left": {
"left": "user_1",
"op": "=",
"right": 0
},
"op": "∧",
"right": {
"left": "loc_2",
"op": "=",
"right": 0
}
}
},
"location": "l"
},
{
"action": "tick",
"destinations": [
{
"assignments": [
{
"comment": "boost_1 <- 1",
"ref": "boost_1",
"value": 1
},
{
"comment": "user_1 <- 2",
"ref": "user_1",
"value": 2
}
],
"location": "l"
}
],
"guard": {
"comment": "((user_1 = 0) & (loc_2 = 0))",
"exp": {
"left": {
"left": "user_1",
"op": "=",
"right": 0
},
"op": "∧",
"right": {
"left": "loc_2",
"op": "=",
"right": 0
}
}
},
"location": "l"
},
{
"action": "tick",
"destinations": [
{
"location": "l"
}
],
"guard": {
"comment": "((user_1 = 2) & !(((loc_2 = 1) & (t_2 = 0))))",
"exp": {
"left": {
"left": "user_1",
"op": "=",
"right": 2
},
"op": "∧",
"right": {
"exp": {
"left": {
"left": "loc_2",
"op": "=",
"right": 1
},
"op": "∧",
"right": {
"left": "t_2",
"op": "=",
"right": 0
}
},
"op": "¬"
}
}
},
"location": "l"
},
{
"action": "tick",
"destinations": [
{
"assignments": [
{
"comment": "boost_1 <- 0",
"ref": "boost_1",
"value": 0
},
{
"comment": "user_1 <- 0",
"ref": "user_1",
"value": 0
}
],
"location": "l"
}
],
"guard": {
"comment": "(((((((user_1 = 2) & ((loc_2 = 1) & (t_2 = 0))) & (loc_1 != 0)) & (loc_2 != 0)) & (loc_3 != 0)) & (loc_4 != 0)) & (loc_5 != 0))",
"exp": {
"left": {
"left": {
"left": {
"left": "loc_5",
"op": "≠",
"right": 0
},
"op": "∧",
"right": {
"left": "t_2",
"op": "=",
"right": 0
}
},
"op": "∧",
"right": {
"left": {
"left": "loc_2",
"op": "≠",
"right": 0
},
"op": "∧",
"right": {
"left": "loc_1",
"op": "≠",
"right": 0
}
}
},
"op": "∧",
"right": {
"left": {
"left": {
"left": "loc_4",
"op": "≠",
"right": 0
},
"op": "∧",
"right": {
"left": "loc_2",
"op": "=",
"right": 1
}
},
"op": "∧",
"right": {
"left": {
"left": "loc_3",
"op": "≠",
"right": 0
},
"op": "∧",
"right": {
"left": "user_1",
"op": "=",
"right": 2
}
}
}
}
},
"location": "l"
},
{
"action": "tick",
"destinations": [
{
"assignments": [
{
"comment": "boost_1 <- 1",
"ref": "boost_1",
"value": 1
},
{
"comment": "user_1 <- 1",
"ref": "user_1",
"value": 1
}
],
"location": "l"
}
],
"guard": {
"comment": "(((user_1 = 2) & ((loc_2 = 1) & (t_2 = 0))) & (loc_1 = 0))",
"exp": {
"left": {
"left": {
"left": "loc_1",
"op": "=",
"right": 0
},
"op": "∧",
"right": {
"left": "t_2",
"op": "=",
"right": 0
}
},
"op": "∧",
"right": {
"left": {
"left": "user_1",
"op": "=",
"right": 2
},
"op": "∧",
"right": {
"left": "loc_2",
"op": "=",
"right": 1
}
}
}
},
"location": "l"
},
{
"action": "tick",
"destinations": [
{
"assignments": [
{
"comment": "boost_1 <- 0",
"ref": "boost_1",
"value": 0
},
{
"comment": "user_1 <- 1",
"ref": "user_1",
"value": 1
}
],
"location": "l"
}
],
"guard": {
"comment": "(((user_1 = 2) & ((loc_2 = 1) & (t_2 = 0))) & (loc_1 = 0))",
"exp": {
"left": {
"left": {
"left": "loc_1",
"op": "=",
"right": 0
},
"op": "∧",
"right": {
"left": "t_2",
"op": "=",
"right": 0
}
},
"op": "∧",
"right": {
"left": {
"left": "user_1",
"op": "=",
"right": 2
},
"op": "∧",
"right": {
"left": "loc_2",
"op": "=",
"right": 1
}
}
}
},
"location": "l"
},
{
"action": "tick",
"destinations": [
{
"assignments": [
{
"comment": "boost_1 <- 1",
"ref": "boost_1",
"value": 1
},
{
"comment": "user_1 <- 3",
"ref": "user_1",
"value": 3
}
],
"location": "l"
}
],
"guard": {
"comment": "(((user_1 = 2) & ((loc_2 = 1) & (t_2 = 0))) & (loc_3 = 0))",
"exp": {
"left": {
"left": {
"left": "loc_3",
"op": "=",
"right": 0
},
"op": "∧",
"right": {
"left": "t_2",
"op": "=",
"right": 0
}
},
"op": "∧",
"right": {
"left": {
"left": "user_1",
"op": "=",
"right": 2
},
"op": "∧",
"right": {
"left": "loc_2",
"op": "=",
"right": 1
}
}
}
},
"location": "l"
},
{
"action": "tick",
"destinations": [
{
"assignments": [
{
"comment": "boost_1 <- 0",
"ref": "boost_1",
"value": 0
},
{
"comment": "user_1 <- 3",
"ref": "user_1",
"value": 3
}
],
"location": "l"
}
],
"guard": {
"comment": "(((user_1 = 2) & ((loc_2 = 1) & (t_2 = 0))) & (loc_3 = 0))",
"exp": {
"left": {
"left": {
"left": "loc_3",
"op": "=",
"right": 0
},
"op": "∧",
"right": {
"left": "t_2",
"op": "=",
"right": 0
}
},
"op": "∧",
"right": {
"left": {
"left": "user_1",
"op": "=",
"right": 2
},
"op": "∧",
"right": {
"left": "loc_2",
"op": "=",
"right": 1
}
}
}
},
"location": "l"
},
{
"action": "tick",
"destinations": [
{
"assignments": [
{
"comment": "boost_1 <- 1",
"ref": "boost_1",
"value": 1
},
{
"comment": "user_1 <- 4",
"ref": "user_1",
"value": 4
}
],
"location": "l"
}
],
"guard": {
"comment": "(((user_1 = 2) & ((loc_2 = 1) & (t_2 = 0))) & (loc_4 = 0))",
"exp": {
"left": {
"left": {
"left": "loc_4",
"op": "=",
"right": 0
},
"op": "∧",
"right": {
"left": "t_2",
"op": "=",
"right": 0
}
},
"op": "∧",
"right": {
"left": {
"left": "user_1",
"op": "=",
"right": 2
},
"op": "∧",
"right": {
"left": "loc_2",
"op": "=",
"right": 1
}
}
}
},
"location": "l"
},
{
"action": "tick",
"destinations": [
{
"assignments": [
{
"comment": "boost_1 <- 0",
"ref": "boost_1",
"value": 0
},
{
"comment": "user_1 <- 4",
"ref": "user_1",
"value": 4
}
],
"location": "l"
}
],
"guard": {
"comment": "(((user_1 = 2) & ((loc_2 = 1) & (t_2 = 0))) & (loc_4 = 0))",
"exp": {
"left": {
"left": {
"left": "loc_4",
"op": "=",
"right": 0
},
"op": "∧",
"right": {
"left": "t_2",
"op": "=",
"right": 0
}
},
"op": "∧",
"right": {
"left": {
"left": "user_1",
"op": "=",
"right": 2
},
"op": "∧",
"right": {
"left": "loc_2",
"op": "=",
"right": 1
}
}
}
},
"location": "l"
},
{
"action": "tick",
"destinations": [
{
"assignments": [
{
"comment": "boost_1 <- 1",
"ref": "boost_1",
"value": 1
},
{
"comment": "user_1 <- 5",
"ref": "user_1",
"value": 5
}
],
"location": "l"
}
],
"guard": {
"comment": "(((user_1 = 2) & ((loc_2 = 1) & (t_2 = 0))) & (loc_5 = 0))",
"exp": {
"left": {
"left": {
"left": "loc_5",
"op": "=",
"right": 0
},
"op": "∧",
"right": {
"left": "t_2",
"op": "=",
"right": 0
}
},
"op": "∧",
"right": {
"left": {
"left": "user_1",
"op": "=",
"right": 2
},
"op": "∧",
"right": {
"left": "loc_2",
"op": "=",
"right": 1
}
}
}
},
"location": "l"
},
{
"action": "tick",
"destinations": [
{
"assignments": [
{
"comment": "boost_1 <- 0",
"ref": "boost_1",
"value": 0
},
{
"comment": "user_1 <- 5",
"ref": "user_1",
"value": 5
}
],
"location": "l"
}
],
"guard": {
"comment": "(((user_1 = 2) & ((loc_2 = 1) & (t_2 = 0))) & (loc_5 = 0))",
"exp": {
"left": {
"left": {
"left": "loc_5",
"op": "=",
"right": 0
},
"op": "∧",
"right": {
"left": "t_2",
"op": "=",
"right": 0
}
},
"op": "∧",
"right": {
"left": {
"left": "user_1",
"op": "=",
"right": 2
},
"op": "∧",
"right": {
"left": "loc_2",
"op": "=",
"right": 1
}
}
}
},
"location": "l"
},
{
"action": "tick",
"destinations": [
{
"assignments": [
{
"comment": "user_1 <- 3",
"ref": "user_1",
"value": 3
}
],
"location": "l"
}
],
"guard": {
"comment": "((user_1 = 0) & (loc_3 = 0))",
"exp": {
"left": {
"left": "user_1",
"op": "=",
"right": 0
},
"op": "∧",
"right": {
"left": "loc_3",
"op": "=",
"right": 0
}
}
},
"location": "l"
},
{
"action": "tick",
"destinations": [
{
"assignments": [
{
"comment": "boost_1 <- 1",
"ref": "boost_1",
"value": 1
},
{
"comment": "user_1 <- 3",
"ref": "user_1",
"value": 3
}
],
"location": "l"
}
],
"guard": {
"comment": "((user_1 = 0) & (loc_3 = 0))",
"exp": {
"left": {
"left": "user_1",
"op": "=",
"right": 0
},
"op": "∧",
"right": {
"left": "loc_3",
"op": "=",
"right": 0
}
}
},
"location": "l"
},
{
"action": "tick",
"destinations": [
{
"location": "l"
}
],
"guard": {
"comment": "((user_1 = 3) & !(((loc_3 = 1) & (t_3 = 0))))",
"exp": {
"left": {
"left": "user_1",
"op": "=",
"right": 3
},
"op": "∧",
"right": {
"exp": {
"left": {
"left": "loc_3",
"op": "=",
"right": 1
},
"op": "∧",
"right": {
"left": "t_3",
"op": "=",
"right": 0
}
},
"op": "¬"
}
}
},
"location": "l"
},
{
"action": "tick",
"destinations": [
{
"assignments": [
{
"comment": "boost_1 <- 0",
"ref": "boost_1",
"value": 0
},
{
"comment": "user_1 <- 0",
"ref": "user_1",
"value": 0
}
],
"location": "l"
}
],
"guard": {
"comment": "(((((((user_1 = 3) & ((loc_3 = 1) & (t_3 = 0))) & (loc_1 != 0)) & (loc_2 != 0)) & (loc_3 != 0)) & (loc_4 != 0)) & (loc_5 != 0))",
"exp": {
"left": {
"left": {
"left": {
"left": "loc_5",
"op": "≠",
"right": 0
},
"op": "∧",
"right": {
"left": "t_3",
"op": "=",
"right": 0
}
},
"op": "∧",
"right": {
"left": {
"left": "loc_2",
"op": "≠",
"right": 0
},
"op": "∧",
"right": {
"left": "loc_1",
"op": "≠",
"right": 0
}
}
},
"op": "∧",
"right": {
"left": {
"left": {
"left": "loc_4",
"op": "≠",
"right": 0
},
"op": "∧",
"right": {
"left": "loc_3",
"op": "=",
"right": 1
}
},
"op": "∧",
"right": {
"left": {
"left": "loc_3",
"op": "≠",
"right": 0
},
"op": "∧",
"right": {
"left": "user_1",
"op": "=",
"right": 3
}
}
}
}
},
"location": "l"
},
{
"action": "tick",
"destinations": [
{
"assignments": [
{
"comment": "boost_1 <- 1",
"ref": "boost_1",
"value": 1
},
{
"comment": "user_1 <- 1",
"ref": "user_1",
"value": 1
}
],
"location": "l"
}
],
"guard": {
"comment": "(((user_1 = 3) & ((loc_3 = 1) & (t_3 = 0))) & (loc_1 = 0))",
"exp": {
"left": {
"left": {
"left": "loc_1",
"op": "=",
"right": 0
},
"op": "∧",
"right": {
"left": "t_3",
"op": "=",
"right": 0
}
},
"op": "∧",
"right": {
"left": {
"left": "user_1",
"op": "=",
"right": 3
},
"op": "∧",
"right": {
"left": "loc_3",
"op": "=",
"right": 1
}
}
}
},
"location": "l"
},
{
"action": "tick",
"destinations": [
{
"assignments": [
{
"comment": "boost_1 <- 0",
"ref": "boost_1",
"value": 0
},
{
"comment": "user_1 <- 1",
"ref": "user_1",
"value": 1
}
],
"location": "l"
}
],
"guard": {
"comment": "(((user_1 = 3) & ((loc_3 = 1) & (t_3 = 0))) & (loc_1 = 0))",
"exp": {
"left": {
"left": {
"left": "loc_1",
"op": "=",
"right": 0
},
"op": "∧",
"right": {
"left": "t_3",
"op": "=",
"right": 0
}
},
"op": "∧",
"right": {
"left": {
"left": "user_1",
"op": "=",
"right": 3
},
"op": "∧",
"right": {
"left": "loc_3",
"op": "=",
"right": 1
}
}
}
},
"location": "l"
},
{
"action": "tick",
"destinations": [
{
"assignments": [
{
"comment": "boost_1 <- 1",
"ref": "boost_1",
"value": 1
},
{
"comment": "user_1 <- 2",
"ref": "user_1",
"value": 2
}
],
"location": "l"
}
],
"guard": {
"comment": "(((user_1 = 3) & ((loc_3 = 1) & (t_3 = 0))) & (loc_2 = 0))",
"exp": {
"left": {
"left": {
"left": "loc_2",
"op": "=",
"right": 0
},
"op": "∧",
"right": {
"left": "t_3",
"op": "=",
"right": 0
}
},
"op": "∧",
"right": {
"left": {
"left": "user_1",
"op": "=",
"right": 3
},
"op": "∧",
"right": {
"left": "loc_3",
"op": "=",
"right": 1
}
}
}
},
"location": "l"
},
{
"action": "tick",
"destinations": [
{
"assignments": [
{
"comment": "boost_1 <- 0",
"ref": "boost_1",
"value": 0
},
{
"comment": "user_1 <- 2",
"ref": "user_1",
"value": 2
}
],
"location": "l"
}
],
"guard": {
"comment": "(((user_1 = 3) & ((loc_3 = 1) & (t_3 = 0))) & (loc_2 = 0))",
"exp": {
"left": {
"left": {
"left": "loc_2",
"op": "=",
"right": 0
},
"op": "∧",
"right": {
"left": "t_3",
"op": "=",
"right": 0
}
},
"op": "∧",
"right": {
"left": {
"left": "user_1",
"op": "=",
"right": 3
},
"op": "∧",
"right": {
"left": "loc_3",
"op": "=",
"right": 1
}
}
}
},
"location": "l"
},
{
"action": "tick",
"destinations": [
{
"assignments": [
{
"comment": "boost_1 <- 1",
"ref": "boost_1",
"value": 1
},
{
"comment": "user_1 <- 4",
"ref": "user_1",
"value": 4
}
],
"location": "l"
}
],
"guard": {
"comment": "(((user_1 = 3) & ((loc_3 = 1) & (t_3 = 0))) & (loc_4 = 0))",
"exp": {
"left": {
"left": {
"left": "loc_4",
"op": "=",
"right": 0
},
"op": "∧",
"right": {
"left": "t_3",
"op": "=",
"right": 0
}
},
"op": "∧",
"right": {
"left": {
"left": "user_1",
"op": "=",
"right": 3
},
"op": "∧",
"right": {
"left": "loc_3",
"op": "=",
"right": 1
}
}
}
},
"location": "l"
},
{
"action": "tick",
"destinations": [
{
"assignments": [
{
"comment": "boost_1 <- 0",
"ref": "boost_1",
"value": 0
},
{
"comment": "user_1 <- 4",
"ref": "user_1",
"value": 4
}
],
"location": "l"
}
],
"guard": {
"comment": "(((user_1 = 3) & ((loc_3 = 1) & (t_3 = 0))) & (loc_4 = 0))",
"exp": {
"left": {
"left": {
"left": "loc_4",
"op": "=",
"right": 0
},
"op": "∧",
"right": {
"left": "t_3",
"op": "=",
"right": 0
}
},
"op": "∧",
"right": {
"left": {
"left": "user_1",
"op": "=",
"right": 3
},
"op": "∧",
"right": {
"left": "loc_3",
"op": "=",
"right": 1
}
}
}
},
"location": "l"
},
{
"action": "tick",
"destinations": [
{
"assignments": [
{
"comment": "boost_1 <- 1",
"ref": "boost_1",
"value": 1
},
{
"comment": "user_1 <- 5",
"ref": "user_1",
"value": 5
}
],
"location": "l"
}
],
"guard": {
"comment": "(((user_1 = 3) & ((loc_3 = 1) & (t_3 = 0))) & (loc_5 = 0))",
"exp": {
"left": {
"left": {
"left": "loc_5",
"op": "=",
"right": 0
},
"op": "∧",
"right": {
"left": "t_3",
"op": "=",
"right": 0
}
},
"op": "∧",
"right": {
"left": {
"left": "user_1",
"op": "=",
"right": 3
},
"op": "∧",
"right": {
"left": "loc_3",
"op": "=",
"right": 1
}
}
}
},
"location": "l"
},
{
"action": "tick",
"destinations": [
{
"assignments": [
{
"comment": "boost_1 <- 0",
"ref": "boost_1",
"value": 0
},
{
"comment": "user_1 <- 5",
"ref": "user_1",
"value": 5
}
],
"location": "l"
}
],
"guard": {
"comment": "(((user_1 = 3) & ((loc_3 = 1) & (t_3 = 0))) & (loc_5 = 0))",
"exp": {
"left": {
"left": {
"left": "loc_5",
"op": "=",
"right": 0
},
"op": "∧",
"right": {
"left": "t_3",
"op": "=",
"right": 0
}
},
"op": "∧",
"right": {
"left": {
"left": "user_1",
"op": "=",
"right": 3
},
"op": "∧",
"right": {
"left": "loc_3",
"op": "=",
"right": 1
}
}
}
},
"location": "l"
},
{
"action": "tick",
"destinations": [
{
"assignments": [
{
"comment": "user_1 <- 4",
"ref": "user_1",
"value": 4
}
],
"location": "l"
}
],
"guard": {
"comment": "((user_1 = 0) & (loc_4 = 0))",
"exp": {
"left": {
"left": "user_1",
"op": "=",
"right": 0
},
"op": "∧",
"right": {
"left": "loc_4",
"op": "=",
"right": 0
}
}
},
"location": "l"
},
{
"action": "tick",
"destinations": [
{
"assignments": [
{
"comment": "boost_1 <- 1",
"ref": "boost_1",
"value": 1
},
{
"comment": "user_1 <- 4",
"ref": "user_1",
"value": 4
}
],
"location": "l"
}
],
"guard": {
"comment": "((user_1 = 0) & (loc_4 = 0))",
"exp": {
"left": {
"left": "user_1",
"op": "=",
"right": 0
},
"op": "∧",
"right": {
"left": "loc_4",
"op": "=",
"right": 0
}
}
},
"location": "l"
},
{
"action": "tick",
"destinations": [
{
"location": "l"
}
],
"guard": {
"comment": "((user_1 = 4) & !(((loc_4 = 1) & (t_4 = 0))))",
"exp": {
"left": {
"left": "user_1",
"op": "=",
"right": 4
},
"op": "∧",
"right": {
"exp": {
"left": {
"left": "loc_4",
"op": "=",
"right": 1
},
"op": "∧",
"right": {
"left": "t_4",
"op": "=",
"right": 0
}
},
"op": "¬"
}
}
},
"location": "l"
},
{
"action": "tick",
"destinations": [
{
"assignments": [
{
"comment": "boost_1 <- 0",
"ref": "boost_1",
"value": 0
},
{
"comment": "user_1 <- 0",
"ref": "user_1",
"value": 0
}
],
"location": "l"
}
],
"guard": {
"comment": "(((((((user_1 = 4) & ((loc_4 = 1) & (t_4 = 0))) & (loc_1 != 0)) & (loc_2 != 0)) & (loc_3 != 0)) & (loc_4 != 0)) & (loc_5 != 0))",
"exp": {
"left": {
"left": {
"left": {
"left": "loc_5",
"op": "≠",
"right": 0
},
"op": "∧",
"right": {
"left": "t_4",
"op": "=",
"right": 0
}
},
"op": "∧",
"right": {
"left": {
"left": "loc_2",
"op": "≠",
"right": 0
},
"op": "∧",
"right": {
"left": "loc_1",
"op": "≠",
"right": 0
}
}
},
"op": "∧",
"right": {
"left": {
"left": {
"left": "loc_4",
"op": "≠",
"right": 0
},
"op": "∧",
"right": {
"left": "loc_4",
"op": "=",
"right": 1
}
},
"op": "∧",
"right": {
"left": {
"left": "loc_3",
"op": "≠",
"right": 0
},
"op": "∧",
"right": {
"left": "user_1",
"op": "=",
"right": 4
}
}
}
}
},
"location": "l"
},
{
"action": "tick",
"destinations": [
{
"assignments": [
{
"comment": "boost_1 <- 1",
"ref": "boost_1",
"value": 1
},
{
"comment": "user_1 <- 1",
"ref": "user_1",
"value": 1
}
],
"location": "l"
}
],
"guard": {
"comment": "(((user_1 = 4) & ((loc_4 = 1) & (t_4 = 0))) & (loc_1 = 0))",
"exp": {
"left": {
"left": {
"left": "loc_1",
"op": "=",
"right": 0
},
"op": "∧",
"right": {
"left": "t_4",
"op": "=",
"right": 0
}
},
"op": "∧",
"right": {
"left": {
"left": "user_1",
"op": "=",
"right": 4
},
"op": "∧",
"right": {
"left": "loc_4",
"op": "=",
"right": 1
}
}
}
},
"location": "l"
},
{
"action": "tick",
"destinations": [
{
"assignments": [
{
"comment": "boost_1 <- 0",
"ref": "boost_1",
"value": 0
},
{
"comment": "user_1 <- 1",
"ref": "user_1",
"value": 1
}
],
"location": "l"
}
],
"guard": {
"comment": "(((user_1 = 4) & ((loc_4 = 1) & (t_4 = 0))) & (loc_1 = 0))",
"exp": {
"left": {
"left": {
"left": "loc_1",
"op": "=",
"right": 0
},
"op": "∧",
"right": {
"left": "t_4",
"op": "=",
"right": 0
}
},
"op": "∧",
"right": {
"left": {
"left": "user_1",
"op": "=",
"right": 4
},
"op": "∧",
"right": {
"left": "loc_4",
"op": "=",
"right": 1
}
}
}
},
"location": "l"
},
{
"action": "tick",
"destinations": [
{
"assignments": [
{
"comment": "boost_1 <- 1",
"ref": "boost_1",
"value": 1
},
{
"comment": "user_1 <- 2",
"ref": "user_1",
"value": 2
}
],
"location": "l"
}
],
"guard": {
"comment": "(((user_1 = 4) & ((loc_4 = 1) & (t_4 = 0))) & (loc_2 = 0))",
"exp": {
"left": {
"left": {
"left": "loc_2",
"op": "=",
"right": 0
},
"op": "∧",
"right": {
"left": "t_4",
"op": "=",
"right": 0
}
},
"op": "∧",
"right": {
"left": {
"left": "user_1",
"op": "=",
"right": 4
},
"op": "∧",
"right": {
"left": "loc_4",
"op": "=",
"right": 1
}
}
}
},
"location": "l"
},
{
"action": "tick",
"destinations": [
{
"assignments": [
{
"comment": "boost_1 <- 0",
"ref": "boost_1",
"value": 0
},
{
"comment": "user_1 <- 2",
"ref": "user_1",
"value": 2
}
],
"location": "l"
}
],
"guard": {
"comment": "(((user_1 = 4) & ((loc_4 = 1) & (t_4 = 0))) & (loc_2 = 0))",
"exp": {
"left": {
"left": {
"left": "loc_2",
"op": "=",
"right": 0
},
"op": "∧",
"right": {
"left": "t_4",
"op": "=",
"right": 0
}
},
"op": "∧",
"right": {
"left": {
"left": "user_1",
"op": "=",
"right": 4
},
"op": "∧",
"right": {
"left": "loc_4",
"op": "=",
"right": 1
}
}
}
},
"location": "l"
},
{
"action": "tick",
"destinations": [
{
"assignments": [
{
"comment": "boost_1 <- 1",
"ref": "boost_1",
"value": 1
},
{
"comment": "user_1 <- 3",
"ref": "user_1",
"value": 3
}
],
"location": "l"
}
],
"guard": {
"comment": "(((user_1 = 4) & ((loc_4 = 1) & (t_4 = 0))) & (loc_3 = 0))",
"exp": {
"left": {
"left": {
"left": "loc_3",
"op": "=",
"right": 0
},
"op": "∧",
"right": {
"left": "t_4",
"op": "=",
"right": 0
}
},
"op": "∧",
"right": {
"left": {
"left": "user_1",
"op": "=",
"right": 4
},
"op": "∧",
"right": {
"left": "loc_4",
"op": "=",
"right": 1
}
}
}
},
"location": "l"
},
{
"action": "tick",
"destinations": [
{
"assignments": [
{
"comment": "boost_1 <- 0",
"ref": "boost_1",
"value": 0
},
{
"comment": "user_1 <- 3",
"ref": "user_1",
"value": 3
}
],
"location": "l"
}
],
"guard": {
"comment": "(((user_1 = 4) & ((loc_4 = 1) & (t_4 = 0))) & (loc_3 = 0))",
"exp": {
"left": {
"left": {
"left": "loc_3",
"op": "=",
"right": 0
},
"op": "∧",
"right": {
"left": "t_4",
"op": "=",
"right": 0
}
},
"op": "∧",
"right": {
"left": {
"left": "user_1",
"op": "=",
"right": 4
},
"op": "∧",
"right": {
"left": "loc_4",
"op": "=",
"right": 1
}
}
}
},
"location": "l"
},
{
"action": "tick",
"destinations": [
{
"assignments": [
{
"comment": "boost_1 <- 1",
"ref": "boost_1",
"value": 1
},
{
"comment": "user_1 <- 5",
"ref": "user_1",
"value": 5
}
],
"location": "l"
}
],
"guard": {
"comment": "(((user_1 = 4) & ((loc_4 = 1) & (t_4 = 0))) & (loc_5 = 0))",
"exp": {
"left": {
"left": {
"left": "loc_5",
"op": "=",
"right": 0
},
"op": "∧",
"right": {
"left": "t_4",
"op": "=",
"right": 0
}
},
"op": "∧",
"right": {
"left": {
"left": "user_1",
"op": "=",
"right": 4
},
"op": "∧",
"right": {
"left": "loc_4",
"op": "=",
"right": 1
}
}
}
},
"location": "l"
},
{
"action": "tick",
"destinations": [
{
"assignments": [
{
"comment": "boost_1 <- 0",
"ref": "boost_1",
"value": 0
},
{
"comment": "user_1 <- 5",
"ref": "user_1",
"value": 5
}
],
"location": "l"
}
],
"guard": {
"comment": "(((user_1 = 4) & ((loc_4 = 1) & (t_4 = 0))) & (loc_5 = 0))",
"exp": {
"left": {
"left": {
"left": "loc_5",
"op": "=",
"right": 0
},
"op": "∧",
"right": {
"left": "t_4",
"op": "=",
"right": 0
}
},
"op": "∧",
"right": {
"left": {
"left": "user_1",
"op": "=",
"right": 4
},
"op": "∧",
"right": {
"left": "loc_4",
"op": "=",
"right": 1
}
}
}
},
"location": "l"
},
{
"action": "tick",
"destinations": [
{
"assignments": [
{
"comment": "user_1 <- 5",
"ref": "user_1",
"value": 5
}
],
"location": "l"
}
],
"guard": {
"comment": "((user_1 = 0) & (loc_5 = 0))",
"exp": {
"left": {
"left": "user_1",
"op": "=",
"right": 0
},
"op": "∧",
"right": {
"left": "loc_5",
"op": "=",
"right": 0
}
}
},
"location": "l"
},
{
"action": "tick",
"destinations": [
{
"assignments": [
{
"comment": "boost_1 <- 1",
"ref": "boost_1",
"value": 1
},
{
"comment": "user_1 <- 5",
"ref": "user_1",
"value": 5
}
],
"location": "l"
}
],
"guard": {
"comment": "((user_1 = 0) & (loc_5 = 0))",
"exp": {
"left": {
"left": "user_1",
"op": "=",
"right": 0
},
"op": "∧",
"right": {
"left": "loc_5",
"op": "=",
"right": 0
}
}
},
"location": "l"
},
{
"action": "tick",
"destinations": [
{
"location": "l"
}
],
"guard": {
"comment": "((user_1 = 5) & !(((loc_5 = 1) & (t_5 = 0))))",
"exp": {
"left": {
"left": "user_1",
"op": "=",
"right": 5
},
"op": "∧",
"right": {
"exp": {
"left": {
"left": "loc_5",
"op": "=",
"right": 1
},
"op": "∧",
"right": {
"left": "t_5",
"op": "=",
"right": 0
}
},
"op": "¬"
}
}
},
"location": "l"
},
{
"action": "tick",
"destinations": [
{
"assignments": [
{
"comment": "boost_1 <- 0",
"ref": "boost_1",
"value": 0
},
{
"comment": "user_1 <- 0",
"ref": "user_1",
"value": 0
}
],
"location": "l"
}
],
"guard": {
"comment": "(((((((user_1 = 5) & ((loc_5 = 1) & (t_5 = 0))) & (loc_1 != 0)) & (loc_2 != 0)) & (loc_3 != 0)) & (loc_4 != 0)) & (loc_5 != 0))",
"exp": {
"left": {
"left": {
"left": {
"left": "loc_5",
"op": "≠",
"right": 0
},
"op": "∧",
"right": {
"left": "t_5",
"op": "=",
"right": 0
}
},
"op": "∧",
"right": {
"left": {
"left": "loc_2",
"op": "≠",
"right": 0
},
"op": "∧",
"right": {
"left": "loc_1",
"op": "≠",
"right": 0
}
}
},
"op": "∧",
"right": {
"left": {
"left": {
"left": "loc_4",
"op": "≠",
"right": 0
},
"op": "∧",
"right": {
"left": "loc_5",
"op": "=",
"right": 1
}
},
"op": "∧",
"right": {
"left": {
"left": "loc_3",
"op": "≠",
"right": 0
},
"op": "∧",
"right": {
"left": "user_1",
"op": "=",
"right": 5
}
}
}
}
},
"location": "l"
},
{
"action": "tick",
"destinations": [
{
"assignments": [
{
"comment": "boost_1 <- 1",
"ref": "boost_1",
"value": 1
},
{
"comment": "user_1 <- 1",
"ref": "user_1",
"value": 1
}
],
"location": "l"
}
],
"guard": {
"comment": "(((user_1 = 5) & ((loc_5 = 1) & (t_5 = 0))) & (loc_1 = 0))",
"exp": {
"left": {
"left": {
"left": "loc_1",
"op": "=",
"right": 0
},
"op": "∧",
"right": {
"left": "t_5",
"op": "=",
"right": 0
}
},
"op": "∧",
"right": {
"left": {
"left": "user_1",
"op": "=",
"right": 5
},
"op": "∧",
"right": {
"left": "loc_5",
"op": "=",
"right": 1
}
}
}
},
"location": "l"
},
{
"action": "tick",
"destinations": [
{
"assignments": [
{
"comment": "boost_1 <- 0",
"ref": "boost_1",
"value": 0
},
{
"comment": "user_1 <- 1",
"ref": "user_1",
"value": 1
}
],
"location": "l"
}
],
"guard": {
"comment": "(((user_1 = 5) & ((loc_5 = 1) & (t_5 = 0))) & (loc_1 = 0))",
"exp": {
"left": {
"left": {
"left": "loc_1",
"op": "=",
"right": 0
},
"op": "∧",
"right": {
"left": "t_5",
"op": "=",
"right": 0
}
},
"op": "∧",
"right": {
"left": {
"left": "user_1",
"op": "=",
"right": 5
},
"op": "∧",
"right": {
"left": "loc_5",
"op": "=",
"right": 1
}
}
}
},
"location": "l"
},
{
"action": "tick",
"destinations": [
{
"assignments": [
{
"comment": "boost_1 <- 1",
"ref": "boost_1",
"value": 1
},
{
"comment": "user_1 <- 2",
"ref": "user_1",
"value": 2
}
],
"location": "l"
}
],
"guard": {
"comment": "(((user_1 = 5) & ((loc_5 = 1) & (t_5 = 0))) & (loc_2 = 0))",
"exp": {
"left": {
"left": {
"left": "loc_2",
"op": "=",
"right": 0
},
"op": "∧",
"right": {
"left": "t_5",
"op": "=",
"right": 0
}
},
"op": "∧",
"right": {
"left": {
"left": "user_1",
"op": "=",
"right": 5
},
"op": "∧",
"right": {
"left": "loc_5",
"op": "=",
"right": 1
}
}
}
},
"location": "l"
},
{
"action": "tick",
"destinations": [
{
"assignments": [
{
"comment": "boost_1 <- 0",
"ref": "boost_1",
"value": 0
},
{
"comment": "user_1 <- 2",
"ref": "user_1",
"value": 2
}
],
"location": "l"
}
],
"guard": {
"comment": "(((user_1 = 5) & ((loc_5 = 1) & (t_5 = 0))) & (loc_2 = 0))",
"exp": {
"left": {
"left": {
"left": "loc_2",
"op": "=",
"right": 0
},
"op": "∧",
"right": {
"left": "t_5",
"op": "=",
"right": 0
}
},
"op": "∧",
"right": {
"left": {
"left": "user_1",
"op": "=",
"right": 5
},
"op": "∧",
"right": {
"left": "loc_5",
"op": "=",
"right": 1
}
}
}
},
"location": "l"
},
{
"action": "tick",
"destinations": [
{
"assignments": [
{
"comment": "boost_1 <- 1",
"ref": "boost_1",
"value": 1
},
{
"comment": "user_1 <- 3",
"ref": "user_1",
"value": 3
}
],
"location": "l"
}
],
"guard": {
"comment": "(((user_1 = 5) & ((loc_5 = 1) & (t_5 = 0))) & (loc_3 = 0))",
"exp": {
"left": {
"left": {
"left": "loc_3",
"op": "=",
"right": 0
},
"op": "∧",
"right": {
"left": "t_5",
"op": "=",
"right": 0
}
},
"op": "∧",
"right": {
"left": {
"left": "user_1",
"op": "=",
"right": 5
},
"op": "∧",
"right": {
"left": "loc_5",
"op": "=",
"right": 1
}
}
}
},
"location": "l"
},
{
"action": "tick",
"destinations": [
{
"assignments": [
{
"comment": "boost_1 <- 0",
"ref": "boost_1",
"value": 0
},
{
"comment": "user_1 <- 3",
"ref": "user_1",
"value": 3
}
],
"location": "l"
}
],
"guard": {
"comment": "(((user_1 = 5) & ((loc_5 = 1) & (t_5 = 0))) & (loc_3 = 0))",
"exp": {
"left": {
"left": {
"left": "loc_3",
"op": "=",
"right": 0
},
"op": "∧",
"right": {
"left": "t_5",
"op": "=",
"right": 0
}
},
"op": "∧",
"right": {
"left": {
"left": "user_1",
"op": "=",
"right": 5
},
"op": "∧",
"right": {
"left": "loc_5",
"op": "=",
"right": 1
}
}
}
},
"location": "l"
},
{
"action": "tick",
"destinations": [
{
"assignments": [
{
"comment": "boost_1 <- 1",
"ref": "boost_1",
"value": 1
},
{
"comment": "user_1 <- 4",
"ref": "user_1",
"value": 4
}
],
"location": "l"
}
],
"guard": {
"comment": "(((user_1 = 5) & ((loc_5 = 1) & (t_5 = 0))) & (loc_4 = 0))",
"exp": {
"left": {
"left": {
"left": "loc_4",
"op": "=",
"right": 0
},
"op": "∧",
"right": {
"left": "t_5",
"op": "=",
"right": 0
}
},
"op": "∧",
"right": {
"left": {
"left": "user_1",
"op": "=",
"right": 5
},
"op": "∧",
"right": {
"left": "loc_5",
"op": "=",
"right": 1
}
}
}
},
"location": "l"
},
{
"action": "tick",
"destinations": [
{
"assignments": [
{
"comment": "boost_1 <- 0",
"ref": "boost_1",
"value": 0
},
{
"comment": "user_1 <- 4",
"ref": "user_1",
"value": 4
}
],
"location": "l"
}
],
"guard": {
"comment": "(((user_1 = 5) & ((loc_5 = 1) & (t_5 = 0))) & (loc_4 = 0))",
"exp": {
"left": {
"left": {
"left": "loc_4",
"op": "=",
"right": 0
},
"op": "∧",
"right": {
"left": "t_5",
"op": "=",
"right": 0
}
},
"op": "∧",
"right": {
"left": {
"left": "user_1",
"op": "=",
"right": 5
},
"op": "∧",
"right": {
"left": "loc_5",
"op": "=",
"right": 1
}
}
}
},
"location": "l"
},
{
"action": "tick",
"destinations": [
{
"location": "l"
}
],
"guard": {
"comment": "((((((user_1 = 0) & (loc_1 != 0)) & (loc_2 != 0)) & (loc_3 != 0)) & (loc_4 != 0)) & (loc_5 != 0))",
"exp": {
"left": {
"left": {
"left": {
"left": "loc_5",
"op": "≠",
"right": 0
},
"op": "∧",
"right": {
"left": "loc_1",
"op": "≠",
"right": 0
}
},
"op": "∧",
"right": {
"left": {
"left": "loc_3",
"op": "≠",
"right": 0
},
"op": "∧",
"right": {
"left": "loc_2",
"op": "≠",
"right": 0
}
}
},
"op": "∧",
"right": {
"left": {
"left": "loc_4",
"op": "≠",
"right": 0
},
"op": "∧",
"right": {
"left": "user_1",
"op": "=",
"right": 0
}
}
}
},
"location": "l"
}
],
"initial-locations": [
"l"
],
"locations": [
{
"name": "l"
}
],
"name": "Resources",
"variables": []
},
{
"edges": [
{
"action": "tick",
"destinations": [
{
"assignments": [
{
"comment": "t_3 <- (t_3 - 1)",
"ref": "t_3",
"value": {
"left": "t_3",
"op": "-",
"right": 1
}
}
],
"location": "l"
}
],
"guard": {
"comment": "((loc_3 = 2) & (t_3 != 0))",
"exp": {
"left": {
"left": "loc_3",
"op": "=",
"right": 2
},
"op": "∧",
"right": {
"left": "t_3",
"op": "≠",
"right": 0
}
}
},
"location": "l"
},
{
"action": "tick",
"destinations": [
{
"assignments": [
{
"comment": "loc_3 <- 0",
"ref": "loc_3",
"value": 0
}
],
"location": "l"
}
],
"guard": {
"comment": "((loc_3 = 2) & (t_3 = 0))",
"exp": {
"left": {
"left": "loc_3",
"op": "=",
"right": 2
},
"op": "∧",
"right": {
"left": "t_3",
"op": "=",
"right": 0
}
}
},
"location": "l"
},
{
"action": "tick",
"destinations": [
{
"assignments": [
{
"comment": "t_3 <- (max(0, (t_3 - 1)))",
"ref": "t_3",
"value": {
"left": 0,
"op": "max",
"right": {
"left": "t_3",
"op": "-",
"right": 1
}
}
}
],
"location": "l"
}
],
"guard": {
"comment": "((loc_3 = 0) & (user_1 != 3))",
"exp": {
"left": {
"left": "loc_3",
"op": "=",
"right": 0
},
"op": "∧",
"right": {
"left": "user_1",
"op": "≠",
"right": 3
}
}
},
"location": "l"
},
{
"action": "tick",
"destinations": [
{
"assignments": [
{
"comment": "t_3 <- 2",
"ref": "t_3",
"value": 2
},
{
"comment": "loc_3 <- 1",
"ref": "loc_3",
"value": 1
}
],
"location": "l",
"probability": {
"comment": "(1 / 3)",
"exp": {
"left": 1,
"op": "/",
"right": 3
}
}
},
{
"assignments": [
{
"comment": "t_3 <- 3",
"ref": "t_3",
"value": 3
},
{
"comment": "loc_3 <- 1",
"ref": "loc_3",
"value": 1
}
],
"location": "l",
"probability": {
"comment": "(2 / 3)",
"exp": {
"left": 2,
"op": "/",
"right": 3
}
}
}
],
"guard": {
"comment": "((loc_3 = 0) & (user_1 = 3))",
"exp": {
"left": {
"left": "loc_3",
"op": "=",
"right": 0
},
"op": "∧",
"right": {
"left": "user_1",
"op": "=",
"right": 3
}
}
},
"location": "l"
},
{
"action": "tick",
"destinations": [
{
"assignments": [
{
"comment": "t_3 <- (max((t_3 - (boost_1 + 1)), 0))",
"ref": "t_3",
"value": {
"left": {
"left": "t_3",
"op": "-",
"right": {
"left": "boost_1",
"op": "+",
"right": 1
}
},
"op": "max",
"right": 0
}
}
],
"location": "l"
}
],
"guard": {
"comment": "((loc_3 = 1) & (t_3 > 0))",
"exp": {
"left": {
"left": "loc_3",
"op": "=",
"right": 1
},
"op": "∧",
"right": {
"left": "t_3",
"op": ">",
"right": 0
}
}
},
"location": "l"
},
{
"action": "tick",
"destinations": [
{
"assignments": [
{
"comment": "t_3 <- 4",
"ref": "t_3",
"value": 4
},
{
"comment": "loc_3 <- 2",
"ref": "loc_3",
"value": 2
}
],
"location": "l",
"probability": {
"comment": "(2 / 3)",
"exp": {
"left": 2,
"op": "/",
"right": 3
}
}
},
{
"assignments": [
{
"comment": "t_3 <- 5",
"ref": "t_3",
"value": 5
},
{
"comment": "loc_3 <- 2",
"ref": "loc_3",
"value": 2
}
],
"location": "l",
"probability": {
"comment": "(1 / 3)",
"exp": {
"left": 1,
"op": "/",
"right": 3
}
}
}
],
"guard": {
"comment": "((loc_3 = 1) & (t_3 = 0))",
"exp": {
"left": {
"left": "loc_3",
"op": "=",
"right": 1
},
"op": "∧",
"right": {
"left": "t_3",
"op": "=",
"right": 0
}
}
},
"location": "l"
}
],
"initial-locations": [
"l"
],
"locations": [
{
"name": "l"
}
],
"name": "Process_3",
"variables": []
},
{
"edges": [
{
"action": "tick",
"destinations": [
{
"assignments": [
{
"comment": "t_5 <- (t_5 - 1)",
"ref": "t_5",
"value": {
"left": "t_5",
"op": "-",
"right": 1
}
}
],
"location": "l"
}
],
"guard": {
"comment": "((loc_5 = 2) & (t_5 != 0))",
"exp": {
"left": {
"left": "loc_5",
"op": "=",
"right": 2
},
"op": "∧",
"right": {
"left": "t_5",
"op": "≠",
"right": 0
}
}
},
"location": "l"
},
{
"action": "tick",
"destinations": [
{
"assignments": [
{
"comment": "loc_5 <- 0",
"ref": "loc_5",
"value": 0
}
],
"location": "l"
}
],
"guard": {
"comment": "((loc_5 = 2) & (t_5 = 0))",
"exp": {
"left": {
"left": "loc_5",
"op": "=",
"right": 2
},
"op": "∧",
"right": {
"left": "t_5",
"op": "=",
"right": 0
}
}
},
"location": "l"
},
{
"action": "tick",
"destinations": [
{
"assignments": [
{
"comment": "t_5 <- (max(0, (t_5 - 1)))",
"ref": "t_5",
"value": {
"left": 0,
"op": "max",
"right": {
"left": "t_5",
"op": "-",
"right": 1
}
}
}
],
"location": "l"
}
],
"guard": {
"comment": "((loc_5 = 0) & (user_1 != 5))",
"exp": {
"left": {
"left": "loc_5",
"op": "=",
"right": 0
},
"op": "∧",
"right": {
"left": "user_1",
"op": "≠",
"right": 5
}
}
},
"location": "l"
},
{
"action": "tick",
"destinations": [
{
"assignments": [
{
"comment": "loc_5 <- 1",
"ref": "loc_5",
"value": 1
},
{
"comment": "t_5 <- 2",
"ref": "t_5",
"value": 2
}
],
"location": "l",
"probability": {
"comment": "(1 / 3)",
"exp": {
"left": 1,
"op": "/",
"right": 3
}
}
},
{
"assignments": [
{
"comment": "loc_5 <- 1",
"ref": "loc_5",
"value": 1
},
{
"comment": "t_5 <- 3",
"ref": "t_5",
"value": 3
}
],
"location": "l",
"probability": {
"comment": "(2 / 3)",
"exp": {
"left": 2,
"op": "/",
"right": 3
}
}
}
],
"guard": {
"comment": "((loc_5 = 0) & (user_1 = 5))",
"exp": {
"left": {
"left": "loc_5",
"op": "=",
"right": 0
},
"op": "∧",
"right": {
"left": "user_1",
"op": "=",
"right": 5
}
}
},
"location": "l"
},
{
"action": "tick",
"destinations": [
{
"assignments": [
{
"comment": "t_5 <- (max((t_5 - (boost_1 + 1)), 0))",
"ref": "t_5",
"value": {
"left": {
"left": "t_5",
"op": "-",
"right": {
"left": "boost_1",
"op": "+",
"right": 1
}
},
"op": "max",
"right": 0
}
}
],
"location": "l"
}
],
"guard": {
"comment": "((loc_5 = 1) & (t_5 > 0))",
"exp": {
"left": {
"left": "loc_5",
"op": "=",
"right": 1
},
"op": "∧",
"right": {
"left": "t_5",
"op": ">",
"right": 0
}
}
},
"location": "l"
},
{
"action": "tick",
"destinations": [
{
"assignments": [
{
"comment": "loc_5 <- 2",
"ref": "loc_5",
"value": 2
},
{
"comment": "t_5 <- 4",
"ref": "t_5",
"value": 4
}
],
"location": "l",
"probability": {
"comment": "(2 / 3)",
"exp": {
"left": 2,
"op": "/",
"right": 3
}
}
},
{
"assignments": [
{
"comment": "loc_5 <- 2",
"ref": "loc_5",
"value": 2
},
{
"comment": "t_5 <- 5",
"ref": "t_5",
"value": 5
}
],
"location": "l",
"probability": {
"comment": "(1 / 3)",
"exp": {
"left": 1,
"op": "/",
"right": 3
}
}
}
],
"guard": {
"comment": "((loc_5 = 1) & (t_5 = 0))",
"exp": {
"left": {
"left": "loc_5",
"op": "=",
"right": 1
},
"op": "∧",
"right": {
"left": "t_5",
"op": "=",
"right": 0
}
}
},
"location": "l"
}
],
"initial-locations": [
"l"
],
"locations": [
{
"name": "l"
}
],
"name": "Process_5",
"variables": []
},
{
"edges": [
{
"action": "tick",
"destinations": [
{
"assignments": [
{
"comment": "t_4 <- (t_4 - 1)",
"ref": "t_4",
"value": {
"left": "t_4",
"op": "-",
"right": 1
}
}
],
"location": "l"
}
],
"guard": {
"comment": "((loc_4 = 2) & (t_4 != 0))",
"exp": {
"left": {
"left": "loc_4",
"op": "=",
"right": 2
},
"op": "∧",
"right": {
"left": "t_4",
"op": "≠",
"right": 0
}
}
},
"location": "l"
},
{
"action": "tick",
"destinations": [
{
"assignments": [
{
"comment": "loc_4 <- 0",
"ref": "loc_4",
"value": 0
}
],
"location": "l"
}
],
"guard": {
"comment": "((loc_4 = 2) & (t_4 = 0))",
"exp": {
"left": {
"left": "loc_4",
"op": "=",
"right": 2
},
"op": "∧",
"right": {
"left": "t_4",
"op": "=",
"right": 0
}
}
},
"location": "l"
},
{
"action": "tick",
"destinations": [
{
"assignments": [
{
"comment": "t_4 <- (max(0, (t_4 - 1)))",
"ref": "t_4",
"value": {
"left": 0,
"op": "max",
"right": {
"left": "t_4",
"op": "-",
"right": 1
}
}
}
],
"location": "l"
}
],
"guard": {
"comment": "((loc_4 = 0) & (user_1 != 4))",
"exp": {
"left": {
"left": "loc_4",
"op": "=",
"right": 0
},
"op": "∧",
"right": {
"left": "user_1",
"op": "≠",
"right": 4
}
}
},
"location": "l"
},
{
"action": "tick",
"destinations": [
{
"assignments": [
{
"comment": "t_4 <- 2",
"ref": "t_4",
"value": 2
},
{
"comment": "loc_4 <- 1",
"ref": "loc_4",
"value": 1
}
],
"location": "l",
"probability": {
"comment": "(1 / 3)",
"exp": {
"left": 1,
"op": "/",
"right": 3
}
}
},
{
"assignments": [
{
"comment": "t_4 <- 3",
"ref": "t_4",
"value": 3
},
{
"comment": "loc_4 <- 1",
"ref": "loc_4",
"value": 1
}
],
"location": "l",
"probability": {
"comment": "(2 / 3)",
"exp": {
"left": 2,
"op": "/",
"right": 3
}
}
}
],
"guard": {
"comment": "((loc_4 = 0) & (user_1 = 4))",
"exp": {
"left": {
"left": "loc_4",
"op": "=",
"right": 0
},
"op": "∧",
"right": {
"left": "user_1",
"op": "=",
"right": 4
}
}
},
"location": "l"
},
{
"action": "tick",
"destinations": [
{
"assignments": [
{
"comment": "t_4 <- (max((t_4 - (boost_1 + 1)), 0))",
"ref": "t_4",
"value": {
"left": {
"left": "t_4",
"op": "-",
"right": {
"left": "boost_1",
"op": "+",
"right": 1
}
},
"op": "max",
"right": 0
}
}
],
"location": "l"
}
],
"guard": {
"comment": "((loc_4 = 1) & (t_4 > 0))",
"exp": {
"left": {
"left": "loc_4",
"op": "=",
"right": 1
},
"op": "∧",
"right": {
"left": "t_4",
"op": ">",
"right": 0
}
}
},
"location": "l"
},
{
"action": "tick",
"destinations": [
{
"assignments": [
{
"comment": "t_4 <- 4",
"ref": "t_4",
"value": 4
},
{
"comment": "loc_4 <- 2",
"ref": "loc_4",
"value": 2
}
],
"location": "l",
"probability": {
"comment": "(2 / 3)",
"exp": {
"left": 2,
"op": "/",
"right": 3
}
}
},
{
"assignments": [
{
"comment": "t_4 <- 5",
"ref": "t_4",
"value": 5
},
{
"comment": "loc_4 <- 2",
"ref": "loc_4",
"value": 2
}
],
"location": "l",
"probability": {
"comment": "(1 / 3)",
"exp": {
"left": 1,
"op": "/",
"right": 3
}
}
}
],
"guard": {
"comment": "((loc_4 = 1) & (t_4 = 0))",
"exp": {
"left": {
"left": "loc_4",
"op": "=",
"right": 1
},
"op": "∧",
"right": {
"left": "t_4",
"op": "=",
"right": 0
}
}
},
"location": "l"
}
],
"initial-locations": [
"l"
],
"locations": [
{
"name": "l"
}
],
"name": "Process_4",
"variables": []
}
],
"constants": [
{
"name": "B",
"type": "int",
"value": 11
},
{
"name": "energy_capacity",
"type": "int",
"value": 250
},
{
"name": "t_max",
"type": "int",
"value": 9
},
{
"name": "undef",
"type": "int",
"value": 0
},
{
"name": "ncrit",
"type": "int",
"value": 2
},
{
"name": "wait",
"type": "int",
"value": 0
},
{
"name": "crit",
"type": "int",
"value": 1
},
{
"name": "none",
"type": "int",
"value": 0
},
{
"name": "process_1",
"type": "int",
"value": 1
},
{
"name": "process_2",
"type": "int",
"value": 2
},
{
"name": "process_3",
"type": "int",
"value": 3
},
{
"name": "process_4",
"type": "int",
"value": 4
},
{
"name": "process_5",
"type": "int",
"value": 5
},
{
"name": "m_1",
"type": "int",
"value": 1
},
{
"name": "m_2",
"type": "int",
"value": 1
},
{
"name": "m_3",
"type": "int",
"value": 2
},
{
"name": "m_4",
"type": "int",
"value": 1
},
{
"name": "m_5",
"type": "int",
"value": 1
},
{
"name": "boost_multiplicator",
"type": "int",
"value": 3
}
],
"features": [
"derived-operators",
"functions"
],
"functions": [
{
"body": {
"left": {
"left": "loc_1",
"op": "=",
"right": 1
},
"op": "∧",
"right": {
"left": "t_1",
"op": "=",
"right": 0
}
},
"name": "process_1_finishes",
"parameters": [],
"type": "bool"
},
{
"body": {
"left": {
"left": {
"left": "loc_1",
"op": "=",
"right": 1
},
"op": "∧",
"right": {
"left": "t_1",
"op": "=",
"right": 0
}
},
"op": "∧",
"right": "failure_1"
},
"name": "localFailure",
"parameters": [],
"type": "bool"
},
{
"body": {
"left": {
"left": "loc_2",
"op": "=",
"right": 1
},
"op": "∧",
"right": {
"left": "t_2",
"op": "=",
"right": 0
}
},
"name": "process_2_finishes",
"parameters": [],
"type": "bool"
},
{
"body": {
"exp": {
"left": {
"left": {
"left": "loc_1",
"op": "=",
"right": 1
},
"op": "∧",
"right": {
"left": "t_1",
"op": "=",
"right": 0
}
},
"op": "∧",
"right": "failure_1"
},
"op": "¬"
},
"name": "noLocalFailure",
"parameters": [],
"type": "bool"
},
{
"body": {
"left": {
"left": "loc_5",
"op": "=",
"right": 1
},
"op": "∧",
"right": {
"left": "t_5",
"op": "=",
"right": 0
}
},
"name": "process_5_finishes",
"parameters": [],
"type": "bool"
},
{
"body": {
"left": {
"left": "loc_3",
"op": "=",
"right": 1
},
"op": "∧",
"right": {
"left": "t_3",
"op": "=",
"right": 0
}
},
"name": "process_3_finishes",
"parameters": [],
"type": "bool"
},
{
"body": {
"left": {
"left": "loc_4",
"op": "=",
"right": 1
},
"op": "∧",
"right": {
"left": "t_4",
"op": "=",
"right": 0
}
},
"name": "process_4_finishes",
"parameters": [],
"type": "bool"
}
],
"jani-version": 1,
"name": "model",
"properties": [
{
"expression": {
"fun": "values",
"op": "filter",
"states": {
"op": "initial"
},
"values": {
"accumulate": [
"steps"
],
"exp": "utilityLocal",
"op": "Emax",
"reach": "emptyBattery"
}
},
"name": "ExpUtil"
}
],
"restrict-initial": {
"exp": true
},
"system": {
"elements": [
{
"automaton": "Battery"
},
{
"automaton": "Process_1"
},
{
"automaton": "Process_2"
},
{
"automaton": "Resources"
},
{
"automaton": "Process_3"
},
{
"automaton": "Process_5"
},
{
"automaton": "Process_4"
}
],
"syncs": [
{
"result": "tick",
"synchronise": [
"tick",
"tick",
"tick",
"tick",
"tick",
"tick",
"tick"
]
}
]
},
"type": "mdp",
"variables": [
{
"initial-value": false,
"name": "emptyBattery",
"transient": true,
"type": "bool"
},
{
"initial-value": 0.0,
"name": "utilityLocal",
"transient": true,
"type": "real"
},
{
"initial-value": 250,
"name": "battery_load",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 250
}
},
{
"initial-value": 2,
"name": "loc_1",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 2
}
},
{
"initial-value": 0,
"name": "t_1",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 9
}
},
{
"initial-value": false,
"name": "failure_1",
"type": "bool"
},
{
"initial-value": 0,
"name": "t_2",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 9
}
},
{
"initial-value": 2,
"name": "loc_2",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 2
}
},
{
"initial-value": 0,
"name": "boost_1",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 1
}
},
{
"initial-value": 0,
"name": "user_1",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 5
}
},
{
"initial-value": 0,
"name": "t_3",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 9
}
},
{
"initial-value": 2,
"name": "loc_3",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 2
}
},
{
"initial-value": 2,
"name": "loc_5",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 2
}
},
{
"initial-value": 0,
"name": "t_5",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 9
}
},
{
"initial-value": 0,
"name": "t_4",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 9
}
},
{
"initial-value": 2,
"name": "loc_4",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 2
}
}
]
}