fix using optional coloring

paynt/quotient/coloring.py

@@ -56,7 +56,7 @@ def __init__(self, mdp, holes, action_to_hole_options):
     @property
     def num_choices(self):
         return len(self.action_to_hole_options)
-        
+
     def select_actions(self, family):
         '''
         Select non-default actions relevant in the provided design space.
@@ -112,3 +112,13 @@ def select_actions(self, family):
         selected_actions_bv = stormpy.synthesis.construct_selection(self.default_actions, selected_actions)
 
         return hole_selected_actions,selected_actions,selected_actions_bv
+
+
+    def choices_to_hole_selection(self, choices):
+        hole_selection = [set() for hole_index in self.holes.hole_indices]
+        for choice in choices:
+            choice_options = self.action_to_hole_options[choice]
+            for hole_index,option in choice_options.items():
+                hole_selection[hole_index].add(option)
+        hole_selection = [list(options) for options in hole_selection]
+        return hole_selection

paynt/quotient/quotient.py

@@ -184,26 +184,15 @@ def state_to_choice_to_choices(self, state_to_choice):
             if choice is not None:
                 choices.set(choice,True)
         return choices
-
-
-    def choices_to_hole_selection(self, choices, coloring=None):
-        if coloring is None:
-            coloring = self.coloring
-        hole_selection = [set() for hole_index in self.design_space.hole_indices]
-        for choice in choices:
-            choice_options = self.coloring.action_to_hole_options[choice]
-            for hole_index,option in choice_options.items():
-                hole_selection[hole_index].add(option)
-        hole_selection = [list(options) for options in hole_selection]
-        return hole_selection
-
 
     def scheduler_selection(self, mdp, scheduler, coloring=None):
         ''' Get hole options involved in the scheduler selection. '''
         assert scheduler.memoryless and scheduler.deterministic
-        state_to_choice = self.scheduler_to_state_to_choice(mdp, scheduler, keep_reachable=True)
+        state_to_choice = self.scheduler_to_state_to_choice(mdp, scheduler)
         choices = self.state_to_choice_to_choices(state_to_choice)
-        hole_selection = self.choices_to_hole_selection(choices,coloring)
+        if coloring is None:
+            coloring = self.coloring
+        hole_selection = coloring.choices_to_hole_selection(choices)
         return hole_selection
 
 

paynt/synthesizer/policy_tree.py

@@ -493,7 +493,7 @@ def verify_family(self, family, game_solver, prop, reference_policy=None):
 
         # map reachable scheduler choices to hole options
         scheduler_choices = self.quotient.state_to_choice_to_choices(state_to_choice)
-        hole_selection = self.quotient.choices_to_hole_selection(scheduler_choices)
+        hole_selection = self.quotient.coloring.choices_to_hole_selection(scheduler_choices)
 
         if False:
             # sanity check