{
"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":4
}
},
{
"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
}
}
],
"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":"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
}
}
},
"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":"coin1",
"right":0
}
},
"right":{
"op":"=",
"left":"coin4",
"right":"coin1"
}
},
"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":"coin1",
"right":0
}
},
"right":{
"op":"¬",
"exp":{
"op":"=",
"left":"coin4",
"right":"coin1"
}
}
},
"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":"coin1",
"right":0
}
},
"right":{
"op":"=",
"left":"coin4",
"right":"coin1"
}
},
"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":"coin1",
"right":0
}
},
"right":{
"op":"¬",
"exp":{
"op":"=",
"left":"coin4",
"right":"coin1"
}
}
},
"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":[
]
}
]
}
]
}
],
"system":{
"elements":[
{
"automaton":"crypt1"
},
{
"automaton":"crypt2"
},
{
"automaton":"crypt3"
},
{
"automaton":"crypt4"
}
],
"syncs":[
{
"synchronise":[
"done",
"done",
"done",
"done"
],
"result":"done"
},
{
"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__"
}
]
}
}