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.
1755 lines
72 KiB
1755 lines
72 KiB
|
|
{
|
|
"jani-version":1,
|
|
"features":[
|
|
"derived-operators"
|
|
],
|
|
"name":"Converted from PRISM by IscasMC",
|
|
"type":"ctmc",
|
|
"actions":[
|
|
{
|
|
"name":"tau__"
|
|
},
|
|
{
|
|
"name":"input_reboot"
|
|
},
|
|
{
|
|
"name":"timeout"
|
|
},
|
|
{
|
|
"name":"output_reboot"
|
|
}
|
|
],
|
|
"constants":[
|
|
{
|
|
"name":"MAX_COUNT",
|
|
"type":"int"
|
|
}
|
|
],
|
|
"variables":[
|
|
{
|
|
"name":"s",
|
|
"type":{
|
|
"kind":"bounded",
|
|
"base":"int",
|
|
"lower-bound":0,
|
|
"upper-bound":3
|
|
}
|
|
},
|
|
{
|
|
"name":"i",
|
|
"type":{
|
|
"kind":"bounded",
|
|
"base":"int",
|
|
"lower-bound":0,
|
|
"upper-bound":2
|
|
}
|
|
},
|
|
{
|
|
"name":"a",
|
|
"type":{
|
|
"kind":"bounded",
|
|
"base":"int",
|
|
"lower-bound":0,
|
|
"upper-bound":2
|
|
}
|
|
},
|
|
{
|
|
"name":"m",
|
|
"type":{
|
|
"kind":"bounded",
|
|
"base":"int",
|
|
"lower-bound":0,
|
|
"upper-bound":1
|
|
}
|
|
},
|
|
{
|
|
"name":"count",
|
|
"type":{
|
|
"kind":"bounded",
|
|
"base":"int",
|
|
"lower-bound":0,
|
|
"upper-bound":{
|
|
"op":"+",
|
|
"left":"MAX_COUNT",
|
|
"right":1
|
|
}
|
|
}
|
|
},
|
|
{
|
|
"name":"comp",
|
|
"type":"bool"
|
|
},
|
|
{
|
|
"name":"reqi",
|
|
"type":"bool"
|
|
},
|
|
{
|
|
"name":"reqo",
|
|
"type":"bool"
|
|
},
|
|
{
|
|
"name":"o",
|
|
"type":{
|
|
"kind":"bounded",
|
|
"base":"int",
|
|
"lower-bound":0,
|
|
"upper-bound":2
|
|
}
|
|
}
|
|
],
|
|
"observables":[
|
|
{
|
|
"name":"\"up\""
|
|
},
|
|
{
|
|
"name":"\"danger\""
|
|
},
|
|
{
|
|
"name":"\"down\""
|
|
}
|
|
],
|
|
"initial-states":{
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"s",
|
|
"right":3
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"i",
|
|
"right":2
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"a",
|
|
"right":2
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"m",
|
|
"right":1
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"count",
|
|
"right":0
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"comp",
|
|
"right":true
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"reqi",
|
|
"right":true
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"reqo",
|
|
"right":false
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"o",
|
|
"right":2
|
|
}
|
|
}
|
|
},
|
|
"automata":[
|
|
{
|
|
"name":"sensors",
|
|
"locations":[
|
|
{
|
|
"name":"location",
|
|
"observables":[
|
|
{
|
|
"ref":"\"up\"",
|
|
"value":{
|
|
"op":"?:",
|
|
"args":[
|
|
{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"¬",
|
|
"exp":{
|
|
"op":"∨",
|
|
"left":{
|
|
"op":"∨",
|
|
"left":{
|
|
"op":"∨",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"i",
|
|
"right":2
|
|
},
|
|
"right":{
|
|
"op":"<",
|
|
"left":"s",
|
|
"right":2
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"count",
|
|
"right":{
|
|
"op":"+",
|
|
"left":"MAX_COUNT",
|
|
"right":1
|
|
}
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"o",
|
|
"right":2
|
|
},
|
|
"right":{
|
|
"op":"<",
|
|
"left":"a",
|
|
"right":1
|
|
}
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"m",
|
|
"right":0
|
|
}
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"¬",
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"¬",
|
|
"exp":{
|
|
"op":"∨",
|
|
"left":{
|
|
"op":"∨",
|
|
"left":{
|
|
"op":"∨",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"i",
|
|
"right":2
|
|
},
|
|
"right":{
|
|
"op":"<",
|
|
"left":"s",
|
|
"right":2
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"count",
|
|
"right":{
|
|
"op":"+",
|
|
"left":"MAX_COUNT",
|
|
"right":1
|
|
}
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"o",
|
|
"right":2
|
|
},
|
|
"right":{
|
|
"op":"<",
|
|
"left":"a",
|
|
"right":1
|
|
}
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"m",
|
|
"right":0
|
|
}
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"∨",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"i",
|
|
"right":1
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"o",
|
|
"right":1
|
|
}
|
|
}
|
|
}
|
|
}
|
|
},
|
|
{
|
|
"op":"/",
|
|
"left":1,
|
|
"right":3600
|
|
},
|
|
0
|
|
]
|
|
}
|
|
},
|
|
{
|
|
"ref":"\"danger\"",
|
|
"value":{
|
|
"op":"?:",
|
|
"args":[
|
|
{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"¬",
|
|
"exp":{
|
|
"op":"∨",
|
|
"left":{
|
|
"op":"∨",
|
|
"left":{
|
|
"op":"∨",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"i",
|
|
"right":2
|
|
},
|
|
"right":{
|
|
"op":"<",
|
|
"left":"s",
|
|
"right":2
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"count",
|
|
"right":{
|
|
"op":"+",
|
|
"left":"MAX_COUNT",
|
|
"right":1
|
|
}
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"o",
|
|
"right":2
|
|
},
|
|
"right":{
|
|
"op":"<",
|
|
"left":"a",
|
|
"right":1
|
|
}
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"m",
|
|
"right":0
|
|
}
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"∨",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"i",
|
|
"right":1
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"o",
|
|
"right":1
|
|
}
|
|
}
|
|
},
|
|
{
|
|
"op":"/",
|
|
"left":1,
|
|
"right":3600
|
|
},
|
|
0
|
|
]
|
|
}
|
|
},
|
|
{
|
|
"ref":"\"down\"",
|
|
"value":{
|
|
"op":"?:",
|
|
"args":[
|
|
{
|
|
"op":"∨",
|
|
"left":{
|
|
"op":"∨",
|
|
"left":{
|
|
"op":"∨",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"i",
|
|
"right":2
|
|
},
|
|
"right":{
|
|
"op":"<",
|
|
"left":"s",
|
|
"right":2
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"count",
|
|
"right":{
|
|
"op":"+",
|
|
"left":"MAX_COUNT",
|
|
"right":1
|
|
}
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"o",
|
|
"right":2
|
|
},
|
|
"right":{
|
|
"op":"<",
|
|
"left":"a",
|
|
"right":1
|
|
}
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"m",
|
|
"right":0
|
|
}
|
|
},
|
|
{
|
|
"op":"/",
|
|
"left":1,
|
|
"right":3600
|
|
},
|
|
0
|
|
]
|
|
}
|
|
}
|
|
]
|
|
}
|
|
],
|
|
"initial-locations":[
|
|
"location"
|
|
],
|
|
"edges":[
|
|
{
|
|
"location":"location",
|
|
"action":"tau__",
|
|
"rate":{
|
|
"exp":{
|
|
"op":"*",
|
|
"left":"s",
|
|
"right":{
|
|
"op":"/",
|
|
"left":1,
|
|
"right":{
|
|
"op":"*",
|
|
"left":{
|
|
"op":"*",
|
|
"left":{
|
|
"op":"*",
|
|
"left":30,
|
|
"right":24
|
|
},
|
|
"right":60
|
|
},
|
|
"right":60
|
|
}
|
|
}
|
|
}
|
|
},
|
|
"guard":{
|
|
"exp":{
|
|
"op":">",
|
|
"left":"s",
|
|
"right":1
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":{
|
|
"op":"/",
|
|
"left":{
|
|
"op":"*",
|
|
"left":"s",
|
|
"right":{
|
|
"op":"/",
|
|
"left":1,
|
|
"right":{
|
|
"op":"*",
|
|
"left":{
|
|
"op":"*",
|
|
"left":{
|
|
"op":"*",
|
|
"left":30,
|
|
"right":24
|
|
},
|
|
"right":60
|
|
},
|
|
"right":60
|
|
}
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"*",
|
|
"left":"s",
|
|
"right":{
|
|
"op":"/",
|
|
"left":1,
|
|
"right":{
|
|
"op":"*",
|
|
"left":{
|
|
"op":"*",
|
|
"left":{
|
|
"op":"*",
|
|
"left":30,
|
|
"right":24
|
|
},
|
|
"right":60
|
|
},
|
|
"right":60
|
|
}
|
|
}
|
|
}
|
|
}
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"s",
|
|
"value":{
|
|
"op":"-",
|
|
"left":"s",
|
|
"right":1
|
|
}
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
}
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"name":"proci",
|
|
"locations":[
|
|
{
|
|
"name":"location"
|
|
}
|
|
],
|
|
"initial-locations":[
|
|
"location"
|
|
],
|
|
"edges":[
|
|
{
|
|
"location":"location",
|
|
"action":"tau__",
|
|
"rate":{
|
|
"exp":{
|
|
"op":"/",
|
|
"left":1,
|
|
"right":{
|
|
"op":"*",
|
|
"left":{
|
|
"op":"*",
|
|
"left":{
|
|
"op":"*",
|
|
"left":365,
|
|
"right":24
|
|
},
|
|
"right":60
|
|
},
|
|
"right":60
|
|
}
|
|
}
|
|
},
|
|
"guard":{
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":">",
|
|
"left":"i",
|
|
"right":0
|
|
},
|
|
"right":{
|
|
"op":"≥",
|
|
"left":"s",
|
|
"right":2
|
|
}
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":{
|
|
"op":"/",
|
|
"left":{
|
|
"op":"/",
|
|
"left":1,
|
|
"right":{
|
|
"op":"*",
|
|
"left":{
|
|
"op":"*",
|
|
"left":{
|
|
"op":"*",
|
|
"left":365,
|
|
"right":24
|
|
},
|
|
"right":60
|
|
},
|
|
"right":60
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"/",
|
|
"left":1,
|
|
"right":{
|
|
"op":"*",
|
|
"left":{
|
|
"op":"*",
|
|
"left":{
|
|
"op":"*",
|
|
"left":365,
|
|
"right":24
|
|
},
|
|
"right":60
|
|
},
|
|
"right":60
|
|
}
|
|
}
|
|
}
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"i",
|
|
"value":0
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"tau__",
|
|
"rate":{
|
|
"exp":{
|
|
"op":"/",
|
|
"left":1,
|
|
"right":{
|
|
"op":"*",
|
|
"left":{
|
|
"op":"*",
|
|
"left":24,
|
|
"right":60
|
|
},
|
|
"right":60
|
|
}
|
|
}
|
|
},
|
|
"guard":{
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"i",
|
|
"right":2
|
|
},
|
|
"right":{
|
|
"op":"≥",
|
|
"left":"s",
|
|
"right":2
|
|
}
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":{
|
|
"op":"/",
|
|
"left":{
|
|
"op":"/",
|
|
"left":1,
|
|
"right":{
|
|
"op":"*",
|
|
"left":{
|
|
"op":"*",
|
|
"left":24,
|
|
"right":60
|
|
},
|
|
"right":60
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"/",
|
|
"left":1,
|
|
"right":{
|
|
"op":"*",
|
|
"left":{
|
|
"op":"*",
|
|
"left":24,
|
|
"right":60
|
|
},
|
|
"right":60
|
|
}
|
|
}
|
|
}
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"i",
|
|
"value":1
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"input_reboot",
|
|
"rate":{
|
|
"exp":{
|
|
"op":"/",
|
|
"left":1,
|
|
"right":30
|
|
}
|
|
},
|
|
"guard":{
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"i",
|
|
"right":1
|
|
},
|
|
"right":{
|
|
"op":"≥",
|
|
"left":"s",
|
|
"right":2
|
|
}
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":{
|
|
"op":"/",
|
|
"left":{
|
|
"op":"/",
|
|
"left":1,
|
|
"right":30
|
|
},
|
|
"right":{
|
|
"op":"/",
|
|
"left":1,
|
|
"right":30
|
|
}
|
|
}
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"i",
|
|
"value":2
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
}
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"name":"actuators",
|
|
"locations":[
|
|
{
|
|
"name":"location"
|
|
}
|
|
],
|
|
"initial-locations":[
|
|
"location"
|
|
],
|
|
"edges":[
|
|
{
|
|
"location":"location",
|
|
"action":"tau__",
|
|
"rate":{
|
|
"exp":{
|
|
"op":"*",
|
|
"left":"a",
|
|
"right":{
|
|
"op":"/",
|
|
"left":1,
|
|
"right":{
|
|
"op":"*",
|
|
"left":{
|
|
"op":"*",
|
|
"left":{
|
|
"op":"*",
|
|
"left":{
|
|
"op":"*",
|
|
"left":2,
|
|
"right":30
|
|
},
|
|
"right":24
|
|
},
|
|
"right":60
|
|
},
|
|
"right":60
|
|
}
|
|
}
|
|
}
|
|
},
|
|
"guard":{
|
|
"exp":{
|
|
"op":">",
|
|
"left":"a",
|
|
"right":0
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":{
|
|
"op":"/",
|
|
"left":{
|
|
"op":"*",
|
|
"left":"a",
|
|
"right":{
|
|
"op":"/",
|
|
"left":1,
|
|
"right":{
|
|
"op":"*",
|
|
"left":{
|
|
"op":"*",
|
|
"left":{
|
|
"op":"*",
|
|
"left":{
|
|
"op":"*",
|
|
"left":2,
|
|
"right":30
|
|
},
|
|
"right":24
|
|
},
|
|
"right":60
|
|
},
|
|
"right":60
|
|
}
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"*",
|
|
"left":"a",
|
|
"right":{
|
|
"op":"/",
|
|
"left":1,
|
|
"right":{
|
|
"op":"*",
|
|
"left":{
|
|
"op":"*",
|
|
"left":{
|
|
"op":"*",
|
|
"left":{
|
|
"op":"*",
|
|
"left":2,
|
|
"right":30
|
|
},
|
|
"right":24
|
|
},
|
|
"right":60
|
|
},
|
|
"right":60
|
|
}
|
|
}
|
|
}
|
|
}
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"a",
|
|
"value":{
|
|
"op":"-",
|
|
"left":"a",
|
|
"right":1
|
|
}
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
}
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"name":"procm",
|
|
"locations":[
|
|
{
|
|
"name":"location"
|
|
}
|
|
],
|
|
"initial-locations":[
|
|
"location"
|
|
],
|
|
"edges":[
|
|
{
|
|
"location":"location",
|
|
"action":"tau__",
|
|
"rate":{
|
|
"exp":{
|
|
"op":"/",
|
|
"left":1,
|
|
"right":{
|
|
"op":"*",
|
|
"left":{
|
|
"op":"*",
|
|
"left":{
|
|
"op":"*",
|
|
"left":365,
|
|
"right":24
|
|
},
|
|
"right":60
|
|
},
|
|
"right":60
|
|
}
|
|
}
|
|
},
|
|
"guard":{
|
|
"exp":{
|
|
"op":"=",
|
|
"left":"m",
|
|
"right":1
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":{
|
|
"op":"/",
|
|
"left":{
|
|
"op":"/",
|
|
"left":1,
|
|
"right":{
|
|
"op":"*",
|
|
"left":{
|
|
"op":"*",
|
|
"left":{
|
|
"op":"*",
|
|
"left":365,
|
|
"right":24
|
|
},
|
|
"right":60
|
|
},
|
|
"right":60
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"/",
|
|
"left":1,
|
|
"right":{
|
|
"op":"*",
|
|
"left":{
|
|
"op":"*",
|
|
"left":{
|
|
"op":"*",
|
|
"left":365,
|
|
"right":24
|
|
},
|
|
"right":60
|
|
},
|
|
"right":60
|
|
}
|
|
}
|
|
}
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"m",
|
|
"value":0
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"timeout",
|
|
"rate":{
|
|
"exp":{
|
|
"op":"/",
|
|
"left":1,
|
|
"right":60
|
|
}
|
|
},
|
|
"guard":{
|
|
"exp":"comp"
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":{
|
|
"op":"/",
|
|
"left":{
|
|
"op":"/",
|
|
"left":1,
|
|
"right":60
|
|
},
|
|
"right":{
|
|
"op":"/",
|
|
"left":1,
|
|
"right":60
|
|
}
|
|
}
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"count",
|
|
"value":0
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"timeout",
|
|
"rate":{
|
|
"exp":{
|
|
"op":"/",
|
|
"left":1,
|
|
"right":60
|
|
}
|
|
},
|
|
"guard":{
|
|
"exp":{
|
|
"op":"¬",
|
|
"exp":"comp"
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":{
|
|
"op":"/",
|
|
"left":{
|
|
"op":"/",
|
|
"left":1,
|
|
"right":60
|
|
},
|
|
"right":{
|
|
"op":"/",
|
|
"left":1,
|
|
"right":60
|
|
}
|
|
}
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"count",
|
|
"value":{
|
|
"op":"min",
|
|
"left":{
|
|
"op":"+",
|
|
"left":"count",
|
|
"right":1
|
|
},
|
|
"right":{
|
|
"op":"+",
|
|
"left":"MAX_COUNT",
|
|
"right":1
|
|
}
|
|
}
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
}
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"name":"bus",
|
|
"locations":[
|
|
{
|
|
"name":"location"
|
|
}
|
|
],
|
|
"initial-locations":[
|
|
"location"
|
|
],
|
|
"edges":[
|
|
{
|
|
"location":"location",
|
|
"action":"input_reboot",
|
|
"rate":{
|
|
"exp":1
|
|
},
|
|
"guard":{
|
|
"exp":true
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":{
|
|
"op":"/",
|
|
"left":1,
|
|
"right":1
|
|
}
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"comp",
|
|
"value":{
|
|
"op":"∨",
|
|
"left":"comp",
|
|
"right":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"m",
|
|
"right":1
|
|
},
|
|
"right":{
|
|
"op":"¬",
|
|
"exp":"reqo"
|
|
}
|
|
}
|
|
}
|
|
},
|
|
{
|
|
"ref":"reqi",
|
|
"value":true
|
|
},
|
|
{
|
|
"ref":"reqo",
|
|
"value":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"¬",
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"o",
|
|
"right":2
|
|
},
|
|
"right":{
|
|
"op":"≥",
|
|
"left":"a",
|
|
"right":1
|
|
}
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"∨",
|
|
"left":"reqo",
|
|
"right":{
|
|
"op":"=",
|
|
"left":"m",
|
|
"right":1
|
|
}
|
|
}
|
|
}
|
|
}
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"output_reboot",
|
|
"rate":{
|
|
"exp":1
|
|
},
|
|
"guard":{
|
|
"exp":true
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":{
|
|
"op":"/",
|
|
"left":1,
|
|
"right":1
|
|
}
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"comp",
|
|
"value":{
|
|
"op":"∨",
|
|
"left":"comp",
|
|
"right":{
|
|
"op":"∧",
|
|
"left":"reqi",
|
|
"right":{
|
|
"op":"=",
|
|
"left":"m",
|
|
"right":1
|
|
}
|
|
}
|
|
}
|
|
},
|
|
{
|
|
"ref":"reqi",
|
|
"value":{
|
|
"op":"∨",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"i",
|
|
"right":2
|
|
},
|
|
"right":{
|
|
"op":"≥",
|
|
"left":"s",
|
|
"right":2
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"∧",
|
|
"left":"reqi",
|
|
"right":{
|
|
"op":"=",
|
|
"left":"m",
|
|
"right":0
|
|
}
|
|
}
|
|
}
|
|
},
|
|
{
|
|
"ref":"reqo",
|
|
"value":false
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"timeout",
|
|
"rate":{
|
|
"exp":1
|
|
},
|
|
"guard":{
|
|
"exp":true
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":{
|
|
"op":"/",
|
|
"left":1,
|
|
"right":1
|
|
}
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"comp",
|
|
"value":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":"reqi",
|
|
"right":{
|
|
"op":"¬",
|
|
"exp":"reqo"
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"m",
|
|
"right":1
|
|
}
|
|
}
|
|
},
|
|
{
|
|
"ref":"reqi",
|
|
"value":{
|
|
"op":"∨",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"i",
|
|
"right":2
|
|
},
|
|
"right":{
|
|
"op":"≥",
|
|
"left":"s",
|
|
"right":2
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"∧",
|
|
"left":"reqi",
|
|
"right":{
|
|
"op":"∨",
|
|
"left":"reqo",
|
|
"right":{
|
|
"op":"=",
|
|
"left":"m",
|
|
"right":0
|
|
}
|
|
}
|
|
}
|
|
}
|
|
},
|
|
{
|
|
"ref":"reqo",
|
|
"value":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"¬",
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"o",
|
|
"right":2
|
|
},
|
|
"right":{
|
|
"op":"≥",
|
|
"left":"a",
|
|
"right":1
|
|
}
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"∨",
|
|
"left":"reqo",
|
|
"right":{
|
|
"op":"∧",
|
|
"left":"reqi",
|
|
"right":{
|
|
"op":"=",
|
|
"left":"m",
|
|
"right":1
|
|
}
|
|
}
|
|
}
|
|
}
|
|
}
|
|
]
|
|
}
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"name":"proco",
|
|
"locations":[
|
|
{
|
|
"name":"location"
|
|
}
|
|
],
|
|
"initial-locations":[
|
|
"location"
|
|
],
|
|
"edges":[
|
|
{
|
|
"location":"location",
|
|
"action":"tau__",
|
|
"rate":{
|
|
"exp":{
|
|
"op":"/",
|
|
"left":1,
|
|
"right":{
|
|
"op":"*",
|
|
"left":{
|
|
"op":"*",
|
|
"left":{
|
|
"op":"*",
|
|
"left":365,
|
|
"right":24
|
|
},
|
|
"right":60
|
|
},
|
|
"right":60
|
|
}
|
|
}
|
|
},
|
|
"guard":{
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":">",
|
|
"left":"o",
|
|
"right":0
|
|
},
|
|
"right":{
|
|
"op":"≥",
|
|
"left":"a",
|
|
"right":1
|
|
}
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":{
|
|
"op":"/",
|
|
"left":{
|
|
"op":"/",
|
|
"left":1,
|
|
"right":{
|
|
"op":"*",
|
|
"left":{
|
|
"op":"*",
|
|
"left":{
|
|
"op":"*",
|
|
"left":365,
|
|
"right":24
|
|
},
|
|
"right":60
|
|
},
|
|
"right":60
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"/",
|
|
"left":1,
|
|
"right":{
|
|
"op":"*",
|
|
"left":{
|
|
"op":"*",
|
|
"left":{
|
|
"op":"*",
|
|
"left":365,
|
|
"right":24
|
|
},
|
|
"right":60
|
|
},
|
|
"right":60
|
|
}
|
|
}
|
|
}
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"o",
|
|
"value":0
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"tau__",
|
|
"rate":{
|
|
"exp":{
|
|
"op":"/",
|
|
"left":1,
|
|
"right":{
|
|
"op":"*",
|
|
"left":{
|
|
"op":"*",
|
|
"left":24,
|
|
"right":60
|
|
},
|
|
"right":60
|
|
}
|
|
}
|
|
},
|
|
"guard":{
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"o",
|
|
"right":2
|
|
},
|
|
"right":{
|
|
"op":"≥",
|
|
"left":"a",
|
|
"right":1
|
|
}
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":{
|
|
"op":"/",
|
|
"left":{
|
|
"op":"/",
|
|
"left":1,
|
|
"right":{
|
|
"op":"*",
|
|
"left":{
|
|
"op":"*",
|
|
"left":24,
|
|
"right":60
|
|
},
|
|
"right":60
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"/",
|
|
"left":1,
|
|
"right":{
|
|
"op":"*",
|
|
"left":{
|
|
"op":"*",
|
|
"left":24,
|
|
"right":60
|
|
},
|
|
"right":60
|
|
}
|
|
}
|
|
}
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"o",
|
|
"value":1
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"output_reboot",
|
|
"rate":{
|
|
"exp":{
|
|
"op":"/",
|
|
"left":1,
|
|
"right":30
|
|
}
|
|
},
|
|
"guard":{
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"o",
|
|
"right":1
|
|
},
|
|
"right":{
|
|
"op":"≥",
|
|
"left":"a",
|
|
"right":1
|
|
}
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":{
|
|
"op":"/",
|
|
"left":{
|
|
"op":"/",
|
|
"left":1,
|
|
"right":30
|
|
},
|
|
"right":{
|
|
"op":"/",
|
|
"left":1,
|
|
"right":30
|
|
}
|
|
}
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"o",
|
|
"value":2
|
|
}
|
|
]
|
|
}
|
|
]
|
|
}
|
|
]
|
|
}
|
|
],
|
|
"system":{
|
|
"elements":[
|
|
{
|
|
"automaton":"sensors"
|
|
},
|
|
{
|
|
"automaton":"proci"
|
|
},
|
|
{
|
|
"automaton":"actuators"
|
|
},
|
|
{
|
|
"automaton":"procm"
|
|
},
|
|
{
|
|
"automaton":"bus"
|
|
},
|
|
{
|
|
"automaton":"proco"
|
|
}
|
|
],
|
|
"syncs":[
|
|
{
|
|
"synchronise":[
|
|
null,
|
|
null,
|
|
null,
|
|
null,
|
|
"output_reboot",
|
|
"output_reboot"
|
|
],
|
|
"result":"output_reboot"
|
|
},
|
|
{
|
|
"synchronise":[
|
|
null,
|
|
"input_reboot",
|
|
null,
|
|
null,
|
|
"input_reboot",
|
|
null
|
|
],
|
|
"result":"input_reboot"
|
|
},
|
|
{
|
|
"synchronise":[
|
|
null,
|
|
null,
|
|
null,
|
|
"timeout",
|
|
"timeout",
|
|
null
|
|
],
|
|
"result":"timeout"
|
|
},
|
|
{
|
|
"synchronise":[
|
|
"tau__",
|
|
null,
|
|
null,
|
|
null,
|
|
null,
|
|
null
|
|
],
|
|
"result":"tau__"
|
|
},
|
|
{
|
|
"synchronise":[
|
|
null,
|
|
"tau__",
|
|
null,
|
|
null,
|
|
null,
|
|
null
|
|
],
|
|
"result":"tau__"
|
|
},
|
|
{
|
|
"synchronise":[
|
|
null,
|
|
null,
|
|
"tau__",
|
|
null,
|
|
null,
|
|
null
|
|
],
|
|
"result":"tau__"
|
|
},
|
|
{
|
|
"synchronise":[
|
|
null,
|
|
null,
|
|
null,
|
|
"tau__",
|
|
null,
|
|
null
|
|
],
|
|
"result":"tau__"
|
|
},
|
|
{
|
|
"synchronise":[
|
|
null,
|
|
null,
|
|
null,
|
|
null,
|
|
null,
|
|
"tau__"
|
|
],
|
|
"result":"tau__"
|
|
}
|
|
]
|
|
}
|
|
}
|