Added computation of random scheduler; prepared PAYNT for DT evaluation

paynt/quotient/mdp.py

@@ -414,6 +414,25 @@ def scheduler_json_to_choices(self, scheduler_json, discard_unreachable_states=F
             scheduler_json_relevant.append(state_decision)
 
         return choices,scheduler_json_relevant
+
+    # gets all choices that represent random action, used to compute the value of uniformly random scheduler
+    def get_random_choices(self):
+        nci = self.quotient_mdp.nondeterministic_choice_indices.copy()
+        state_to_choice = self.empty_scheduler()
+        random_action = self.action_labels.index(MdpQuotient.DONT_CARE_ACTION_LABEL)
+        for state in range(self.quotient_mdp.nr_states):
+            # find a choice that executes this action
+            for choice in range(nci[state],nci[state+1]):
+                if self.choice_to_action[choice] == random_action:
+                    state_to_choice[state] = choice
+                    break
+        for state,choice in enumerate(state_to_choice):
+            if choice is None:
+                state_to_choice[state] = nci[state]
+
+        choices = self.state_to_choice_to_choices(state_to_choice)
+
+        return choices
 
 
     def reset_tree(self, depth, enable_harmonization=True):

paynt/synthesizer/decision_tree.py

@@ -230,6 +230,14 @@ def run(self, optimum_threshold=None):
         opt_result_value = mc_result.value
         logger.info(f"the optimal scheduler has value: {opt_result_value}")
 
+        if self.quotient.DONT_CARE_ACTION_LABEL in self.quotient.action_labels:
+            random_choices = self.quotient.get_random_choices()
+            submdp_random = self.quotient.build_from_choice_mask(random_choices)
+            mc_result_random = submdp_random.model_check_property(self.quotient.get_property())
+            random_result_value = mc_result_random.value
+            logger.info(f"the random scheduler has value: {random_result_value}")
+            # self.set_optimality_threshold(random_result_value)
+
         self.best_assignment = self.best_assignment_value = None
         self.best_tree = self.best_tree_value = None
         if scheduler_choices is not None:
@@ -249,6 +257,8 @@ def run(self, optimum_threshold=None):
                 self.synthesize_tree_sequence(opt_result_value)
 
         logger.info(f"the optimal scheduler has value: {opt_result_value}")
+        if self.quotient.DONT_CARE_ACTION_LABEL in self.quotient.action_labels:
+            logger.info(f"the random scheduler has value: {random_result_value}")
         if self.best_tree is None:
             logger.info("no admissible tree found")
         else:
@@ -259,6 +269,8 @@ def run(self, optimum_threshold=None):
             logger.info(f"synthesized tree of depth {depth} with {num_nodes} decision nodes")
             if self.quotient.specification.has_optimality:
                 logger.info(f"the synthesized tree has value {self.best_tree_value}")
+            if self.quotient.DONT_CARE_ACTION_LABEL in self.quotient.action_labels:
+                logger.info(f"the synthesized tree has relative value: {(self.best_tree_value-random_result_value)/(opt_result_value-random_result_value)}")
             logger.info(f"printing the synthesized tree below:")
             print(self.best_tree.to_string())
             # logger.info(f"printing the PRISM module below:")

paynt/synthesizer/synthesizer_ar.py

@@ -111,7 +111,7 @@ def update_optimum(self, family):
         self.quotient.specification.optimality.update_optimum(iv)
         self.best_assignment = ia
         self.best_assignment_value = iv
-        # logger.info(f"value {round(iv,4)} achieved after {round(paynt.utils.timer.GlobalTimer.read(),2)} seconds")
+        logger.info(f"value {round(iv,4)} achieved after {round(paynt.utils.timer.GlobalTimer.read(),2)} seconds")
         if isinstance(self.quotient, paynt.quotient.pomdp.PomdpQuotient):
             self.stat.new_fsc_found(family.analysis_result.improving_value, ia, self.quotient.policy_size(ia))