{
"actions": [
{
"name": "NewFile"
},
{
"name": "SyncWait"
},
{
"name": "TO_Ack"
},
{
"name": "TO_Msg"
},
{
"name": "aA"
},
{
"name": "aB"
},
{
"name": "aF"
},
{
"name": "aG"
}
],
"automata": [
{
"edges": [
{
"destinations": [
{
"assignments": [
{
"ref": "s",
"value": 5
},
{
"ref": "srep",
"value": 1
}
],
"location": "l"
}
],
"guard": {
"comment": "(((s = 3) & (nrtr = MAX)) & (i < N))",
"exp": {
"left": {
"left": {
"left": "s",
"op": "=",
"right": 3
},
"op": "∧",
"right": {
"left": "nrtr",
"op": "=",
"right": "MAX"
}
},
"op": "∧",
"right": {
"left": "i",
"op": "<",
"right": "N"
}
}
},
"location": "l"
},
{
"destinations": [
{
"assignments": [
{
"ref": "s",
"value": 5
},
{
"ref": "srep",
"value": 2
}
],
"location": "l"
}
],
"guard": {
"comment": "(((s = 3) & (nrtr = MAX)) & (i = N))",
"exp": {
"left": {
"left": {
"left": "s",
"op": "=",
"right": 3
},
"op": "∧",
"right": {
"left": "nrtr",
"op": "=",
"right": "MAX"
}
},
"op": "∧",
"right": {
"left": "i",
"op": "=",
"right": "N"
}
}
},
"location": "l"
},
{
"destinations": [
{
"assignments": [
{
"ref": "s",
"value": 1
},
{
"ref": "i",
"value": {
"left": "i",
"op": "+",
"right": 1
}
}
],
"location": "l"
}
],
"guard": {
"comment": "((s = 4) & (i < N))",
"exp": {
"left": {
"left": "s",
"op": "=",
"right": 4
},
"op": "∧",
"right": {
"left": "i",
"op": "<",
"right": "N"
}
}
},
"location": "l"
},
{
"destinations": [
{
"assignments": [
{
"ref": "s",
"value": 0
},
{
"ref": "srep",
"value": 3
}
],
"location": "l"
}
],
"guard": {
"comment": "((s = 4) & (i = N))",
"exp": {
"left": {
"left": "s",
"op": "=",
"right": 4
},
"op": "∧",
"right": {
"left": "i",
"op": "=",
"right": "N"
}
}
},
"location": "l"
},
{
"action": "NewFile",
"destinations": [
{
"assignments": [
{
"ref": "s",
"value": 1
},
{
"ref": "srep",
"value": 0
},
{
"ref": "i",
"value": 1
}
],
"location": "l"
}
],
"guard": {
"comment": "(s = 0)",
"exp": {
"left": "s",
"op": "=",
"right": 0
}
},
"location": "l"
},
{
"action": "SyncWait",
"destinations": [
{
"assignments": [
{
"ref": "s",
"value": 6
}
],
"location": "l"
}
],
"guard": {
"comment": "(s = 5)",
"exp": {
"left": "s",
"op": "=",
"right": 5
}
},
"location": "l"
},
{
"action": "SyncWait",
"destinations": [
{
"assignments": [
{
"ref": "s_ab",
"value": false
},
{
"ref": "s",
"value": 0
}
],
"location": "l"
}
],
"guard": {
"comment": "(s = 6)",
"exp": {
"left": "s",
"op": "=",
"right": 6
}
},
"location": "l"
},
{
"action": "TO_Ack",
"destinations": [
{
"assignments": [
{
"ref": "s",
"value": 3
}
],
"location": "l"
}
],
"guard": {
"comment": "(s = 2)",
"exp": {
"left": "s",
"op": "=",
"right": 2
}
},
"location": "l"
},
{
"action": "TO_Msg",
"destinations": [
{
"assignments": [
{
"ref": "s",
"value": 3
}
],
"location": "l"
}
],
"guard": {
"comment": "(s = 2)",
"exp": {
"left": "s",
"op": "=",
"right": 2
}
},
"location": "l"
},
{
"action": "aB",
"destinations": [
{
"assignments": [
{
"ref": "s_ab",
"value": {
"exp": "s_ab",
"op": "¬"
}
},
{
"ref": "s",
"value": 4
}
],
"location": "l"
}
],
"guard": {
"comment": "(s = 2)",
"exp": {
"left": "s",
"op": "=",
"right": 2
}
},
"location": "l"
},
{
"action": "aF",
"destinations": [
{
"assignments": [
{
"ref": "bs",
"value": "s_ab"
},
{
"ref": "fs",
"value": {
"left": "i",
"op": "=",
"right": 1
}
},
{
"ref": "ls",
"value": {
"left": "i",
"op": "=",
"right": "N"
}
},
{
"ref": "s",
"value": 2
},
{
"ref": "nrtr",
"value": 0
}
],
"location": "l"
}
],
"guard": {
"comment": "(s = 1)",
"exp": {
"left": "s",
"op": "=",
"right": 1
}
},
"location": "l"
},
{
"action": "aF",
"destinations": [
{
"assignments": [
{
"ref": "bs",
"value": "s_ab"
},
{
"ref": "fs",
"value": {
"left": "i",
"op": "=",
"right": 1
}
},
{
"ref": "ls",
"value": {
"left": "i",
"op": "=",
"right": "N"
}
},
{
"ref": "s",
"value": 2
},
{
"ref": "nrtr",
"value": {
"left": "nrtr",
"op": "+",
"right": 1
}
}
],
"location": "l"
}
],
"guard": {
"comment": "((s = 3) & (nrtr < MAX))",
"exp": {
"left": {
"left": "s",
"op": "=",
"right": 3
},
"op": "∧",
"right": {
"left": "nrtr",
"op": "<",
"right": "MAX"
}
}
},
"location": "l"
}
],
"initial-locations": [
"l"
],
"locations": [
{
"name": "l"
}
],
"name": "sender",
"variables": []
},
{
"edges": [
{
"destinations": [
{
"assignments": [
{
"ref": "r_ab",
"value": "br"
},
{
"ref": "r",
"value": 2
}
],
"location": "l"
}
],
"guard": {
"comment": "(r = 1)",
"exp": {
"left": "r",
"op": "=",
"right": 1
}
},
"location": "l"
},
{
"destinations": [
{
"assignments": [
{
"ref": "r",
"value": 3
},
{
"ref": "rrep",
"value": 1
}
],
"location": "l"
}
],
"guard": {
"comment": "((((r = 2) & (r_ab = br)) & (fr = true)) & (lr = false))",
"exp": {
"left": {
"left": {
"left": {
"left": "r",
"op": "=",
"right": 2
},
"op": "∧",
"right": {
"left": "r_ab",
"op": "=",
"right": "br"
}
},
"op": "∧",
"right": {
"left": "fr",
"op": "=",
"right": true
}
},
"op": "∧",
"right": {
"left": "lr",
"op": "=",
"right": false
}
}
},
"location": "l"
},
{
"destinations": [
{
"assignments": [
{
"ref": "r",
"value": 3
},
{
"ref": "rrep",
"value": 2
}
],
"location": "l"
}
],
"guard": {
"comment": "((((r = 2) & (r_ab = br)) & (fr = false)) & (lr = false))",
"exp": {
"left": {
"left": {
"left": {
"left": "r",
"op": "=",
"right": 2
},
"op": "∧",
"right": {
"left": "r_ab",
"op": "=",
"right": "br"
}
},
"op": "∧",
"right": {
"left": "fr",
"op": "=",
"right": false
}
},
"op": "∧",
"right": {
"left": "lr",
"op": "=",
"right": false
}
}
},
"location": "l"
},
{
"destinations": [
{
"assignments": [
{
"ref": "r",
"value": 3
},
{
"ref": "rrep",
"value": 3
}
],
"location": "l"
}
],
"guard": {
"comment": "((((r = 2) & (r_ab = br)) & (fr = false)) & (lr = true))",
"exp": {
"left": {
"left": {
"left": {
"left": "r",
"op": "=",
"right": 2
},
"op": "∧",
"right": {
"left": "r_ab",
"op": "=",
"right": "br"
}
},
"op": "∧",
"right": {
"left": "fr",
"op": "=",
"right": false
}
},
"op": "∧",
"right": {
"left": "lr",
"op": "=",
"right": true
}
}
},
"location": "l"
},
{
"action": "SyncWait",
"destinations": [
{
"assignments": [
{
"ref": "r",
"value": 0
}
],
"location": "l"
}
],
"guard": {
"comment": "(r = 0)",
"exp": {
"left": "r",
"op": "=",
"right": 0
}
},
"location": "l"
},
{
"action": "SyncWait",
"destinations": [
{
"assignments": [
{
"ref": "r",
"value": 5
}
],
"location": "l"
}
],
"guard": {
"comment": "((r = 4) & (ls = true))",
"exp": {
"left": {
"left": "r",
"op": "=",
"right": 4
},
"op": "∧",
"right": {
"left": "ls",
"op": "=",
"right": true
}
}
},
"location": "l"
},
{
"action": "SyncWait",
"destinations": [
{
"assignments": [
{
"ref": "r",
"value": 5
},
{
"ref": "rrep",
"value": 4
}
],
"location": "l"
}
],
"guard": {
"comment": "((r = 4) & (ls = false))",
"exp": {
"left": {
"left": "r",
"op": "=",
"right": 4
},
"op": "∧",
"right": {
"left": "ls",
"op": "=",
"right": false
}
}
},
"location": "l"
},
{
"action": "SyncWait",
"destinations": [
{
"assignments": [
{
"ref": "r",
"value": 0
},
{
"ref": "rrep",
"value": 0
}
],
"location": "l"
}
],
"guard": {
"comment": "(r = 5)",
"exp": {
"left": "r",
"op": "=",
"right": 5
}
},
"location": "l"
},
{
"action": "aA",
"destinations": [
{
"assignments": [
{
"ref": "r_ab",
"value": {
"exp": "r_ab",
"op": "¬"
}
},
{
"ref": "r",
"value": 4
}
],
"location": "l"
}
],
"guard": {
"comment": "(r = 3)",
"exp": {
"left": "r",
"op": "=",
"right": 3
}
},
"location": "l"
},
{
"action": "aA",
"destinations": [
{
"assignments": [
{
"ref": "r",
"value": 4
}
],
"location": "l"
}
],
"guard": {
"comment": "((r = 2) & !((r_ab = br)))",
"exp": {
"left": {
"left": "r",
"op": "=",
"right": 2
},
"op": "∧",
"right": {
"exp": {
"left": "r_ab",
"op": "=",
"right": "br"
},
"op": "¬"
}
}
},
"location": "l"
},
{
"action": "aG",
"destinations": [
{
"assignments": [
{
"ref": "fr",
"value": "fs"
},
{
"ref": "lr",
"value": "ls"
},
{
"ref": "br",
"value": "bs"
},
{
"ref": "recv",
"value": "T"
},
{
"ref": "r",
"value": 1
}
],
"location": "l"
}
],
"guard": {
"comment": "(r = 0)",
"exp": {
"left": "r",
"op": "=",
"right": 0
}
},
"location": "l"
},
{
"action": "aG",
"destinations": [
{
"assignments": [
{
"ref": "fr",
"value": "fs"
},
{
"ref": "lr",
"value": "ls"
},
{
"ref": "br",
"value": "bs"
},
{
"ref": "recv",
"value": "T"
},
{
"ref": "r",
"value": 2
}
],
"location": "l"
}
],
"guard": {
"comment": "(r = 4)",
"exp": {
"left": "r",
"op": "=",
"right": 4
}
},
"location": "l"
}
],
"initial-locations": [
"l"
],
"locations": [
{
"name": "l"
}
],
"name": "receiver",
"variables": []
},
{
"edges": [
{
"action": "NewFile",
"destinations": [
{
"assignments": [
{
"ref": "T",
"value": true
}
],
"location": "l"
}
],
"guard": {
"comment": "(T = false)",
"exp": {
"left": "T",
"op": "=",
"right": false
}
},
"location": "l"
}
],
"initial-locations": [
"l"
],
"locations": [
{
"name": "l"
}
],
"name": "checker",
"variables": []
},
{
"edges": [
{
"action": "TO_Msg",
"destinations": [
{
"assignments": [
{
"ref": "k",
"value": 0
}
],
"location": "l"
}
],
"guard": {
"comment": "(k = 2)",
"exp": {
"left": "k",
"op": "=",
"right": 2
}
},
"location": "l"
},
{
"action": "aF",
"destinations": [
{
"assignments": [
{
"ref": "k",
"value": 1
}
],
"location": "l",
"probability": {
"comment": "49/50",
"exp": 0.98
}
},
{
"assignments": [
{
"ref": "k",
"value": 2
}
],
"location": "l",
"probability": {
"comment": "1/50",
"exp": 0.02
}
}
],
"guard": {
"comment": "(k = 0)",
"exp": {
"left": "k",
"op": "=",
"right": 0
}
},
"location": "l"
},
{
"action": "aG",
"destinations": [
{
"assignments": [
{
"ref": "k",
"value": 0
}
],
"location": "l"
}
],
"guard": {
"comment": "(k = 1)",
"exp": {
"left": "k",
"op": "=",
"right": 1
}
},
"location": "l"
}
],
"initial-locations": [
"l"
],
"locations": [
{
"name": "l"
}
],
"name": "channelK",
"variables": []
},
{
"edges": [
{
"action": "TO_Ack",
"destinations": [
{
"assignments": [
{
"ref": "l",
"value": 0
}
],
"location": "l"
}
],
"guard": {
"comment": "(l = 2)",
"exp": {
"left": "l",
"op": "=",
"right": 2
}
},
"location": "l"
},
{
"action": "aA",
"destinations": [
{
"assignments": [
{
"ref": "l",
"value": 1
}
],
"location": "l",
"probability": {
"comment": "99/100",
"exp": 0.99
}
},
{
"assignments": [
{
"ref": "l",
"value": 2
}
],
"location": "l",
"probability": {
"comment": "1/100",
"exp": 0.01
}
}
],
"guard": {
"comment": "(l = 0)",
"exp": {
"left": "l",
"op": "=",
"right": 0
}
},
"location": "l"
},
{
"action": "aB",
"destinations": [
{
"assignments": [
{
"ref": "l",
"value": 0
}
],
"location": "l"
}
],
"guard": {
"comment": "(l = 1)",
"exp": {
"left": "l",
"op": "=",
"right": 1
}
},
"location": "l"
}
],
"initial-locations": [
"l"
],
"locations": [
{
"name": "l"
}
],
"name": "channelL",
"variables": []
}
],
"constants": [
{
"name": "N",
"type": "int"
},
{
"name": "MAX",
"type": "int"
}
],
"features": [
"derived-operators"
],
"jani-version": 1,
"name": "jani_from_prism",
"properties": [],
"restrict-initial": {
"exp": true
},
"system": {
"elements": [
{
"automaton": "sender"
},
{
"automaton": "receiver"
},
{
"automaton": "checker"
},
{
"automaton": "channelK"
},
{
"automaton": "channelL"
}
],
"syncs": [
{
"result": "NewFile",
"synchronise": [
"NewFile",
null,
"NewFile",
null,
null
]
},
{
"result": "SyncWait",
"synchronise": [
"SyncWait",
"SyncWait",
null,
null,
null
]
},
{
"result": "TO_Ack",
"synchronise": [
"TO_Ack",
null,
null,
null,
"TO_Ack"
]
},
{
"result": "TO_Msg",
"synchronise": [
"TO_Msg",
null,
null,
"TO_Msg",
null
]
},
{
"result": "aA",
"synchronise": [
null,
"aA",
null,
null,
"aA"
]
},
{
"result": "aB",
"synchronise": [
"aB",
null,
null,
null,
"aB"
]
},
{
"result": "aF",
"synchronise": [
"aF",
null,
null,
"aF",
null
]
},
{
"result": "aG",
"synchronise": [
null,
"aG",
null,
"aG",
null
]
}
]
},
"type": "dtmc",
"variables": [
{
"initial-value": 0,
"name": "s",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 6
}
},
{
"initial-value": 0,
"name": "srep",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 3
}
},
{
"initial-value": 0,
"name": "nrtr",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": "MAX"
}
},
{
"initial-value": 0,
"name": "i",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": "N"
}
},
{
"initial-value": false,
"name": "bs",
"type": "bool"
},
{
"initial-value": false,
"name": "s_ab",
"type": "bool"
},
{
"initial-value": false,
"name": "fs",
"type": "bool"
},
{
"initial-value": false,
"name": "ls",
"type": "bool"
},
{
"initial-value": 0,
"name": "r",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 5
}
},
{
"initial-value": 0,
"name": "rrep",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 4
}
},
{
"initial-value": false,
"name": "fr",
"type": "bool"
},
{
"initial-value": false,
"name": "lr",
"type": "bool"
},
{
"initial-value": false,
"name": "br",
"type": "bool"
},
{
"initial-value": false,
"name": "r_ab",
"type": "bool"
},
{
"initial-value": false,
"name": "recv",
"type": "bool"
},
{
"initial-value": false,
"name": "T",
"type": "bool"
},
{
"initial-value": 0,
"name": "k",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 2
}
},
{
"initial-value": 0,
"name": "l",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 2
}
}
]
}