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.
2788 lines
105 KiB
2788 lines
105 KiB
|
|
{
|
|
"jani-version":1,
|
|
"features":[
|
|
"derived-operators"
|
|
],
|
|
"name":"Converted from PRISM by IscasMC",
|
|
"type":"mdp",
|
|
"actions":[
|
|
{
|
|
"name":"tau__"
|
|
},
|
|
{
|
|
"name":"done"
|
|
}
|
|
],
|
|
"variables":[
|
|
{
|
|
"name":"pay",
|
|
"type":{
|
|
"kind":"bounded",
|
|
"base":"int",
|
|
"lower-bound":0,
|
|
"upper-bound":7
|
|
}
|
|
},
|
|
{
|
|
"name":"coin1",
|
|
"type":{
|
|
"kind":"bounded",
|
|
"base":"int",
|
|
"lower-bound":0,
|
|
"upper-bound":2
|
|
}
|
|
},
|
|
{
|
|
"name":"s1",
|
|
"type":{
|
|
"kind":"bounded",
|
|
"base":"int",
|
|
"lower-bound":0,
|
|
"upper-bound":1
|
|
}
|
|
},
|
|
{
|
|
"name":"agree1",
|
|
"type":{
|
|
"kind":"bounded",
|
|
"base":"int",
|
|
"lower-bound":0,
|
|
"upper-bound":1
|
|
}
|
|
},
|
|
{
|
|
"name":"coin2",
|
|
"type":{
|
|
"kind":"bounded",
|
|
"base":"int",
|
|
"lower-bound":0,
|
|
"upper-bound":2
|
|
}
|
|
},
|
|
{
|
|
"name":"s2",
|
|
"type":{
|
|
"kind":"bounded",
|
|
"base":"int",
|
|
"lower-bound":0,
|
|
"upper-bound":1
|
|
}
|
|
},
|
|
{
|
|
"name":"agree2",
|
|
"type":{
|
|
"kind":"bounded",
|
|
"base":"int",
|
|
"lower-bound":0,
|
|
"upper-bound":1
|
|
}
|
|
},
|
|
{
|
|
"name":"coin3",
|
|
"type":{
|
|
"kind":"bounded",
|
|
"base":"int",
|
|
"lower-bound":0,
|
|
"upper-bound":2
|
|
}
|
|
},
|
|
{
|
|
"name":"s3",
|
|
"type":{
|
|
"kind":"bounded",
|
|
"base":"int",
|
|
"lower-bound":0,
|
|
"upper-bound":1
|
|
}
|
|
},
|
|
{
|
|
"name":"agree3",
|
|
"type":{
|
|
"kind":"bounded",
|
|
"base":"int",
|
|
"lower-bound":0,
|
|
"upper-bound":1
|
|
}
|
|
},
|
|
{
|
|
"name":"coin4",
|
|
"type":{
|
|
"kind":"bounded",
|
|
"base":"int",
|
|
"lower-bound":0,
|
|
"upper-bound":2
|
|
}
|
|
},
|
|
{
|
|
"name":"s4",
|
|
"type":{
|
|
"kind":"bounded",
|
|
"base":"int",
|
|
"lower-bound":0,
|
|
"upper-bound":1
|
|
}
|
|
},
|
|
{
|
|
"name":"agree4",
|
|
"type":{
|
|
"kind":"bounded",
|
|
"base":"int",
|
|
"lower-bound":0,
|
|
"upper-bound":1
|
|
}
|
|
},
|
|
{
|
|
"name":"coin5",
|
|
"type":{
|
|
"kind":"bounded",
|
|
"base":"int",
|
|
"lower-bound":0,
|
|
"upper-bound":2
|
|
}
|
|
},
|
|
{
|
|
"name":"s5",
|
|
"type":{
|
|
"kind":"bounded",
|
|
"base":"int",
|
|
"lower-bound":0,
|
|
"upper-bound":1
|
|
}
|
|
},
|
|
{
|
|
"name":"agree5",
|
|
"type":{
|
|
"kind":"bounded",
|
|
"base":"int",
|
|
"lower-bound":0,
|
|
"upper-bound":1
|
|
}
|
|
},
|
|
{
|
|
"name":"coin6",
|
|
"type":{
|
|
"kind":"bounded",
|
|
"base":"int",
|
|
"lower-bound":0,
|
|
"upper-bound":2
|
|
}
|
|
},
|
|
{
|
|
"name":"s6",
|
|
"type":{
|
|
"kind":"bounded",
|
|
"base":"int",
|
|
"lower-bound":0,
|
|
"upper-bound":1
|
|
}
|
|
},
|
|
{
|
|
"name":"agree6",
|
|
"type":{
|
|
"kind":"bounded",
|
|
"base":"int",
|
|
"lower-bound":0,
|
|
"upper-bound":1
|
|
}
|
|
},
|
|
{
|
|
"name":"coin7",
|
|
"type":{
|
|
"kind":"bounded",
|
|
"base":"int",
|
|
"lower-bound":0,
|
|
"upper-bound":2
|
|
}
|
|
},
|
|
{
|
|
"name":"s7",
|
|
"type":{
|
|
"kind":"bounded",
|
|
"base":"int",
|
|
"lower-bound":0,
|
|
"upper-bound":1
|
|
}
|
|
},
|
|
{
|
|
"name":"agree7",
|
|
"type":{
|
|
"kind":"bounded",
|
|
"base":"int",
|
|
"lower-bound":0,
|
|
"upper-bound":1
|
|
}
|
|
}
|
|
],
|
|
"observables":[
|
|
],
|
|
"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":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"coin1",
|
|
"right":0
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"s1",
|
|
"right":0
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"agree1",
|
|
"right":0
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"coin2",
|
|
"right":0
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"s2",
|
|
"right":0
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"agree2",
|
|
"right":0
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"coin3",
|
|
"right":0
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"s3",
|
|
"right":0
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"agree3",
|
|
"right":0
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"coin4",
|
|
"right":0
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"s4",
|
|
"right":0
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"agree4",
|
|
"right":0
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"coin5",
|
|
"right":0
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"s5",
|
|
"right":0
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"agree5",
|
|
"right":0
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"coin6",
|
|
"right":0
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"s6",
|
|
"right":0
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"agree6",
|
|
"right":0
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"coin7",
|
|
"right":0
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"s7",
|
|
"right":0
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"agree7",
|
|
"right":0
|
|
}
|
|
}
|
|
},
|
|
"automata":[
|
|
{
|
|
"name":"crypt1",
|
|
"locations":[
|
|
{
|
|
"name":"location"
|
|
}
|
|
],
|
|
"initial-locations":[
|
|
"location"
|
|
],
|
|
"edges":[
|
|
{
|
|
"location":"location",
|
|
"action":"tau__",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"=",
|
|
"left":"coin1",
|
|
"right":0
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":0.5000000
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"coin1",
|
|
"value":1
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
},
|
|
{
|
|
"probability":{
|
|
"exp":0.5000000
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"coin1",
|
|
"value":2
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"tau__",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"s1",
|
|
"right":0
|
|
},
|
|
"right":{
|
|
"op":">",
|
|
"left":"coin1",
|
|
"right":0
|
|
}
|
|
},
|
|
"right":{
|
|
"op":">",
|
|
"left":"coin2",
|
|
"right":0
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"coin1",
|
|
"right":"coin2"
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"≠",
|
|
"left":"pay",
|
|
"right":1
|
|
}
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":1
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"s1",
|
|
"value":1
|
|
},
|
|
{
|
|
"ref":"agree1",
|
|
"value":1
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"tau__",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"s1",
|
|
"right":0
|
|
},
|
|
"right":{
|
|
"op":">",
|
|
"left":"coin1",
|
|
"right":0
|
|
}
|
|
},
|
|
"right":{
|
|
"op":">",
|
|
"left":"coin2",
|
|
"right":0
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"¬",
|
|
"exp":{
|
|
"op":"=",
|
|
"left":"coin1",
|
|
"right":"coin2"
|
|
}
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"≠",
|
|
"left":"pay",
|
|
"right":1
|
|
}
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":1
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"s1",
|
|
"value":1
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"tau__",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"s1",
|
|
"right":0
|
|
},
|
|
"right":{
|
|
"op":">",
|
|
"left":"coin1",
|
|
"right":0
|
|
}
|
|
},
|
|
"right":{
|
|
"op":">",
|
|
"left":"coin2",
|
|
"right":0
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"coin1",
|
|
"right":"coin2"
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"pay",
|
|
"right":1
|
|
}
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":1
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"s1",
|
|
"value":1
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"tau__",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"s1",
|
|
"right":0
|
|
},
|
|
"right":{
|
|
"op":">",
|
|
"left":"coin1",
|
|
"right":0
|
|
}
|
|
},
|
|
"right":{
|
|
"op":">",
|
|
"left":"coin2",
|
|
"right":0
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"¬",
|
|
"exp":{
|
|
"op":"=",
|
|
"left":"coin1",
|
|
"right":"coin2"
|
|
}
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"pay",
|
|
"right":1
|
|
}
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":1
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"s1",
|
|
"value":1
|
|
},
|
|
{
|
|
"ref":"agree1",
|
|
"value":1
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"done",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"=",
|
|
"left":"s1",
|
|
"right":1
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":1
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
],
|
|
"observables":[
|
|
]
|
|
}
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"name":"crypt2",
|
|
"locations":[
|
|
{
|
|
"name":"location"
|
|
}
|
|
],
|
|
"initial-locations":[
|
|
"location"
|
|
],
|
|
"edges":[
|
|
{
|
|
"location":"location",
|
|
"action":"tau__",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"=",
|
|
"left":"coin2",
|
|
"right":0
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":0.5000000
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"coin2",
|
|
"value":1
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
},
|
|
{
|
|
"probability":{
|
|
"exp":0.5000000
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"coin2",
|
|
"value":2
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"tau__",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"s2",
|
|
"right":0
|
|
},
|
|
"right":{
|
|
"op":">",
|
|
"left":"coin2",
|
|
"right":0
|
|
}
|
|
},
|
|
"right":{
|
|
"op":">",
|
|
"left":"coin3",
|
|
"right":0
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"coin2",
|
|
"right":"coin3"
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"≠",
|
|
"left":"pay",
|
|
"right":2
|
|
}
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":1
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"s2",
|
|
"value":1
|
|
},
|
|
{
|
|
"ref":"agree2",
|
|
"value":1
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"tau__",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"s2",
|
|
"right":0
|
|
},
|
|
"right":{
|
|
"op":">",
|
|
"left":"coin2",
|
|
"right":0
|
|
}
|
|
},
|
|
"right":{
|
|
"op":">",
|
|
"left":"coin3",
|
|
"right":0
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"¬",
|
|
"exp":{
|
|
"op":"=",
|
|
"left":"coin2",
|
|
"right":"coin3"
|
|
}
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"≠",
|
|
"left":"pay",
|
|
"right":2
|
|
}
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":1
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"s2",
|
|
"value":1
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"tau__",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"s2",
|
|
"right":0
|
|
},
|
|
"right":{
|
|
"op":">",
|
|
"left":"coin2",
|
|
"right":0
|
|
}
|
|
},
|
|
"right":{
|
|
"op":">",
|
|
"left":"coin3",
|
|
"right":0
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"coin2",
|
|
"right":"coin3"
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"pay",
|
|
"right":2
|
|
}
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":1
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"s2",
|
|
"value":1
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"tau__",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"s2",
|
|
"right":0
|
|
},
|
|
"right":{
|
|
"op":">",
|
|
"left":"coin2",
|
|
"right":0
|
|
}
|
|
},
|
|
"right":{
|
|
"op":">",
|
|
"left":"coin3",
|
|
"right":0
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"¬",
|
|
"exp":{
|
|
"op":"=",
|
|
"left":"coin2",
|
|
"right":"coin3"
|
|
}
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"pay",
|
|
"right":2
|
|
}
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":1
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"s2",
|
|
"value":1
|
|
},
|
|
{
|
|
"ref":"agree2",
|
|
"value":1
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"done",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"=",
|
|
"left":"s2",
|
|
"right":1
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":1
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
]
|
|
}
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"name":"crypt3",
|
|
"locations":[
|
|
{
|
|
"name":"location"
|
|
}
|
|
],
|
|
"initial-locations":[
|
|
"location"
|
|
],
|
|
"edges":[
|
|
{
|
|
"location":"location",
|
|
"action":"tau__",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"=",
|
|
"left":"coin3",
|
|
"right":0
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":0.5000000
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"coin3",
|
|
"value":1
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
},
|
|
{
|
|
"probability":{
|
|
"exp":0.5000000
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"coin3",
|
|
"value":2
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"tau__",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"s3",
|
|
"right":0
|
|
},
|
|
"right":{
|
|
"op":">",
|
|
"left":"coin3",
|
|
"right":0
|
|
}
|
|
},
|
|
"right":{
|
|
"op":">",
|
|
"left":"coin4",
|
|
"right":0
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"coin3",
|
|
"right":"coin4"
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"≠",
|
|
"left":"pay",
|
|
"right":3
|
|
}
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":1
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"s3",
|
|
"value":1
|
|
},
|
|
{
|
|
"ref":"agree3",
|
|
"value":1
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"tau__",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"s3",
|
|
"right":0
|
|
},
|
|
"right":{
|
|
"op":">",
|
|
"left":"coin3",
|
|
"right":0
|
|
}
|
|
},
|
|
"right":{
|
|
"op":">",
|
|
"left":"coin4",
|
|
"right":0
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"¬",
|
|
"exp":{
|
|
"op":"=",
|
|
"left":"coin3",
|
|
"right":"coin4"
|
|
}
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"≠",
|
|
"left":"pay",
|
|
"right":3
|
|
}
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":1
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"s3",
|
|
"value":1
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"tau__",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"s3",
|
|
"right":0
|
|
},
|
|
"right":{
|
|
"op":">",
|
|
"left":"coin3",
|
|
"right":0
|
|
}
|
|
},
|
|
"right":{
|
|
"op":">",
|
|
"left":"coin4",
|
|
"right":0
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"coin3",
|
|
"right":"coin4"
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"pay",
|
|
"right":3
|
|
}
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":1
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"s3",
|
|
"value":1
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"tau__",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"s3",
|
|
"right":0
|
|
},
|
|
"right":{
|
|
"op":">",
|
|
"left":"coin3",
|
|
"right":0
|
|
}
|
|
},
|
|
"right":{
|
|
"op":">",
|
|
"left":"coin4",
|
|
"right":0
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"¬",
|
|
"exp":{
|
|
"op":"=",
|
|
"left":"coin3",
|
|
"right":"coin4"
|
|
}
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"pay",
|
|
"right":3
|
|
}
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":1
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"s3",
|
|
"value":1
|
|
},
|
|
{
|
|
"ref":"agree3",
|
|
"value":1
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"done",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"=",
|
|
"left":"s3",
|
|
"right":1
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":1
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
]
|
|
}
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"name":"crypt4",
|
|
"locations":[
|
|
{
|
|
"name":"location"
|
|
}
|
|
],
|
|
"initial-locations":[
|
|
"location"
|
|
],
|
|
"edges":[
|
|
{
|
|
"location":"location",
|
|
"action":"tau__",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"=",
|
|
"left":"coin4",
|
|
"right":0
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":0.5000000
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"coin4",
|
|
"value":1
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
},
|
|
{
|
|
"probability":{
|
|
"exp":0.5000000
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"coin4",
|
|
"value":2
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"tau__",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"s4",
|
|
"right":0
|
|
},
|
|
"right":{
|
|
"op":">",
|
|
"left":"coin4",
|
|
"right":0
|
|
}
|
|
},
|
|
"right":{
|
|
"op":">",
|
|
"left":"coin5",
|
|
"right":0
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"coin4",
|
|
"right":"coin5"
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"≠",
|
|
"left":"pay",
|
|
"right":4
|
|
}
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":1
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"s4",
|
|
"value":1
|
|
},
|
|
{
|
|
"ref":"agree4",
|
|
"value":1
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"tau__",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"s4",
|
|
"right":0
|
|
},
|
|
"right":{
|
|
"op":">",
|
|
"left":"coin4",
|
|
"right":0
|
|
}
|
|
},
|
|
"right":{
|
|
"op":">",
|
|
"left":"coin5",
|
|
"right":0
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"¬",
|
|
"exp":{
|
|
"op":"=",
|
|
"left":"coin4",
|
|
"right":"coin5"
|
|
}
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"≠",
|
|
"left":"pay",
|
|
"right":4
|
|
}
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":1
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"s4",
|
|
"value":1
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"tau__",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"s4",
|
|
"right":0
|
|
},
|
|
"right":{
|
|
"op":">",
|
|
"left":"coin4",
|
|
"right":0
|
|
}
|
|
},
|
|
"right":{
|
|
"op":">",
|
|
"left":"coin5",
|
|
"right":0
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"coin4",
|
|
"right":"coin5"
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"pay",
|
|
"right":4
|
|
}
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":1
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"s4",
|
|
"value":1
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"tau__",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"s4",
|
|
"right":0
|
|
},
|
|
"right":{
|
|
"op":">",
|
|
"left":"coin4",
|
|
"right":0
|
|
}
|
|
},
|
|
"right":{
|
|
"op":">",
|
|
"left":"coin5",
|
|
"right":0
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"¬",
|
|
"exp":{
|
|
"op":"=",
|
|
"left":"coin4",
|
|
"right":"coin5"
|
|
}
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"pay",
|
|
"right":4
|
|
}
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":1
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"s4",
|
|
"value":1
|
|
},
|
|
{
|
|
"ref":"agree4",
|
|
"value":1
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"done",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"=",
|
|
"left":"s4",
|
|
"right":1
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":1
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
]
|
|
}
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"name":"crypt5",
|
|
"locations":[
|
|
{
|
|
"name":"location"
|
|
}
|
|
],
|
|
"initial-locations":[
|
|
"location"
|
|
],
|
|
"edges":[
|
|
{
|
|
"location":"location",
|
|
"action":"tau__",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"=",
|
|
"left":"coin5",
|
|
"right":0
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":0.5000000
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"coin5",
|
|
"value":1
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
},
|
|
{
|
|
"probability":{
|
|
"exp":0.5000000
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"coin5",
|
|
"value":2
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"tau__",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"s5",
|
|
"right":0
|
|
},
|
|
"right":{
|
|
"op":">",
|
|
"left":"coin5",
|
|
"right":0
|
|
}
|
|
},
|
|
"right":{
|
|
"op":">",
|
|
"left":"coin6",
|
|
"right":0
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"coin5",
|
|
"right":"coin6"
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"≠",
|
|
"left":"pay",
|
|
"right":5
|
|
}
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":1
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"s5",
|
|
"value":1
|
|
},
|
|
{
|
|
"ref":"agree5",
|
|
"value":1
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"tau__",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"s5",
|
|
"right":0
|
|
},
|
|
"right":{
|
|
"op":">",
|
|
"left":"coin5",
|
|
"right":0
|
|
}
|
|
},
|
|
"right":{
|
|
"op":">",
|
|
"left":"coin6",
|
|
"right":0
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"¬",
|
|
"exp":{
|
|
"op":"=",
|
|
"left":"coin5",
|
|
"right":"coin6"
|
|
}
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"≠",
|
|
"left":"pay",
|
|
"right":5
|
|
}
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":1
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"s5",
|
|
"value":1
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"tau__",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"s5",
|
|
"right":0
|
|
},
|
|
"right":{
|
|
"op":">",
|
|
"left":"coin5",
|
|
"right":0
|
|
}
|
|
},
|
|
"right":{
|
|
"op":">",
|
|
"left":"coin6",
|
|
"right":0
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"coin5",
|
|
"right":"coin6"
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"pay",
|
|
"right":5
|
|
}
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":1
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"s5",
|
|
"value":1
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"tau__",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"s5",
|
|
"right":0
|
|
},
|
|
"right":{
|
|
"op":">",
|
|
"left":"coin5",
|
|
"right":0
|
|
}
|
|
},
|
|
"right":{
|
|
"op":">",
|
|
"left":"coin6",
|
|
"right":0
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"¬",
|
|
"exp":{
|
|
"op":"=",
|
|
"left":"coin5",
|
|
"right":"coin6"
|
|
}
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"pay",
|
|
"right":5
|
|
}
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":1
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"s5",
|
|
"value":1
|
|
},
|
|
{
|
|
"ref":"agree5",
|
|
"value":1
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"done",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"=",
|
|
"left":"s5",
|
|
"right":1
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":1
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
]
|
|
}
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"name":"crypt6",
|
|
"locations":[
|
|
{
|
|
"name":"location"
|
|
}
|
|
],
|
|
"initial-locations":[
|
|
"location"
|
|
],
|
|
"edges":[
|
|
{
|
|
"location":"location",
|
|
"action":"tau__",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"=",
|
|
"left":"coin6",
|
|
"right":0
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":0.5000000
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"coin6",
|
|
"value":1
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
},
|
|
{
|
|
"probability":{
|
|
"exp":0.5000000
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"coin6",
|
|
"value":2
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"tau__",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"s6",
|
|
"right":0
|
|
},
|
|
"right":{
|
|
"op":">",
|
|
"left":"coin6",
|
|
"right":0
|
|
}
|
|
},
|
|
"right":{
|
|
"op":">",
|
|
"left":"coin7",
|
|
"right":0
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"coin6",
|
|
"right":"coin7"
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"≠",
|
|
"left":"pay",
|
|
"right":6
|
|
}
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":1
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"s6",
|
|
"value":1
|
|
},
|
|
{
|
|
"ref":"agree6",
|
|
"value":1
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"tau__",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"s6",
|
|
"right":0
|
|
},
|
|
"right":{
|
|
"op":">",
|
|
"left":"coin6",
|
|
"right":0
|
|
}
|
|
},
|
|
"right":{
|
|
"op":">",
|
|
"left":"coin7",
|
|
"right":0
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"¬",
|
|
"exp":{
|
|
"op":"=",
|
|
"left":"coin6",
|
|
"right":"coin7"
|
|
}
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"≠",
|
|
"left":"pay",
|
|
"right":6
|
|
}
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":1
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"s6",
|
|
"value":1
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"tau__",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"s6",
|
|
"right":0
|
|
},
|
|
"right":{
|
|
"op":">",
|
|
"left":"coin6",
|
|
"right":0
|
|
}
|
|
},
|
|
"right":{
|
|
"op":">",
|
|
"left":"coin7",
|
|
"right":0
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"coin6",
|
|
"right":"coin7"
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"pay",
|
|
"right":6
|
|
}
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":1
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"s6",
|
|
"value":1
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"tau__",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"s6",
|
|
"right":0
|
|
},
|
|
"right":{
|
|
"op":">",
|
|
"left":"coin6",
|
|
"right":0
|
|
}
|
|
},
|
|
"right":{
|
|
"op":">",
|
|
"left":"coin7",
|
|
"right":0
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"¬",
|
|
"exp":{
|
|
"op":"=",
|
|
"left":"coin6",
|
|
"right":"coin7"
|
|
}
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"pay",
|
|
"right":6
|
|
}
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":1
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"s6",
|
|
"value":1
|
|
},
|
|
{
|
|
"ref":"agree6",
|
|
"value":1
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"done",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"=",
|
|
"left":"s6",
|
|
"right":1
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":1
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
]
|
|
}
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"name":"crypt7",
|
|
"locations":[
|
|
{
|
|
"name":"location"
|
|
}
|
|
],
|
|
"initial-locations":[
|
|
"location"
|
|
],
|
|
"edges":[
|
|
{
|
|
"location":"location",
|
|
"action":"tau__",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"=",
|
|
"left":"coin7",
|
|
"right":0
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":0.5000000
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"coin7",
|
|
"value":1
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
},
|
|
{
|
|
"probability":{
|
|
"exp":0.5000000
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"coin7",
|
|
"value":2
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"tau__",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"s7",
|
|
"right":0
|
|
},
|
|
"right":{
|
|
"op":">",
|
|
"left":"coin7",
|
|
"right":0
|
|
}
|
|
},
|
|
"right":{
|
|
"op":">",
|
|
"left":"coin1",
|
|
"right":0
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"coin7",
|
|
"right":"coin1"
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"≠",
|
|
"left":"pay",
|
|
"right":7
|
|
}
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":1
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"s7",
|
|
"value":1
|
|
},
|
|
{
|
|
"ref":"agree7",
|
|
"value":1
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"tau__",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"s7",
|
|
"right":0
|
|
},
|
|
"right":{
|
|
"op":">",
|
|
"left":"coin7",
|
|
"right":0
|
|
}
|
|
},
|
|
"right":{
|
|
"op":">",
|
|
"left":"coin1",
|
|
"right":0
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"¬",
|
|
"exp":{
|
|
"op":"=",
|
|
"left":"coin7",
|
|
"right":"coin1"
|
|
}
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"≠",
|
|
"left":"pay",
|
|
"right":7
|
|
}
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":1
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"s7",
|
|
"value":1
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"tau__",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"s7",
|
|
"right":0
|
|
},
|
|
"right":{
|
|
"op":">",
|
|
"left":"coin7",
|
|
"right":0
|
|
}
|
|
},
|
|
"right":{
|
|
"op":">",
|
|
"left":"coin1",
|
|
"right":0
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"coin7",
|
|
"right":"coin1"
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"pay",
|
|
"right":7
|
|
}
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":1
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"s7",
|
|
"value":1
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"tau__",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"s7",
|
|
"right":0
|
|
},
|
|
"right":{
|
|
"op":">",
|
|
"left":"coin7",
|
|
"right":0
|
|
}
|
|
},
|
|
"right":{
|
|
"op":">",
|
|
"left":"coin1",
|
|
"right":0
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"¬",
|
|
"exp":{
|
|
"op":"=",
|
|
"left":"coin7",
|
|
"right":"coin1"
|
|
}
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"pay",
|
|
"right":7
|
|
}
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":1
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"s7",
|
|
"value":1
|
|
},
|
|
{
|
|
"ref":"agree7",
|
|
"value":1
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"done",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"=",
|
|
"left":"s7",
|
|
"right":1
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":1
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
]
|
|
}
|
|
]
|
|
}
|
|
]
|
|
}
|
|
],
|
|
"system":{
|
|
"elements":[
|
|
{
|
|
"automaton":"crypt1"
|
|
},
|
|
{
|
|
"automaton":"crypt2"
|
|
},
|
|
{
|
|
"automaton":"crypt3"
|
|
},
|
|
{
|
|
"automaton":"crypt4"
|
|
},
|
|
{
|
|
"automaton":"crypt5"
|
|
},
|
|
{
|
|
"automaton":"crypt6"
|
|
},
|
|
{
|
|
"automaton":"crypt7"
|
|
}
|
|
],
|
|
"syncs":[
|
|
{
|
|
"synchronise":[
|
|
"done",
|
|
"done",
|
|
"done",
|
|
"done",
|
|
"done",
|
|
"done",
|
|
"done"
|
|
],
|
|
"result":"done"
|
|
},
|
|
{
|
|
"synchronise":[
|
|
"tau__",
|
|
null,
|
|
null,
|
|
null,
|
|
null,
|
|
null,
|
|
null
|
|
],
|
|
"result":"tau__"
|
|
},
|
|
{
|
|
"synchronise":[
|
|
null,
|
|
"tau__",
|
|
null,
|
|
null,
|
|
null,
|
|
null,
|
|
null
|
|
],
|
|
"result":"tau__"
|
|
},
|
|
{
|
|
"synchronise":[
|
|
null,
|
|
null,
|
|
"tau__",
|
|
null,
|
|
null,
|
|
null,
|
|
null
|
|
],
|
|
"result":"tau__"
|
|
},
|
|
{
|
|
"synchronise":[
|
|
null,
|
|
null,
|
|
null,
|
|
"tau__",
|
|
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__"
|
|
},
|
|
{
|
|
"synchronise":[
|
|
null,
|
|
null,
|
|
null,
|
|
null,
|
|
null,
|
|
null,
|
|
"tau__"
|
|
],
|
|
"result":"tau__"
|
|
}
|
|
]
|
|
}
|
|
}
|