Merge pull request #23 from TheGreatfpmK/adaptive-hybrid

Re-introduced adaptive hybrid

paynt/synthesizer/synthesizer_hybrid.py

@@ -1,5 +1,3 @@
-import stormpy.synthesis
-
 from .synthesizer import Synthesizer
 from .synthesizer_ar import SynthesizerAR
 from .synthesizer_cegis import SynthesizerCEGIS
@@ -21,11 +19,17 @@ class StageControl:
     only_ar = False
     # whether 1 AR followed by only CEGIS is performed
     only_cegis = False
+    # whether adaptive hybrid is enabled
+    adaptive_hybrid = True
 
-    def __init__(self):
+    def __init__(self, family_size):
         # timings
         self.timer_ar = Timer()
         self.timer_cegis = Timer()
+
+        self.family_size = family_size
+        self.pruned_ar = 0
+        self.pruned_cegis = 0
 
         # multiplier to derive time allocated for cegis
         # time_ar * factor = time_cegis
@@ -40,6 +44,12 @@ def start_cegis(self):
         self.timer_ar.stop()
         self.timer_cegis.start()
 
+    def prune_ar(self, pruned):
+        self.pruned_ar += pruned / self.family_size
+
+    def prune_cegis(self, pruned):
+        self.pruned_cegis += pruned / self.family_size
+
     def cegis_has_time(self):
         """
         :return True if cegis still has some time
@@ -59,6 +69,19 @@ def cegis_has_time(self):
 
         # stop CEGIS
         self.timer_cegis.stop()
+
+        if StageControl.adaptive_hybrid:
+            if self.pruned_ar == 0 and self.pruned_cegis == 0:
+                self.cegis_efficiency = 1
+            elif self.pruned_ar == 0 and self.pruned_cegis > 0:
+                self.cegis_efficiency = 2
+            elif self.pruned_ar > 0 and self.pruned_cegis == 0:
+                self.cegis_efficiency = 0.5
+            else:
+                success_rate_cegis = self.pruned_cegis / self.timer_cegis.read()
+                success_rate_ar = self.pruned_ar / self.timer_ar.read()
+                self.cegis_efficiency = success_rate_cegis / success_rate_ar
+
         return False
 
 
@@ -76,7 +99,7 @@ def synthesize_assignment(self, family):
         # AR-CEGIS loop
         satisfying_assignment = None
         families = [family]
-        self.stage_control = StageControl()
+        self.stage_control = StageControl(family.size)
         while families:
 
             # initiate AR analysis
@@ -95,13 +118,17 @@ def synthesize_assignment(self, family):
                 satisfying_assignment = family.analysis_result.improving_assignment
             if family.analysis_result.can_improve == False:
                 self.explore(family)
+                self.stage_control.prune_ar(family.size)
                 continue
 
             # undecided: initiate CEGIS analysis
             self.stage_control.start_cegis()
 
             # construct priority subfamily that corresponds to primary scheduler
-            scheduler_selection = family.analysis_result.optimality_result.primary_selection
+            if family.analysis_result.optimality_result is not None:
+                scheduler_selection = family.analysis_result.optimality_result.primary_selection
+            else:
+                scheduler_selection = family.analysis_result.constraints_result.results[0].primary_selection
             priority_subfamily = family.copy()
             priority_subfamily.assume_options(scheduler_selection)
 
@@ -122,6 +149,7 @@ def synthesize_assignment(self, family):
                 conflicts, accepting_assignment = self.analyze_family_assignment_cegis(family, assignment)
                 pruned = smt_solver.exclude_conflicts(family, assignment, conflicts)
                 self.explored += pruned
+                self.stage_control.prune_cegis(pruned)
 
                 if accepting_assignment is not None:
                     satisfying_assignment = accepting_assignment
@@ -137,4 +165,3 @@ def synthesize_assignment(self, family):
             families = families + subfamilies
 
         return satisfying_assignment
-