Skip to content

Commit

Permalink
add game_formula to Property init
Browse files Browse the repository at this point in the history
  • Loading branch information
PurpleDragon64 committed Nov 18, 2024
1 parent 3beadd3 commit 356acb6
Showing 1 changed file with 9 additions and 0 deletions.
9 changes: 9 additions & 0 deletions paynt/verification/property.py
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down

0 comments on commit 356acb6

Please sign in to comment.