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.
1708 lines
60 KiB
1708 lines
60 KiB
|
|
{
|
|
"jani-version":1,
|
|
"features":[
|
|
"derived-operators"
|
|
],
|
|
"name":"Converted from PRISM by IscasMC",
|
|
"type":"mdp",
|
|
"actions":[
|
|
{
|
|
"name":"t1_nlb_up"
|
|
},
|
|
{
|
|
"name":"t1_nrb_up"
|
|
},
|
|
{
|
|
"name":"t1_enter_l"
|
|
},
|
|
{
|
|
"name":"t1_enter_r"
|
|
},
|
|
{
|
|
"name":"t1_must_l"
|
|
},
|
|
{
|
|
"name":"t1_must_r"
|
|
},
|
|
{
|
|
"name":"t1_l_up"
|
|
},
|
|
{
|
|
"name":"t1_r_up"
|
|
},
|
|
{
|
|
"name":"t1_l_copy"
|
|
},
|
|
{
|
|
"name":"t1_r_copy"
|
|
},
|
|
{
|
|
"name":"t1_l_exit"
|
|
},
|
|
{
|
|
"name":"t1_r_exit"
|
|
}
|
|
],
|
|
"variables":[
|
|
{
|
|
"name":"nlb",
|
|
"type":{
|
|
"kind":"bounded",
|
|
"base":"int",
|
|
"lower-bound":0,
|
|
"upper-bound":8
|
|
}
|
|
},
|
|
{
|
|
"name":"lbm",
|
|
"type":{
|
|
"kind":"bounded",
|
|
"base":"int",
|
|
"lower-bound":0,
|
|
"upper-bound":1
|
|
}
|
|
},
|
|
{
|
|
"name":"nrb",
|
|
"type":{
|
|
"kind":"bounded",
|
|
"base":"int",
|
|
"lower-bound":0,
|
|
"upper-bound":8
|
|
}
|
|
},
|
|
{
|
|
"name":"rbm",
|
|
"type":{
|
|
"kind":"bounded",
|
|
"base":"int",
|
|
"lower-bound":0,
|
|
"upper-bound":1
|
|
}
|
|
},
|
|
{
|
|
"name":"rin",
|
|
"type":{
|
|
"kind":"bounded",
|
|
"base":"int",
|
|
"lower-bound":0,
|
|
"upper-bound":1
|
|
}
|
|
},
|
|
{
|
|
"name":"lin",
|
|
"type":{
|
|
"kind":"bounded",
|
|
"base":"int",
|
|
"lower-bound":0,
|
|
"upper-bound":1
|
|
}
|
|
},
|
|
{
|
|
"name":"flag",
|
|
"type":{
|
|
"kind":"bounded",
|
|
"base":"int",
|
|
"lower-bound":0,
|
|
"upper-bound":1
|
|
}
|
|
},
|
|
{
|
|
"name":"t1_loc",
|
|
"type":{
|
|
"kind":"bounded",
|
|
"base":"int",
|
|
"lower-bound":0,
|
|
"upper-bound":2
|
|
}
|
|
},
|
|
{
|
|
"name":"t1_val",
|
|
"type":{
|
|
"kind":"bounded",
|
|
"base":"int",
|
|
"lower-bound":0,
|
|
"upper-bound":8
|
|
}
|
|
},
|
|
{
|
|
"name":"t1_com",
|
|
"type":{
|
|
"kind":"bounded",
|
|
"base":"int",
|
|
"lower-bound":0,
|
|
"upper-bound":1
|
|
}
|
|
}
|
|
],
|
|
"observables":[
|
|
{
|
|
"name":""
|
|
}
|
|
],
|
|
"initial-states":{
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"nlb",
|
|
"right":0
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"lbm",
|
|
"right":0
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"nrb",
|
|
"right":0
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"rbm",
|
|
"right":0
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"rin",
|
|
"right":0
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"lin",
|
|
"right":0
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"flag",
|
|
"right":0
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"t1_loc",
|
|
"right":1
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"t1_val",
|
|
"right":0
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"t1_com",
|
|
"right":0
|
|
}
|
|
}
|
|
},
|
|
"automata":[
|
|
{
|
|
"name":"leftboard",
|
|
"locations":[
|
|
{
|
|
"name":"location",
|
|
"observables":[
|
|
{
|
|
"ref":"",
|
|
"value":{
|
|
"op":"?:",
|
|
"args":[
|
|
{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"≠",
|
|
"left":"lin",
|
|
"right":1
|
|
},
|
|
"right":{
|
|
"op":"≠",
|
|
"left":"rin",
|
|
"right":1
|
|
}
|
|
},
|
|
1,
|
|
0
|
|
]
|
|
}
|
|
}
|
|
]
|
|
}
|
|
],
|
|
"initial-locations":[
|
|
"location"
|
|
],
|
|
"edges":[
|
|
{
|
|
"location":"location",
|
|
"action":"t1_nlb_up",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"lbm",
|
|
"right":0
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"t1_loc",
|
|
"right":0
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"lin",
|
|
"right":0
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"t1_val",
|
|
"right":"nlb"
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"≤",
|
|
"left":{
|
|
"op":"+",
|
|
"left":"nlb",
|
|
"right":3
|
|
},
|
|
"right":8
|
|
}
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":0.5000000
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"nlb",
|
|
"value":{
|
|
"op":"+",
|
|
"left":"nlb",
|
|
"right":2
|
|
}
|
|
},
|
|
{
|
|
"ref":"lbm",
|
|
"value":0
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
},
|
|
{
|
|
"probability":{
|
|
"exp":0.5000000
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"nlb",
|
|
"value":{
|
|
"op":"+",
|
|
"left":"nlb",
|
|
"right":3
|
|
}
|
|
},
|
|
{
|
|
"ref":"lbm",
|
|
"value":1
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"t1_nlb_up",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"lbm",
|
|
"right":1
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"t1_loc",
|
|
"right":0
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"lin",
|
|
"right":0
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"t1_val",
|
|
"right":"nlb"
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"≤",
|
|
"left":{
|
|
"op":"+",
|
|
"left":"nlb",
|
|
"right":2
|
|
},
|
|
"right":8
|
|
}
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":0.5000000
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"nlb",
|
|
"value":{
|
|
"op":"+",
|
|
"left":"nlb",
|
|
"right":2
|
|
}
|
|
},
|
|
{
|
|
"ref":"lbm",
|
|
"value":1
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
},
|
|
{
|
|
"probability":{
|
|
"exp":0.5000000
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"nlb",
|
|
"value":{
|
|
"op":"+",
|
|
"left":"nlb",
|
|
"right":1
|
|
}
|
|
},
|
|
{
|
|
"ref":"lbm",
|
|
"value":0
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
}
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"name":"rightboard",
|
|
"locations":[
|
|
{
|
|
"name":"location"
|
|
}
|
|
],
|
|
"initial-locations":[
|
|
"location"
|
|
],
|
|
"edges":[
|
|
{
|
|
"location":"location",
|
|
"action":"t1_nrb_up",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"rbm",
|
|
"right":0
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"t1_loc",
|
|
"right":1
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"rin",
|
|
"right":0
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"t1_val",
|
|
"right":"nrb"
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"≤",
|
|
"left":{
|
|
"op":"+",
|
|
"left":"nrb",
|
|
"right":3
|
|
},
|
|
"right":8
|
|
}
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":0.5000000
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"nrb",
|
|
"value":{
|
|
"op":"+",
|
|
"left":"nrb",
|
|
"right":2
|
|
}
|
|
},
|
|
{
|
|
"ref":"rbm",
|
|
"value":0
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
},
|
|
{
|
|
"probability":{
|
|
"exp":0.5000000
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"nrb",
|
|
"value":{
|
|
"op":"+",
|
|
"left":"nrb",
|
|
"right":3
|
|
}
|
|
},
|
|
{
|
|
"ref":"rbm",
|
|
"value":1
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"t1_nrb_up",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"rbm",
|
|
"right":1
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"t1_loc",
|
|
"right":1
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"rin",
|
|
"right":0
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"t1_val",
|
|
"right":"nrb"
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"≤",
|
|
"left":{
|
|
"op":"+",
|
|
"left":"nrb",
|
|
"right":2
|
|
},
|
|
"right":8
|
|
}
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":0.5000000
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"nrb",
|
|
"value":{
|
|
"op":"+",
|
|
"left":"nrb",
|
|
"right":2
|
|
}
|
|
},
|
|
{
|
|
"ref":"rbm",
|
|
"value":1
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
},
|
|
{
|
|
"probability":{
|
|
"exp":0.5000000
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"nrb",
|
|
"value":{
|
|
"op":"+",
|
|
"left":"nrb",
|
|
"right":1
|
|
}
|
|
},
|
|
{
|
|
"ref":"rbm",
|
|
"value":0
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
}
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"name":"counter",
|
|
"locations":[
|
|
{
|
|
"name":"location"
|
|
}
|
|
],
|
|
"initial-locations":[
|
|
"location"
|
|
],
|
|
"edges":[
|
|
{
|
|
"location":"location",
|
|
"action":"t1_enter_l",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"t1_loc",
|
|
"right":0
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"flag",
|
|
"right":0
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"lin",
|
|
"right":0
|
|
}
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":1
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"lin",
|
|
"value":{
|
|
"op":"+",
|
|
"left":"lin",
|
|
"right":1
|
|
}
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"t1_enter_r",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"t1_loc",
|
|
"right":1
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"flag",
|
|
"right":0
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"rin",
|
|
"right":0
|
|
}
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":1
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"rin",
|
|
"value":{
|
|
"op":"+",
|
|
"left":"rin",
|
|
"right":1
|
|
}
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"t1_must_l",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"t1_loc",
|
|
"right":0
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"flag",
|
|
"right":0
|
|
}
|
|
},
|
|
"right":{
|
|
"op":">",
|
|
"left":"lin",
|
|
"right":0
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"≤",
|
|
"left":{
|
|
"op":"+",
|
|
"left":"lin",
|
|
"right":1
|
|
},
|
|
"right":1
|
|
}
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":1
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"lin",
|
|
"value":{
|
|
"op":"+",
|
|
"left":"lin",
|
|
"right":1
|
|
}
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"t1_must_r",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"t1_loc",
|
|
"right":1
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"flag",
|
|
"right":0
|
|
}
|
|
},
|
|
"right":{
|
|
"op":">",
|
|
"left":"rin",
|
|
"right":0
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"≤",
|
|
"left":{
|
|
"op":"+",
|
|
"left":"rin",
|
|
"right":1
|
|
},
|
|
"right":1
|
|
}
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":1
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"rin",
|
|
"value":{
|
|
"op":"+",
|
|
"left":"rin",
|
|
"right":1
|
|
}
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
}
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"name":"semaphore",
|
|
"locations":[
|
|
{
|
|
"name":"location"
|
|
}
|
|
],
|
|
"initial-locations":[
|
|
"location"
|
|
],
|
|
"edges":[
|
|
{
|
|
"location":"location",
|
|
"action":"t1_nlb_up",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"=",
|
|
"left":"flag",
|
|
"right":0
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":1
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"flag",
|
|
"value":1
|
|
}
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"t1_nrb_up",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"=",
|
|
"left":"flag",
|
|
"right":0
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":1
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"flag",
|
|
"value":1
|
|
}
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"t1_l_up",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"=",
|
|
"left":"flag",
|
|
"right":1
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":1
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"flag",
|
|
"value":0
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"t1_r_up",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"=",
|
|
"left":"flag",
|
|
"right":1
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":1
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"flag",
|
|
"value":0
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
}
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"name":"tourist1",
|
|
"locations":[
|
|
{
|
|
"name":"location"
|
|
}
|
|
],
|
|
"initial-locations":[
|
|
"location"
|
|
],
|
|
"edges":[
|
|
{
|
|
"location":"location",
|
|
"action":"t1_nlb_up",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"t1_com",
|
|
"right":0
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"t1_loc",
|
|
"right":0
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"lin",
|
|
"right":0
|
|
}
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":1
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"t1_com",
|
|
"value":1
|
|
}
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"t1_nrb_up",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"t1_com",
|
|
"right":0
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"t1_loc",
|
|
"right":1
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"rin",
|
|
"right":0
|
|
}
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":1
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"t1_com",
|
|
"value":1
|
|
}
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"t1_l_up",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"t1_com",
|
|
"right":1
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"t1_loc",
|
|
"right":0
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"lin",
|
|
"right":0
|
|
}
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":1
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"t1_val",
|
|
"value":"nlb"
|
|
},
|
|
{
|
|
"ref":"t1_loc",
|
|
"value":1
|
|
},
|
|
{
|
|
"ref":"t1_com",
|
|
"value":0
|
|
}
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"t1_r_up",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"t1_com",
|
|
"right":1
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"t1_loc",
|
|
"right":1
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"rin",
|
|
"right":0
|
|
}
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":1
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"t1_val",
|
|
"value":"nrb"
|
|
},
|
|
{
|
|
"ref":"t1_loc",
|
|
"value":0
|
|
},
|
|
{
|
|
"ref":"t1_com",
|
|
"value":0
|
|
}
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"t1_l_copy",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"flag",
|
|
"right":0
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"t1_loc",
|
|
"right":0
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"<",
|
|
"left":"t1_val",
|
|
"right":"nlb"
|
|
}
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":1
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"t1_val",
|
|
"value":"nlb"
|
|
},
|
|
{
|
|
"ref":"t1_loc",
|
|
"value":1
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"t1_r_copy",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"flag",
|
|
"right":0
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"t1_loc",
|
|
"right":1
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"<",
|
|
"left":"t1_val",
|
|
"right":"nrb"
|
|
}
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":1
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"t1_val",
|
|
"value":"nrb"
|
|
},
|
|
{
|
|
"ref":"t1_loc",
|
|
"value":0
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"t1_enter_l",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"flag",
|
|
"right":0
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"t1_loc",
|
|
"right":0
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"lin",
|
|
"right":0
|
|
}
|
|
},
|
|
"right":{
|
|
"op":">",
|
|
"left":"t1_val",
|
|
"right":"nlb"
|
|
}
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":1
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"t1_loc",
|
|
"value":2
|
|
}
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"t1_enter_r",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"flag",
|
|
"right":0
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"t1_loc",
|
|
"right":1
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"rin",
|
|
"right":0
|
|
}
|
|
},
|
|
"right":{
|
|
"op":">",
|
|
"left":"t1_val",
|
|
"right":"nrb"
|
|
}
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":1
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"t1_loc",
|
|
"value":2
|
|
}
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"t1_must_l",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"flag",
|
|
"right":0
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"t1_loc",
|
|
"right":0
|
|
}
|
|
},
|
|
"right":{
|
|
"op":">",
|
|
"left":"lin",
|
|
"right":0
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"≤",
|
|
"left":{
|
|
"op":"+",
|
|
"left":"lin",
|
|
"right":1
|
|
},
|
|
"right":1
|
|
}
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":1
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"t1_loc",
|
|
"value":2
|
|
}
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"t1_must_r",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"flag",
|
|
"right":0
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"t1_loc",
|
|
"right":1
|
|
}
|
|
},
|
|
"right":{
|
|
"op":">",
|
|
"left":"rin",
|
|
"right":0
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"≤",
|
|
"left":{
|
|
"op":"+",
|
|
"left":"rin",
|
|
"right":1
|
|
},
|
|
"right":1
|
|
}
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":1
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"t1_loc",
|
|
"value":2
|
|
}
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"t1_l_exit",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"flag",
|
|
"right":0
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"lin",
|
|
"right":1
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"t1_loc",
|
|
"right":2
|
|
}
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":1
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"t1_val",
|
|
"value":"t1_val"
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"t1_r_exit",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"flag",
|
|
"right":0
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"rin",
|
|
"right":1
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"t1_loc",
|
|
"right":2
|
|
}
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":1
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"t1_val",
|
|
"value":"t1_val"
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
}
|
|
]
|
|
}
|
|
]
|
|
}
|
|
],
|
|
"system":{
|
|
"elements":[
|
|
{
|
|
"automaton":"leftboard"
|
|
},
|
|
{
|
|
"automaton":"rightboard"
|
|
},
|
|
{
|
|
"automaton":"counter"
|
|
},
|
|
{
|
|
"automaton":"semaphore"
|
|
},
|
|
{
|
|
"automaton":"tourist1"
|
|
}
|
|
],
|
|
"syncs":[
|
|
{
|
|
"synchronise":[
|
|
"t1_nlb_up",
|
|
null,
|
|
null,
|
|
"t1_nlb_up",
|
|
"t1_nlb_up"
|
|
],
|
|
"result":"t1_nlb_up"
|
|
},
|
|
{
|
|
"synchronise":[
|
|
null,
|
|
"t1_nrb_up",
|
|
null,
|
|
"t1_nrb_up",
|
|
"t1_nrb_up"
|
|
],
|
|
"result":"t1_nrb_up"
|
|
},
|
|
{
|
|
"synchronise":[
|
|
null,
|
|
null,
|
|
"t1_enter_l",
|
|
null,
|
|
"t1_enter_l"
|
|
],
|
|
"result":"t1_enter_l"
|
|
},
|
|
{
|
|
"synchronise":[
|
|
null,
|
|
null,
|
|
"t1_enter_r",
|
|
null,
|
|
"t1_enter_r"
|
|
],
|
|
"result":"t1_enter_r"
|
|
},
|
|
{
|
|
"synchronise":[
|
|
null,
|
|
null,
|
|
"t1_must_l",
|
|
null,
|
|
"t1_must_l"
|
|
],
|
|
"result":"t1_must_l"
|
|
},
|
|
{
|
|
"synchronise":[
|
|
null,
|
|
null,
|
|
"t1_must_r",
|
|
null,
|
|
"t1_must_r"
|
|
],
|
|
"result":"t1_must_r"
|
|
},
|
|
{
|
|
"synchronise":[
|
|
null,
|
|
null,
|
|
null,
|
|
"t1_l_up",
|
|
"t1_l_up"
|
|
],
|
|
"result":"t1_l_up"
|
|
},
|
|
{
|
|
"synchronise":[
|
|
null,
|
|
null,
|
|
null,
|
|
"t1_r_up",
|
|
"t1_r_up"
|
|
],
|
|
"result":"t1_r_up"
|
|
},
|
|
{
|
|
"synchronise":[
|
|
null,
|
|
null,
|
|
null,
|
|
null,
|
|
"t1_l_copy"
|
|
],
|
|
"result":"t1_l_copy"
|
|
},
|
|
{
|
|
"synchronise":[
|
|
null,
|
|
null,
|
|
null,
|
|
null,
|
|
"t1_r_copy"
|
|
],
|
|
"result":"t1_r_copy"
|
|
},
|
|
{
|
|
"synchronise":[
|
|
null,
|
|
null,
|
|
null,
|
|
null,
|
|
"t1_l_exit"
|
|
],
|
|
"result":"t1_l_exit"
|
|
},
|
|
{
|
|
"synchronise":[
|
|
null,
|
|
null,
|
|
null,
|
|
null,
|
|
"t1_r_exit"
|
|
],
|
|
"result":"t1_r_exit"
|
|
}
|
|
]
|
|
}
|
|
}
|