Skip to content

Commit 212c123

Browse files
authored
Merge pull request #9 from convince-project/t3.4-dev
MDP + Policy to SCXML Converters for T3.4
2 parents ffa9f97 + 320ec95 commit 212c123

16 files changed

+118483
-31
lines changed

bin/generate_bookstore_scxml.py

Lines changed: 184 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,184 @@
1+
#!/usr/bin/env python3
2+
"""A script to build the bookstore MDP and output the corresponding SCXML file.
3+
4+
Author: Charlie Street
5+
Owner: Charlie Street
6+
"""
7+
8+
from refine_plan.models.condition import Label, EqCondition, AndCondition, OrCondition
9+
from refine_plan.algorithms.semi_mdp_solver import synthesise_policy
10+
from refine_plan.models.state_factor import StateFactor
11+
from refine_plan.models.dbn_option import DBNOption
12+
from refine_plan.models.semi_mdp import SemiMDP
13+
from refine_plan.models.state import State
14+
import sys
15+
16+
# Global map setup
17+
18+
GRAPH = {
19+
"v1": {"e12": "v2", "e13": "v3", "e14": "v4"},
20+
"v2": {"e12": "v1", "e23": "v3", "e25": "v5", "e26": "v6"},
21+
"v3": {
22+
"e13": "v1",
23+
"e23": "v2",
24+
"e34": "v4",
25+
"e35": "v5",
26+
"e36": "v6",
27+
"e37": "v7",
28+
},
29+
"v4": {"e14": "v1", "e34": "v3", "e46": "v6", "e47": "v7"},
30+
"v5": {"e25": "v2", "e35": "v3", "e56": "v6", "e58": "v8"},
31+
"v6": {
32+
"e26": "v2",
33+
"e36": "v3",
34+
"e46": "v4",
35+
"e56": "v5",
36+
"e67": "v7",
37+
"e68": "v8",
38+
},
39+
"v7": {
40+
"e37": "v3",
41+
"e47": "v4",
42+
"e67": "v6",
43+
"e78": "v8",
44+
},
45+
"v8": {"e58": "v5", "e68": "v6", "e78": "v7"},
46+
}
47+
48+
CORRESPONDING_DOOR = {
49+
"e12": None,
50+
"e14": None,
51+
"e58": "v5",
52+
"e78": "v7",
53+
"e13": None,
54+
"e36": "v3",
55+
"e68": "v6",
56+
"e25": "v2",
57+
"e47": "v4",
58+
"e26": "v2",
59+
"e35": "v3",
60+
"e46": "v4",
61+
"e37": "v3",
62+
"e23": None,
63+
"e34": None,
64+
"e56": None,
65+
"e67": None,
66+
}
67+
68+
# Problem Setup
69+
INITIAL_LOC = "v1"
70+
GOAL_LOC = "v8"
71+
72+
73+
def _get_enabled_cond(sf_list, option):
74+
"""Get the enabled condition for an option.
75+
76+
Args:
77+
sf_list: The list of state factors
78+
option: The option we want the condition for
79+
80+
Returns:
81+
The enabled condition for the option
82+
"""
83+
sf_dict = {sf.get_name(): sf for sf in sf_list}
84+
85+
door_locs = ["v{}".format(i) for i in range(2, 8)]
86+
87+
if option == "check_door" or option == "open_door":
88+
enabled_cond = OrCondition()
89+
door_status = "unknown" if option == "check_door" else "closed"
90+
for door in door_locs:
91+
enabled_cond.add_cond(
92+
AndCondition(
93+
EqCondition(sf_dict["location"], door),
94+
EqCondition(sf_dict["{}_door".format(door)], door_status),
95+
)
96+
)
97+
return enabled_cond
98+
else: # edge navigation option
99+
enabled_cond = OrCondition()
100+
for node in GRAPH:
101+
if option in GRAPH[node]:
102+
enabled_cond.add_cond(EqCondition(sf_dict["location"], node))
103+
door = CORRESPONDING_DOOR[option]
104+
if door != None:
105+
enabled_cond = AndCondition(
106+
enabled_cond, EqCondition(sf_dict["{}_door".format(door)], "open")
107+
)
108+
return enabled_cond
109+
110+
111+
def generate_mdp_scxml():
112+
"""Generate the bookstore MDP and write out the corresponding SCXML file."""
113+
114+
loc_sf = StateFactor("location", ["v{}".format(i) for i in range(1, 9)])
115+
door_sfs = [
116+
StateFactor("v2_door", ["unknown", "closed", "open"]),
117+
StateFactor("v3_door", ["unknown", "closed", "open"]),
118+
StateFactor("v4_door", ["unknown", "closed", "open"]),
119+
StateFactor("v5_door", ["unknown", "closed", "open"]),
120+
StateFactor("v6_door", ["unknown", "closed", "open"]),
121+
StateFactor("v7_door", ["unknown", "closed", "open"]),
122+
]
123+
sf_list = [loc_sf] + door_sfs
124+
125+
labels = [Label("goal", EqCondition(loc_sf, "v8"))]
126+
127+
option_names = [
128+
"e12",
129+
"e14",
130+
"e58",
131+
"e78",
132+
"e13",
133+
"e36",
134+
"e68",
135+
"e25",
136+
"e47",
137+
"e26",
138+
"e35",
139+
"e46",
140+
"e37",
141+
"e23",
142+
"e34",
143+
"e56",
144+
"e67",
145+
"check_door",
146+
"open_door",
147+
]
148+
149+
assert len(set(option_names)) == 19 # Quick safety check
150+
151+
init_state_dict = {sf: "unknown" for sf in door_sfs}
152+
init_state_dict[loc_sf] = "v1"
153+
init_state = State(init_state_dict)
154+
155+
option_list = []
156+
for option in option_names:
157+
print("Reading in option: {}".format(option))
158+
t_path = "../data/bookstore/{}_transition.bifxml".format(option)
159+
r_path = "../data/bookstore/{}_reward.bifxml".format(option)
160+
option_list.append(
161+
DBNOption(
162+
option, t_path, r_path, sf_list, _get_enabled_cond(sf_list, option)
163+
)
164+
)
165+
166+
print("Creating MDP...")
167+
semi_mdp = SemiMDP(sf_list, option_list, labels, initial_state=init_state)
168+
print("Writing SCXML file")
169+
semi_mdp.to_scxml_file(
170+
"../data/bookstore/bookstore_mdp.scxml", "Bookstore_Policy", name="Bookstore"
171+
)
172+
print("Synthesising Policy...")
173+
policy = synthesise_policy(semi_mdp, prism_prop='Rmin=?[F "goal"]')
174+
policy.to_scxml(
175+
"../data/bookstore/bookstore_policy.scxml",
176+
model_name="Bookstore",
177+
initial_state=init_state,
178+
name="Bookstore_Policy",
179+
)
180+
# policy.write_policy("../data/bookstore/bookstore_refined_policy.yaml")
181+
182+
183+
if __name__ == "__main__":
184+
generate_mdp_scxml()

0 commit comments

Comments
 (0)