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.
1580 lines
55 KiB
1580 lines
55 KiB
|
|
{
|
|
"jani-version":1,
|
|
"features":[
|
|
"derived-operators"
|
|
],
|
|
"name":"Converted from PRISM by IscasMC",
|
|
"type":"ctmc",
|
|
"actions":[
|
|
{
|
|
"name":"in"
|
|
},
|
|
{
|
|
"name":"tau__"
|
|
},
|
|
{
|
|
"name":"s1"
|
|
},
|
|
{
|
|
"name":"s2"
|
|
}
|
|
],
|
|
"constants":[
|
|
{
|
|
"name":"t",
|
|
"type":"int"
|
|
}
|
|
],
|
|
"variables":[
|
|
{
|
|
"name":"w1",
|
|
"type":{
|
|
"kind":"bounded",
|
|
"base":"int",
|
|
"lower-bound":0,
|
|
"upper-bound":"t"
|
|
}
|
|
},
|
|
{
|
|
"name":"x1",
|
|
"type":{
|
|
"kind":"bounded",
|
|
"base":"int",
|
|
"lower-bound":0,
|
|
"upper-bound":"t"
|
|
}
|
|
},
|
|
{
|
|
"name":"y1",
|
|
"type":{
|
|
"kind":"bounded",
|
|
"base":"int",
|
|
"lower-bound":0,
|
|
"upper-bound":"t"
|
|
}
|
|
},
|
|
{
|
|
"name":"z1",
|
|
"type":{
|
|
"kind":"bounded",
|
|
"base":"int",
|
|
"lower-bound":0,
|
|
"upper-bound":"t"
|
|
}
|
|
},
|
|
{
|
|
"name":"w2",
|
|
"type":{
|
|
"kind":"bounded",
|
|
"base":"int",
|
|
"lower-bound":0,
|
|
"upper-bound":"t"
|
|
}
|
|
},
|
|
{
|
|
"name":"x2",
|
|
"type":{
|
|
"kind":"bounded",
|
|
"base":"int",
|
|
"lower-bound":0,
|
|
"upper-bound":"t"
|
|
}
|
|
},
|
|
{
|
|
"name":"y2",
|
|
"type":{
|
|
"kind":"bounded",
|
|
"base":"int",
|
|
"lower-bound":0,
|
|
"upper-bound":"t"
|
|
}
|
|
},
|
|
{
|
|
"name":"z2",
|
|
"type":{
|
|
"kind":"bounded",
|
|
"base":"int",
|
|
"lower-bound":0,
|
|
"upper-bound":"t"
|
|
}
|
|
},
|
|
{
|
|
"name":"w3",
|
|
"type":{
|
|
"kind":"bounded",
|
|
"base":"int",
|
|
"lower-bound":0,
|
|
"upper-bound":"t"
|
|
}
|
|
},
|
|
{
|
|
"name":"x3",
|
|
"type":{
|
|
"kind":"bounded",
|
|
"base":"int",
|
|
"lower-bound":0,
|
|
"upper-bound":"t"
|
|
}
|
|
},
|
|
{
|
|
"name":"y3",
|
|
"type":{
|
|
"kind":"bounded",
|
|
"base":"int",
|
|
"lower-bound":0,
|
|
"upper-bound":"t"
|
|
}
|
|
},
|
|
{
|
|
"name":"z3",
|
|
"type":{
|
|
"kind":"bounded",
|
|
"base":"int",
|
|
"lower-bound":0,
|
|
"upper-bound":"t"
|
|
}
|
|
},
|
|
{
|
|
"name":"w4",
|
|
"type":{
|
|
"kind":"bounded",
|
|
"base":"int",
|
|
"lower-bound":0,
|
|
"upper-bound":"t"
|
|
}
|
|
},
|
|
{
|
|
"name":"x4",
|
|
"type":{
|
|
"kind":"bounded",
|
|
"base":"int",
|
|
"lower-bound":0,
|
|
"upper-bound":"t"
|
|
}
|
|
},
|
|
{
|
|
"name":"y4",
|
|
"type":{
|
|
"kind":"bounded",
|
|
"base":"int",
|
|
"lower-bound":0,
|
|
"upper-bound":"t"
|
|
}
|
|
},
|
|
{
|
|
"name":"z4",
|
|
"type":{
|
|
"kind":"bounded",
|
|
"base":"int",
|
|
"lower-bound":0,
|
|
"upper-bound":"t"
|
|
}
|
|
}
|
|
],
|
|
"observables":[
|
|
{
|
|
"name":"\"tokens_cell1\""
|
|
},
|
|
{
|
|
"name":"\"tokens_cell2\""
|
|
},
|
|
{
|
|
"name":"\"tokens_cell3\""
|
|
},
|
|
{
|
|
"name":"\"tokens_cell4\""
|
|
},
|
|
{
|
|
"name":"\"throughput\""
|
|
}
|
|
],
|
|
"initial-states":{
|
|
"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":"w1",
|
|
"right":0
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"x1",
|
|
"right":0
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"y1",
|
|
"right":0
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"z1",
|
|
"right":0
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"w2",
|
|
"right":0
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"x2",
|
|
"right":0
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"y2",
|
|
"right":0
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"z2",
|
|
"right":0
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"w3",
|
|
"right":0
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"x3",
|
|
"right":0
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"y3",
|
|
"right":0
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"z3",
|
|
"right":0
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"w4",
|
|
"right":0
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"x4",
|
|
"right":0
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"y4",
|
|
"right":0
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"z4",
|
|
"right":0
|
|
}
|
|
}
|
|
},
|
|
"automata":[
|
|
{
|
|
"name":"k1",
|
|
"locations":[
|
|
{
|
|
"name":"location",
|
|
"observables":[
|
|
{
|
|
"ref":"\"tokens_cell1\"",
|
|
"value":{
|
|
"op":"+",
|
|
"left":{
|
|
"op":"+",
|
|
"left":"x1",
|
|
"right":"y1"
|
|
},
|
|
"right":"z1"
|
|
}
|
|
},
|
|
{
|
|
"ref":"\"tokens_cell2\"",
|
|
"value":{
|
|
"op":"+",
|
|
"left":{
|
|
"op":"+",
|
|
"left":"x2",
|
|
"right":"y2"
|
|
},
|
|
"right":"z2"
|
|
}
|
|
},
|
|
{
|
|
"ref":"\"tokens_cell3\"",
|
|
"value":{
|
|
"op":"+",
|
|
"left":{
|
|
"op":"+",
|
|
"left":"x3",
|
|
"right":"y3"
|
|
},
|
|
"right":"z3"
|
|
}
|
|
},
|
|
{
|
|
"ref":"\"tokens_cell4\"",
|
|
"value":{
|
|
"op":"+",
|
|
"left":{
|
|
"op":"+",
|
|
"left":"x4",
|
|
"right":"y4"
|
|
},
|
|
"right":"z4"
|
|
}
|
|
}
|
|
]
|
|
}
|
|
],
|
|
"initial-locations":[
|
|
"location"
|
|
],
|
|
"edges":[
|
|
{
|
|
"location":"location",
|
|
"action":"in",
|
|
"rate":{
|
|
"exp":1.0000000
|
|
},
|
|
"guard":{
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"<",
|
|
"left":"w1",
|
|
"right":"t"
|
|
},
|
|
"right":{
|
|
"op":"<",
|
|
"left":"x1",
|
|
"right":"t"
|
|
}
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":{
|
|
"op":"/",
|
|
"left":1.0000000,
|
|
"right":1.0000000
|
|
}
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"w1",
|
|
"value":{
|
|
"op":"+",
|
|
"left":"w1",
|
|
"right":1
|
|
}
|
|
},
|
|
{
|
|
"ref":"x1",
|
|
"value":{
|
|
"op":"+",
|
|
"left":"x1",
|
|
"right":1
|
|
}
|
|
}
|
|
],
|
|
"observables":[
|
|
{
|
|
"ref":"\"throughput\"",
|
|
"value":1
|
|
}
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"tau__",
|
|
"rate":{
|
|
"exp":0.3600000
|
|
},
|
|
"guard":{
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":">",
|
|
"left":"x1",
|
|
"right":0
|
|
},
|
|
"right":{
|
|
"op":"<",
|
|
"left":"y1",
|
|
"right":"t"
|
|
}
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":{
|
|
"op":"/",
|
|
"left":0.3600000,
|
|
"right":0.3600000
|
|
}
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"x1",
|
|
"value":{
|
|
"op":"-",
|
|
"left":"x1",
|
|
"right":1
|
|
}
|
|
},
|
|
{
|
|
"ref":"y1",
|
|
"value":{
|
|
"op":"+",
|
|
"left":"y1",
|
|
"right":1
|
|
}
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"tau__",
|
|
"rate":{
|
|
"exp":0.8400000
|
|
},
|
|
"guard":{
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":">",
|
|
"left":"x1",
|
|
"right":0
|
|
},
|
|
"right":{
|
|
"op":"<",
|
|
"left":"z1",
|
|
"right":"t"
|
|
}
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":{
|
|
"op":"/",
|
|
"left":0.8400000,
|
|
"right":0.8400000
|
|
}
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"x1",
|
|
"value":{
|
|
"op":"-",
|
|
"left":"x1",
|
|
"right":1
|
|
}
|
|
},
|
|
{
|
|
"ref":"z1",
|
|
"value":{
|
|
"op":"+",
|
|
"left":"z1",
|
|
"right":1
|
|
}
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"tau__",
|
|
"rate":{
|
|
"exp":0.3000000
|
|
},
|
|
"guard":{
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":">",
|
|
"left":"y1",
|
|
"right":0
|
|
},
|
|
"right":{
|
|
"op":"<",
|
|
"left":"x1",
|
|
"right":"t"
|
|
}
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":{
|
|
"op":"/",
|
|
"left":0.3000000,
|
|
"right":0.3000000
|
|
}
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"y1",
|
|
"value":{
|
|
"op":"-",
|
|
"left":"y1",
|
|
"right":1
|
|
}
|
|
},
|
|
{
|
|
"ref":"x1",
|
|
"value":{
|
|
"op":"+",
|
|
"left":"x1",
|
|
"right":1
|
|
}
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"s1",
|
|
"rate":{
|
|
"exp":0.4000000
|
|
},
|
|
"guard":{
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":">",
|
|
"left":"z1",
|
|
"right":0
|
|
},
|
|
"right":{
|
|
"op":">",
|
|
"left":"w1",
|
|
"right":0
|
|
}
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":{
|
|
"op":"/",
|
|
"left":0.4000000,
|
|
"right":0.4000000
|
|
}
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"z1",
|
|
"value":{
|
|
"op":"-",
|
|
"left":"z1",
|
|
"right":1
|
|
}
|
|
},
|
|
{
|
|
"ref":"w1",
|
|
"value":{
|
|
"op":"-",
|
|
"left":"w1",
|
|
"right":1
|
|
}
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
}
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"name":"k2",
|
|
"locations":[
|
|
{
|
|
"name":"location"
|
|
}
|
|
],
|
|
"initial-locations":[
|
|
"location"
|
|
],
|
|
"edges":[
|
|
{
|
|
"location":"location",
|
|
"action":"s1",
|
|
"rate":{
|
|
"exp":1
|
|
},
|
|
"guard":{
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"<",
|
|
"left":"w2",
|
|
"right":"t"
|
|
},
|
|
"right":{
|
|
"op":"<",
|
|
"left":"x2",
|
|
"right":"t"
|
|
}
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":{
|
|
"op":"/",
|
|
"left":1,
|
|
"right":1
|
|
}
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"w2",
|
|
"value":{
|
|
"op":"+",
|
|
"left":"w2",
|
|
"right":1
|
|
}
|
|
},
|
|
{
|
|
"ref":"x2",
|
|
"value":{
|
|
"op":"+",
|
|
"left":"x2",
|
|
"right":1
|
|
}
|
|
}
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"tau__",
|
|
"rate":{
|
|
"exp":0.4200000
|
|
},
|
|
"guard":{
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":">",
|
|
"left":"x2",
|
|
"right":0
|
|
},
|
|
"right":{
|
|
"op":"<",
|
|
"left":"y2",
|
|
"right":"t"
|
|
}
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":{
|
|
"op":"/",
|
|
"left":0.4200000,
|
|
"right":0.4200000
|
|
}
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"x2",
|
|
"value":{
|
|
"op":"-",
|
|
"left":"x2",
|
|
"right":1
|
|
}
|
|
},
|
|
{
|
|
"ref":"y2",
|
|
"value":{
|
|
"op":"+",
|
|
"left":"y2",
|
|
"right":1
|
|
}
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"tau__",
|
|
"rate":{
|
|
"exp":0.9800000
|
|
},
|
|
"guard":{
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":">",
|
|
"left":"x2",
|
|
"right":0
|
|
},
|
|
"right":{
|
|
"op":"<",
|
|
"left":"z2",
|
|
"right":"t"
|
|
}
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":{
|
|
"op":"/",
|
|
"left":0.9800000,
|
|
"right":0.9800000
|
|
}
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"x2",
|
|
"value":{
|
|
"op":"-",
|
|
"left":"x2",
|
|
"right":1
|
|
}
|
|
},
|
|
{
|
|
"ref":"z2",
|
|
"value":{
|
|
"op":"+",
|
|
"left":"z2",
|
|
"right":1
|
|
}
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"tau__",
|
|
"rate":{
|
|
"exp":0.3000000
|
|
},
|
|
"guard":{
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":">",
|
|
"left":"y2",
|
|
"right":0
|
|
},
|
|
"right":{
|
|
"op":"<",
|
|
"left":"x2",
|
|
"right":"t"
|
|
}
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":{
|
|
"op":"/",
|
|
"left":0.3000000,
|
|
"right":0.3000000
|
|
}
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"y2",
|
|
"value":{
|
|
"op":"-",
|
|
"left":"y2",
|
|
"right":1
|
|
}
|
|
},
|
|
{
|
|
"ref":"x2",
|
|
"value":{
|
|
"op":"+",
|
|
"left":"x2",
|
|
"right":1
|
|
}
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"s2",
|
|
"rate":{
|
|
"exp":1
|
|
},
|
|
"guard":{
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":">",
|
|
"left":"z2",
|
|
"right":0
|
|
},
|
|
"right":{
|
|
"op":">",
|
|
"left":"w2",
|
|
"right":0
|
|
}
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":{
|
|
"op":"/",
|
|
"left":1,
|
|
"right":1
|
|
}
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"z2",
|
|
"value":{
|
|
"op":"-",
|
|
"left":"z2",
|
|
"right":1
|
|
}
|
|
},
|
|
{
|
|
"ref":"w2",
|
|
"value":{
|
|
"op":"-",
|
|
"left":"w2",
|
|
"right":1
|
|
}
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
}
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"name":"k3",
|
|
"locations":[
|
|
{
|
|
"name":"location"
|
|
}
|
|
],
|
|
"initial-locations":[
|
|
"location"
|
|
],
|
|
"edges":[
|
|
{
|
|
"location":"location",
|
|
"action":"s1",
|
|
"rate":{
|
|
"exp":1
|
|
},
|
|
"guard":{
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"<",
|
|
"left":"w3",
|
|
"right":"t"
|
|
},
|
|
"right":{
|
|
"op":"<",
|
|
"left":"x3",
|
|
"right":"t"
|
|
}
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":{
|
|
"op":"/",
|
|
"left":1,
|
|
"right":1
|
|
}
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"w3",
|
|
"value":{
|
|
"op":"+",
|
|
"left":"w3",
|
|
"right":1
|
|
}
|
|
},
|
|
{
|
|
"ref":"x3",
|
|
"value":{
|
|
"op":"+",
|
|
"left":"x3",
|
|
"right":1
|
|
}
|
|
}
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"tau__",
|
|
"rate":{
|
|
"exp":0.3900000
|
|
},
|
|
"guard":{
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":">",
|
|
"left":"x3",
|
|
"right":0
|
|
},
|
|
"right":{
|
|
"op":"<",
|
|
"left":"y3",
|
|
"right":"t"
|
|
}
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":{
|
|
"op":"/",
|
|
"left":0.3900000,
|
|
"right":0.3900000
|
|
}
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"x3",
|
|
"value":{
|
|
"op":"-",
|
|
"left":"x3",
|
|
"right":1
|
|
}
|
|
},
|
|
{
|
|
"ref":"y3",
|
|
"value":{
|
|
"op":"+",
|
|
"left":"y3",
|
|
"right":1
|
|
}
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"tau__",
|
|
"rate":{
|
|
"exp":0.9100000
|
|
},
|
|
"guard":{
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":">",
|
|
"left":"x3",
|
|
"right":0
|
|
},
|
|
"right":{
|
|
"op":"<",
|
|
"left":"z3",
|
|
"right":"t"
|
|
}
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":{
|
|
"op":"/",
|
|
"left":0.9100000,
|
|
"right":0.9100000
|
|
}
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"x3",
|
|
"value":{
|
|
"op":"-",
|
|
"left":"x3",
|
|
"right":1
|
|
}
|
|
},
|
|
{
|
|
"ref":"z3",
|
|
"value":{
|
|
"op":"+",
|
|
"left":"z3",
|
|
"right":1
|
|
}
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"tau__",
|
|
"rate":{
|
|
"exp":0.3000000
|
|
},
|
|
"guard":{
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":">",
|
|
"left":"y3",
|
|
"right":0
|
|
},
|
|
"right":{
|
|
"op":"<",
|
|
"left":"x3",
|
|
"right":"t"
|
|
}
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":{
|
|
"op":"/",
|
|
"left":0.3000000,
|
|
"right":0.3000000
|
|
}
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"y3",
|
|
"value":{
|
|
"op":"-",
|
|
"left":"y3",
|
|
"right":1
|
|
}
|
|
},
|
|
{
|
|
"ref":"x3",
|
|
"value":{
|
|
"op":"+",
|
|
"left":"x3",
|
|
"right":1
|
|
}
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"s2",
|
|
"rate":{
|
|
"exp":1
|
|
},
|
|
"guard":{
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":">",
|
|
"left":"z3",
|
|
"right":0
|
|
},
|
|
"right":{
|
|
"op":">",
|
|
"left":"w3",
|
|
"right":0
|
|
}
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":{
|
|
"op":"/",
|
|
"left":1,
|
|
"right":1
|
|
}
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"z3",
|
|
"value":{
|
|
"op":"-",
|
|
"left":"z3",
|
|
"right":1
|
|
}
|
|
},
|
|
{
|
|
"ref":"w3",
|
|
"value":{
|
|
"op":"-",
|
|
"left":"w3",
|
|
"right":1
|
|
}
|
|
}
|
|
]
|
|
}
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"name":"k4",
|
|
"locations":[
|
|
{
|
|
"name":"location"
|
|
}
|
|
],
|
|
"initial-locations":[
|
|
"location"
|
|
],
|
|
"edges":[
|
|
{
|
|
"location":"location",
|
|
"action":"s2",
|
|
"rate":{
|
|
"exp":0.5000000
|
|
},
|
|
"guard":{
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"<",
|
|
"left":"w4",
|
|
"right":"t"
|
|
},
|
|
"right":{
|
|
"op":"<",
|
|
"left":"x4",
|
|
"right":"t"
|
|
}
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":{
|
|
"op":"/",
|
|
"left":0.5000000,
|
|
"right":0.5000000
|
|
}
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"w4",
|
|
"value":{
|
|
"op":"+",
|
|
"left":"w4",
|
|
"right":1
|
|
}
|
|
},
|
|
{
|
|
"ref":"x4",
|
|
"value":{
|
|
"op":"+",
|
|
"left":"x4",
|
|
"right":1
|
|
}
|
|
}
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"tau__",
|
|
"rate":{
|
|
"exp":0.3300000
|
|
},
|
|
"guard":{
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":">",
|
|
"left":"x4",
|
|
"right":0
|
|
},
|
|
"right":{
|
|
"op":"<",
|
|
"left":"y4",
|
|
"right":"t"
|
|
}
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":{
|
|
"op":"/",
|
|
"left":0.3300000,
|
|
"right":0.3300000
|
|
}
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"x4",
|
|
"value":{
|
|
"op":"-",
|
|
"left":"x4",
|
|
"right":1
|
|
}
|
|
},
|
|
{
|
|
"ref":"y4",
|
|
"value":{
|
|
"op":"+",
|
|
"left":"y4",
|
|
"right":1
|
|
}
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"tau__",
|
|
"rate":{
|
|
"exp":0.7700000
|
|
},
|
|
"guard":{
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":">",
|
|
"left":"x4",
|
|
"right":0
|
|
},
|
|
"right":{
|
|
"op":"<",
|
|
"left":"z4",
|
|
"right":"t"
|
|
}
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":{
|
|
"op":"/",
|
|
"left":0.7700000,
|
|
"right":0.7700000
|
|
}
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"x4",
|
|
"value":{
|
|
"op":"-",
|
|
"left":"x4",
|
|
"right":1
|
|
}
|
|
},
|
|
{
|
|
"ref":"z4",
|
|
"value":{
|
|
"op":"+",
|
|
"left":"z4",
|
|
"right":1
|
|
}
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"tau__",
|
|
"rate":{
|
|
"exp":0.3000000
|
|
},
|
|
"guard":{
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":">",
|
|
"left":"y4",
|
|
"right":0
|
|
},
|
|
"right":{
|
|
"op":"<",
|
|
"left":"x4",
|
|
"right":"t"
|
|
}
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":{
|
|
"op":"/",
|
|
"left":0.3000000,
|
|
"right":0.3000000
|
|
}
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"y4",
|
|
"value":{
|
|
"op":"-",
|
|
"left":"y4",
|
|
"right":1
|
|
}
|
|
},
|
|
{
|
|
"ref":"x4",
|
|
"value":{
|
|
"op":"+",
|
|
"left":"x4",
|
|
"right":1
|
|
}
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"tau__",
|
|
"rate":{
|
|
"exp":0.9000000
|
|
},
|
|
"guard":{
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":">",
|
|
"left":"z4",
|
|
"right":0
|
|
},
|
|
"right":{
|
|
"op":">",
|
|
"left":"w4",
|
|
"right":0
|
|
}
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":{
|
|
"op":"/",
|
|
"left":0.9000000,
|
|
"right":0.9000000
|
|
}
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"z4",
|
|
"value":{
|
|
"op":"-",
|
|
"left":"z4",
|
|
"right":1
|
|
}
|
|
},
|
|
{
|
|
"ref":"w4",
|
|
"value":{
|
|
"op":"-",
|
|
"left":"w4",
|
|
"right":1
|
|
}
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
}
|
|
]
|
|
}
|
|
]
|
|
}
|
|
],
|
|
"system":{
|
|
"elements":[
|
|
{
|
|
"automaton":"k1"
|
|
},
|
|
{
|
|
"automaton":"k2"
|
|
},
|
|
{
|
|
"automaton":"k3"
|
|
},
|
|
{
|
|
"automaton":"k4"
|
|
}
|
|
],
|
|
"syncs":[
|
|
{
|
|
"synchronise":[
|
|
null,
|
|
"s2",
|
|
"s2",
|
|
"s2"
|
|
],
|
|
"result":"s2"
|
|
},
|
|
{
|
|
"synchronise":[
|
|
"s1",
|
|
"s1",
|
|
"s1",
|
|
null
|
|
],
|
|
"result":"s1"
|
|
},
|
|
{
|
|
"synchronise":[
|
|
"in",
|
|
null,
|
|
null,
|
|
null
|
|
],
|
|
"result":"in"
|
|
},
|
|
{
|
|
"synchronise":[
|
|
"tau__",
|
|
null,
|
|
null,
|
|
null
|
|
],
|
|
"result":"tau__"
|
|
},
|
|
{
|
|
"synchronise":[
|
|
null,
|
|
"tau__",
|
|
null,
|
|
null
|
|
],
|
|
"result":"tau__"
|
|
},
|
|
{
|
|
"synchronise":[
|
|
null,
|
|
null,
|
|
"tau__",
|
|
null
|
|
],
|
|
"result":"tau__"
|
|
},
|
|
{
|
|
"synchronise":[
|
|
null,
|
|
null,
|
|
null,
|
|
"tau__"
|
|
],
|
|
"result":"tau__"
|
|
}
|
|
]
|
|
}
|
|
}
|