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.
2033 lines
69 KiB
2033 lines
69 KiB
|
|
{
|
|
"jani-version":1,
|
|
"name":"brp",
|
|
"type":"dtmc",
|
|
"features":[
|
|
"derived-operators"
|
|
],
|
|
"actions":[
|
|
{
|
|
"name":"NewFile"
|
|
},
|
|
{
|
|
"name":"aF"
|
|
},
|
|
{
|
|
"name":"aB"
|
|
},
|
|
{
|
|
"name":"TO_Msg"
|
|
},
|
|
{
|
|
"name":"TO_Ack"
|
|
},
|
|
{
|
|
"name":"τ"
|
|
},
|
|
{
|
|
"name":"SyncWait"
|
|
},
|
|
{
|
|
"name":"aG"
|
|
},
|
|
{
|
|
"name":"aA"
|
|
}
|
|
],
|
|
"constants":[
|
|
{
|
|
"name":"N",
|
|
"type":"int"
|
|
},
|
|
{
|
|
"name":"MAX",
|
|
"type":"int"
|
|
}
|
|
],
|
|
"variables":[
|
|
{
|
|
"name":"s",
|
|
"type":{
|
|
"kind":"bounded",
|
|
"base":"int",
|
|
"lower-bound":0,
|
|
"upper-bound":6
|
|
}
|
|
},
|
|
{
|
|
"name":"srep",
|
|
"type":{
|
|
"kind":"bounded",
|
|
"base":"int",
|
|
"lower-bound":0,
|
|
"upper-bound":3
|
|
}
|
|
},
|
|
{
|
|
"name":"nrtr",
|
|
"type":{
|
|
"kind":"bounded",
|
|
"base":"int",
|
|
"lower-bound":0,
|
|
"upper-bound":"MAX"
|
|
}
|
|
},
|
|
{
|
|
"name":"i",
|
|
"type":{
|
|
"kind":"bounded",
|
|
"base":"int",
|
|
"lower-bound":0,
|
|
"upper-bound":"N"
|
|
}
|
|
},
|
|
{
|
|
"name":"bs",
|
|
"type":"bool"
|
|
},
|
|
{
|
|
"name":"s_ab",
|
|
"type":"bool"
|
|
},
|
|
{
|
|
"name":"fs",
|
|
"type":"bool"
|
|
},
|
|
{
|
|
"name":"ls",
|
|
"type":"bool"
|
|
},
|
|
{
|
|
"name":"r",
|
|
"type":{
|
|
"kind":"bounded",
|
|
"base":"int",
|
|
"lower-bound":0,
|
|
"upper-bound":5
|
|
}
|
|
},
|
|
{
|
|
"name":"rrep",
|
|
"type":{
|
|
"kind":"bounded",
|
|
"base":"int",
|
|
"lower-bound":0,
|
|
"upper-bound":4
|
|
}
|
|
},
|
|
{
|
|
"name":"fr",
|
|
"type":"bool"
|
|
},
|
|
{
|
|
"name":"lr",
|
|
"type":"bool"
|
|
},
|
|
{
|
|
"name":"br",
|
|
"type":"bool"
|
|
},
|
|
{
|
|
"name":"r_ab",
|
|
"type":"bool"
|
|
},
|
|
{
|
|
"name":"recv",
|
|
"type":"bool"
|
|
},
|
|
{
|
|
"name":"T",
|
|
"type":"bool"
|
|
},
|
|
{
|
|
"name":"k",
|
|
"type":{
|
|
"kind":"bounded",
|
|
"base":"int",
|
|
"lower-bound":0,
|
|
"upper-bound":2
|
|
}
|
|
},
|
|
{
|
|
"name":"l",
|
|
"type":{
|
|
"kind":"bounded",
|
|
"base":"int",
|
|
"lower-bound":0,
|
|
"upper-bound":2
|
|
}
|
|
},
|
|
{
|
|
"name":"reward_",
|
|
"type":"real",
|
|
"initial-value":0.0,
|
|
"transient":true
|
|
}
|
|
],
|
|
"restrict-initial":{
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"s",
|
|
"right":0
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"srep",
|
|
"right":0
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"nrtr",
|
|
"right":0
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"i",
|
|
"right":0
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"bs",
|
|
"right":false
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"s_ab",
|
|
"right":false
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"fs",
|
|
"right":false
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"ls",
|
|
"right":false
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"r",
|
|
"right":0
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"rrep",
|
|
"right":0
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"fr",
|
|
"right":false
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"lr",
|
|
"right":false
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"br",
|
|
"right":false
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"r_ab",
|
|
"right":false
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"recv",
|
|
"right":false
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"T",
|
|
"right":false
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"k",
|
|
"right":0
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"l",
|
|
"right":0
|
|
}
|
|
}
|
|
},
|
|
"properties":[
|
|
{
|
|
"name":"Property_brp_0",
|
|
"expression":{
|
|
"op":"filter",
|
|
"fun":"min",
|
|
"values":{
|
|
"op":"Pmax",
|
|
"exp":{
|
|
"op":"U",
|
|
"left":true,
|
|
"right":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"srep",
|
|
"right":1
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"rrep",
|
|
"right":3
|
|
}
|
|
},
|
|
"right":"recv"
|
|
}
|
|
}
|
|
},
|
|
"states":{
|
|
"op":"initial"
|
|
}
|
|
},
|
|
"comment":"P=?[ F srep=1 & rrep=3 & recv ]"
|
|
},
|
|
{
|
|
"name":"Property_brp_1",
|
|
"expression":{
|
|
"op":"filter",
|
|
"fun":"max",
|
|
"values":{
|
|
"op":"Pmax",
|
|
"exp":{
|
|
"op":"U",
|
|
"left":true,
|
|
"right":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"srep",
|
|
"right":1
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"rrep",
|
|
"right":3
|
|
}
|
|
},
|
|
"right":"recv"
|
|
}
|
|
}
|
|
},
|
|
"states":{
|
|
"op":"initial"
|
|
}
|
|
},
|
|
"comment":"P=?[ F srep=1 & rrep=3 & recv ]"
|
|
},
|
|
{
|
|
"name":"Property_brp_2",
|
|
"expression":{
|
|
"op":"filter",
|
|
"fun":"min",
|
|
"values":{
|
|
"op":"Pmax",
|
|
"exp":{
|
|
"op":"U",
|
|
"left":true,
|
|
"right":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"srep",
|
|
"right":3
|
|
},
|
|
"right":{
|
|
"op":"¬",
|
|
"exp":{
|
|
"op":"=",
|
|
"left":"rrep",
|
|
"right":3
|
|
}
|
|
}
|
|
},
|
|
"right":"recv"
|
|
}
|
|
}
|
|
},
|
|
"states":{
|
|
"op":"initial"
|
|
}
|
|
},
|
|
"comment":"P=?[ F srep=3 & !(rrep=3) & recv ]"
|
|
},
|
|
{
|
|
"name":"Property_brp_3",
|
|
"expression":{
|
|
"op":"filter",
|
|
"fun":"max",
|
|
"values":{
|
|
"op":"Pmax",
|
|
"exp":{
|
|
"op":"U",
|
|
"left":true,
|
|
"right":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"srep",
|
|
"right":3
|
|
},
|
|
"right":{
|
|
"op":"¬",
|
|
"exp":{
|
|
"op":"=",
|
|
"left":"rrep",
|
|
"right":3
|
|
}
|
|
}
|
|
},
|
|
"right":"recv"
|
|
}
|
|
}
|
|
},
|
|
"states":{
|
|
"op":"initial"
|
|
}
|
|
},
|
|
"comment":"P=?[ F srep=3 & !(rrep=3) & recv ]"
|
|
},
|
|
{
|
|
"name":"Property_brp_4",
|
|
"expression":{
|
|
"op":"filter",
|
|
"fun":"min",
|
|
"values":{
|
|
"op":"Pmax",
|
|
"exp":{
|
|
"op":"U",
|
|
"left":true,
|
|
"right":{
|
|
"op":"=",
|
|
"left":"s",
|
|
"right":5
|
|
}
|
|
}
|
|
},
|
|
"states":{
|
|
"op":"initial"
|
|
}
|
|
},
|
|
"comment":"P=?[ F s=5 ]"
|
|
},
|
|
{
|
|
"name":"Property_brp_5",
|
|
"expression":{
|
|
"op":"filter",
|
|
"fun":"max",
|
|
"values":{
|
|
"op":"Pmax",
|
|
"exp":{
|
|
"op":"U",
|
|
"left":true,
|
|
"right":{
|
|
"op":"=",
|
|
"left":"s",
|
|
"right":5
|
|
}
|
|
}
|
|
},
|
|
"states":{
|
|
"op":"initial"
|
|
}
|
|
},
|
|
"comment":"P=?[ F s=5 ]"
|
|
},
|
|
{
|
|
"name":"Property_brp_6",
|
|
"expression":{
|
|
"op":"filter",
|
|
"fun":"min",
|
|
"values":{
|
|
"op":"Pmax",
|
|
"exp":{
|
|
"op":"U",
|
|
"left":true,
|
|
"right":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"s",
|
|
"right":5
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"srep",
|
|
"right":2
|
|
}
|
|
}
|
|
}
|
|
},
|
|
"states":{
|
|
"op":"initial"
|
|
}
|
|
},
|
|
"comment":"P=?[ F s=5 & srep=2 ]"
|
|
},
|
|
{
|
|
"name":"Property_brp_7",
|
|
"expression":{
|
|
"op":"filter",
|
|
"fun":"max",
|
|
"values":{
|
|
"op":"Pmax",
|
|
"exp":{
|
|
"op":"U",
|
|
"left":true,
|
|
"right":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"s",
|
|
"right":5
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"srep",
|
|
"right":2
|
|
}
|
|
}
|
|
}
|
|
},
|
|
"states":{
|
|
"op":"initial"
|
|
}
|
|
},
|
|
"comment":"P=?[ F s=5 & srep=2 ]"
|
|
},
|
|
{
|
|
"name":"Property_brp_8",
|
|
"expression":{
|
|
"op":"filter",
|
|
"fun":"min",
|
|
"values":{
|
|
"op":"Pmax",
|
|
"exp":{
|
|
"op":"U",
|
|
"left":true,
|
|
"right":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"s",
|
|
"right":5
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"srep",
|
|
"right":1
|
|
}
|
|
},
|
|
"right":{
|
|
"op":">",
|
|
"left":"i",
|
|
"right":8
|
|
}
|
|
}
|
|
}
|
|
},
|
|
"states":{
|
|
"op":"initial"
|
|
}
|
|
},
|
|
"comment":"P=?[ F s=5 & srep=1 & i>8 ]"
|
|
},
|
|
{
|
|
"name":"Property_brp_9",
|
|
"expression":{
|
|
"op":"filter",
|
|
"fun":"max",
|
|
"values":{
|
|
"op":"Pmax",
|
|
"exp":{
|
|
"op":"U",
|
|
"left":true,
|
|
"right":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"s",
|
|
"right":5
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"srep",
|
|
"right":1
|
|
}
|
|
},
|
|
"right":{
|
|
"op":">",
|
|
"left":"i",
|
|
"right":8
|
|
}
|
|
}
|
|
}
|
|
},
|
|
"states":{
|
|
"op":"initial"
|
|
}
|
|
},
|
|
"comment":"P=?[ F s=5 & srep=1 & i>8 ]"
|
|
},
|
|
{
|
|
"name":"Property_brp_10",
|
|
"expression":{
|
|
"op":"filter",
|
|
"fun":"min",
|
|
"values":{
|
|
"op":"Pmax",
|
|
"exp":{
|
|
"op":"U",
|
|
"left":true,
|
|
"right":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"¬",
|
|
"exp":{
|
|
"op":"=",
|
|
"left":"srep",
|
|
"right":0
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"¬",
|
|
"exp":"recv"
|
|
}
|
|
}
|
|
}
|
|
},
|
|
"states":{
|
|
"op":"initial"
|
|
}
|
|
},
|
|
"comment":"P=?[ F !(srep=0) & !recv ]"
|
|
},
|
|
{
|
|
"name":"Property_brp_11",
|
|
"expression":{
|
|
"op":"filter",
|
|
"fun":"max",
|
|
"values":{
|
|
"op":"Pmax",
|
|
"exp":{
|
|
"op":"U",
|
|
"left":true,
|
|
"right":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"¬",
|
|
"exp":{
|
|
"op":"=",
|
|
"left":"srep",
|
|
"right":0
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"¬",
|
|
"exp":"recv"
|
|
}
|
|
}
|
|
}
|
|
},
|
|
"states":{
|
|
"op":"initial"
|
|
}
|
|
},
|
|
"comment":"P=?[ F !(srep=0) & !recv ]"
|
|
}
|
|
],
|
|
"automata":[
|
|
{
|
|
"name":"sender",
|
|
"locations":[
|
|
{
|
|
"name":"location"
|
|
}
|
|
],
|
|
"initial-locations":[
|
|
"location"
|
|
],
|
|
"edges":[
|
|
{
|
|
"location":"location",
|
|
"action":"NewFile",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"=",
|
|
"left":"s",
|
|
"right":0
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":1
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"s",
|
|
"value":1
|
|
},
|
|
{
|
|
"ref":"i",
|
|
"value":1
|
|
},
|
|
{
|
|
"ref":"srep",
|
|
"value":0
|
|
}
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"aF",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"=",
|
|
"left":"s",
|
|
"right":1
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":1
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"s",
|
|
"value":2
|
|
},
|
|
{
|
|
"ref":"fs",
|
|
"value":{
|
|
"op":"=",
|
|
"left":"i",
|
|
"right":1
|
|
}
|
|
},
|
|
{
|
|
"ref":"ls",
|
|
"value":{
|
|
"op":"=",
|
|
"left":"i",
|
|
"right":"N"
|
|
}
|
|
},
|
|
{
|
|
"ref":"bs",
|
|
"value":"s_ab"
|
|
},
|
|
{
|
|
"ref":"nrtr",
|
|
"value":0
|
|
},
|
|
{
|
|
"ref":"reward_",
|
|
"value":{
|
|
"op":"ite",
|
|
"if":{
|
|
"op":"=",
|
|
"left":"i",
|
|
"right":1
|
|
},
|
|
"then":1,
|
|
"else":0
|
|
}
|
|
}
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"aB",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"=",
|
|
"left":"s",
|
|
"right":2
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":1
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"s",
|
|
"value":4
|
|
},
|
|
{
|
|
"ref":"s_ab",
|
|
"value":{
|
|
"op":"¬",
|
|
"exp":"s_ab"
|
|
}
|
|
}
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"TO_Msg",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"=",
|
|
"left":"s",
|
|
"right":2
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":1
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"s",
|
|
"value":3
|
|
}
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"TO_Ack",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"=",
|
|
"left":"s",
|
|
"right":2
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":1
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"s",
|
|
"value":3
|
|
}
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"aF",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"s",
|
|
"right":3
|
|
},
|
|
"right":{
|
|
"op":"<",
|
|
"left":"nrtr",
|
|
"right":"MAX"
|
|
}
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":1
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"s",
|
|
"value":2
|
|
},
|
|
{
|
|
"ref":"fs",
|
|
"value":{
|
|
"op":"=",
|
|
"left":"i",
|
|
"right":1
|
|
}
|
|
},
|
|
{
|
|
"ref":"ls",
|
|
"value":{
|
|
"op":"=",
|
|
"left":"i",
|
|
"right":"N"
|
|
}
|
|
},
|
|
{
|
|
"ref":"bs",
|
|
"value":"s_ab"
|
|
},
|
|
{
|
|
"ref":"nrtr",
|
|
"value":{
|
|
"op":"+",
|
|
"left":"nrtr",
|
|
"right":1
|
|
}
|
|
},
|
|
{
|
|
"ref":"reward_",
|
|
"value":{
|
|
"op":"ite",
|
|
"if":{
|
|
"op":"=",
|
|
"left":"i",
|
|
"right":1
|
|
},
|
|
"then":1,
|
|
"else":0
|
|
}
|
|
}
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"τ",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"s",
|
|
"right":3
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"nrtr",
|
|
"right":"MAX"
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"<",
|
|
"left":"i",
|
|
"right":"N"
|
|
}
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":1
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"s",
|
|
"value":5
|
|
},
|
|
{
|
|
"ref":"srep",
|
|
"value":1
|
|
}
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"τ",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"s",
|
|
"right":3
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"nrtr",
|
|
"right":"MAX"
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"i",
|
|
"right":"N"
|
|
}
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":1
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"s",
|
|
"value":5
|
|
},
|
|
{
|
|
"ref":"srep",
|
|
"value":2
|
|
}
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"τ",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"s",
|
|
"right":4
|
|
},
|
|
"right":{
|
|
"op":"<",
|
|
"left":"i",
|
|
"right":"N"
|
|
}
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":1
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"s",
|
|
"value":1
|
|
},
|
|
{
|
|
"ref":"i",
|
|
"value":{
|
|
"op":"+",
|
|
"left":"i",
|
|
"right":1
|
|
}
|
|
}
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"τ",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"s",
|
|
"right":4
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"i",
|
|
"right":"N"
|
|
}
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":1
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"s",
|
|
"value":0
|
|
},
|
|
{
|
|
"ref":"srep",
|
|
"value":3
|
|
}
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"SyncWait",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"=",
|
|
"left":"s",
|
|
"right":5
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":1
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"s",
|
|
"value":6
|
|
}
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"SyncWait",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"=",
|
|
"left":"s",
|
|
"right":6
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":1
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"s",
|
|
"value":0
|
|
},
|
|
{
|
|
"ref":"s_ab",
|
|
"value":false
|
|
}
|
|
]
|
|
}
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"name":"receiver",
|
|
"locations":[
|
|
{
|
|
"name":"location"
|
|
}
|
|
],
|
|
"initial-locations":[
|
|
"location"
|
|
],
|
|
"edges":[
|
|
{
|
|
"location":"location",
|
|
"action":"SyncWait",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"=",
|
|
"left":"r",
|
|
"right":0
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":1
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"r",
|
|
"value":0
|
|
}
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"aG",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"=",
|
|
"left":"r",
|
|
"right":0
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":1
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"r",
|
|
"value":1
|
|
},
|
|
{
|
|
"ref":"fr",
|
|
"value":"fs"
|
|
},
|
|
{
|
|
"ref":"lr",
|
|
"value":"ls"
|
|
},
|
|
{
|
|
"ref":"br",
|
|
"value":"bs"
|
|
},
|
|
{
|
|
"ref":"recv",
|
|
"value":"T"
|
|
}
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"τ",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"=",
|
|
"left":"r",
|
|
"right":1
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":1
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"r",
|
|
"value":2
|
|
},
|
|
{
|
|
"ref":"r_ab",
|
|
"value":"br"
|
|
}
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"τ",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"r",
|
|
"right":2
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"r_ab",
|
|
"right":"br"
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"fr",
|
|
"right":true
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"lr",
|
|
"right":false
|
|
}
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":1
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"r",
|
|
"value":3
|
|
},
|
|
{
|
|
"ref":"rrep",
|
|
"value":1
|
|
}
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"τ",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"r",
|
|
"right":2
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"r_ab",
|
|
"right":"br"
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"fr",
|
|
"right":false
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"lr",
|
|
"right":false
|
|
}
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":1
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"r",
|
|
"value":3
|
|
},
|
|
{
|
|
"ref":"rrep",
|
|
"value":2
|
|
}
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"τ",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"r",
|
|
"right":2
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"r_ab",
|
|
"right":"br"
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"fr",
|
|
"right":false
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"lr",
|
|
"right":true
|
|
}
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":1
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"r",
|
|
"value":3
|
|
},
|
|
{
|
|
"ref":"rrep",
|
|
"value":3
|
|
}
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"aA",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"r",
|
|
"right":2
|
|
},
|
|
"right":{
|
|
"op":"¬",
|
|
"exp":{
|
|
"op":"=",
|
|
"left":"r_ab",
|
|
"right":"br"
|
|
}
|
|
}
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":1
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"r",
|
|
"value":4
|
|
}
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"aA",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"=",
|
|
"left":"r",
|
|
"right":3
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":1
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"r",
|
|
"value":4
|
|
},
|
|
{
|
|
"ref":"r_ab",
|
|
"value":{
|
|
"op":"¬",
|
|
"exp":"r_ab"
|
|
}
|
|
}
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"aG",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"=",
|
|
"left":"r",
|
|
"right":4
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":1
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"r",
|
|
"value":2
|
|
},
|
|
{
|
|
"ref":"fr",
|
|
"value":"fs"
|
|
},
|
|
{
|
|
"ref":"lr",
|
|
"value":"ls"
|
|
},
|
|
{
|
|
"ref":"br",
|
|
"value":"bs"
|
|
},
|
|
{
|
|
"ref":"recv",
|
|
"value":"T"
|
|
}
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"SyncWait",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"r",
|
|
"right":4
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"ls",
|
|
"right":true
|
|
}
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":1
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"r",
|
|
"value":5
|
|
}
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"SyncWait",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"r",
|
|
"right":4
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"ls",
|
|
"right":false
|
|
}
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":1
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"r",
|
|
"value":5
|
|
},
|
|
{
|
|
"ref":"rrep",
|
|
"value":4
|
|
}
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"SyncWait",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"=",
|
|
"left":"r",
|
|
"right":5
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":1
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"r",
|
|
"value":0
|
|
},
|
|
{
|
|
"ref":"rrep",
|
|
"value":0
|
|
}
|
|
]
|
|
}
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"name":"checker",
|
|
"locations":[
|
|
{
|
|
"name":"location"
|
|
}
|
|
],
|
|
"initial-locations":[
|
|
"location"
|
|
],
|
|
"edges":[
|
|
{
|
|
"location":"location",
|
|
"action":"NewFile",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"=",
|
|
"left":"T",
|
|
"right":false
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":1
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"T",
|
|
"value":true
|
|
}
|
|
]
|
|
}
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"name":"channelK",
|
|
"locations":[
|
|
{
|
|
"name":"location"
|
|
}
|
|
],
|
|
"initial-locations":[
|
|
"location"
|
|
],
|
|
"edges":[
|
|
{
|
|
"location":"location",
|
|
"action":"aF",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"=",
|
|
"left":"k",
|
|
"right":0
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":0.9800000
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"k",
|
|
"value":1
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"probability":{
|
|
"exp":0.0200000
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"k",
|
|
"value":2
|
|
}
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"aG",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"=",
|
|
"left":"k",
|
|
"right":1
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":1
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"k",
|
|
"value":0
|
|
}
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"TO_Msg",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"=",
|
|
"left":"k",
|
|
"right":2
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":1
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"k",
|
|
"value":0
|
|
}
|
|
]
|
|
}
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"name":"channelL",
|
|
"locations":[
|
|
{
|
|
"name":"location"
|
|
}
|
|
],
|
|
"initial-locations":[
|
|
"location"
|
|
],
|
|
"edges":[
|
|
{
|
|
"location":"location",
|
|
"action":"aA",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"=",
|
|
"left":"l",
|
|
"right":0
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":0.9900000
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"l",
|
|
"value":1
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"probability":{
|
|
"exp":0.0100000
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"l",
|
|
"value":2
|
|
}
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"aB",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"=",
|
|
"left":"l",
|
|
"right":1
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":1
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"l",
|
|
"value":0
|
|
}
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"TO_Ack",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"=",
|
|
"left":"l",
|
|
"right":2
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":1
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"l",
|
|
"value":0
|
|
}
|
|
]
|
|
}
|
|
]
|
|
}
|
|
]
|
|
}
|
|
],
|
|
"system":{
|
|
"elements":[
|
|
{
|
|
"automaton":"sender"
|
|
},
|
|
{
|
|
"automaton":"receiver"
|
|
},
|
|
{
|
|
"automaton":"checker"
|
|
},
|
|
{
|
|
"automaton":"channelK"
|
|
},
|
|
{
|
|
"automaton":"channelL"
|
|
}
|
|
],
|
|
"syncs":[
|
|
{
|
|
"synchronise":[
|
|
"aB",
|
|
null,
|
|
null,
|
|
null,
|
|
"aB"
|
|
],
|
|
"result":"aB"
|
|
},
|
|
{
|
|
"synchronise":[
|
|
"TO_Ack",
|
|
null,
|
|
null,
|
|
null,
|
|
"TO_Ack"
|
|
],
|
|
"result":"TO_Ack"
|
|
},
|
|
{
|
|
"synchronise":[
|
|
null,
|
|
"aA",
|
|
null,
|
|
null,
|
|
"aA"
|
|
],
|
|
"result":"aA"
|
|
},
|
|
{
|
|
"synchronise":[
|
|
"aF",
|
|
null,
|
|
null,
|
|
"aF",
|
|
null
|
|
],
|
|
"result":"aF"
|
|
},
|
|
{
|
|
"synchronise":[
|
|
"TO_Msg",
|
|
null,
|
|
null,
|
|
"TO_Msg",
|
|
null
|
|
],
|
|
"result":"TO_Msg"
|
|
},
|
|
{
|
|
"synchronise":[
|
|
null,
|
|
"aG",
|
|
null,
|
|
"aG",
|
|
null
|
|
],
|
|
"result":"aG"
|
|
},
|
|
{
|
|
"synchronise":[
|
|
"NewFile",
|
|
null,
|
|
"NewFile",
|
|
null,
|
|
null
|
|
],
|
|
"result":"NewFile"
|
|
},
|
|
{
|
|
"synchronise":[
|
|
"SyncWait",
|
|
"SyncWait",
|
|
null,
|
|
null,
|
|
null
|
|
],
|
|
"result":"SyncWait"
|
|
},
|
|
{
|
|
"synchronise":[
|
|
"τ",
|
|
null,
|
|
null,
|
|
null,
|
|
null
|
|
],
|
|
"result":"τ"
|
|
},
|
|
{
|
|
"synchronise":[
|
|
null,
|
|
"τ",
|
|
null,
|
|
null,
|
|
null
|
|
],
|
|
"result":"τ"
|
|
}
|
|
]
|
|
}
|
|
}
|