From d41ba6258fb42ab947db4941a8fa0d434adbeff8 Mon Sep 17 00:00:00 2001 From: Thomas Knoll Date: Fri, 22 Sep 2023 13:38:46 +0200 Subject: [PATCH] adversary handling --- examples/shields/rl/helpers.py | 23 +++++++--- examples/shields/rl/shieldhandlers.py | 65 ++++++++++++++++++++------- 2 files changed, 68 insertions(+), 20 deletions(-) diff --git a/examples/shields/rl/helpers.py b/examples/shields/rl/helpers.py index 9c5b520..20dac9e 100644 --- a/examples/shields/rl/helpers.py +++ b/examples/shields/rl/helpers.py @@ -37,7 +37,7 @@ def extract_keys(env): if env.carrying and env.carrying.type == "key": keys.append((env.carrying, -1, -1)) - + # TODO Maybe need to add ordering of keys so it matches the order in the shield return keys def extract_doors(env): @@ -51,6 +51,18 @@ def extract_doors(env): return doors +def extract_adversaries(env): + adv = [] + + if not hasattr(env, "adversaries"): + return [] + + for color, adversary in env.adversaries.items(): + adv.append(adversary) + + + return adv + def create_log_dir(args): return F"{args.log_dir}sh:{args.shielding}-env:{args.env}" @@ -87,6 +99,7 @@ def parse_arguments(argparse): help="gym environment to load", default="MiniGrid-LavaCrossingS9N1-v0", choices=[ + "MiniGrid-Adv-8x8-v0", "MiniGrid-LavaCrossingS9N1-v0", "MiniGrid-LavaCrossingS9N3-v0", "MiniGrid-LavaSlipperyS12-v0", @@ -94,10 +107,10 @@ def parse_arguments(argparse): "MiniGrid-LavaSlipperyS12-v2", "MiniGrid-LavaSlipperyS12-v3", "MiniGrid-DoorKey-8x8-v0", - "MiniGrid-DoubleDoor-16x16-v0", - "MiniGrid-DoubleDoor-12x12-v0", - "MiniGrid-DoubleDoor-10x8-v0", - "MiniGrid-SingleDoor-7x6-v0", + # "MiniGrid-DoubleDoor-16x16-v0", + # "MiniGrid-DoubleDoor-12x12-v0", + # "MiniGrid-DoubleDoor-10x8-v0", + # "MiniGrid-SingleDoor-7x6-v0", # "MiniGrid-LockedRoom-v0", # "MiniGrid-FourRooms-v0", # "MiniGrid-LavaGapS7-v0", diff --git a/examples/shields/rl/shieldhandlers.py b/examples/shields/rl/shieldhandlers.py index 1f95228..3cf95a3 100644 --- a/examples/shields/rl/shieldhandlers.py +++ b/examples/shields/rl/shieldhandlers.py @@ -9,11 +9,11 @@ import stormpy.examples import stormpy.examples.files -from helpers import extract_doors, extract_keys +from helpers import extract_doors, extract_keys, extract_adversaries from abc import ABC import os - +import time class Action(): def __init__(self, idx, prob=1, labels=[]) -> None: self.idx = idx @@ -40,7 +40,7 @@ class MiniGridShieldHandler(ShieldHandler): def __create_prism(self): - result = os.system(F"{self.grid_to_prism_path} -v 'agent' -i {self.grid_file} -o {self.prism_path}") + result = os.system(F"{self.grid_to_prism_path} -v 'Agent,Blue' -i {self.grid_file} -o {self.prism_path}") assert result == 0, "Prism file could not be generated" @@ -67,19 +67,18 @@ class MiniGridShieldHandler(ShieldHandler): assert result.has_shield shield = result.shield stormpy.shields.export_shield(model, shield, "Grid.shield") - action_dictionary = {} shield_scheduler = shield.construct() + state_valuations = model.state_valuations + choice_labeling = model.choice_labeling for stateID in model.states: choice = shield_scheduler.get_choice(stateID) choices = choice.choice_map - state_valuation = model.state_valuations.get_string(stateID) - - actions_to_be_executed = [Action(idx= choice[1], prob=choice[0], labels=model.choice_labeling.get_labels_of_choice(model.get_choice_index(stateID, choice[1]))) for choice in choices] - + state_valuation = state_valuations.get_string(stateID) + actions_to_be_executed = [Action(idx= choice[1], prob=choice[0], labels=choice_labeling.get_labels_of_choice(model.get_choice_index(stateID, choice[1]))) for choice in choices] action_dictionary[state_valuation] = actions_to_be_executed - + return action_dictionary @@ -93,15 +92,16 @@ class MiniGridShieldHandler(ShieldHandler): def create_shield_query(env): coordinates = env.env.agent_pos view_direction = env.env.agent_dir - + keys = extract_keys(env) doors = extract_doors(env) + adversaries = extract_adversaries(env) if env.carrying: - carrying = F"Agent_is_carrying_object\t" + agent_carrying = F"Agent_is_carrying_object\t" else: - carrying = "!Agent_is_carrying_object\t" + agent_carrying = "!Agent_is_carrying_object\t" key_positions = [] agent_key_status = [] @@ -110,7 +110,6 @@ def create_shield_query(env): key_color = key[0].color key_x = key[1] key_y = key[2] - # '[!Agent_is_carrying_object\t& !Agent_has_yellow_key\t& !AgentDone\t& Dooryellowlocked\t& !Dooryellowopen\t& xAgent=1\t& yAgent=1\t& viewAgent=0\t& xKeyyellow=2\t& yKeyyellow=2]' if env.carrying and env.carrying.type == "key": agent_key_text = F"Agent_has_{env.carrying.color}_key\t& " key_position = F"xKey{key_color}={key_x}\t& yKey{key_color}={key_y}\t" @@ -121,7 +120,8 @@ def create_shield_query(env): key_positions.append(key_position) agent_key_status.append(agent_key_text) - key_positions[-1] = key_positions[-1].strip() + if key_positions: + key_positions[-1] = key_positions[-1].strip() door_status = [] for door in doors: @@ -134,11 +134,46 @@ def create_shield_query(env): status = F"!Door{door.color}locked\t& !Door{door.color}open\t&" door_status.append(status) + + adv_status = [] + adv_positions = [] + + for adversary in adversaries: + status = "" + position = "" + if adversary.carrying: + carrying = F"{adversary.name}_is_carrying_object\t" + else: + carrying = F"!{adversary.name}_is_carrying_object\t" + + status = F"{carrying}& !{adversary.name}Done\t& " + position = F"x{adversary.name}={adversary.cur_pos[1]}\t& y{adversary.name}={adversary.cur_pos[0]}\t& view{adversary.name}={adversary.adversary_dir}" + adv_status.append(status) + adv_positions.append(position) + door_status_text = "" + + if door_status: + door_status_text = F"& {''.join(door_status)}\t" + + adv_status_text = "" + + if adv_status: + adv_status_text = F"& {''.join(adv_status)}" + + adv_positions_text = "" + + if adv_positions: + adv_positions_text = F"\t& {''.join(adv_positions)}" + + key_positions_text = "" + + if key_positions: + key_positions_text = F"\t& {''.join(key_positions)}" agent_position = F"xAgent={coordinates[0]}\t& yAgent={coordinates[1]}\t& viewAgent={view_direction}" - query = f"[{carrying}& {''.join(agent_key_status)}!AgentDone\t& {''.join(door_status)} {agent_position}\t& {''.join(key_positions)}]" + query = f"[{agent_carrying}& {''.join(agent_key_status)}!AgentDone\t{adv_status_text}{door_status_text}{agent_position}{adv_positions_text}{key_positions_text}]" return query \ No newline at end of file