export reward name

randriu · Nov 24, 2023 · 91bde67 · 91bde67
1 parent 1e7a389
commit 91bde67
Show file tree

Hide file tree

Showing 3 changed files with 7 additions and 3 deletions.
diff --git a/paynt/quotient/quotient.py b/paynt/quotient/quotient.py
@@ -482,9 +482,9 @@ def identify_absorbing_states(self, model):
                     break
         return state_is_absorbing
 
-    def extract_target_label(self):
+    def get_property(self):
         assert self.specification.num_properties == 1, "expecting a single property"
-        return self.specification.all_properties()[0].get_target_label()
+        return self.specification.all_properties()[0]
 
 
 

diff --git a/paynt/verification/property.py b/paynt/verification/property.py
@@ -139,6 +139,10 @@ def negate(self):
     def get_target_label(self):
         return str(self.formula.subformula.subformula)
 
+    def get_reward_name(self):
+        assert self.reward
+        return self.formula.reward_name
+
 
 
 class OptimalityProperty(Property):

diff --git a/paynt_pomdp_sketch.py b/paynt_pomdp_sketch.py
@@ -13,7 +13,7 @@ def load_sketch(project_path):
     properties_path = os.path.join(project_path, "sketch.props")    
     pomdp_sketch = paynt.parser.sketch.Sketch.load_sketch(sketch_path, properties_path)
 
-    target_label = pomdp_sketch.extract_target_label()
+    target_label = pomdp_sketch.get_property().get_target_label()
     target_states = pomdp_sketch.quotient_mdp.labeling.get_states(target_label)
     for state in pomdp_sketch.quotient_mdp.labeling.get_states("deadlock"):
         assert state in target_states, "have deadlock in a non-target state {}".format(state)