remove deprecated stuff, move model checking to quotient

paynt/cli.py

@@ -54,8 +54,6 @@ def setup_logger(log_path = None):
     help="name of the properties file in the project")
 @click.option("--relative-error", type=click.FLOAT, default="0", show_default=True,
     help="relative error for optimal synthesis")
-@click.option("--discount-factor", type=click.FLOAT, default="1", show_default=True,
-    help="discount factor")
 @click.option("--optimum-threshold", type=click.FLOAT,
     help="known optimum bound")
 @click.option("--precision", type=click.FLOAT, default=1e-4,
@@ -139,7 +137,7 @@ def setup_logger(log_path = None):
     help="run profiling")
 
 def paynt_run(
-    project, sketch, props, relative_error, discount_factor, optimum_threshold, precision,
+    project, sketch, props, relative_error, optimum_threshold, precision,
     export,
     method,
     incomplete_search, disable_expected_visits,
@@ -162,7 +160,7 @@ def paynt_run(
 
     # set CLI parameters
     paynt.synthesizer.synthesizer.Synthesizer.incomplete_search = incomplete_search
-    paynt.quotient.quotient.Quotient.compute_expected_visits = not disable_expected_visits
+    paynt.quotient.quotient.Quotient.disable_expected_visits = disable_expected_visits
     paynt.synthesizer.synthesizer_cegis.SynthesizerCEGIS.conflict_generator_type = ce_generator
     paynt.quotient.pomdp.PomdpQuotient.initial_memory_size = pomdp_memory_size
     paynt.quotient.pomdp.PomdpQuotient.posterior_aware = posterior_aware
@@ -182,7 +180,7 @@ def paynt_run(
     sketch_path = os.path.join(project, sketch)
     properties_path = os.path.join(project, props)
     if all_in_one is None:
-        quotient = paynt.parser.sketch.Sketch.load_sketch(sketch_path, properties_path, export, relative_error, discount_factor, precision, constraint_bound)
+        quotient = paynt.parser.sketch.Sketch.load_sketch(sketch_path, properties_path, export, relative_error, precision, constraint_bound)
         synthesizer = paynt.synthesizer.synthesizer.Synthesizer.choose_synthesizer(quotient, method, fsc_synthesis, storm_control)
         synthesizer.run(optimum_threshold, export_evaluation)
     else:

paynt/family/family.py

@@ -136,8 +136,6 @@ class ParentInfo():
     def __init__(self):
         # list of constraint indices still undecided in this family
         self.constraint_indices = None
-        # for each undecided property contains analysis results
-        self.analysis_hints = None
 
         # how many refinements were needed to create this family
         self.refinement_depth = None
@@ -179,61 +177,9 @@ def copy(self):
         return DesignSpace(super().copy())
 
 
-    def generalize_hint(self, hint):
-        hint_global = dict()
-        hint = list(hint.get_values())
-        for state in range(self.mdp.states):
-            hint_global[self.mdp.quotient_state_map[state]] = hint[state]
-        return hint_global
-
-
-    def generalize_hints(self, result):
-        hint_prim = self.generalize_hint(result.primary.result)
-        hint_seco = self.generalize_hint(result.secondary.result) if result.secondary is not None else None
-        return (hint_prim, hint_seco)
-
-
-    def collect_analysis_hints(self, specification):
-        res = self.analysis_result
-        analysis_hints = dict()
-        for index in res.constraints_result.undecided_constraints:
-            prop = specification.constraints[index]
-            hints = self.generalize_hints(res.constraints_result.results[index])
-            analysis_hints[prop] = hints
-        if res.optimality_result is not None:
-            prop = specification.optimality
-            hints = self.generalize_hints(res.optimality_result)
-            analysis_hints[prop] = hints
-        return analysis_hints
-
-
-    def translate_analysis_hint(self, hint):
-        if hint is None:
-            return None
-        translated_hint = [0] * self.mdp.states
-        for state in range(self.mdp.states):
-            global_state = self.mdp.quotient_state_map[state]
-            translated_hint[state] = hint[global_state]
-        return translated_hint
-
-
-    def translate_analysis_hints(self):
-        if not DesignSpace.store_hints or self.parent_info is None:
-            return None
-
-        analysis_hints = dict()
-        for prop,hints in self.parent_info.analysis_hints.items():
-            hint_prim,hint_seco = hints
-            translated_hint_prim = self.translate_analysis_hint(hint_prim)
-            translated_hint_seco = self.translate_analysis_hint(hint_seco)
-            analysis_hints[prop] = (translated_hint_prim,translated_hint_seco)
-
-        return analysis_hints
-
     def collect_parent_info(self, specification):
         pi = ParentInfo()
         pi.refinement_depth = self.refinement_depth
-        pi.analysis_hints = self.collect_analysis_hints(specification)
         cr = self.analysis_result.constraints_result
         pi.constraint_indices = cr.undecided_constraints if cr is not None else []
         pi.splitter = self.splitter

paynt/parser/jani.py

@@ -2,7 +2,7 @@
 import payntbind
 
 import paynt.verification.property
-from ..quotient.models import MarkovChain
+import paynt.quotient.models
 
 import itertools
 from collections import defaultdict
@@ -49,19 +49,14 @@ def __init__(self, prism, hole_expressions, specification, family):
         properties_unpacked = []
         for index,prop_old in enumerate(properties_old):
             prop_new = properties[index]
-            discount_factor = prop_old.discount_factor
             if type(prop_old) == paynt.verification.property.Property:
-                p = paynt.verification.property.Property(prop_new,discount_factor)
+                p = paynt.verification.property.Property(prop_new)
             else:
                 epsilon = prop_old.epsilon
-                if type(prop_old) == paynt.verification.property.OptimalityProperty:
-                    p = paynt.verification.property.OptimalityProperty(prop_new,discount_factor,epsilon)
-                else:
-                    dminimizing = prop_old.dminimizing
-                    p = paynt.verification.property.DoubleOptimalityProperty(prop_new,dminimizing,discount_factor,epsilon)
+                p = paynt.verification.property.OptimalityProperty(prop_new,epsilon)
             properties_unpacked.append(p)
         self.specification = paynt.verification.property.Specification(properties_unpacked)
-        MarkovChain.initialize(self.specification)
+        paynt.quotient.models.Mdp.initialize(self.specification)
 
         # unfold holes in the program
         self.hole_expressions = hole_expressions
@@ -71,7 +66,7 @@ def __init__(self, prism, hole_expressions, specification, family):
         logger.debug("constructing the quotient...")
 
         # construct the explicit quotient
-        quotient_mdp = stormpy.build_sparse_model_with_options(self.jani_unfolded, MarkovChain.builder_options)
+        quotient_mdp = stormpy.build_sparse_model_with_options(self.jani_unfolded, paynt.quotient.models.Mdp.builder_options)
 
         # associate each action of a quotient MDP with hole options
         # reconstruct choice labels from choice origins

paynt/parser/prism_parser.py

@@ -4,9 +4,7 @@
 import paynt.family.family
 import paynt.verification.property
 import paynt.parser.jani
-
-from ..quotient.models import MarkovChain
-
+import paynt.quotient.models
 
 import os
 import re
@@ -19,7 +17,7 @@
 class PrismParser:
 
     @classmethod
-    def read_prism(cls, sketch_path, properties_path, relative_error, discount_factor):
+    def read_prism(cls, sketch_path, properties_path, relative_error):
 
         # parse the program
         prism, hole_definitions = PrismParser.load_sketch_prism(sketch_path)
@@ -42,7 +40,7 @@ def read_prism(cls, sketch_path, properties_path, relative_error, discount_facto
             logger.info("processing hole definitions...")
             prism, hole_expressions, family = PrismParser.parse_holes(prism, expression_parser, hole_definitions)
 
-        specification = PrismParser.parse_specification(properties_path, relative_error, discount_factor, prism)
+        specification = PrismParser.parse_specification(properties_path, relative_error, prism)
 
         # construct the quotient
         coloring = None
@@ -55,13 +53,13 @@ def read_prism(cls, sketch_path, properties_path, relative_error, discount_facto
             specification = jani_unfolder.specification
             quotient_mdp = jani_unfolder.quotient_mdp
             coloring = payntbind.synthesis.Coloring(family.family, quotient_mdp.nondeterministic_choice_indices, jani_unfolder.choice_to_hole_options)
-            MarkovChain.initialize(specification)
+            paynt.quotient.models.Mdp.initialize(specification)
             if prism.model_type == stormpy.storage.PrismModelType.POMDP:
                 obs_evaluator = payntbind.synthesis.ObservationEvaluator(prism, quotient_mdp)
             quotient_mdp = payntbind.synthesis.addChoiceLabelsFromJani(quotient_mdp)
         else:
-            MarkovChain.initialize(specification)
-            quotient_mdp = MarkovChain.from_prism(prism)
+            paynt.quotient.models.Mdp.initialize(specification)
+            quotient_mdp = paynt.quotient.models.Mdp.from_prism(prism)
 
         return prism, quotient_mdp, specification, family, coloring, jani_unfolder, obs_evaluator
 
@@ -195,49 +193,28 @@ def parse_property(cls, line, prism=None):
         return props[0]
 
     @classmethod
-    def parse_specification(cls, properties_path, relative_error, discount_factor, prism=None, family=None):
+    def parse_specification(cls, properties_path, relative_error=0, prism=None):
         '''
         Expecting one property per line. The line may be terminated with a semicolon.
         Empty lines or comments are allowed.
         '''
-
         if not os.path.isfile(properties_path):
             raise ValueError(f"the properties file {properties_path} does not exist")
         logger.info(f"loading properties from {properties_path} ...")
 
-        mdp_spec = re.compile(r'^\s*(min|max)\s+(.*)$')
-
         lines = ""
         with open(properties_path) as file:
             lines = [line for line in file]
 
         properties = []
 
         for line in lines:
-            minmax = None
-            match = mdp_spec.search(line)
-            if match is not None:
-                minmax = match.group(1)
-                line = match.group(2)
-            prop = PrismParser.parse_property(line,prism)
-            if prop is None:
+            formula = PrismParser.parse_property(line,prism)
+            if formula is None:
                 continue
-
-            rf = prop.raw_formula
-            assert rf.has_bound != rf.has_optimality_type, \
-                "optimizing formula contains a bound or a comparison formula does not"
-            if minmax is None:
-                if rf.has_bound:
-                    prop = paynt.verification.property.Property(prop,discount_factor)
-                else:
-                    prop = paynt.verification.property.OptimalityProperty(prop, discount_factor, relative_error)
-            else:
-                assert not rf.has_bound, "double-optimality objective cannot contain a bound"
-                dminimizing = (minmax=="min")
-                prop = paynt.verification.property.DoubleOptimalityProperty(prop, dminimizing, discount_factor, relative_error)
+            prop = paynt.verification.property.construct_property(formula, relative_error)
             properties.append(prop)
 
         specification = paynt.verification.property.Specification(properties)
         logger.info(f"found the following specification: {specification}")
-        assert not specification.has_double_optimality, "did not expect double-optimality property"
         return specification

paynt/parser/sketch.py

@@ -57,11 +57,7 @@ class Sketch:
 
     @classmethod
     def load_sketch(cls, sketch_path, properties_path,
-        export=None, relative_error=0, discount_factor=1, precision=1e-4, constraint_bound=None):
-
-        assert discount_factor>0 and discount_factor<=1, "discount factor must be in the interval (0,1]"
-        if discount_factor < 1:
-            logger.warning("ignoring non-trivial discount factor")
+        export=None, relative_error=0, precision=1e-4, constraint_bound=None):
 
         prism = None
         explicit_quotient = None
@@ -83,15 +79,15 @@ def load_sketch(cls, sketch_path, properties_path,
         try:
             logger.info(f"assuming sketch in PRISM format...")
             prism, explicit_quotient, specification, family, coloring, jani_unfolder, obs_evaluator = PrismParser.read_prism(
-                        sketch_path, properties_path, relative_error, discount_factor)
+                        sketch_path, properties_path, relative_error)
             filetype = "prism"
         except SyntaxError:
             pass
         if filetype is None:
             try:
                 logger.info(f"assuming sketch in DRN format...")
                 explicit_quotient = PomdpParser.read_pomdp_drn(sketch_path)
-                specification = PrismParser.parse_specification(properties_path, relative_error, discount_factor)
+                specification = PrismParser.parse_specification(properties_path, relative_error)
                 filetype = "drn"
             except:
                 pass
@@ -107,7 +103,7 @@ def load_sketch(cls, sketch_path, properties_path,
                 decpomdp_manager.apply_discount_factor_transformation()
                 explicit_quotient = decpomdp_manager.construct_pomdp()
                 if constraint_bound is not None:
-                    specification = PrismParser.parse_specification(properties_path, relative_error, discount_factor)
+                    specification = PrismParser.parse_specification(properties_path, relative_error)
                 else:
                     optimality = paynt.verification.property.construct_reward_property(
                         decpomdp_manager.reward_model_name,
@@ -121,7 +117,7 @@ def load_sketch(cls, sketch_path, properties_path,
         assert filetype is not None, "unknow format of input file"
         logger.info("sketch parsing OK")
 
-        paynt.quotient.models.MarkovChain.initialize(specification)
+        paynt.quotient.models.Mdp.initialize(specification)
         paynt.verification.property.Property.initialize()
 
         make_rewards_action_based(explicit_quotient)
@@ -165,7 +161,7 @@ def load_sketch_as_all_in_one(cls, sketch_path, properties_path):
                 logger.info("processing hole definitions...")
                 prism, hole_expressions, family = PrismParser.parse_holes(prism, expression_parser, hole_definitions)
 
-            specification = PrismParser.parse_specification(properties_path, 0, 1, prism)
+            specification = PrismParser.parse_specification(properties_path, prism=prism)
 
             prism = prism.replace_variable_initialization_by_init_expression()
             expression_manager = prism.expression_manager

paynt/quotient/mdp_family.py

@@ -219,5 +219,4 @@ def build_assignment(self, family):
         assert family.size == 1, "expecting family of size 1"
         choices = self.coloring.selectCompatibleChoices(family.family)
         model,state_map,choice_map = self.restrict_quotient(choices)
-        mdp = paynt.quotient.models.MDP(model,self,state_map,choice_map,family)
-        return mdp
+        return paynt.quotient.models.SubMdp(model,state_map,choice_map)