diff --git a/models/archive/cav23-saynt/lrv/sketch.props b/models/archive/cav23-saynt/lrv/sketch.props
new file mode 100755
index 000000000..94d15c4de
--- /dev/null
+++ b/models/archive/cav23-saynt/lrv/sketch.props
@@ -0,0 +1 @@
+R{"cost"}min=? [F "goal"];
\ No newline at end of file
diff --git a/models/archive/cav23-saynt/lrv/sketch.templ b/models/archive/cav23-saynt/lrv/sketch.templ
new file mode 100755
index 000000000..2d0f1ee2a
--- /dev/null
+++ b/models/archive/cav23-saynt/lrv/sketch.templ
@@ -0,0 +1,97 @@
+pomdp
+
+observables
+started, x, y, m1taken, m1lastobs, m2taken, m2lastobs, m3taken, m3lastobs, finish
+endobservables
+
+const int N = 8;
+const int xMx = N;
+const int yMx = N;
+const int xMIN = 0;
+const int yMIN = 0;
+const double slippery = 0.0;
+
+const m1x = N/2;
+const m1y = N/2;
+
+const m2x = 1;
+const m2y = 1;
+
+const m3x = 1;
+const m3y = N;
+
+
+const double goodmineral = 0.6;
+
+formula done = x = xMx & y = yMx;
+
+formula maxdist = xMx-xMIN+yMx-yMIN;
+
+formula m1dist = max(m1x-x,x-m1x) + max(m1y-y,y-m1y);
+formula m2dist = max(m2x-x,x-m2x) + max(m2y-y,y-m2y);
+formula m3dist = max(m3x-x,x-m3x) + max(m3y-y,y-m3y);
+
+formula normdistrm1 = 1+(m1dist/maxdist);
+formula normdistrm2 = 1+(m2dist/maxdist);
+formula normdistrm3 = 1+(m3dist/maxdist);
+
+
+module master
+    started : bool init false;
+    finish : bool init false;
+
+    [placement] !started -> (started'=true);
+    [north] started & !done -> true;
+    [south] started  & !done -> true;
+    [east] started  & !done-> true;
+    [west] started & !done -> true;
+    [finish] done & !finish -> 1:(finish'=true);
+endmodule
+
+module mineral1
+    m1qual : bool init false;
+    m1taken : bool init false;
+    m1lastobs : bool init false;
+    [placement] true -> goodmineral : (m1qual'=true) + (1-goodmineral) : (m1qual'=false);
+
+    [m1collect] started & (x = m1x & y = m1y & !m1taken) -> 1:(m1taken'=true);
+    [m1sense] started & !m1taken -> (1/normdistrm1): (m1lastobs'=m1qual) +  (1-(1/normdistrm1)): (m1lastobs'=!m1qual);
+    [north] true -> (m1lastobs'=false);
+    [south] true -> (m1lastobs'=false);
+    [east] true -> (m1lastobs'=false);
+    [west] true -> (m1lastobs'=false);
+endmodule
+
+module mineral2 = mineral1[m1collect=m2collect, m1sense=m2sense, m1x = m2x, m1y = m2y, m1qual=m2qual,m1taken=m2taken,m1lastobs=m2lastobs,normdistrm1=normdistrm2] endmodule
+module mineral3 = mineral1[m1collect=m3collect, m1sense=m3sense, m1x = m3x, m1y = m3y, m1qual=m3qual,m1taken=m3taken,m1lastobs=m3lastobs,normdistrm1=normdistrm3] endmodule
+
+module lrv
+    x : [xMIN..xMx] init 0;
+    y : [yMIN..yMx] init 0;
+
+    [west] true -> (1-slippery): (x'=max(x-1,xMIN)) + slippery: (x'=max(x,xMIN));
+    [east] true -> (1-slippery): (x'=min(x+1,xMx)) + slippery: (x'=min(x,xMx));
+    [south]  true -> (1-slippery): (y'=min(y+1,yMx)) + slippery: (y'=min(y,yMx));
+    [north]  true -> (1-slippery): (y'=max(y-1,yMIN)) + slippery: (y'=max(y,yMIN));
+endmodule
+
+rewards "cost"
+    [m1sense] true : 1;
+    [m2sense] true : 1;
+    [m3sense] true : 1;
+
+    [m1collect] true : 2;
+    [m2collect] true : 2;
+    [m3collect] true : 2;
+
+    [north] true : 1;
+    [south] true : 1;
+    [west] true : 1;
+    [east] true : 1;
+    [finish] true : (m1taken & !m1qual ? 4 : 0) + (m2taken & !m2qual ? 4 : 0) +
+                    (m3taken & !m3qual ? 4 : 0) +
+                    ((m1taken & m2taken & m1qual & m2qual) | (m1taken & m3taken & m1qual & m3qual) |
+                    (m2taken & m3taken & m2qual & m3qual) ? 0 : 18);
+endrewards
+
+label "goal" = finish;
\ No newline at end of file
diff --git a/models/pomdp/grid/evade/sketch.props b/models/pomdp/grid/evade/sketch.props
index 7c7dc5af2..c36288bae 100755
--- a/models/pomdp/grid/evade/sketch.props
+++ b/models/pomdp/grid/evade/sketch.props
@@ -1,2 +1,2 @@
-//Pmax=?["notbad" U "goal"];
-R{"steps"}min=? ["notbad" U "goal"]
\ No newline at end of file
+Pmax=?["notbad" U "goal"];
+//R{"steps"}min=? ["notbad" U "goal"]
\ No newline at end of file
diff --git a/models/pomdp/other/cheese/sketch.props b/models/pomdp/other/cheese/sketch.props
index 4ea216c91..5c97650cf 100644
--- a/models/pomdp/other/cheese/sketch.props
+++ b/models/pomdp/other/cheese/sketch.props
@@ -1,2 +1,2 @@
-//P<0.5 [F "bad"]
-R{"rew0"}max=? [F "goal"]
\ No newline at end of file
+P<0.5 [F "bad"]
+//R{"rew0"}max=? [F "goal"]
\ No newline at end of file
diff --git a/paynt/cli.py b/paynt/cli.py
index 64fab21a6..fe665147b 100644
--- a/paynt/cli.py
+++ b/paynt/cli.py
@@ -1,3 +1,4 @@
+import paynt.synthesizer.synthesizer_ar
 from . import version
 
 import paynt.parser.sketch
@@ -129,6 +130,17 @@ def setup_logger(log_path = None):
     "--constraint-bound", type=click.FLOAT, help="bound for creating constrained POMDP for cassandra models",
 )
 
+#------------xshevc01---------------- 
+@click.option("--use-inheritance", is_flag=True, default=False,
+    help="# if set, inheritance dependencies (IDAR) will be used for the synthesis of FSCs")
+@click.option("--use-inheritance-extended", is_flag=True, default=False,
+    help="# if set, extended inheritance dependencies (EIDAR) will be used for the synthesis of FSCs")
+@click.option("--use-smart-inheritance", is_flag=True, default=False,
+    help="# if set, combines classic AR with EIDAR (SEIDAR) for more efficient synthesis of FSCs")
+@click.option("--iterations", default=0, show_default=True,
+    help=" experimental purposes: implicit number of iterations for the synthesis of FSCs")
+#------------------------------------
+
 @click.option(
     "--ce-generator", type=click.Choice(["dtmc", "mdp"]), default="dtmc", show_default=True,
     help="counterexample generator",
@@ -148,13 +160,19 @@ def paynt_run(
     all_in_one,
     mdp_split_wrt_mdp, mdp_discard_unreachable_choices, mdp_use_randomized_abstraction,
     constraint_bound,
+    #------------xshevc01---------------- 
+    use_inheritance,
+    use_inheritance_extended,
+    use_smart_inheritance,
+    iterations,
+    #------------------------------------
     ce_generator,
     profiling
 ):
     profiler = None
     if profiling:
         profiler = cProfile.Profile()
-        profiler.enable()
+        # profiler.enable()
 
     logger.info("This is Paynt version {}.".format(version()))
 
@@ -169,6 +187,14 @@ def paynt_run(
     paynt.synthesizer.policy_tree.SynthesizerPolicyTree.discard_unreachable_choices = mdp_discard_unreachable_choices
     paynt.synthesizer.policy_tree.SynthesizerPolicyTree.use_randomized_abstraction = mdp_use_randomized_abstraction
 
+    #------------xshevc01---------------- 
+    paynt.quotient.quotient.Quotient.use_inheritance = use_inheritance
+    paynt.quotient.quotient.Quotient.use_inheritance_extended = use_inheritance_extended
+    paynt.quotient.quotient.Quotient.use_smart_inheritance = use_smart_inheritance
+    paynt.synthesizer.synthesizer_ar.SynthesizerAR.iterations = iterations
+    #------------------------------------
+
+    
     storm_control = None
     if storm_pomdp:
         storm_control = paynt.quotient.storm_pomdp_control.StormPOMDPControl()
@@ -182,7 +208,10 @@ def paynt_run(
     if all_in_one is None:
         quotient = paynt.parser.sketch.Sketch.load_sketch(sketch_path, properties_path, export, relative_error, precision, constraint_bound)
         synthesizer = paynt.synthesizer.synthesizer.Synthesizer.choose_synthesizer(quotient, method, fsc_synthesis, storm_control)
+        if profiling:
+            profiler.enable()
         synthesizer.run(optimum_threshold, export_evaluation)
+
     else:
         all_in_one_program, specification, family = paynt.parser.sketch.Sketch.load_sketch_as_all_in_one(sketch_path, properties_path)
         all_in_one_analysis = paynt.synthesizer.all_in_one.AllInOne(all_in_one_program, specification, all_in_one, family)
diff --git a/paynt/family/family.py b/paynt/family/family.py
index 6e6978e04..aa88416ec 100644
--- a/paynt/family/family.py
+++ b/paynt/family/family.py
@@ -143,6 +143,11 @@ def __init__(self):
         # index of a hole used to split the family
         self.splitter = None
 
+        # explicit list of all non-default actions in the MDP
+        self.selected_choices = None
+        # for each hole and for each option explicit list of all non-default actions in the MDP
+        self.hole_selected_choices = None
+
 
 class DesignSpace(Family):
     '''
@@ -159,6 +164,9 @@ def __init__(self, family = None, parent_info = None):
         super().__init__(family)
 
         self.mdp = None
+
+        self.hole_selected_choices = None
+        self.selected_choices = None
         
         # SMT encoding
         self.encoding = None
@@ -179,11 +187,14 @@ def copy(self):
     
     def collect_parent_info(self, specification):
         pi = ParentInfo()
+        pi.hole_selected_choices = self.hole_selected_choices
+        pi.selected_choices = self.selected_choices
         pi.refinement_depth = self.refinement_depth
         cr = self.analysis_result.constraints_result
         pi.constraint_indices = cr.undecided_constraints if cr is not None else []
         pi.splitter = self.splitter
         pi.mdp = self.mdp
+        pi.analysis_result = self.analysis_result
         return pi
 
     def encode(self, smt_solver):
diff --git a/paynt/quotient/pomdp.py b/paynt/quotient/pomdp.py
index f0f9a29ae..e04fa78bf 100644
--- a/paynt/quotient/pomdp.py
+++ b/paynt/quotient/pomdp.py
@@ -369,6 +369,7 @@ def estimate_scheduler_difference(self, mdp, quotient_choice_map, inconsistent_a
         # create inverse quotient-choice-to-mdp-choice map
         # TODO optimize this for multiple properties
         quotient_to_restricted_action_map = [None] * self.quotient_mdp.nr_choices
+        # print(self.quotient_mdp.nr_choices)
         for choice in range(mdp.nr_choices):
             quotient_to_restricted_action_map[quotient_choice_map[choice]] = choice
 
@@ -404,8 +405,13 @@ def estimate_scheduler_difference(self, mdp, quotient_choice_map, inconsistent_a
 
                     assert len(self.hole_option_to_actions[hole_index][option]) > choice_index
                     choice_global = self.hole_option_to_actions[hole_index][option][choice_index]
-                    choice = quotient_to_restricted_action_map[choice_global]
+                    choice = quotient_to_restricted_action_map[choice_global]                    
+                    if choice is None:
+                        continue
+
                     choice_value = choice_values[choice]
+                    # print(choice_value)
+                    # print()
                     state_values.append(choice_value)
 
                 min_value = min(state_values)
diff --git a/paynt/quotient/quotient.py b/paynt/quotient/quotient.py
index 73f461dc3..a2b9ba037 100644
--- a/paynt/quotient/quotient.py
+++ b/paynt/quotient/quotient.py
@@ -15,6 +15,12 @@ class Quotient:
 
     # if True, expected visits will not be computed for hole scoring
     disable_expected_visits = False
+    #------------xshevc01----------------
+    use_inheritance = False
+    use_inheritance_extended = False
+    use_smart_inheritance = False
+    #------------------------------------
+    
 
     @staticmethod
     def make_vector_defined(vector):
@@ -77,13 +83,176 @@ def build_from_choice_mask(self, choices):
         mdp,state_map,choice_map = self.restrict_quotient(choices)
         return paynt.quotient.models.SubMdp(mdp, state_map, choice_map)
     
+
+    #------------xshevc01----------------    
+    def find_all_predecessors(self):
+        """ Find all predecessors for each state in the quotient MDP """
+        self.predecessors_list = payntbind.synthesis.findAllPredecessors(self.quotient_mdp)
+
+
+    def idar_get_parents_scheduler(self, family, compatible_choices):
+        """ Use parent's scheduler to find the affected states """
+
+        parent_mdp = family.parent_info.mdp
+        parent_result = family.parent_info.analysis_result.optimality_result.primary.result
+        scheduler = parent_result.scheduler
+        return self.idar_get_parent_scheduler_choices(parent_mdp, scheduler, compatible_choices)
+    
+    
+    def idar_get_parent_scheduler_choices(self, parent_mdp, scheduler, compatible_choices):
+        """ Get parent's optimal choices and if they are not
+            compatible with the family, mark the corresponding states as affected """
+
+        state_to_quotient_choice = payntbind.synthesis.schedulerToStateToGlobalChoice(scheduler, parent_mdp.model, parent_mdp.quotient_choice_map)
+        parent_state_choice = [-1] * self.quotient_mdp.nr_states
+        states_affected = [False for state in range(self.quotient_mdp.nr_states)]
+        for state in range(parent_mdp.model.nr_states):
+            qchoice = state_to_quotient_choice[state]
+            qstate = parent_mdp.quotient_state_map[state]
+            parent_state_choice[qstate] = qchoice
+            if not compatible_choices.get(qchoice):
+                states_affected[qstate] = True
+        return parent_state_choice, states_affected
+    
+
+    def find_reachable_affected_states(self, states_affected, parent_state_choice):
+        """ Mark all predecessors of affected states as affected """
+
+        state_queue = [s for s in range(self.quotient_mdp.nr_states) if states_affected[s]]
+        while state_queue:
+            state = state_queue.pop()
+            for pred in self.predecessors_list[state]:
+                qchoice = parent_state_choice[pred]
+                if not states_affected[pred] and qchoice != -1:
+                    state_queue.append(pred)
+                    states_affected[pred] = True
+
+    
+    def convert_to_bitvector(self, states_affected):
+        """ Converts a list of affected states to a bit vector"""
+
+        states_affected_bit_vector = stormpy.BitVector(self.quotient_mdp.nr_states,False)
+        for state in range(self.quotient_mdp.nr_states):
+            if states_affected[state]:
+                states_affected_bit_vector.set(state, True)
+        return states_affected_bit_vector
+
+    
+    def affected_states_to_mask(self, family, states_affected_bit_vector, parent_state_choice, compatible_choices):
+        """ Compute the result choices for the family """
+        
+        parent_mdp = family.parent_info.mdp
+        return payntbind.synthesis.affectedStatesToMask(parent_mdp.quotient_choice_map, parent_mdp.quotient_state_map, parent_mdp.model, states_affected_bit_vector, parent_state_choice, compatible_choices)
+    
+
+    def idar_build_inheritance(self, family, compatible_choices):
+        """ Construct the quotient MDP for the family using inheritance dependencies (IDAR) """
+
+        if family.parent_info is None:
+            self.perc_affected_sum = 0
+            self.perc_affected_entries = 0
+            self.choices_per_affected_sum = 0
+            return compatible_choices
+        parent_state_choice, states_affected = self.idar_get_parents_scheduler(family, compatible_choices)
+        self.find_reachable_affected_states(states_affected, parent_state_choice)
+        states_affected_bit_vector = self.convert_to_bitvector(states_affected)
+        result_choices = self.affected_states_to_mask(family, states_affected_bit_vector, parent_state_choice, compatible_choices)
+        self.count_affected_states(states_affected_bit_vector, family, result_choices)
+        return result_choices
+
+
+    def map_choices_to_states(self):
+        """ Map choices to states in the quotient MDP (EIDAR) """
+
+        self.choices_to_states = payntbind.synthesis.mapChoicesToStates(self.quotient_mdp)
+
+
+    def eidar_get_parents_scheduler(self, family):
+        """ Use parent's scheduler to find the affected choices (EIDAR) """
+
+        parent_mdp = family.parent_info.mdp
+        parent_result = family.parent_info.analysis_result.optimality_result.primary.result
+        scheduler = parent_result.scheduler
+        return self.eidar_get_parent_scheduler_choices(parent_mdp, scheduler)
+    
+
+    def eidar_get_parent_scheduler_choices(self, parent_mdp, scheduler):
+        """ Get parent's optimal choices and if they are not
+            compatible with the family, mark the corresponding choices as affected (EIDAR) """
+
+        state_to_quotient_choice = payntbind.synthesis.schedulerToStateToGlobalChoice(scheduler, parent_mdp.model, parent_mdp.quotient_choice_map)
+        parent_state_choice = [-1] * self.quotient_mdp.nr_states
+        optimal_choices = stormpy.BitVector(self.quotient_mdp.nr_choices, False)
+        for state in range(parent_mdp.model.nr_states):
+            qchoice = state_to_quotient_choice[state]
+            optimal_choices.set(qchoice, True)
+            qstate = parent_mdp.quotient_state_map[state]
+            parent_state_choice[qstate] = qchoice
+        return parent_state_choice, optimal_choices
+
+
+    def find_optimal_leading_choices(self, parent_state_choice):
+        """ Find the optimal leading choices (EIDAR) """
+
+        return payntbind.synthesis.findOptimalLeadingChoices(self.quotient_mdp, parent_state_choice)
+    
+
+    def optimal_choices_to_affected_states(self, optimal_choices, compatible_choices, leading_optimals_to_state):
+        """ Compute the affected states from the optimal choices (EIDAR) """
+
+        return payntbind.synthesis.optimalChoicesToAffectedStates(self.quotient_mdp, self.choices_to_states, optimal_choices, compatible_choices, leading_optimals_to_state)
+
+
+    def eidar_build_inheritance(self, family, compatible_choices):
+        """ Construct the quotient MDP for the family using extended inheritance dependencies (EIDAR)"""
+
+        if family.parent_info is None:
+            self.perc_affected_sum = 0
+            self.perc_affected_entries = 0
+            self.choices_per_affected_sum = 0
+            return compatible_choices
+        parent_state_choice, optimal_choices = self.eidar_get_parents_scheduler(family)
+        leading_optimals_to_state = self.find_optimal_leading_choices(parent_state_choice)
+        affected_states = self.optimal_choices_to_affected_states(optimal_choices, compatible_choices, leading_optimals_to_state)
+        result_choices = self.affected_states_to_mask(family, affected_states, parent_state_choice, compatible_choices)
+        self.count_affected_states(affected_states, family, result_choices)
+        return result_choices
+    
+
+    def count_affected_states(self, states_affected_bit_vector, family, choices):
+        """ Count statistics """
+
+        num_affected = states_affected_bit_vector.number_of_set_bits()
+        perc_affected = round(num_affected / family.parent_info.mdp.model.nr_states  * 100)
+        choices_per_affected = (choices.number_of_set_bits() - family.parent_info.mdp.model.nr_states + num_affected) / num_affected
+        self.perc_affected_sum += perc_affected
+        self.perc_affected_entries += 1
+        self.choices_per_affected_sum += choices_per_affected
+    
+
     def build(self, family):
         ''' Construct the quotient MDP for the family. '''
-        # select actions compatible with the family and restrict the quotient
-        choices = self.coloring.selectCompatibleChoices(family.family)
-        family.mdp = self.build_from_choice_mask(choices)
-        family.selected_choices = choices
+
+        compatible_choices = self.coloring.selectCompatibleChoices(family.family)
+
+        if self.use_inheritance:
+            result_choices = self.idar_build_inheritance(family, compatible_choices)
+        elif self.use_inheritance_extended or self.use_smart_inheritance:
+            result_choices = self.eidar_build_inheritance(family, compatible_choices)
+        else:
+            result_choices = compatible_choices
+
+        family.selected_choices = result_choices
+        family.mdp = self.build_from_choice_mask(result_choices)
+        if self.use_inheritance and family.parent_info is None:
+            self.find_all_predecessors()
+        if (self.use_inheritance_extended or self.use_smart_inheritance) and family.parent_info is None:
+            self.map_choices_to_states()
+        if self.use_smart_inheritance and family.parent_info is None and math.log10(family.size) <= 15:
+            self.use_smart_inheritance = False
+            print("SWITCHING TO AR DUE TO THE SIZE OF THE FAMILY")
         family.mdp.design_space = family
+    #------------------------------------
 
 
     def build_with_second_coloring(self, family, main_coloring, main_family):
@@ -371,6 +540,7 @@ def split(self, family, incomplete_search):
             design_subspace.hole_set_options(splitter, suboption)
             design_subspaces.append(design_subspace)
 
+        # print(splitter, suboptions)
         return design_subspaces
 
 
diff --git a/paynt/synthesizer/statistic.py b/paynt/synthesizer/statistic.py
index 89090e5b9..fe3c5fe64 100644
--- a/paynt/synthesizer/statistic.py
+++ b/paynt/synthesizer/statistic.py
@@ -30,6 +30,9 @@ class Statistic:
     synthesis_timer_total = paynt.utils.profiler.Timer()
     
     def __init__(self, synthesizer):
+        #------------xshevc01---------------- 
+        self.stop = False
+        #------------------------------------
         
         self.synthesizer = synthesizer
         self.quotient = self.synthesizer.quotient
@@ -86,7 +89,15 @@ def iteration_dtmc(self, size_dtmc):
         self.acc_size_dtmc += size_dtmc
         self.print_status()
 
-    def iteration_mdp(self, size_mdp):
+    def iteration_mdp(self, size_mdp, use_smart_inheritance):
+        #------------xshevc01---------------- 
+        if use_smart_inheritance and not self.stop:
+            discarded = self.quotient.discarded
+            fraction_explored = (self.synthesizer.explored + discarded) / self.family_size
+            percentage_explored = int(fraction_explored * 100000) / 1000.0
+            if percentage_explored > 20:
+                self.stop = True
+        #------------------------------------
         if self.iterations_mdp is None:
             self.iterations_mdp = 0
         self.iterations_mdp += 1
@@ -210,7 +221,13 @@ def get_summary_evaluation(self):
         members_total = self.quotient.design_space.size
         members_sat_percentage = int(round(members_sat/members_total*100,0))
         return f"satisfied {members_sat}/{members_total} members ({members_sat_percentage}%)"
-
+    
+    #------------xshevc01---------------- 
+    def get_summary_affected(self):
+        if not self.quotient.use_inheritance and not self.quotient.use_inheritance_extended and not self.quotient.use_smart_inheritance or self.quotient.perc_affected_entries == 0:
+            return ""
+        return f"\n\naffected states average: {self.quotient.perc_affected_sum/self.quotient.perc_affected_entries:.2f} %\nchoices per affected state average: {self.quotient.choices_per_affected_sum/self.quotient.perc_affected_entries:.2f}"
+    #------------------------------------
     
     def get_summary(self):
         specification = self.get_summary_specification()
@@ -220,8 +237,10 @@ def get_summary(self):
 
         quotient_states = self.quotient.quotient_mdp.nr_states
         quotient_actions = self.quotient.quotient_mdp.nr_choices
-        design_space = f"number of holes: {self.quotient.design_space.num_holes}, family size: {self.quotient.design_space.size_or_order}, quotient: {quotient_states} states / {quotient_actions} actions"
+        # design_space = f"number of holes: {self.quotient.design_space.num_holes}, family size: {self.quotient.design_space.size}, quotient: {quotient_states} states / {quotient_actions} actions"
+        design_space = f"number of holes: {self.quotient.design_space.num_holes}, quotient: {quotient_states} states / {quotient_actions} actions"
         timing = f"method: {self.synthesizer.method_name}, synthesis time: {round(self.synthesis_timer.time, 2)} s"
+        affected = self.get_summary_affected()
 
         iterations = self.get_summary_iterations()
         
@@ -234,7 +253,7 @@ def get_summary(self):
         summary = f"{sep}"\
                 f"Synthesis summary:\n" \
                 f"{specification}\n{timing}\n{design_space}\n{explored}\n" \
-                f"{iterations}\n{result}\n"\
+                f"{iterations}\n{result}{affected}\n"\
                 f"{sep}"
         return summary
     
diff --git a/paynt/synthesizer/synthesizer.py b/paynt/synthesizer/synthesizer.py
index 88ad12db4..6da7778e0 100644
--- a/paynt/synthesizer/synthesizer.py
+++ b/paynt/synthesizer/synthesizer.py
@@ -130,7 +130,7 @@ def synthesize(self, family=None, optimum_threshold=None, keep_optimum=False, re
             self.quotient.specification.optimality.update_optimum(optimum_threshold)
             logger.debug(f"optimality threshold set to {optimum_threshold}")
         
-        logger.info("synthesis initiated, design space: {}".format(family.size_or_order))
+        # logger.info("synthesis initiated, design space: {}".format(family.size_or_order))
         self.quotient.discarded = 0
         self.stat.start(family)
         assignment = self.synthesize_one(family)
diff --git a/paynt/synthesizer/synthesizer_ar.py b/paynt/synthesizer/synthesizer_ar.py
index 79790ac04..5897c70db 100644
--- a/paynt/synthesizer/synthesizer_ar.py
+++ b/paynt/synthesizer/synthesizer_ar.py
@@ -7,13 +7,17 @@
 
 class SynthesizerAR(paynt.synthesizer.synthesizer.Synthesizer):
 
+    #------------xshevc01----------------  
+    iterations = 0
+    #------------------------------------
+
     @property
     def method_name(self):
         return "AR"
     
     def verify_family(self, family):
         self.quotient.build(family)
-        self.stat.iteration_mdp(family.mdp.states)
+        self.stat.iteration_mdp(family.mdp.states, self.quotient.use_smart_inheritance)
         res = self.quotient.check_specification_for_mdp(family.mdp, family.constraint_indices)
         if res.improving_assignment == "any":
             res.improving_assignment = family
@@ -39,7 +43,24 @@ def synthesize_one(self, family):
         satisfying_assignment = None
         families = [family]
 
+        iteration_count = 0
+
         while families:
+            #------------xshevc01----------------
+            iteration_count += 1
+            if self.iterations != 0 and iteration_count > self.iterations:
+                 break
+            
+            if self.quotient.use_smart_inheritance and (self.iterations != 0 and iteration_count > self.iterations / 5.0 or iteration_count > 100 or self.stat.stop):
+                    self.quotient.use_smart_inheritance = False
+                    affected_states_average = self.quotient.perc_affected_sum/self.quotient.perc_affected_entries
+                    choices_per_affected_state = self.quotient.choices_per_affected_sum/self.quotient.perc_affected_entries
+                    if affected_states_average > 85 or choices_per_affected_state < 5.5:
+                        print("SWITCHING TO AR DUE TO AFFECTED STATES")
+                    else:
+                        self.quotient.use_inheritance_extended = True
+                        print("SWITCHING TO EIDAR")
+            #------------------------------------
 
             family = families.pop(-1)
 
diff --git a/payntbind/src/synthesis/quotient/bindings.cpp b/payntbind/src/synthesis/quotient/bindings.cpp
index 79f73100f..5b857823b 100644
--- a/payntbind/src/synthesis/quotient/bindings.cpp
+++ b/payntbind/src/synthesis/quotient/bindings.cpp
@@ -11,6 +11,8 @@
 
 #include <storm/storage/Scheduler.h>
 
+#include <queue>
+
 namespace synthesis {
 
 template<typename ValueType>
@@ -210,6 +212,174 @@ storm::storage::BitVector policyToChoicesForFamily(
 }
 
 
+//----------------xshevc01----------------
+/**
+ * Finds all predecessors of each state
+ * 
+ * @param quotient_mdp The quotient MDP
+ * 
+ * @return The predecessors of each state
+*/
+template<typename ValueType>
+std::vector<std::set<uint64_t>> findAllPredecessors(
+    storm::models::sparse::Mdp<ValueType> const& quotient_mdp
+){
+    auto num_states = quotient_mdp.getNumberOfStates();
+    auto const& row_groups = quotient_mdp.getNondeterministicChoiceIndices();
+    std::vector<std::set<uint64_t>> predecessors(num_states);
+    for(uint64_t state=0; state<num_states; ++state) {
+        for(uint64_t choice=row_groups[state]; choice<row_groups[state+1]; ++choice) {
+            for(auto const& entry: quotient_mdp.getTransitionMatrix().getRow(choice)) {
+                uint64_t entry_state = entry.getColumn();
+                predecessors[entry_state].insert(state);
+            }
+        }
+    }
+    return predecessors;
+}
+
+/**
+ * Maps choices to corresponding states
+ * 
+ * @param quotient_mdp The quotient MDP
+ * 
+ * @return Mapping from choices to states
+*/
+template<typename ValueType>
+std::vector<uint64_t> mapChoicesToStates(
+    storm::models::sparse::Mdp<ValueType> const& quotient_mdp
+){
+    auto num_states = quotient_mdp.getNumberOfStates();
+    auto num_choices = quotient_mdp.getNumberOfChoices();
+    auto const& row_groups = quotient_mdp.getNondeterministicChoiceIndices();
+    std::vector<uint64_t> choices_to_states(num_choices);
+    std::vector<std::set<uint64_t>> leading_choices(num_states);
+    for(uint64_t state=0; state<num_states; ++state) {
+        for(uint64_t choice=row_groups[state]; choice<row_groups[state+1]; ++choice) {
+            choices_to_states[choice] = state;
+        }
+    }
+    return choices_to_states;
+}
+
+
+/**
+ * Among all compatible choices, for not affected states leaves only scheduler's choice
+ * and for affected states does not change anything
+ * 
+ * @param quotient_choice_map The mapping of choices to quotient choices
+ * @param quotient_state_map The mapping of states to quotient states
+ * @param quotient_mdp The parent MDP
+ * @param states_affected The bit vector of affected states
+ * @param parent_state_choice The choices of the parent's scheduler
+ * @param compatible_choices The choices that are compatible with the family
+ * 
+ * @return The final bit vector of choices for the family
+*/
+template<typename ValueType>
+storm::storage::BitVector affectedStatesToMask(
+    std::vector<uint64_t>const& quotient_choice_map,
+    std::vector<uint64_t>const& quotient_state_map,
+    storm::models::sparse::Mdp<ValueType> const& quotient_mdp,
+    storm::storage::BitVector const& states_affected,
+    std::vector<int>& parent_state_choice,
+    storm::storage::BitVector& compatible_choices
+) {
+    auto const& row_groups = quotient_mdp.getNondeterministicChoiceIndices();
+    uint64_t num_states = quotient_mdp.getNumberOfStates();
+    storm::storage::BitVector mask(compatible_choices.size(), true);
+    for(uint64_t state=0; state<num_states; ++state) {
+        uint64_t qstate = quotient_state_map[state];
+        if (states_affected.get(qstate)){
+            continue;
+        }
+        for(uint64_t choice=row_groups[state]; choice<row_groups[state+1]; ++choice) {
+            uint64_t qchoice = quotient_choice_map[choice];
+            mask.set(qchoice, false);
+        }
+        uint64_t parent_choice = parent_state_choice[qstate];
+        mask.set(parent_choice, true);
+    }
+    return mask & compatible_choices;
+}
+
+/**
+ * Finds all optimal choices leading to each state
+ * 
+ * @param quotient_mdp The quotient MDP
+ * @param parent_state_choice The choices of the parent's scheduler
+ * 
+ * @return Optimal leading choices for each state
+*/
+template<typename ValueType>
+std::vector<std::set<uint64_t>> findOptimalLeadingChoices(
+    storm::models::sparse::Mdp<ValueType> const& quotient_mdp,
+    std::vector<int>& parent_state_choice
+){
+    auto num_states = quotient_mdp.getNumberOfStates();
+    auto const& row_groups = quotient_mdp.getNondeterministicChoiceIndices();
+    std::vector<std::set<uint64_t>> optimal_leading_choices(num_states);
+    for(uint64_t state=0; state<num_states; ++state) {
+        int parent_choice = parent_state_choice[state];
+        if (parent_choice == -1) {
+            continue;
+        }
+        for(auto const& entry: quotient_mdp.getTransitionMatrix().getRow(parent_choice)) {
+            uint64_t entry_state = entry.getColumn();
+            optimal_leading_choices[entry_state].insert(parent_choice);
+        }
+    }
+    return optimal_leading_choices;
+}
+
+/**
+ * Finds all affected states from affected choices
+ * 
+ * @param quotient_mdp The quotient MDP
+ * @param choices_to_states The mapping from choices to states
+ * @param optimal_choices The bit vector of optimal choices
+ * @param compatible_choices The bit vector of compatible choices
+ * @param leading_optimals_to_state The optimal leading choices for each state
+ * 
+ * @return Affected states
+*/
+template<typename ValueType>
+storm::storage::BitVector optimalChoicesToAffectedStates(
+    storm::models::sparse::Mdp<ValueType> const& quotient_mdp,
+    std::vector<uint64_t> choices_to_states,
+    storm::storage::BitVector const& optimal_choices,
+    storm::storage::BitVector const& compatible_choices,
+    std::vector<std::set<uint64_t>> leading_optimals_to_state
+) {
+    uint64_t num_states = quotient_mdp.getNumberOfStates();
+    uint64_t num_choices = quotient_mdp.getNumberOfChoices();
+    storm::storage::BitVector affected_states(num_states, false);
+    storm::storage::BitVector was_in_queue(num_choices, false);
+    std::queue<uint64_t> queue_affected_choices;
+
+    for(uint64_t choice=0; choice<optimal_choices.size(); ++choice){
+        if(optimal_choices.get(choice) && !compatible_choices.get(choice)){
+            queue_affected_choices.push(choice);
+            was_in_queue.set(choice, true);
+        }
+    }
+    while(!queue_affected_choices.empty()){
+        uint64_t affected_qchoice = queue_affected_choices.front();
+        queue_affected_choices.pop();
+        uint64_t affected_qstate = choices_to_states[affected_qchoice];
+        affected_states.set(affected_qstate, true);
+        for (uint64_t leading_qchoice: leading_optimals_to_state[affected_qstate]){
+            if (compatible_choices.get(leading_qchoice) && !was_in_queue.get(leading_qchoice)){
+                queue_affected_choices.push(leading_qchoice);
+                was_in_queue.set(leading_qchoice, true);
+            }
+        }
+    }
+    return affected_states;
+}
+//---------------------------------------
+
+
 /*std::pair<std::vector<uint64_t>,storm::storage::BitVector> fixPolicyForFamily(
     std::vector<uint64_t> const& policy, uint64_t invalid_action,
     storm::storage::BitVector const& family_choices,
@@ -264,12 +434,19 @@ void bindings_coloring(py::module& m) {
     m.def("addChoiceLabelsFromJani", &synthesis::addChoiceLabelsFromJani<double>);
 
     m.def("computeChoiceDestinations", &synthesis::computeChoiceDestinations<double>);
-
+    //----------------xshevc01----------------
+    m.def("findAllPredecessors", &synthesis::findAllPredecessors<double>);
+    m.def("mapChoicesToStates", &synthesis::mapChoicesToStates<double>);
+    m.def("affectedStatesToMask", &synthesis::affectedStatesToMask<double>);
+    m.def("findOptimalLeadingChoices", &synthesis::findOptimalLeadingChoices<double>);
+    m.def("optimalChoicesToAffectedStates", &synthesis::optimalChoicesToAffectedStates<double>);
+    //---------------------------------------
     m.def("schedulerToStateToGlobalChoice", &synthesis::schedulerToStateToGlobalChoice<double>);
     m.def("computeInconsistentHoleVariance", &synthesis::computeInconsistentHoleVariance);
     
     m.def("policyToChoicesForFamily", &synthesis::policyToChoicesForFamily);
 
+    
 
     py::class_<synthesis::Family>(m, "Family")
         .def(py::init<>(), "Constructor.")