You can not select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
1401 lines
46 KiB
1401 lines
46 KiB
{
|
|
"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
|
|
}
|
|
}
|
|
]
|
|
}
|