Fixing SAYNT

paynt/cli.py

@@ -17,7 +17,6 @@
 
 from .quotient.storm_pomdp_control import StormPOMDPControl
 
-
 import click
 import sys
 import os
@@ -114,9 +113,6 @@ def setup_logger(log_path = None):
 @click.option("--export-fsc-paynt", type=click.Path(), default=None,
     help="path to output file for SAYNT inductive FSC")
 
-#@click.option("--storm-parallel", is_flag=True, default=False,
-#    help="run storm analysis in parallel (can only be used together with --storm-pomdp-analysis flag)")
-
 @click.option(
     "--ce-generator",
     default="storm",

paynt/quotient/models.py

@@ -270,5 +270,5 @@ def check_specification(self, specification, constraint_indices = None, short_ev
         constraints_result, optimality_result = super().check_specification(specification,constraint_indices,short_evaluation)
         if optimality_result is not None and optimality_result.improving_assignment is not None and double_check:
             optimality_result.improving_assignment, optimality_result.improving_value = self.quotient_container.double_check_assignment(optimality_result.improving_assignment)
-            print(optimality_result.improving_assignment, optimality_result.improving_value)
+            # print(optimality_result.improving_assignment, optimality_result.improving_value)
         return MdpSpecificationResult(constraints_result, optimality_result)

paynt/quotient/quotient_pomdp.py

@@ -88,7 +88,7 @@ def __init__(self, pomdp, specification, decpomdp_manager=None):
                     agent_obs = decpomdp_manager.joint_observations[obs][0]
                     agent_obs_label = decpomdp_manager.agent_observation_labels[0][agent_obs]
                     self.observation_labels.append(agent_obs_label)
-        logger.debug(f"Observation labels: {self.observation_labels}")
+        # logger.debug(f"Observation labels: {self.observation_labels}")
 
         # compute actions available at each observation
         self.actions_at_observation = [0] * self.observations
@@ -712,25 +712,21 @@ def policy_size(self, assignment):
         return size_gamma + size_delta
 
 
-    # constructs pomdp from the quotient MDP
+    # constructs pomdp from the quotient MDP, used for computing POMDP abstraction bounds
     def get_family_pomdp(self, mdp):
         no_obs = self.pomdp.nr_observations
-        #print(mdp.model)
         tm = mdp.model.transition_matrix
         components = stormpy.storage.SparseModelComponents(tm, mdp.model.labeling, mdp.model.reward_models)
 
         full_observ_list = []
-        #full_choice_labels = []
         for state in range(self.pomdp.nr_states):
             obs = self.pomdp.get_observation(state)
             for mem in range(self.observation_memory_size[obs]):
                 full_observ_list.append(obs + mem * no_obs)
-                #full_choice_labels.append(list(range(self.pomdp.get_nr_available_actions(state))))
-
-        #print(full_choice_labels)
 
         choice_labeling = stormpy.storage.ChoiceLabeling(mdp.choices)
 
+        # assign observations to states
         observ_list = []
         choice_labels = []
         for state in range(mdp.model.nr_states):
@@ -739,12 +735,11 @@ def get_family_pomdp(self, mdp):
             actions = [action for action in range(mdp.model.get_nr_available_actions(state))]
             choice_labels.append(actions)
 
-        # LABELING
+        # construct labeling
         labels_list = [item for sublists in choice_labels for item in sublists]
         labels = list(set(labels_list))
         for label in labels:
             choice_labeling.add_label(str(label))
-
         for choice in range(mdp.choices):
             choice_labeling.add_label_to_choice(str(labels_list[choice]), choice)
 
@@ -754,7 +749,4 @@ def get_family_pomdp(self, mdp):
         pomdp = stormpy.storage.SparsePomdp(components)
         pomdp = stormpy.pomdp.make_canonic(pomdp)
 
-        #stormpy.export_to_drn(pomdp, "pomdp-test.out")
-        #print(pomdp)
-
         return pomdp