fix target state detection for discounted reward properties

paynt/quotient/mdp.py

@@ -181,8 +181,8 @@ def to_graphviz(self, graphviz_tree, variables, action_labels):
 
         graphviz_tree.node(self.graphviz_id, label=node_label, shape="box", style="rounded", margin="0.05,0.05")
         if not self.is_terminal:
-            graphviz_tree.edge(self.graphviz_id,self.child_true.graphviz_id,label="True")
-            graphviz_tree.edge(self.graphviz_id,self.child_false.graphviz_id,label="False")
+            graphviz_tree.edge(self.graphviz_id,self.child_true.graphviz_id,label="T")
+            graphviz_tree.edge(self.graphviz_id,self.child_false.graphviz_id,label="F")
 
 
 
@@ -235,8 +235,9 @@ def to_list(self):
             node_info[node.identifier] = (parent,child_true,child_false)
         return node_info
 
-    def simplify(self):
-        self.root.simplify(self.variables, self.state_valuations)
+    def simplify(self, target_state_mask):
+        state_valuations = [self.state_valuations[state] for state in ~target_state_mask]
+        self.root.simplify(self.variables, state_valuations)
 
     def to_string(self):
         return self.root.to_string(self.variables,self.quotient.action_labels)

paynt/quotient/quotient.py

@@ -328,6 +328,12 @@ def identify_absorbing_states(self, model):
                     break
         return state_is_absorbing
 
-    def identify_target_states(self, model, prop):
+    def identify_target_states(self, model=None, prop=None):
+        if model is None:
+            model = self.quotient_mdp
+        if prop is None:
+            prop = self.get_property()
+        if prop.is_discounted_reward:
+            return stormpy.BitVector(model.nr_states,False)
         target_label = prop.get_target_label()
         return model.labeling.get_states(target_label)

paynt/synthesizer/decision_tree.py

@@ -259,7 +259,8 @@ def run(self, optimum_threshold=None):
         if self.best_tree is None:
             logger.info("no admissible tree found")
         else:
-            self.best_tree.simplify()
+            target_states = self.quotient.identify_target_states()
+            self.best_tree.simplify(target_states)
             depth = self.best_tree.get_depth()
             num_nodes = len(self.best_tree.collect_nonterminals())
             logger.info(f"synthesized tree of depth {depth} with {num_nodes} decision nodes")

paynt/verification/property.py

@@ -124,6 +124,10 @@ def __str__(self):
     def reward(self):
         return self.formula.is_reward_operator
 
+    @property
+    def is_discounted_reward(self):
+        return self.formula.is_reward_operator and self.formula.subformula.is_discounted_total_reward_formula
+
     @property
     def maximizing(self):
         return not self.minimizing