various fixes

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:

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)
 

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
+}