Merge pull request #56 from lukovdm/master

Add synthesis for exact POMDPs

.gitignore

@@ -8,3 +8,5 @@ prerequisites/
 
 # OSX
 .DS_Store
+
+build/

paynt/cli.py

@@ -32,7 +32,7 @@ def setup_logger(log_path = None):
     # root.setLevel(logging.INFO)
 
     # formatter = logging.Formatter('%(asctime)s %(threadName)s - %(name)s - %(levelname)s - %(message)s')
-    formatter = logging.Formatter('%(asctime)s - %(filename)s - %(message)s')
+    formatter = logging.Formatter('%(asctime)s - %(filename)s:%(lineno)d - %(message)s')
 
     handlers = []
     if log_path is not None:
@@ -61,6 +61,8 @@ def setup_logger(log_path = None):
     help="known optimum bound")
 @click.option("--precision", type=click.FLOAT, default=1e-4,
     help="model checking precision")
+@click.option("--exact", is_flag=True, default=False,
+    help="use exact synthesis (very limited at the moment)")
 @click.option("--timeout", type=int,
     help="timeout (s)")
 
@@ -138,7 +140,7 @@ def setup_logger(log_path = None):
     help="run profiling")
 
 def paynt_run(
-    project, sketch, props, relative_error, optimum_threshold, precision, timeout,
+    project, sketch, props, relative_error, optimum_threshold, precision, exact, timeout,
     export,
     method,
     disable_expected_visits,
@@ -187,7 +189,7 @@ def paynt_run(
 
     sketch_path = os.path.join(project, sketch)
     properties_path = os.path.join(project, props)
-    quotient = paynt.parser.sketch.Sketch.load_sketch(sketch_path, properties_path, export, relative_error, precision, constraint_bound)
+    quotient = paynt.parser.sketch.Sketch.load_sketch(sketch_path, properties_path, export, relative_error, precision, constraint_bound, exact)
     synthesizer = paynt.synthesizer.synthesizer.Synthesizer.choose_synthesizer(quotient, method, fsc_synthesis, storm_control)
     synthesizer.run(optimum_threshold)
 

paynt/family/__init__.py

@@ -0,0 +1,10 @@
+__version__ = "unknown"
+
+try:
+    from .._version import __version__
+except ImportError:
+    # We're running in a tree that doesn't have a _version.py, so we don't know what our version is.
+    pass
+
+def version():
+    return __version__

paynt/models/__init__.py

@@ -0,0 +1,10 @@
+__version__ = "unknown"
+
+try:
+    from .._version import __version__
+except ImportError:
+    # We're running in a tree that doesn't have a _version.py, so we don't know what our version is.
+    pass
+
+def version():
+    return __version__

paynt/models/model_builder.py

@@ -29,12 +29,15 @@ def from_jani(cls, program, specification = None):
         return model
 
     @classmethod
-    def from_prism(cls, program, specification = None):
+    def from_prism(cls, program, specification = None, use_exact=False):
         assert program.model_type in [stormpy.storage.PrismModelType.MDP, stormpy.storage.PrismModelType.POMDP]
         builder_options = cls.default_builder_options(specification)
-        model = stormpy.build_sparse_model_with_options(program, builder_options)
+        if use_exact:
+            model = stormpy.build_sparse_exact_model_with_options(program, builder_options)
+        else:
+            model = stormpy.build_sparse_model_with_options(program, builder_options)
         return model
 
     @classmethod
-    def from_drn(cls, drn_path):
-        return DrnParser.parse_drn(drn_path)
+    def from_drn(cls, drn_path, use_exact=False):
+        return DrnParser.parse_drn(drn_path, use_exact)

paynt/parser/drn_parser.py

@@ -17,20 +17,22 @@ class DrnParser:
     WHITESPACES = ' \t\n\v\f\r'
 
     @classmethod
-    def parse_drn(cls, sketch_path):
+    def parse_drn(cls, sketch_path, use_exact=False):
         # try to read a drn file and return POSMG or POMDP based on the type
         # ValueError if file is not dnr or the model is of unsupported type
         explicit_model = None
         try:
             type = DrnParser.decide_type_of_drn(sketch_path)
             if type == 'POSMG':
+                if use_exact:
+                    raise ValueError('Exact synthesis is not supported for POSMG models')
                 pomdp_path = sketch_path + '.tmp'
                 state_player_indications = DrnParser.pomdp_from_posmg(sketch_path, pomdp_path)
                 pomdp = DrnParser.read_drn(pomdp_path)
                 explicit_model = payntbind.synthesis.posmg_from_pomdp(pomdp, state_player_indications)
                 os.remove(pomdp_path)
             else:
-                explicit_model = DrnParser.read_drn(sketch_path)
+                explicit_model = DrnParser.read_drn(sketch_path, use_exact)
         except Exception as e:
             print(e)
             raise ValueError('Failed to read sketch file in a .drn format')
@@ -91,10 +93,13 @@ def str_remove_range(string: str, start_idx: int, end_idx: int) -> str:
         return string[:start_idx] + string[end_idx+1:]
 
     @classmethod
-    def read_drn(cls, sketch_path):
+    def read_drn(cls, sketch_path, use_exact=False):
         builder_options = stormpy.core.DirectEncodingParserOptions()
         builder_options.build_choice_labels = True
-        return stormpy.build_model_from_drn(sketch_path, builder_options)
+        if use_exact:
+            return stormpy.core._build_sparse_exact_model_from_drn(sketch_path, builder_options)
+        else:
+            return stormpy.build_model_from_drn(sketch_path, builder_options)
 
     @staticmethod
     def parse_posmg_specification(properties_path):

paynt/parser/prism_parser.py

@@ -17,7 +17,7 @@
 class PrismParser:
 
     @classmethod
-    def read_prism(cls, sketch_path, properties_path, relative_error):
+    def read_prism(cls, sketch_path, properties_path, relative_error, use_exact=False):
 
         # parse the program
         prism, hole_definitions = PrismParser.load_sketch_prism(sketch_path)
@@ -41,7 +41,7 @@ def read_prism(cls, sketch_path, properties_path, relative_error):
             prism, hole_expressions, family = PrismParser.parse_holes(prism, expression_parser, hole_definitions)
         prism = prism.label_unlabelled_commands({})
 
-        specification = PrismParser.parse_specification(properties_path, relative_error, prism)
+        specification = PrismParser.parse_specification(properties_path, relative_error, prism, use_exact=use_exact)
 
         # construct the quotient
         coloring = None
@@ -58,7 +58,7 @@ def read_prism(cls, sketch_path, properties_path, relative_error):
                 obs_evaluator = payntbind.synthesis.ObservationEvaluator(prism, quotient_mdp)
             quotient_mdp = payntbind.synthesis.addChoiceLabelsFromJani(quotient_mdp)
         else:
-            quotient_mdp = paynt.models.model_builder.ModelBuilder.from_prism(prism, specification)
+            quotient_mdp = paynt.models.model_builder.ModelBuilder.from_prism(prism, specification, use_exact)
 
         return prism, quotient_mdp, specification, family, coloring, jani_unfolder, obs_evaluator
 
@@ -192,7 +192,7 @@ def parse_property(cls, line, prism=None):
         return props[0]
 
     @classmethod
-    def parse_specification(cls, properties_path, relative_error=0, prism=None):
+    def parse_specification(cls, properties_path, relative_error=0, prism=None, use_exact=False):
         '''
         Expecting one property per line. The line may be terminated with a semicolon.
         Empty lines or comments are allowed.
@@ -211,7 +211,7 @@ def parse_specification(cls, properties_path, relative_error=0, prism=None):
             formula = PrismParser.parse_property(line,prism)
             if formula is None:
                 continue
-            prop = paynt.verification.property.construct_property(formula, relative_error)
+            prop = paynt.verification.property.construct_property(formula, relative_error, use_exact)
             properties.append(prop)
 
         specification = paynt.verification.property.Specification(properties)

paynt/parser/sketch.py

@@ -48,15 +48,20 @@ def make_rewards_action_based(model):
             for action in range(tm.get_row_group_start(state),tm.get_row_group_end(state)):
                 action_reward[action] += state_reward
 
-        payntbind.synthesis.remove_reward_model(model,name)
-        new_reward_model = stormpy.storage.SparseRewardModel(optional_state_action_reward_vector=action_reward)
-        model.add_reward_model(name, new_reward_model)
+        if model.is_exact:
+            payntbind.synthesis.remove_reward_model_exact(model,name)
+            new_reward_model = stormpy.storage.SparseExactRewardModel(optional_state_action_reward_vector=action_reward)
+            model.add_reward_model(name, new_reward_model)
+        else:
+            payntbind.synthesis.remove_reward_model(model,name)
+            new_reward_model = stormpy.storage.SparseRewardModel(optional_state_action_reward_vector=action_reward)
+            model.add_reward_model(name, new_reward_model)
 
 class Sketch:
 
     @classmethod
     def load_sketch(cls, sketch_path, properties_path,
-        export=None, relative_error=0, precision=1e-4, constraint_bound=None):
+        export=None, relative_error=0, precision=1e-4, constraint_bound=None, use_exact=False):
 
         prism = None
         explicit_quotient = None
@@ -78,15 +83,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)
+                        sketch_path, properties_path, relative_error, use_exact)
             filetype = "prism"
         except SyntaxError:
             pass
         if filetype is None:
             try:
                 logger.info(f"assuming sketch in DRN format...")
-                explicit_quotient = paynt.models.model_builder.ModelBuilder.from_drn(sketch_path)
-                specification = PrismParser.parse_specification(properties_path, relative_error)
+                explicit_quotient = paynt.models.model_builder.ModelBuilder.from_drn(sketch_path, use_exact)
+                specification = PrismParser.parse_specification(properties_path, relative_error, use_exact=use_exact)
                 filetype = "drn"
                 project_path = os.path.dirname(sketch_path)
                 valuations_filename = "state-valuations.json"
@@ -96,6 +101,8 @@ def load_sketch(cls, sketch_path, properties_path,
                     with open(valuations_path) as file:
                         state_valuations = json.load(file)
                 if state_valuations is not None:
+                    if use_exact:
+                        raise Exception("exact synthesis is not supported with state valuations")
                     logger.info(f"found state valuations in {valuations_path}, adding to the model...")
                     explicit_quotient = payntbind.synthesis.addStateValuations(explicit_quotient,state_valuations)
             except Exception as e:
@@ -128,7 +135,10 @@ def load_sketch(cls, sketch_path, properties_path,
         logger.info("sketch parsing OK")
 
         paynt.verification.property.Property.initialize()
-        updated = payntbind.synthesis.addMissingChoiceLabels(explicit_quotient)
+        if explicit_quotient.is_exact:
+            updated = payntbind.synthesis.addMissingChoiceLabelsExact(explicit_quotient)
+        else:
+            updated = payntbind.synthesis.addMissingChoiceLabels(explicit_quotient)
         if updated is not None: explicit_quotient = updated
         if not payntbind.synthesis.assertChoiceLabelingIsCanonic(explicit_quotient.nondeterministic_choice_indices,explicit_quotient.choice_labeling,False):
             logger.warning("WARNING: choice labeling for the quotient is not canonic")

paynt/quotient/pomdp.py

@@ -63,7 +63,7 @@ def __init__(self, pomdp, specification, decpomdp_manager=None):
         # ^ this also asserts that states with the same observation have the
         # same number and the same order of available actions
 
-        logger.info(f"constructed POMDP having {self.observations} observations.")
+        logger.info(f"constructed {'exact' if self.pomdp.is_exact else ''} POMDP having {self.observations} observations.")
 
         state_obs = self.pomdp.observations.copy()
 
@@ -116,10 +116,16 @@ def __init__(self, pomdp, specification, decpomdp_manager=None):
             self.observation_states[state_obs[state]] += 1
 
         # initialize POMDP manager
-        if not PomdpQuotient.posterior_aware:
-            self.pomdp_manager = payntbind.synthesis.PomdpManager(self.pomdp)
+        if self.pomdp.is_exact:
+            if not PomdpQuotient.posterior_aware:
+                self.pomdp_manager = payntbind.synthesis.ExactPomdpManager(self.pomdp)
+            else:
+                self.pomdp_manager = payntbind.synthesis.ExactPomdpManagerAposteriori(self.pomdp)
         else:
-            self.pomdp_manager = payntbind.synthesis.PomdpManagerAposteriori(self.pomdp)
+            if not PomdpQuotient.posterior_aware:
+                self.pomdp_manager = payntbind.synthesis.PomdpManager(self.pomdp)
+            else:
+                self.pomdp_manager = payntbind.synthesis.PomdpManagerAposteriori(self.pomdp)
 
         # do initial unfolding
         self.set_imperfect_memory_size(PomdpQuotient.initial_memory_size)
@@ -339,7 +345,10 @@ def unfold_memory(self):
 
         logger.debug("unfolding {}-FSC template into POMDP...".format(max(self.observation_memory_size)))
         self.quotient_mdp = self.pomdp_manager.construct_mdp()
-        self.choice_destinations = payntbind.synthesis.computeChoiceDestinations(self.quotient_mdp)
+        if self.quotient_mdp.is_exact:
+            self.choice_destinations = payntbind.synthesis.computeChoiceDestinationsExact(self.quotient_mdp)
+        else:
+            self.choice_destinations = payntbind.synthesis.computeChoiceDestinations(self.quotient_mdp)
         logger.debug(f"constructed quotient MDP having {self.quotient_mdp.nr_states} states and {self.quotient_mdp.nr_choices} actions.")
 
         self.family, choice_to_hole_options = self.create_coloring()

paynt/quotient/quotient.py

@@ -89,9 +89,14 @@ def mdp_to_dtmc(mdp):
         tm = mdp.transition_matrix
         tm.make_row_grouping_trivial()
         assert tm.nr_columns == tm.nr_rows, "expected transition matrix without non-trivial row groups"
-        components = stormpy.storage.SparseModelComponents(tm, mdp.labeling, mdp.reward_models)
-        dtmc = stormpy.storage.SparseDtmc(components)
-        return dtmc
+        if mdp.is_exact:
+            components = stormpy.storage.SparseExactModelComponents(tm, mdp.labeling, mdp.reward_models)
+            dtmc = stormpy.storage.SparseExactDtmc(components)
+            return dtmc
+        else:
+            components = stormpy.storage.SparseModelComponents(tm, mdp.labeling, mdp.reward_models)
+            dtmc = stormpy.storage.SparseDtmc(components)
+            return dtmc
 
     def build_assignment(self, family):
         assert family.size == 1, "expecting family of size 1"
@@ -121,7 +126,10 @@ def discard_unreachable_choices(self, state_to_choice):
         return state_to_choice_reachable
 
     def scheduler_to_state_to_choice(self, submdp, scheduler, discard_unreachable_choices=True):
-        state_to_quotient_choice = payntbind.synthesis.schedulerToStateToGlobalChoice(scheduler, submdp.model, submdp.quotient_choice_map)
+        if submdp.model.is_exact:
+            state_to_quotient_choice = payntbind.synthesis.schedulerToStateToGlobalChoiceExact(scheduler, submdp.model, submdp.quotient_choice_map)
+        else:
+            state_to_quotient_choice = payntbind.synthesis.schedulerToStateToGlobalChoice(scheduler, submdp.model, submdp.quotient_choice_map)
         state_to_choice = self.empty_scheduler()
         for state in range(submdp.model.nr_states):
             quotient_choice = state_to_quotient_choice[state]
@@ -159,7 +167,10 @@ def choice_values(self, mdp, prop, state_values):
         '''
 
         # multiply probability with model checking results
-        choice_values = payntbind.synthesis.multiply_with_vector(mdp.transition_matrix, state_values)
+        if mdp.is_exact:
+            choice_values = payntbind.synthesis.multiply_with_vector_exact(mdp.transition_matrix, state_values)
+        else:
+            choice_values = payntbind.synthesis.multiply_with_vector(mdp.transition_matrix, state_values)
         choice_values = Quotient.make_vector_defined(choice_values)
 
         # if the associated reward model has state-action rewards, then these must be added to choice values

paynt/synthesizer/statistic.py

@@ -74,9 +74,9 @@ def iteration(self, model):
         ''' Identify the type of the model and count corresponding iteration. '''
         if isinstance(model, paynt.models.models.Mdp):
             model = model.model
-        if type(model) == stormpy.storage.SparseDtmc:
+        if type(model) in [stormpy.storage.SparseDtmc, stormpy.storage.SparseExactDtmc]:
             self.iteration_dtmc(model.nr_states)
-        elif type(model) == stormpy.storage.SparseMdp:
+        elif type(model) in [stormpy.storage.SparseMdp, stormpy.storage.SparseExactMdp]:
             self.iteration_mdp(model.nr_states)
         else:
             logger.debug(f"unknown model type {type(model)}")
@@ -150,7 +150,9 @@ def status(self):
             if opt is None:
                 opt = spec.optimality.optimum
             if opt is not None:
-                ret_str += f", opt = {round(opt,4)}"
+                if not isinstance(opt, stormpy.Rational):
+                    opt = round(opt, 4)
+                ret_str += f", opt = {opt}"
         return ret_str
 
 
@@ -202,7 +204,10 @@ def get_summary_iterations(self):
     def get_summary_synthesis(self):
         spec = self.quotient.specification
         if spec.has_optimality and spec.optimality.optimum is not None:
-            optimum = round(spec.optimality.optimum, 6)
+            if isinstance(spec.optimality.optimum, stormpy.Rational):
+                optimum = spec.optimality.optimum
+            else:
+                optimum = round(spec.optimality.optimum, 6)
             return f"optimum: {optimum}"
         else:
             feasible = "yes" if self.synthesized_assignment is not None else "no"