Inheritance dependencies for AR

models/archive/cav23-saynt/lrv/sketch.props

@@ -0,0 +1 @@
+R{"cost"}min=? [F "goal"];

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;

models/pomdp/grid/evade/sketch.props

@@ -1,2 +1,2 @@
-//Pmax=?["notbad" U "goal"];
-R{"steps"}min=? ["notbad" U "goal"]
+Pmax=?["notbad" U "goal"];
+//R{"steps"}min=? ["notbad" U "goal"]

models/pomdp/other/cheese/sketch.props

@@ -1,2 +1,2 @@
-//P<0.5 [F "bad"]
-R{"rew0"}max=? [F "goal"]
+P<0.5 [F "bad"]
+//R{"rew0"}max=? [F "goal"]

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)

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):

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)