diff --git a/paynt/quotient/quotient.py b/paynt/quotient/quotient.py index e5e1dc012..6ab52d0ea 100644 --- 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 index cce4c93a5..4ce2569c5 100644 --- 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 index 4b5d58f15..ebb85a271 100644 --- 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)