From ba97d1c1f6fab35ffad1ee7b9135baf6d20fece4 Mon Sep 17 00:00:00 2001 From: Roman Andriushchenko Date: Tue, 26 Nov 2024 16:40:01 +0100 Subject: [PATCH] various fixes --- paynt/parser/prism_parser.py | 4 ++-- paynt/verification/property.py | 4 ++-- payntbind/src/synthesis/synthesis.cpp | 7 ++++--- 3 files changed, 8 insertions(+), 7 deletions(-) diff --git a/paynt/parser/prism_parser.py b/paynt/parser/prism_parser.py index 42c57faf..a91ba4f5 100644 --- a/paynt/parser/prism_parser.py +++ b/paynt/parser/prism_parser.py @@ -70,8 +70,8 @@ def load_sketch_prism(cls, sketch_path): sketch_lines = f.readlines() # replace hole definitions with constants - hole_re_brace = re.compile(r'^\s*hole\s+(.*?)\s+(.*?)\s+in\s+\{(.*?)\}\s*;\s*$') - # hole_re_bracket = re.compile(r'^\s*hole\s+(.*?)\s+(.*?)\s+in\s+[(.*?)]\s+;\s+$') + hole_re_brace = re.compile(r'^\s*hole\s+(.*?)\s+(.*?)\s+in\s+\{(.*?)\}\s*;') + # hole_re_bracket = re.compile(r'^\s*hole\s+(.*?)\s+(.*?)\s+in\s+[(.*?)]\s+;') sketch_output = [] hole_definitions = [] for line in sketch_lines: diff --git a/paynt/verification/property.py b/paynt/verification/property.py index 6699da4f..c7de16d1 100644 --- a/paynt/verification/property.py +++ b/paynt/verification/property.py @@ -167,7 +167,7 @@ def transform_until_to_eventually(self): if not self.is_until: return logger.info("converting until formula to eventually...") - formula = payntbind.synthesis.transform_until_to_eventually(self.formula) + formula = payntbind.synthesis.transform_until_to_eventually(self.property.raw_formula) prop = stormpy.core.Property("", formula) self.__init__(prop) @@ -306,7 +306,7 @@ def transform_until_to_eventually(self): if not self.is_until: return logger.info("converting until formula to eventually...") - formula = payntbind.synthesis.transform_until_to_eventually(self.formula) + formula = payntbind.synthesis.transform_until_to_eventually(self.property.raw_formula) prop = stormpy.core.Property("", formula) self.__init__(prop, self.epsilon) diff --git a/payntbind/src/synthesis/synthesis.cpp b/payntbind/src/synthesis/synthesis.cpp index 1d73fb65..c33c3325 100644 --- a/payntbind/src/synthesis/synthesis.cpp +++ b/payntbind/src/synthesis/synthesis.cpp @@ -8,10 +8,11 @@ void define_synthesis(py::module& m) { bindings_decpomdp(m); bindings_counterexamples(m); bindings_pomdp_family(m); - bindings_posmg(m); bindings_coloring(m); + #ifndef DISABLE_SMG bindings_smg(m); -} - + bindings_posmg(m); + #endif // DISABLE_SMG +} \ No newline at end of file