change policy tree output format

paynt/quotient/mdp_family.py

@@ -1,11 +1,9 @@
-import stormpy
 import payntbind
 
 import paynt.family.family
 import paynt.quotient.quotient
 import paynt.models.models
 
-import collections
 import json
 
 import logging
@@ -110,17 +108,24 @@ def policy_to_state_valuation_actions(self, policy):
         ]
         return state_valuation_to_action
 
-    def policy_to_json(self, state_valuation_to_action, indent=""):
-        import json
-        json_string = "[\n"
-        for index,valuation_action in enumerate(state_valuation_to_action):
-            valuation,action = valuation_action
-            if index > 0:
-                json_string += ",\n"
-            json_string += indent + json.dumps(valuation_action)
-        json_string += "\n" + indent + "]"
-        return json_string
+    def policy_to_json(self, state_valuation_to_action, dt_control=True):
+        '''
+        :param state_valuation_to_action: a list of tuples (valuation,action) where valuation is a dictionary of variable
+        :param dt_control: if True, outputs JSON in the format expected by the DT control tool,
+                otherwise simpler format is used
+        '''
+        json_whole = []
+        for index, valuation_action in enumerate(state_valuation_to_action):
+            if dt_control:
+                json_unit = {}
+                valuation, action = valuation_action
+                json_unit["c"] = [{"origin": {"action-label": action}}]
+                json_unit["s"] = valuation
+                json_whole.append(json_unit)
+            else:
+                json_whole.append(valuation_action)
 
+        return json_whole
 
 
     def fix_and_apply_policy_to_family(self, family, policy):

paynt/synthesizer/policy_tree.py

@@ -792,21 +792,18 @@ def evaluate_all(self, family, prop, keep_value_only=False):
 
 
     def run(self, optimum_threshold=None):
-        return self.evaluate(export_filename_base=paynt.synthesizer.synthesizer.Synthesizer.export_synthesis_filename_base)
+        return self.evaluate()
 
 
     def export_evaluation_result(self, evaluations, export_filename_base):
         import json
         policies = self.policy_tree.extract_policies(self.quotient)
-        policies_string = "{\n"
+        policies_json = {}
         for index,key_value in enumerate(policies.items()):
             policy_id,policy = key_value
-            if index > 0:
-                policies_string += ",\n"
-            policy_json = self.quotient.policy_to_json(policy, indent= "  ")
-
-            policies_string += f'"{policy_id}" : {policy_json}'
-        policies_string += "}\n"
+            policy_json = self.quotient.policy_to_json(policy)
+            policies_json[policy_id] = policy_json
+        policies_string = json.dumps(policies_json, indent=4)
 
         policies_filename = export_filename_base + ".json"
         with open(policies_filename, 'w') as file:

paynt/synthesizer/synthesizer.py

@@ -119,7 +119,7 @@ def export_evaluation_result(self, evaluations, export_filename_base):
         ''' to be overridden '''
         pass
 
-    def evaluate(self, family=None, prop=None, keep_value_only=False, print_stats=True, export_filename_base=None):
+    def evaluate(self, family=None, prop=None, keep_value_only=False, print_stats=True):
         '''
         Evaluate each member of the family wrt the given property.
         :param family if None, then the design space of the quotient will be used
@@ -143,8 +143,8 @@ def evaluate(self, family=None, prop=None, keep_value_only=False, print_stats=Tr
         self.stat.finished_evaluation(evaluations)
         logger.info("evaluation finished")
 
-        if export_filename_base is not None:
-            self.export_evaluation_result(evaluations, export_filename_base)
+        if self.export_synthesis_filename_base is not None:
+            self.export_evaluation_result(evaluations, self.export_synthesis_filename_base)
 
         if print_stats:
             self.stat.print()