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.
3906 lines
153 KiB
3906 lines
153 KiB
|
|
{
|
|
"jani-version":1,
|
|
"features":[
|
|
"derived-operators"
|
|
],
|
|
"name":"Converted from PRISM by IscasMC",
|
|
"type":"dtmc",
|
|
"actions":[
|
|
{
|
|
"name":"tau__"
|
|
},
|
|
{
|
|
"name":"BID"
|
|
},
|
|
{
|
|
"name":"CBID"
|
|
},
|
|
{
|
|
"name":"PURCHASE"
|
|
},
|
|
{
|
|
"name":"STOP"
|
|
}
|
|
],
|
|
"variables":[
|
|
{
|
|
"name":"b",
|
|
"type":{
|
|
"kind":"bounded",
|
|
"base":"int",
|
|
"lower-bound":0,
|
|
"upper-bound":6
|
|
}
|
|
},
|
|
{
|
|
"name":"bid",
|
|
"type":{
|
|
"kind":"bounded",
|
|
"base":"int",
|
|
"lower-bound":1,
|
|
"upper-bound":1000
|
|
}
|
|
},
|
|
{
|
|
"name":"tb",
|
|
"type":{
|
|
"kind":"bounded",
|
|
"base":"int",
|
|
"lower-bound":0,
|
|
"upper-bound":50
|
|
}
|
|
},
|
|
{
|
|
"name":"Bcon",
|
|
"type":"bool"
|
|
},
|
|
{
|
|
"name":"Bstop",
|
|
"type":"bool"
|
|
},
|
|
{
|
|
"name":"Bswitch",
|
|
"type":"bool"
|
|
},
|
|
{
|
|
"name":"Bagreed",
|
|
"type":"bool"
|
|
},
|
|
{
|
|
"name":"s",
|
|
"type":{
|
|
"kind":"bounded",
|
|
"base":"int",
|
|
"lower-bound":0,
|
|
"upper-bound":7
|
|
}
|
|
},
|
|
{
|
|
"name":"cbid",
|
|
"type":{
|
|
"kind":"bounded",
|
|
"base":"int",
|
|
"lower-bound":1,
|
|
"upper-bound":1000
|
|
}
|
|
},
|
|
{
|
|
"name":"ts",
|
|
"type":{
|
|
"kind":"bounded",
|
|
"base":"int",
|
|
"lower-bound":0,
|
|
"upper-bound":50
|
|
}
|
|
},
|
|
{
|
|
"name":"Scon",
|
|
"type":"bool"
|
|
},
|
|
{
|
|
"name":"Sstop",
|
|
"type":"bool"
|
|
},
|
|
{
|
|
"name":"Sswitch",
|
|
"type":"bool"
|
|
}
|
|
],
|
|
"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":"b",
|
|
"right":0
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"bid",
|
|
"right":1
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"tb",
|
|
"right":0
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"Bcon",
|
|
"right":false
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"Bstop",
|
|
"right":false
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"Bswitch",
|
|
"right":false
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"Bagreed",
|
|
"right":false
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"s",
|
|
"right":0
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"cbid",
|
|
"right":1000
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"ts",
|
|
"right":0
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"Scon",
|
|
"right":true
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"Sstop",
|
|
"right":false
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"Sswitch",
|
|
"right":false
|
|
}
|
|
}
|
|
},
|
|
"automata":[
|
|
{
|
|
"name":"Buyer",
|
|
"locations":[
|
|
{
|
|
"name":"location"
|
|
}
|
|
],
|
|
"initial-locations":[
|
|
"location"
|
|
],
|
|
"edges":[
|
|
{
|
|
"location":"location",
|
|
"action":"tau__",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"b",
|
|
"right":0
|
|
},
|
|
"right":{
|
|
"op":"¬",
|
|
"exp":"Bswitch"
|
|
}
|
|
},
|
|
"right":"Bcon"
|
|
},
|
|
"right":{
|
|
"op":">",
|
|
"left":{
|
|
"op":"-",
|
|
"left":1000,
|
|
"right":"bid"
|
|
},
|
|
"right":{
|
|
"op":"*",
|
|
"left":1,
|
|
"right":100
|
|
}
|
|
}
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":1
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"b",
|
|
"value":1
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"tau__",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"b",
|
|
"right":0
|
|
},
|
|
"right":{
|
|
"op":"¬",
|
|
"exp":"Bswitch"
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"¬",
|
|
"exp":"Bcon"
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"<",
|
|
"left":"tb",
|
|
"right":20
|
|
}
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":1
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"b",
|
|
"value":1
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"tau__",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"b",
|
|
"right":0
|
|
},
|
|
"right":"Bswitch"
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":1
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"b",
|
|
"value":1
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"tau__",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"b",
|
|
"right":0
|
|
},
|
|
"right":{
|
|
"op":"¬",
|
|
"exp":"Bswitch"
|
|
}
|
|
},
|
|
"right":"Bcon"
|
|
},
|
|
"right":{
|
|
"op":"≤",
|
|
"left":{
|
|
"op":"-",
|
|
"left":1000,
|
|
"right":"bid"
|
|
},
|
|
"right":{
|
|
"op":"*",
|
|
"left":1,
|
|
"right":100
|
|
}
|
|
}
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":1
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"b",
|
|
"value":1
|
|
},
|
|
{
|
|
"ref":"Bcon",
|
|
"value":false
|
|
},
|
|
{
|
|
"ref":"Bswitch",
|
|
"value":true
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"tau__",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"b",
|
|
"right":0
|
|
},
|
|
"right":{
|
|
"op":"¬",
|
|
"exp":"Bswitch"
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"¬",
|
|
"exp":"Bcon"
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"tb",
|
|
"right":20
|
|
}
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":1
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"b",
|
|
"value":1
|
|
},
|
|
{
|
|
"ref":"Bcon",
|
|
"value":true
|
|
},
|
|
{
|
|
"ref":"Bswitch",
|
|
"value":true
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"BID",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"b",
|
|
"right":1
|
|
},
|
|
"right":"Sstop"
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":1
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"b",
|
|
"value":4
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"BID",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"b",
|
|
"right":1
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"tb",
|
|
"right":0
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"¬",
|
|
"exp":"Sstop"
|
|
}
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":1
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"b",
|
|
"value":6
|
|
},
|
|
{
|
|
"ref":"tb",
|
|
"value":{
|
|
"op":"+",
|
|
"left":"tb",
|
|
"right":1
|
|
}
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"BID",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"b",
|
|
"right":1
|
|
},
|
|
"right":"Bcon"
|
|
},
|
|
"right":{
|
|
"op":">",
|
|
"left":"tb",
|
|
"right":0
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"<",
|
|
"left":"tb",
|
|
"right":{
|
|
"op":"-",
|
|
"left":50,
|
|
"right":1
|
|
}
|
|
}
|
|
},
|
|
"right":{
|
|
"op":">",
|
|
"left":{
|
|
"op":"-",
|
|
"left":1000,
|
|
"right":"bid"
|
|
},
|
|
"right":100
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"¬",
|
|
"exp":"Sstop"
|
|
}
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":1
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"b",
|
|
"value":6
|
|
},
|
|
{
|
|
"ref":"bid",
|
|
"value":{
|
|
"op":"+",
|
|
"left":"bid",
|
|
"right":100
|
|
}
|
|
},
|
|
{
|
|
"ref":"tb",
|
|
"value":{
|
|
"op":"+",
|
|
"left":"tb",
|
|
"right":1
|
|
}
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"BID",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"b",
|
|
"right":1
|
|
},
|
|
"right":{
|
|
"op":"¬",
|
|
"exp":"Bcon"
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":">",
|
|
"left":"tb",
|
|
"right":0
|
|
},
|
|
"right":{
|
|
"op":"<",
|
|
"left":"tb",
|
|
"right":{
|
|
"op":"-",
|
|
"left":50,
|
|
"right":1
|
|
}
|
|
}
|
|
}
|
|
},
|
|
"right":{
|
|
"op":">",
|
|
"left":{
|
|
"op":"-",
|
|
"left":1000,
|
|
"right":"bid"
|
|
},
|
|
"right":1
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"¬",
|
|
"exp":"Sstop"
|
|
}
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":1
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"b",
|
|
"value":6
|
|
},
|
|
{
|
|
"ref":"bid",
|
|
"value":{
|
|
"op":"+",
|
|
"left":"bid",
|
|
"right":1
|
|
}
|
|
},
|
|
{
|
|
"ref":"tb",
|
|
"value":{
|
|
"op":"+",
|
|
"left":"tb",
|
|
"right":1
|
|
}
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"BID",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"b",
|
|
"right":1
|
|
},
|
|
"right":{
|
|
"op":">",
|
|
"left":"tb",
|
|
"right":0
|
|
}
|
|
},
|
|
"right":"Bcon"
|
|
},
|
|
"right":{
|
|
"op":"¬",
|
|
"exp":"Sstop"
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"∨",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"tb",
|
|
"right":{
|
|
"op":"-",
|
|
"left":50,
|
|
"right":1
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"≤",
|
|
"left":{
|
|
"op":"-",
|
|
"left":1000,
|
|
"right":"bid"
|
|
},
|
|
"right":100
|
|
}
|
|
}
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":1
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"b",
|
|
"value":6
|
|
},
|
|
{
|
|
"ref":"bid",
|
|
"value":1000
|
|
},
|
|
{
|
|
"ref":"tb",
|
|
"value":{
|
|
"op":"+",
|
|
"left":"tb",
|
|
"right":1
|
|
}
|
|
},
|
|
{
|
|
"ref":"Bstop",
|
|
"value":true
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"BID",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"b",
|
|
"right":1
|
|
},
|
|
"right":{
|
|
"op":">",
|
|
"left":"tb",
|
|
"right":0
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"¬",
|
|
"exp":"Bcon"
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"¬",
|
|
"exp":"Sstop"
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"∨",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"tb",
|
|
"right":{
|
|
"op":"-",
|
|
"left":50,
|
|
"right":1
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"≤",
|
|
"left":{
|
|
"op":"-",
|
|
"left":1000,
|
|
"right":"bid"
|
|
},
|
|
"right":1
|
|
}
|
|
}
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":1
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"b",
|
|
"value":6
|
|
},
|
|
{
|
|
"ref":"bid",
|
|
"value":1000
|
|
},
|
|
{
|
|
"ref":"tb",
|
|
"value":{
|
|
"op":"+",
|
|
"left":"tb",
|
|
"right":1
|
|
}
|
|
},
|
|
{
|
|
"ref":"Bstop",
|
|
"value":true
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"tau__",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"b",
|
|
"right":6
|
|
},
|
|
"right":{
|
|
"op":"¬",
|
|
"exp":"Bswitch"
|
|
}
|
|
},
|
|
"right":"Bcon"
|
|
},
|
|
"right":{
|
|
"op":">",
|
|
"left":{
|
|
"op":"-",
|
|
"left":1000,
|
|
"right":"bid"
|
|
},
|
|
"right":{
|
|
"op":"*",
|
|
"left":1,
|
|
"right":100
|
|
}
|
|
}
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":1
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"b",
|
|
"value":2
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"tau__",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"b",
|
|
"right":6
|
|
},
|
|
"right":{
|
|
"op":"¬",
|
|
"exp":"Bswitch"
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"¬",
|
|
"exp":"Bcon"
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"<",
|
|
"left":"tb",
|
|
"right":20
|
|
}
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":1
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"b",
|
|
"value":2
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"tau__",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"b",
|
|
"right":6
|
|
},
|
|
"right":"Bswitch"
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":1
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"b",
|
|
"value":2
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"tau__",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"b",
|
|
"right":6
|
|
},
|
|
"right":{
|
|
"op":"¬",
|
|
"exp":"Bswitch"
|
|
}
|
|
},
|
|
"right":"Bcon"
|
|
},
|
|
"right":{
|
|
"op":"≤",
|
|
"left":{
|
|
"op":"-",
|
|
"left":1000,
|
|
"right":"bid"
|
|
},
|
|
"right":{
|
|
"op":"*",
|
|
"left":1,
|
|
"right":100
|
|
}
|
|
}
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":1
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"b",
|
|
"value":2
|
|
},
|
|
{
|
|
"ref":"Bcon",
|
|
"value":false
|
|
},
|
|
{
|
|
"ref":"Bswitch",
|
|
"value":true
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"tau__",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"b",
|
|
"right":6
|
|
},
|
|
"right":{
|
|
"op":"¬",
|
|
"exp":"Bswitch"
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"¬",
|
|
"exp":"Bcon"
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"tb",
|
|
"right":20
|
|
}
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":1
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"b",
|
|
"value":2
|
|
},
|
|
{
|
|
"ref":"Bcon",
|
|
"value":true
|
|
},
|
|
{
|
|
"ref":"Bswitch",
|
|
"value":true
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"tau__",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"b",
|
|
"right":2
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"s",
|
|
"right":2
|
|
}
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":1
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"b",
|
|
"value":3
|
|
},
|
|
{
|
|
"ref":"Bagreed",
|
|
"value":true
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"CBID",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"b",
|
|
"right":2
|
|
},
|
|
"right":{
|
|
"op":"¬",
|
|
"exp":"Bstop"
|
|
}
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":1
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"b",
|
|
"value":4
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"CBID",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"b",
|
|
"right":2
|
|
},
|
|
"right":"Bstop"
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":1
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"b",
|
|
"value":5
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"PURCHASE",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"=",
|
|
"left":"b",
|
|
"right":3
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":1
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"b",
|
|
"value":3
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"tau__",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"b",
|
|
"right":4
|
|
},
|
|
"right":"Bcon"
|
|
},
|
|
"right":{
|
|
"op":"<",
|
|
"left":"tb",
|
|
"right":{
|
|
"op":"-",
|
|
"left":50,
|
|
"right":1
|
|
}
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"≥",
|
|
"left":{
|
|
"op":"+",
|
|
"left":"bid",
|
|
"right":100
|
|
},
|
|
"right":"cbid"
|
|
}
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":1
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"b",
|
|
"value":3
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"tau__",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"b",
|
|
"right":4
|
|
},
|
|
"right":"Bcon"
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"tb",
|
|
"right":{
|
|
"op":"-",
|
|
"left":50,
|
|
"right":1
|
|
}
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"≥",
|
|
"left":1000,
|
|
"right":"cbid"
|
|
}
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":1
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"b",
|
|
"value":3
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"tau__",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"b",
|
|
"right":4
|
|
},
|
|
"right":"Bcon"
|
|
},
|
|
"right":{
|
|
"op":"¬",
|
|
"exp":"Sstop"
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"∨",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"<",
|
|
"left":"tb",
|
|
"right":{
|
|
"op":"-",
|
|
"left":50,
|
|
"right":1
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"<",
|
|
"left":{
|
|
"op":"+",
|
|
"left":"bid",
|
|
"right":100
|
|
},
|
|
"right":"cbid"
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"tb",
|
|
"right":{
|
|
"op":"-",
|
|
"left":50,
|
|
"right":1
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"<",
|
|
"left":1000,
|
|
"right":"cbid"
|
|
}
|
|
}
|
|
}
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":{
|
|
"op":"max",
|
|
"left":0,
|
|
"right":{
|
|
"op":"+",
|
|
"left":1,
|
|
"right":{
|
|
"op":"/",
|
|
"left":{
|
|
"op":"+",
|
|
"left":1,
|
|
"right":10000
|
|
},
|
|
"right":{
|
|
"op":"-",
|
|
"left":"cbid",
|
|
"right":{
|
|
"op":"+",
|
|
"left":{
|
|
"op":"+",
|
|
"left":1000,
|
|
"right":1
|
|
},
|
|
"right":10000
|
|
}
|
|
}
|
|
}
|
|
}
|
|
}
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"b",
|
|
"value":3
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
},
|
|
{
|
|
"probability":{
|
|
"exp":{
|
|
"op":"-",
|
|
"left":1,
|
|
"right":{
|
|
"op":"max",
|
|
"left":0,
|
|
"right":{
|
|
"op":"+",
|
|
"left":1,
|
|
"right":{
|
|
"op":"/",
|
|
"left":{
|
|
"op":"+",
|
|
"left":1,
|
|
"right":10000
|
|
},
|
|
"right":{
|
|
"op":"-",
|
|
"left":"cbid",
|
|
"right":{
|
|
"op":"+",
|
|
"left":{
|
|
"op":"+",
|
|
"left":1000,
|
|
"right":1
|
|
},
|
|
"right":10000
|
|
}
|
|
}
|
|
}
|
|
}
|
|
}
|
|
}
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"b",
|
|
"value":0
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"tau__",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"b",
|
|
"right":4
|
|
},
|
|
"right":"Bcon"
|
|
},
|
|
"right":"Sstop"
|
|
},
|
|
"right":{
|
|
"op":"∨",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"<",
|
|
"left":"tb",
|
|
"right":{
|
|
"op":"-",
|
|
"left":50,
|
|
"right":1
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"<",
|
|
"left":{
|
|
"op":"+",
|
|
"left":"bid",
|
|
"right":100
|
|
},
|
|
"right":"cbid"
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"tb",
|
|
"right":{
|
|
"op":"-",
|
|
"left":50,
|
|
"right":1
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"<",
|
|
"left":1000,
|
|
"right":"cbid"
|
|
}
|
|
}
|
|
}
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":{
|
|
"op":"max",
|
|
"left":0,
|
|
"right":{
|
|
"op":"+",
|
|
"left":1,
|
|
"right":{
|
|
"op":"/",
|
|
"left":{
|
|
"op":"+",
|
|
"left":1,
|
|
"right":10000
|
|
},
|
|
"right":{
|
|
"op":"-",
|
|
"left":"cbid",
|
|
"right":{
|
|
"op":"+",
|
|
"left":{
|
|
"op":"+",
|
|
"left":1000,
|
|
"right":1
|
|
},
|
|
"right":10000
|
|
}
|
|
}
|
|
}
|
|
}
|
|
}
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"b",
|
|
"value":3
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
},
|
|
{
|
|
"probability":{
|
|
"exp":{
|
|
"op":"-",
|
|
"left":1,
|
|
"right":{
|
|
"op":"max",
|
|
"left":0,
|
|
"right":{
|
|
"op":"+",
|
|
"left":1,
|
|
"right":{
|
|
"op":"/",
|
|
"left":{
|
|
"op":"+",
|
|
"left":1,
|
|
"right":10000
|
|
},
|
|
"right":{
|
|
"op":"-",
|
|
"left":"cbid",
|
|
"right":{
|
|
"op":"+",
|
|
"left":{
|
|
"op":"+",
|
|
"left":1000,
|
|
"right":1
|
|
},
|
|
"right":10000
|
|
}
|
|
}
|
|
}
|
|
}
|
|
}
|
|
}
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"b",
|
|
"value":5
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"tau__",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"b",
|
|
"right":4
|
|
},
|
|
"right":{
|
|
"op":"¬",
|
|
"exp":"Bcon"
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"<",
|
|
"left":"tb",
|
|
"right":{
|
|
"op":"-",
|
|
"left":50,
|
|
"right":1
|
|
}
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"≥",
|
|
"left":{
|
|
"op":"+",
|
|
"left":"bid",
|
|
"right":1
|
|
},
|
|
"right":"cbid"
|
|
}
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":1
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"b",
|
|
"value":3
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"tau__",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"b",
|
|
"right":4
|
|
},
|
|
"right":{
|
|
"op":"¬",
|
|
"exp":"Bcon"
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"tb",
|
|
"right":{
|
|
"op":"-",
|
|
"left":50,
|
|
"right":1
|
|
}
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"≥",
|
|
"left":1000,
|
|
"right":"cbid"
|
|
}
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":1
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"b",
|
|
"value":3
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"tau__",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"b",
|
|
"right":4
|
|
},
|
|
"right":{
|
|
"op":"¬",
|
|
"exp":"Bcon"
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"¬",
|
|
"exp":"Sstop"
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"<",
|
|
"left":"tb",
|
|
"right":{
|
|
"op":"-",
|
|
"left":50,
|
|
"right":1
|
|
}
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"<",
|
|
"left":{
|
|
"op":"+",
|
|
"left":"bid",
|
|
"right":1
|
|
},
|
|
"right":"cbid"
|
|
}
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":{
|
|
"op":"max",
|
|
"left":0,
|
|
"right":{
|
|
"op":"+",
|
|
"left":1,
|
|
"right":{
|
|
"op":"/",
|
|
"left":{
|
|
"op":"+",
|
|
"left":1,
|
|
"right":10000
|
|
},
|
|
"right":{
|
|
"op":"-",
|
|
"left":"cbid",
|
|
"right":{
|
|
"op":"+",
|
|
"left":{
|
|
"op":"+",
|
|
"left":1000,
|
|
"right":1
|
|
},
|
|
"right":10000
|
|
}
|
|
}
|
|
}
|
|
}
|
|
}
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"b",
|
|
"value":3
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
},
|
|
{
|
|
"probability":{
|
|
"exp":{
|
|
"op":"-",
|
|
"left":1,
|
|
"right":{
|
|
"op":"max",
|
|
"left":0,
|
|
"right":{
|
|
"op":"+",
|
|
"left":1,
|
|
"right":{
|
|
"op":"/",
|
|
"left":{
|
|
"op":"+",
|
|
"left":1,
|
|
"right":10000
|
|
},
|
|
"right":{
|
|
"op":"-",
|
|
"left":"cbid",
|
|
"right":{
|
|
"op":"+",
|
|
"left":{
|
|
"op":"+",
|
|
"left":1000,
|
|
"right":1
|
|
},
|
|
"right":10000
|
|
}
|
|
}
|
|
}
|
|
}
|
|
}
|
|
}
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"b",
|
|
"value":0
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"tau__",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"b",
|
|
"right":4
|
|
},
|
|
"right":{
|
|
"op":"¬",
|
|
"exp":"Bcon"
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"Sstop",
|
|
"right":true
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"<",
|
|
"left":"tb",
|
|
"right":{
|
|
"op":"-",
|
|
"left":50,
|
|
"right":1
|
|
}
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"<",
|
|
"left":{
|
|
"op":"+",
|
|
"left":"bid",
|
|
"right":1
|
|
},
|
|
"right":"cbid"
|
|
}
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":{
|
|
"op":"max",
|
|
"left":0,
|
|
"right":{
|
|
"op":"+",
|
|
"left":1,
|
|
"right":{
|
|
"op":"/",
|
|
"left":{
|
|
"op":"+",
|
|
"left":1,
|
|
"right":10000
|
|
},
|
|
"right":{
|
|
"op":"-",
|
|
"left":"cbid",
|
|
"right":{
|
|
"op":"+",
|
|
"left":{
|
|
"op":"+",
|
|
"left":1000,
|
|
"right":1
|
|
},
|
|
"right":10000
|
|
}
|
|
}
|
|
}
|
|
}
|
|
}
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"b",
|
|
"value":3
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
},
|
|
{
|
|
"probability":{
|
|
"exp":{
|
|
"op":"-",
|
|
"left":1,
|
|
"right":{
|
|
"op":"max",
|
|
"left":0,
|
|
"right":{
|
|
"op":"+",
|
|
"left":1,
|
|
"right":{
|
|
"op":"/",
|
|
"left":{
|
|
"op":"+",
|
|
"left":1,
|
|
"right":10000
|
|
},
|
|
"right":{
|
|
"op":"-",
|
|
"left":"cbid",
|
|
"right":{
|
|
"op":"+",
|
|
"left":{
|
|
"op":"+",
|
|
"left":1000,
|
|
"right":1
|
|
},
|
|
"right":10000
|
|
}
|
|
}
|
|
}
|
|
}
|
|
}
|
|
}
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"b",
|
|
"value":5
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"STOP",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"=",
|
|
"left":"b",
|
|
"right":5
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":1
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"b",
|
|
"value":5
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
}
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"name":"Seller",
|
|
"locations":[
|
|
{
|
|
"name":"location"
|
|
}
|
|
],
|
|
"initial-locations":[
|
|
"location"
|
|
],
|
|
"edges":[
|
|
{
|
|
"location":"location",
|
|
"action":"BID",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"s",
|
|
"right":0
|
|
},
|
|
"right":{
|
|
"op":"¬",
|
|
"exp":"Bstop"
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"¬",
|
|
"exp":"Sstop"
|
|
}
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":1
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"s",
|
|
"value":1
|
|
}
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"BID",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"s",
|
|
"right":0
|
|
},
|
|
"right":{
|
|
"op":"∨",
|
|
"left":"Bstop",
|
|
"right":"Sstop"
|
|
}
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":1
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"s",
|
|
"value":5
|
|
}
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"tau__",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"s",
|
|
"right":1
|
|
},
|
|
"right":"Scon"
|
|
},
|
|
"right":{
|
|
"op":"≤",
|
|
"left":{
|
|
"op":"-",
|
|
"left":"cbid",
|
|
"right":100
|
|
},
|
|
"right":"bid"
|
|
}
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":1
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"s",
|
|
"value":2
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"tau__",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"s",
|
|
"right":1
|
|
},
|
|
"right":"Scon"
|
|
},
|
|
"right":{
|
|
"op":"¬",
|
|
"exp":"Bstop"
|
|
}
|
|
},
|
|
"right":{
|
|
"op":">",
|
|
"left":{
|
|
"op":"-",
|
|
"left":"cbid",
|
|
"right":100
|
|
},
|
|
"right":"bid"
|
|
}
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":{
|
|
"op":"max",
|
|
"left":0,
|
|
"right":{
|
|
"op":"-",
|
|
"left":1,
|
|
"right":{
|
|
"op":"/",
|
|
"left":{
|
|
"op":"+",
|
|
"left":1,
|
|
"right":10000
|
|
},
|
|
"right":{
|
|
"op":"+",
|
|
"left":"bid",
|
|
"right":10000
|
|
}
|
|
}
|
|
}
|
|
}
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"s",
|
|
"value":2
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
},
|
|
{
|
|
"probability":{
|
|
"exp":{
|
|
"op":"-",
|
|
"left":1,
|
|
"right":{
|
|
"op":"max",
|
|
"left":0,
|
|
"right":{
|
|
"op":"-",
|
|
"left":1,
|
|
"right":{
|
|
"op":"/",
|
|
"left":{
|
|
"op":"+",
|
|
"left":1,
|
|
"right":10000
|
|
},
|
|
"right":{
|
|
"op":"+",
|
|
"left":"bid",
|
|
"right":10000
|
|
}
|
|
}
|
|
}
|
|
}
|
|
}
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"s",
|
|
"value":6
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"tau__",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"s",
|
|
"right":1
|
|
},
|
|
"right":"Scon"
|
|
},
|
|
"right":"Bstop"
|
|
},
|
|
"right":{
|
|
"op":">",
|
|
"left":{
|
|
"op":"-",
|
|
"left":"cbid",
|
|
"right":100
|
|
},
|
|
"right":"bid"
|
|
}
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":{
|
|
"op":"max",
|
|
"left":0,
|
|
"right":{
|
|
"op":"-",
|
|
"left":1,
|
|
"right":{
|
|
"op":"/",
|
|
"left":{
|
|
"op":"+",
|
|
"left":1,
|
|
"right":10000
|
|
},
|
|
"right":{
|
|
"op":"+",
|
|
"left":"bid",
|
|
"right":10000
|
|
}
|
|
}
|
|
}
|
|
}
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"s",
|
|
"value":2
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
},
|
|
{
|
|
"probability":{
|
|
"exp":{
|
|
"op":"-",
|
|
"left":1,
|
|
"right":{
|
|
"op":"max",
|
|
"left":0,
|
|
"right":{
|
|
"op":"-",
|
|
"left":1,
|
|
"right":{
|
|
"op":"/",
|
|
"left":{
|
|
"op":"+",
|
|
"left":1,
|
|
"right":10000
|
|
},
|
|
"right":{
|
|
"op":"+",
|
|
"left":"bid",
|
|
"right":10000
|
|
}
|
|
}
|
|
}
|
|
}
|
|
}
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"s",
|
|
"value":5
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"tau__",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"s",
|
|
"right":1
|
|
},
|
|
"right":{
|
|
"op":"¬",
|
|
"exp":"Scon"
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"<",
|
|
"left":"ts",
|
|
"right":{
|
|
"op":"-",
|
|
"left":50,
|
|
"right":1
|
|
}
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"≤",
|
|
"left":{
|
|
"op":"-",
|
|
"left":"cbid",
|
|
"right":1
|
|
},
|
|
"right":"bid"
|
|
}
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":1
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"s",
|
|
"value":2
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"tau__",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"s",
|
|
"right":1
|
|
},
|
|
"right":{
|
|
"op":"¬",
|
|
"exp":"Scon"
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"ts",
|
|
"right":{
|
|
"op":"-",
|
|
"left":50,
|
|
"right":1
|
|
}
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"≤",
|
|
"left":{
|
|
"op":"-",
|
|
"left":"cbid",
|
|
"right":1
|
|
},
|
|
"right":"bid"
|
|
}
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":1
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"s",
|
|
"value":2
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"tau__",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"s",
|
|
"right":1
|
|
},
|
|
"right":{
|
|
"op":"¬",
|
|
"exp":"Scon"
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"¬",
|
|
"exp":"Bstop"
|
|
}
|
|
},
|
|
"right":{
|
|
"op":">",
|
|
"left":{
|
|
"op":"-",
|
|
"left":"cbid",
|
|
"right":1
|
|
},
|
|
"right":"bid"
|
|
}
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":{
|
|
"op":"max",
|
|
"left":0,
|
|
"right":{
|
|
"op":"-",
|
|
"left":1,
|
|
"right":{
|
|
"op":"/",
|
|
"left":{
|
|
"op":"+",
|
|
"left":1,
|
|
"right":10000
|
|
},
|
|
"right":{
|
|
"op":"+",
|
|
"left":"bid",
|
|
"right":10000
|
|
}
|
|
}
|
|
}
|
|
}
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"s",
|
|
"value":2
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
},
|
|
{
|
|
"probability":{
|
|
"exp":{
|
|
"op":"-",
|
|
"left":1,
|
|
"right":{
|
|
"op":"max",
|
|
"left":0,
|
|
"right":{
|
|
"op":"-",
|
|
"left":1,
|
|
"right":{
|
|
"op":"/",
|
|
"left":{
|
|
"op":"+",
|
|
"left":1,
|
|
"right":10000
|
|
},
|
|
"right":{
|
|
"op":"+",
|
|
"left":"bid",
|
|
"right":10000
|
|
}
|
|
}
|
|
}
|
|
}
|
|
}
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"s",
|
|
"value":6
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"tau__",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"s",
|
|
"right":1
|
|
},
|
|
"right":{
|
|
"op":"¬",
|
|
"exp":"Scon"
|
|
}
|
|
},
|
|
"right":"Bstop"
|
|
},
|
|
"right":{
|
|
"op":">",
|
|
"left":{
|
|
"op":"-",
|
|
"left":"cbid",
|
|
"right":1
|
|
},
|
|
"right":"bid"
|
|
}
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":{
|
|
"op":"max",
|
|
"left":0,
|
|
"right":{
|
|
"op":"-",
|
|
"left":1,
|
|
"right":{
|
|
"op":"/",
|
|
"left":{
|
|
"op":"+",
|
|
"left":1,
|
|
"right":10000
|
|
},
|
|
"right":{
|
|
"op":"+",
|
|
"left":"bid",
|
|
"right":10000
|
|
}
|
|
}
|
|
}
|
|
}
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"s",
|
|
"value":2
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
},
|
|
{
|
|
"probability":{
|
|
"exp":{
|
|
"op":"-",
|
|
"left":1,
|
|
"right":{
|
|
"op":"max",
|
|
"left":0,
|
|
"right":{
|
|
"op":"-",
|
|
"left":1,
|
|
"right":{
|
|
"op":"/",
|
|
"left":{
|
|
"op":"+",
|
|
"left":1,
|
|
"right":10000
|
|
},
|
|
"right":{
|
|
"op":"+",
|
|
"left":"bid",
|
|
"right":10000
|
|
}
|
|
}
|
|
}
|
|
}
|
|
}
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"s",
|
|
"value":5
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"PURCHASE",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"=",
|
|
"left":"s",
|
|
"right":2
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":1
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"s",
|
|
"value":2
|
|
}
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"tau__",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"s",
|
|
"right":6
|
|
},
|
|
"right":{
|
|
"op":"¬",
|
|
"exp":"Sswitch"
|
|
}
|
|
},
|
|
"right":"Scon"
|
|
},
|
|
"right":{
|
|
"op":">",
|
|
"left":{
|
|
"op":"-",
|
|
"left":"cbid",
|
|
"right":1
|
|
},
|
|
"right":{
|
|
"op":"*",
|
|
"left":8,
|
|
"right":100
|
|
}
|
|
}
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":1
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"s",
|
|
"value":3
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"tau__",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"s",
|
|
"right":6
|
|
},
|
|
"right":{
|
|
"op":"¬",
|
|
"exp":"Sswitch"
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"¬",
|
|
"exp":"Scon"
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"<",
|
|
"left":"ts",
|
|
"right":48
|
|
}
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":1
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"s",
|
|
"value":3
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"tau__",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"s",
|
|
"right":6
|
|
},
|
|
"right":"Sswitch"
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":1
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"s",
|
|
"value":3
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"tau__",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"s",
|
|
"right":6
|
|
},
|
|
"right":{
|
|
"op":"¬",
|
|
"exp":"Sswitch"
|
|
}
|
|
},
|
|
"right":"Scon"
|
|
},
|
|
"right":{
|
|
"op":"≤",
|
|
"left":{
|
|
"op":"-",
|
|
"left":"cbid",
|
|
"right":1
|
|
},
|
|
"right":{
|
|
"op":"*",
|
|
"left":8,
|
|
"right":100
|
|
}
|
|
}
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":1
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"s",
|
|
"value":3
|
|
},
|
|
{
|
|
"ref":"Scon",
|
|
"value":false
|
|
},
|
|
{
|
|
"ref":"Sswitch",
|
|
"value":true
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"tau__",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"s",
|
|
"right":6
|
|
},
|
|
"right":{
|
|
"op":"¬",
|
|
"exp":"Sswitch"
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"¬",
|
|
"exp":"Scon"
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"ts",
|
|
"right":48
|
|
}
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":1
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"s",
|
|
"value":3
|
|
},
|
|
{
|
|
"ref":"Scon",
|
|
"value":true
|
|
},
|
|
{
|
|
"ref":"Sswitch",
|
|
"value":true
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"CBID",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"s",
|
|
"right":3
|
|
},
|
|
"right":"Bstop"
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":1
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"s",
|
|
"value":5
|
|
}
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"CBID",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"s",
|
|
"right":3
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"ts",
|
|
"right":0
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"¬",
|
|
"exp":"Bstop"
|
|
}
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":1
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"s",
|
|
"value":7
|
|
},
|
|
{
|
|
"ref":"ts",
|
|
"value":{
|
|
"op":"+",
|
|
"left":"ts",
|
|
"right":1
|
|
}
|
|
}
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"CBID",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"s",
|
|
"right":3
|
|
},
|
|
"right":"Scon"
|
|
},
|
|
"right":{
|
|
"op":"¬",
|
|
"exp":"Bstop"
|
|
}
|
|
},
|
|
"right":{
|
|
"op":">",
|
|
"left":"ts",
|
|
"right":0
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"<",
|
|
"left":"ts",
|
|
"right":{
|
|
"op":"-",
|
|
"left":50,
|
|
"right":1
|
|
}
|
|
}
|
|
},
|
|
"right":{
|
|
"op":">",
|
|
"left":{
|
|
"op":"-",
|
|
"left":"cbid",
|
|
"right":1
|
|
},
|
|
"right":100
|
|
}
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":1
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"s",
|
|
"value":7
|
|
},
|
|
{
|
|
"ref":"cbid",
|
|
"value":{
|
|
"op":"-",
|
|
"left":"cbid",
|
|
"right":100
|
|
}
|
|
},
|
|
{
|
|
"ref":"ts",
|
|
"value":{
|
|
"op":"+",
|
|
"left":"ts",
|
|
"right":1
|
|
}
|
|
}
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"CBID",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"s",
|
|
"right":3
|
|
},
|
|
"right":{
|
|
"op":"¬",
|
|
"exp":"Scon"
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"¬",
|
|
"exp":"Bstop"
|
|
}
|
|
},
|
|
"right":{
|
|
"op":">",
|
|
"left":"ts",
|
|
"right":0
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"<",
|
|
"left":"ts",
|
|
"right":{
|
|
"op":"-",
|
|
"left":50,
|
|
"right":1
|
|
}
|
|
}
|
|
},
|
|
"right":{
|
|
"op":">",
|
|
"left":{
|
|
"op":"-",
|
|
"left":"cbid",
|
|
"right":1
|
|
},
|
|
"right":1
|
|
}
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":1
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"s",
|
|
"value":7
|
|
},
|
|
{
|
|
"ref":"cbid",
|
|
"value":{
|
|
"op":"-",
|
|
"left":"cbid",
|
|
"right":1
|
|
}
|
|
},
|
|
{
|
|
"ref":"ts",
|
|
"value":{
|
|
"op":"+",
|
|
"left":"ts",
|
|
"right":1
|
|
}
|
|
}
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"CBID",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"s",
|
|
"right":3
|
|
},
|
|
"right":{
|
|
"op":">",
|
|
"left":"ts",
|
|
"right":0
|
|
}
|
|
},
|
|
"right":"Scon"
|
|
},
|
|
"right":{
|
|
"op":"¬",
|
|
"exp":"Bstop"
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"∨",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"ts",
|
|
"right":{
|
|
"op":"-",
|
|
"left":50,
|
|
"right":1
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"≤",
|
|
"left":{
|
|
"op":"-",
|
|
"left":"cbid",
|
|
"right":1
|
|
},
|
|
"right":100
|
|
}
|
|
}
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":1
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"s",
|
|
"value":7
|
|
},
|
|
{
|
|
"ref":"cbid",
|
|
"value":1
|
|
},
|
|
{
|
|
"ref":"ts",
|
|
"value":{
|
|
"op":"+",
|
|
"left":"ts",
|
|
"right":1
|
|
}
|
|
},
|
|
{
|
|
"ref":"Sstop",
|
|
"value":true
|
|
}
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"CBID",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"s",
|
|
"right":3
|
|
},
|
|
"right":{
|
|
"op":">",
|
|
"left":"ts",
|
|
"right":0
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"¬",
|
|
"exp":"Scon"
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"¬",
|
|
"exp":"Bstop"
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"∨",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"ts",
|
|
"right":{
|
|
"op":"-",
|
|
"left":50,
|
|
"right":1
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"≤",
|
|
"left":{
|
|
"op":"-",
|
|
"left":"cbid",
|
|
"right":1
|
|
},
|
|
"right":1
|
|
}
|
|
}
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":1
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"s",
|
|
"value":7
|
|
},
|
|
{
|
|
"ref":"cbid",
|
|
"value":1
|
|
},
|
|
{
|
|
"ref":"ts",
|
|
"value":{
|
|
"op":"+",
|
|
"left":"ts",
|
|
"right":1
|
|
}
|
|
},
|
|
{
|
|
"ref":"Sstop",
|
|
"value":true
|
|
}
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"tau__",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"s",
|
|
"right":4
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"b",
|
|
"right":1
|
|
}
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":1
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"s",
|
|
"value":0
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"tau__",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"s",
|
|
"right":4
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"b",
|
|
"right":3
|
|
}
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":1
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"s",
|
|
"value":2
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"STOP",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"=",
|
|
"left":"s",
|
|
"right":5
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":1
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"s",
|
|
"value":5
|
|
}
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"tau__",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"s",
|
|
"right":7
|
|
},
|
|
"right":{
|
|
"op":"¬",
|
|
"exp":"Sswitch"
|
|
}
|
|
},
|
|
"right":"Scon"
|
|
},
|
|
"right":{
|
|
"op":">",
|
|
"left":{
|
|
"op":"-",
|
|
"left":"cbid",
|
|
"right":1
|
|
},
|
|
"right":{
|
|
"op":"*",
|
|
"left":8,
|
|
"right":100
|
|
}
|
|
}
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":1
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"s",
|
|
"value":4
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"tau__",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"s",
|
|
"right":7
|
|
},
|
|
"right":{
|
|
"op":"¬",
|
|
"exp":"Sswitch"
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"¬",
|
|
"exp":"Scon"
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"<",
|
|
"left":"ts",
|
|
"right":48
|
|
}
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":1
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"s",
|
|
"value":4
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"tau__",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"s",
|
|
"right":7
|
|
},
|
|
"right":"Sswitch"
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":1
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"s",
|
|
"value":4
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"tau__",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"s",
|
|
"right":7
|
|
},
|
|
"right":{
|
|
"op":"¬",
|
|
"exp":"Sswitch"
|
|
}
|
|
},
|
|
"right":"Scon"
|
|
},
|
|
"right":{
|
|
"op":"≤",
|
|
"left":{
|
|
"op":"-",
|
|
"left":"cbid",
|
|
"right":1
|
|
},
|
|
"right":{
|
|
"op":"*",
|
|
"left":8,
|
|
"right":100
|
|
}
|
|
}
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":1
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"s",
|
|
"value":4
|
|
},
|
|
{
|
|
"ref":"Scon",
|
|
"value":false
|
|
},
|
|
{
|
|
"ref":"Sswitch",
|
|
"value":true
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
}
|
|
]
|
|
},
|
|
{
|
|
"location":"location",
|
|
"action":"tau__",
|
|
"guard":{
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"s",
|
|
"right":7
|
|
},
|
|
"right":{
|
|
"op":"¬",
|
|
"exp":"Sswitch"
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"¬",
|
|
"exp":"Scon"
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"ts",
|
|
"right":48
|
|
}
|
|
}
|
|
},
|
|
"destinations":[
|
|
{
|
|
"probability":{
|
|
"exp":1
|
|
},
|
|
"location":"location",
|
|
"assignments":[
|
|
{
|
|
"ref":"s",
|
|
"value":4
|
|
},
|
|
{
|
|
"ref":"Scon",
|
|
"value":true
|
|
},
|
|
{
|
|
"ref":"Sswitch",
|
|
"value":true
|
|
}
|
|
],
|
|
"observables":[
|
|
]
|
|
}
|
|
]
|
|
}
|
|
]
|
|
}
|
|
],
|
|
"system":{
|
|
"elements":[
|
|
{
|
|
"automaton":"Buyer"
|
|
},
|
|
{
|
|
"automaton":"Seller"
|
|
}
|
|
],
|
|
"syncs":[
|
|
{
|
|
"synchronise":[
|
|
"BID",
|
|
"BID"
|
|
],
|
|
"result":"BID"
|
|
},
|
|
{
|
|
"synchronise":[
|
|
"CBID",
|
|
"CBID"
|
|
],
|
|
"result":"CBID"
|
|
},
|
|
{
|
|
"synchronise":[
|
|
"PURCHASE",
|
|
"PURCHASE"
|
|
],
|
|
"result":"PURCHASE"
|
|
},
|
|
{
|
|
"synchronise":[
|
|
"STOP",
|
|
"STOP"
|
|
],
|
|
"result":"STOP"
|
|
},
|
|
{
|
|
"synchronise":[
|
|
"tau__",
|
|
null
|
|
],
|
|
"result":"tau__"
|
|
},
|
|
{
|
|
"synchronise":[
|
|
null,
|
|
"tau__"
|
|
],
|
|
"result":"tau__"
|
|
}
|
|
]
|
|
}
|
|
}
|