diff --git a/paynt/verification/property.py b/paynt/verification/property.py index 02952eac..6699da4f 100644 --- a/paynt/verification/property.py +++ b/paynt/verification/property.py @@ -95,7 +95,9 @@ def above_model_checking_precision(a, b): def __init__(self, prop): self.property = prop rf = prop.raw_formula + self.game_optimizing_player = None # player index for game properties + self.game_formula = None # use comparison type to deduce optimizing direction comparison_type = rf.comparison_type @@ -157,6 +159,10 @@ def maximizing(self): def is_until(self): return self.formula.subformula.is_until_formula + @property + def has_game_formula(self): + return self.game_formula is not None + def transform_until_to_eventually(self): if not self.is_until: return @@ -236,6 +242,9 @@ def __init__(self, prop, epsilon=0): self.property = prop rf = prop.raw_formula + self.game_optimizing_player = None # player index for game properties + self.game_formula = None + # use comparison type to deduce optimizing direction if rf.optimality_type == stormpy.OptimizationDirection.Minimize: self.minimizing = True