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.
928 lines
29 KiB
928 lines
29 KiB
|
|
{
|
|
"jani-version":1,
|
|
"features":[
|
|
"derived-operators"
|
|
],
|
|
"name":"Converted from PRISM by IscasMC",
|
|
"type":"mdp",
|
|
"actions":[
|
|
{
|
|
"name":"s12"
|
|
},
|
|
{
|
|
"name":"s13"
|
|
},
|
|
{
|
|
"name":"s14"
|
|
},
|
|
{
|
|
"name":"s23"
|
|
},
|
|
{
|
|
"name":"s24"
|
|
},
|
|
{
|
|
"name":"s34"
|
|
},
|
|
{
|
|
"name":"tau__"
|
|
}
|
|
],
|
|
"constants":[
|
|
{
|
|
"name":"p",
|
|
"type":"real"
|
|
}
|
|
],
|
|
"variables":[
|
|
{
|
|
"name":"pc",
|
|
"type":{
|
|
"kind":"bounded",
|
|
"base":"int",
|
|
"lower-bound":0,
|
|
"upper-bound":12
|
|
}
|
|
},
|
|
{
|
|
"name":"x12",
|
|
"type":"bool"
|
|
},
|
|
{
|
|
"name":"x13",
|
|
"type":"bool"
|
|
},
|
|
{
|
|
"name":"x14",
|
|
"type":"bool"
|
|
},
|
|
{
|
|
"name":"x23",
|
|
"type":"bool"
|
|
},
|
|
{
|
|
"name":"x24",
|
|
"type":"bool"
|
|
},
|
|
{
|
|
"name":"x34",
|
|
"type":"bool"
|
|
}
|
|
],
|
|
"observables":[
|
|
],
|
|
"initial-states":{
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"pc",
|
|
"right":0
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"x12",
|
|
"right":false
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"x13",
|
|
"right":false
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"x14",
|
|
"right":false
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"x23",
|
|
"right":false
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"x24",
|
|
"right":false
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"x34",
|
|
"right":false
|
|
}
|
|
}
|
|
},
|
|
"automata":[
|
|
{
|
|
"name":"PC",
|
|
"locations":[
|
|
{
|
|
"name":"location"
|
|
}
|
|
],
|
|
"initial-locations":[
|
|
"location"
|
|
],
|
|
"edges":[
|
|
{
|
|
"location":"location",
|
|
"action":"s12",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"=",
|
|
"left":"pc",
|
|
"right":0
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":1
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"pc",
|
|
"value":{
|
|
"op":"+",
|
|
"left":"pc",
|
|
"right":1
|
|
}
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"s13",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"=",
|
|
"left":"pc",
|
|
"right":1
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":1
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"pc",
|
|
"value":{
|
|
"op":"+",
|
|
"left":"pc",
|
|
"right":1
|
|
}
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"s14",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"=",
|
|
"left":"pc",
|
|
"right":2
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":1
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"pc",
|
|
"value":{
|
|
"op":"+",
|
|
"left":"pc",
|
|
"right":1
|
|
}
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"s23",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"=",
|
|
"left":"pc",
|
|
"right":3
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":1
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"pc",
|
|
"value":{
|
|
"op":"+",
|
|
"left":"pc",
|
|
"right":1
|
|
}
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"s24",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"=",
|
|
"left":"pc",
|
|
"right":4
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":1
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"pc",
|
|
"value":{
|
|
"op":"+",
|
|
"left":"pc",
|
|
"right":1
|
|
}
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"s34",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"=",
|
|
"left":"pc",
|
|
"right":5
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":1
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"pc",
|
|
"value":{
|
|
"op":"+",
|
|
"left":"pc",
|
|
"right":1
|
|
}
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
}
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"name":"M12",
|
|
"locations":[
|
|
{
|
|
"name":"location"
|
|
}
|
|
],
|
|
"initial-locations":[
|
|
"location"
|
|
],
|
|
"edges":[
|
|
{
|
|
"location":"location",
|
|
"action":"s12",
|
|
"guard":{
|
|
"exp":true
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":"p"
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"x12",
|
|
"value":true
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"probability":{
|
|
"exp":{
|
|
"op":"-",
|
|
"left":1,
|
|
"right":"p"
|
|
}
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"x12",
|
|
"value":false
|
|
}
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"tau__",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"pc",
|
|
"right":6
|
|
},
|
|
"right":{
|
|
"op":"¬",
|
|
"exp":"x12"
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"∨",
|
|
"left":{
|
|
"op":"∨",
|
|
"left":false,
|
|
"right":{
|
|
"op":"∧",
|
|
"left":"x13",
|
|
"right":"x23"
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"∧",
|
|
"left":"x14",
|
|
"right":"x24"
|
|
}
|
|
}
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":1
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"x12",
|
|
"value":true
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
}
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"name":"M13",
|
|
"locations":[
|
|
{
|
|
"name":"location"
|
|
}
|
|
],
|
|
"initial-locations":[
|
|
"location"
|
|
],
|
|
"edges":[
|
|
{
|
|
"location":"location",
|
|
"action":"s13",
|
|
"guard":{
|
|
"exp":true
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":"p"
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"x13",
|
|
"value":true
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"probability":{
|
|
"exp":{
|
|
"op":"-",
|
|
"left":1,
|
|
"right":"p"
|
|
}
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"x13",
|
|
"value":false
|
|
}
|
|
]
|
|
}
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"name":"M14",
|
|
"locations":[
|
|
{
|
|
"name":"location"
|
|
}
|
|
],
|
|
"initial-locations":[
|
|
"location"
|
|
],
|
|
"edges":[
|
|
{
|
|
"location":"location",
|
|
"action":"s14",
|
|
"guard":{
|
|
"exp":true
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":"p"
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"x14",
|
|
"value":true
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"probability":{
|
|
"exp":{
|
|
"op":"-",
|
|
"left":1,
|
|
"right":"p"
|
|
}
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"x14",
|
|
"value":false
|
|
}
|
|
]
|
|
}
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"name":"M23",
|
|
"locations":[
|
|
{
|
|
"name":"location"
|
|
}
|
|
],
|
|
"initial-locations":[
|
|
"location"
|
|
],
|
|
"edges":[
|
|
{
|
|
"location":"location",
|
|
"action":"s23",
|
|
"guard":{
|
|
"exp":true
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":"p"
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"x23",
|
|
"value":true
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"probability":{
|
|
"exp":{
|
|
"op":"-",
|
|
"left":1,
|
|
"right":"p"
|
|
}
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"x23",
|
|
"value":false
|
|
}
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"tau__",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"pc",
|
|
"right":6
|
|
},
|
|
"right":{
|
|
"op":"¬",
|
|
"exp":"x23"
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"∨",
|
|
"left":{
|
|
"op":"∨",
|
|
"left":false,
|
|
"right":{
|
|
"op":"∧",
|
|
"left":"x12",
|
|
"right":"x13"
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"∧",
|
|
"left":"x24",
|
|
"right":"x34"
|
|
}
|
|
}
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":1
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"x23",
|
|
"value":true
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
}
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"name":"M24",
|
|
"locations":[
|
|
{
|
|
"name":"location"
|
|
}
|
|
],
|
|
"initial-locations":[
|
|
"location"
|
|
],
|
|
"edges":[
|
|
{
|
|
"location":"location",
|
|
"action":"s24",
|
|
"guard":{
|
|
"exp":true
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":"p"
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"x24",
|
|
"value":true
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"probability":{
|
|
"exp":{
|
|
"op":"-",
|
|
"left":1,
|
|
"right":"p"
|
|
}
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"x24",
|
|
"value":false
|
|
}
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"tau__",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"pc",
|
|
"right":6
|
|
},
|
|
"right":{
|
|
"op":"¬",
|
|
"exp":"x24"
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"∨",
|
|
"left":{
|
|
"op":"∨",
|
|
"left":false,
|
|
"right":{
|
|
"op":"∧",
|
|
"left":"x12",
|
|
"right":"x14"
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"∧",
|
|
"left":"x23",
|
|
"right":"x34"
|
|
}
|
|
}
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":1
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"x24",
|
|
"value":true
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
}
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"name":"M34",
|
|
"locations":[
|
|
{
|
|
"name":"location"
|
|
}
|
|
],
|
|
"initial-locations":[
|
|
"location"
|
|
],
|
|
"edges":[
|
|
{
|
|
"location":"location",
|
|
"action":"s34",
|
|
"guard":{
|
|
"exp":true
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":"p"
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"x34",
|
|
"value":true
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"probability":{
|
|
"exp":{
|
|
"op":"-",
|
|
"left":1,
|
|
"right":"p"
|
|
}
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"x34",
|
|
"value":false
|
|
}
|
|
]
|
|
}
|
|
]
|
|
}
|
|
]
|
|
}
|
|
],
|
|
"system":{
|
|
"elements":[
|
|
{
|
|
"automaton":"PC"
|
|
},
|
|
{
|
|
"automaton":"M12"
|
|
},
|
|
{
|
|
"automaton":"M13"
|
|
},
|
|
{
|
|
"automaton":"M14"
|
|
},
|
|
{
|
|
"automaton":"M23"
|
|
},
|
|
{
|
|
"automaton":"M24"
|
|
},
|
|
{
|
|
"automaton":"M34"
|
|
}
|
|
],
|
|
"syncs":[
|
|
{
|
|
"synchronise":[
|
|
"s34",
|
|
null,
|
|
null,
|
|
null,
|
|
null,
|
|
null,
|
|
"s34"
|
|
],
|
|
"result":"s34"
|
|
},
|
|
{
|
|
"synchronise":[
|
|
"s24",
|
|
null,
|
|
null,
|
|
null,
|
|
null,
|
|
"s24",
|
|
null
|
|
],
|
|
"result":"s24"
|
|
},
|
|
{
|
|
"synchronise":[
|
|
"s23",
|
|
null,
|
|
null,
|
|
null,
|
|
"s23",
|
|
null,
|
|
null
|
|
],
|
|
"result":"s23"
|
|
},
|
|
{
|
|
"synchronise":[
|
|
"s14",
|
|
null,
|
|
null,
|
|
"s14",
|
|
null,
|
|
null,
|
|
null
|
|
],
|
|
"result":"s14"
|
|
},
|
|
{
|
|
"synchronise":[
|
|
"s13",
|
|
null,
|
|
"s13",
|
|
null,
|
|
null,
|
|
null,
|
|
null
|
|
],
|
|
"result":"s13"
|
|
},
|
|
{
|
|
"synchronise":[
|
|
"s12",
|
|
"s12",
|
|
null,
|
|
null,
|
|
null,
|
|
null,
|
|
null
|
|
],
|
|
"result":"s12"
|
|
},
|
|
{
|
|
"synchronise":[
|
|
null,
|
|
"tau__",
|
|
null,
|
|
null,
|
|
null,
|
|
null,
|
|
null
|
|
],
|
|
"result":"tau__"
|
|
},
|
|
{
|
|
"synchronise":[
|
|
null,
|
|
null,
|
|
null,
|
|
null,
|
|
"tau__",
|
|
null,
|
|
null
|
|
],
|
|
"result":"tau__"
|
|
},
|
|
{
|
|
"synchronise":[
|
|
null,
|
|
null,
|
|
null,
|
|
null,
|
|
null,
|
|
"tau__",
|
|
null
|
|
],
|
|
"result":"tau__"
|
|
}
|
|
]
|
|
}
|
|
}
|