Commit 68466b67 authored by Lars Schieffer's avatar Lars Schieffer
Browse files

update tests

parent 49446fb7
{
"actions": [
{
"name": "NewFile"
},
{
"name": "SyncWait"
},
{
"name": "TO_Ack"
},
{
"name": "TO_Msg"
},
{
"name": "aA"
},
{
"name": "aB"
},
{
"name": "aF"
},
{
"name": "aG"
}
],
"automata": [
{
"edges": [
{
"destinations": [
{
"assignments": [
{
"comment": "s <- 5",
"ref": "s",
"value": 5
},
{
"comment": "srep <- 1",
"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": [
{
"comment": "s <- 5",
"ref": "s",
"value": 5
},
{
"comment": "srep <- 2",
"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": [
{
"comment": "s <- 1",
"ref": "s",
"value": 1
},
{
"comment": "i <- (i + 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": [
{
"comment": "s <- 0",
"ref": "s",
"value": 0
},
{
"comment": "srep <- 3",
"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": [
{
"comment": "s <- 1",
"ref": "s",
"value": 1
},
{
"comment": "srep <- 0",
"ref": "srep",
"value": 0
},
{
"comment": "i <- 1",
"ref": "i",
"value": 1
}
],
"location": "l"
}
],
"guard": {
"comment": "(s = 0)",
"exp": {
"left": "s",
"op": "=",
"right": 0
}
},
"location": "l"
},
{
"action": "SyncWait",
"destinations": [
{
"assignments": [
{
"comment": "s <- 6",
"ref": "s",
"value": 6
}
],
"location": "l"
}
],
"guard": {
"comment": "(s = 5)",
"exp": {
"left": "s",
"op": "=",
"right": 5
}
},
"location": "l"
},
{
"action": "SyncWait",
"destinations": [
{
"assignments": [
{
"comment": "s_ab <- false",
"ref": "s_ab",
"value": false
},
{
"comment": "s <- 0",
"ref": "s",
"value": 0
}
],
"location": "l"
}
],
"guard": {
"comment": "(s = 6)",
"exp": {
"left": "s",
"op": "=",
"right": 6
}
},
"location": "l"
},
{
"action": "TO_Ack",
"destinations": [
{
"assignments": [
{
"comment": "s <- 3",
"ref": "s",
"value": 3
}
],
"location": "l"
}
],
"guard": {
"comment": "(s = 2)",
"exp": {
"left": "s",
"op": "=",
"right": 2
}
},
"location": "l"
},
{
"action": "TO_Msg",
"destinations": [
{
"assignments": [
{
"comment": "s <- 3",
"ref": "s",
"value": 3
}
],
"location": "l"
}
],
"guard": {
"comment": "(s = 2)",
"exp": {
"left": "s",
"op": "=",
"right": 2
}
},
"location": "l"
},
{
"action": "aB",
"destinations": [
{
"assignments": [
{
"comment": "s_ab <- !(s_ab)",
"ref": "s_ab",
"value": {
"exp": "s_ab",
"op": "¬"
}
},
{
"comment": "s <- 4",
"ref": "s",
"value": 4
}
],
"location": "l"
}
],
"guard": {
"comment": "(s = 2)",
"exp": {
"left": "s",
"op": "=",
"right": 2
}
},
"location": "l"
},
{
"action": "aF",
"destinations": [
{
"assignments": [
{
"comment": "bs <- s_ab",
"ref": "bs",
"value": "s_ab"
},
{
"comment": "fs <- (i = 1)",
"ref": "fs",
"value": {
"left": "i",
"op": "=",
"right": 1
}
},
{
"comment": "ls <- (i = N)",
"ref": "ls",
"value": {
"left": "i",
"op": "=",
"right": "N"
}
},
{
"comment": "s <- 2",
"ref": "s",
"value": 2
},
{
"comment": "nrtr <- 0",
"ref": "nrtr",
"value": 0
}
],
"location": "l"
}
],
"guard": {
"comment": "(s = 1)",
"exp": {
"left": "s",
"op": "=",
"right": 1
}
},
"location": "l"
},
{
"action": "aF",
"destinations": [
{
"assignments": [
{
"comment": "bs <- s_ab",
"ref": "bs",
"value": "s_ab"
},
{
"comment": "fs <- (i = 1)",
"ref": "fs",
"value": {
"left": "i",
"op": "=",
"right": 1
}
},
{
"comment": "ls <- (i = N)",
"ref": "ls",
"value": {
"left": "i",
"op": "=",
"right": "N"
}
},
{
"comment": "s <- 2",
"ref": "s",
"value": 2
},
{
"comment": "nrtr <- (nrtr + 1)",
"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": [
{
"comment": "r_ab <- br",
"ref": "r_ab",
"value": "br"
},
{
"comment": "r <- 2",
"ref": "r",
"value": 2
}
],
"location": "l"
}
],
"guard": {
"comment": "(r = 1)",
"exp": {
"left": "r",
"op": "=",
"right": 1
}
},
"location": "l"
},
{
"destinations": [
{
"assignments": [
{
"comment": "r <- 3",
"ref": "r",
"value": 3
},
{
"comment": "rrep <- 1",
"ref": "rrep",
"value": 1
}
],
"location": "l"
}
],
"guard": {
"comment": "((((r = 2) & (r_ab = br)) & (fr = true)) & (lr = false))",
"exp": {
"left": {
"left": {
"left": "lr",
"op": "=",
"right": false
},
"op": "∧",
"right": {
"left": "r_ab",
"op": "=",
"right": "br"
}
},
"op": "∧",
"right": {
"left": {
"left": "fr",
"op": "=",
"right": true
},
"op": "∧",
"right": {
"left": "r",
"op": "=",
"right": 2
}
}
}
},
"location": "l"
},
{
"destinations": [
{
"assignments": [
{
"comment": "r <- 3",
"ref": "r",
"value": 3
},
{
"comment": "rrep <- 2",
"ref": "rrep",
"value": 2
}
],
"location": "l"
}
],
"guard": {
"comment": "((((r = 2) & (r_ab = br)) & (fr = false)) & (lr = false))",
"exp": {
"left": {
"left": {
"left": "lr",
"op": "=",
"right": false
},
"op": "∧",
"right": {
"left": "r_ab",
"op": "=",
"right": "br"
}
},
"op": "∧",
"right": {
"left": {
"left": "fr",
"op": "=",
"right": false
},
"op": "∧",
"right": {
"left": "r",
"op": "=",
"right": 2
}
}
}
},
"location": "l"
},
{
"destinations": [
{
"assignments": [
{
"comment": "r <- 3",
"ref": "r",
"value": 3
},
{
"comment": "rrep <- 3",
"ref": "rrep",
"value": 3
}
],
"location": "l"
}
],
"guard": {
"comment": "((((r = 2) & (r_ab = br)) & (fr = false)) & (lr = true))",
"exp": {
"left": {
"left": {
"left": "lr",
"op": "=",
"right": true
},
"op": "∧",