inconsistency for decision tree templates via SMT

paynt/cli.py

@@ -1,5 +1,6 @@
 from . import version
 
+import paynt.utils.profiler
 import paynt.parser.sketch
 
 import paynt.quotient
@@ -59,6 +60,8 @@ def setup_logger(log_path = None):
     help="known optimum bound")
 @click.option("--precision", type=click.FLOAT, default=1e-4,
     help="model checking precision")
+@click.option("--timeout", type=int,
+    help="timeout (s)")
 
 @click.option("--export",
     type=click.Choice(['jani', 'drn', 'pomdp']),
@@ -132,7 +135,7 @@ def setup_logger(log_path = None):
     help="decision tree synthesis: if set, all trees of size at most tree_depth will be enumerated")
 
 @click.option(
-    "--constraint-bound", type=click.FLOAT, help="bound for creating constrained POMDP for cassandra models",
+    "--constraint-bound", type=click.FLOAT, help="bound for creating constrained POMDP for Cassandra models",
 )
 
 @click.option(
@@ -143,7 +146,7 @@ def setup_logger(log_path = None):
     help="run profiling")
 
 def paynt_run(
-    project, sketch, props, relative_error, optimum_threshold, precision,
+    project, sketch, props, relative_error, optimum_threshold, precision, timeout,
     export,
     method,
     disable_expected_visits,
@@ -158,10 +161,12 @@ def paynt_run(
     ce_generator,
     profiling
 ):
+
     profiler = None
     if profiling:
         profiler = cProfile.Profile()
         profiler.enable()
+    paynt.utils.profiler.GlobalTimeoutTimer.start(timeout)
 
     logger.info("This is Paynt version {}.".format(version()))
 

paynt/family/family.py

@@ -10,6 +10,21 @@
 logger = logging.getLogger(__name__)
 
 
+class ParentInfo():
+    '''
+    Container for stuff to be remembered when splitting an undecided family into subfamilies. Generally used to
+    speed-up work with the subfamilies.
+    :note it is better to store these things in a separate container instead
+        of having a reference to the parent family (that will never be considered again) for memory efficiency.
+    '''
+    def __init__(self):
+        pass
+        self.selected_choices = None
+        self.constraint_indices = None
+        self.refinement_depth = None
+        self.splitter = None
+
+
 class Family:
 
     def __init__(self, other=None):
@@ -22,6 +37,21 @@ def __init__(self, other=None):
             self.hole_to_name = other.hole_to_name
             self.hole_to_option_labels = other.hole_to_option_labels
 
+        self.parent_info = None
+        self.refinement_depth = 0
+        self.constraint_indices = None
+
+        self.selected_choices = None
+        self.mdp = None
+        self.analysis_result = None
+        self.splitter = None
+        self.encoding = None
+
+    def add_parent_info(self, parent_info):
+        self.parent_info = parent_info
+        self.refinement_depth = parent_info.refinement_depth + 1
+        self.constraint_indices = parent_info.constraint_indices
+
     @property
     def num_holes(self):
         return self.family.numHoles()
@@ -121,61 +151,6 @@ def subholes(self, hole_index, options):
         shallow_copy.hole_set_options(hole_index,options)
         return shallow_copy
 
-
-
-class ParentInfo():
-    '''
-    Container for stuff to be remembered when splitting an undecided family
-    into subfamilies. Generally used to speed-up work with the subfamilies.
-    :note it is better to store these things in a separate container instead
-      of having a reference to the parent family (that will never be considered
-      again) for the purposes of memory efficiency.
-    '''
-    def __init__(self):
-        # list of constraint indices still undecided in this family
-        self.constraint_indices = None
-
-        # how many refinements were needed to create this family
-        self.refinement_depth = None
-
-        # index of a hole used to split the family
-        self.splitter = None
-
-
-class DesignSpace(Family):
-    '''
-    List of holes supplied with
-    - a list of constraint indices to investigate in this design space
-    - (optionally) z3 encoding of this design space
-    :note z3 (re-)encoding construction must be invoked manually
-    '''
-
-    # whether hints will be stored for subsequent MDP model checking
-    store_hints = True
-
-    def __init__(self, family = None, parent_info = None):
-        super().__init__(family)
-
-        self.mdp = None
-        self.selected_choices = None
-
-        # SMT encoding
-        self.encoding = None
-
-        self.refinement_depth = 0
-        self.constraint_indices = None
-
-        self.analysis_result = None
-        self.splitter = None
-        self.parent_info = parent_info
-        if parent_info is not None:
-            self.refinement_depth = parent_info.refinement_depth + 1
-            self.constraint_indices = parent_info.constraint_indices
-
-    def copy(self):
-        return DesignSpace(super().copy())
-
-
     def collect_parent_info(self, specification):
         pi = ParentInfo()
         pi.selected_choices = self.selected_choices

paynt/models/models.py

@@ -37,6 +37,25 @@ def model_check_property(self, prop, alt=False):
         value = result.at(self.initial_state)
         return paynt.verification.property_result.PropertyResult(prop, result, value)
 
+    def check_specification(self, spec, constraint_indices=None, short_evaluation=False):
+        ''' Assuming this is a DTMC. '''
+        if constraint_indices is None:
+            constraint_indices = spec.all_constraint_indices()
+        results = [None for _ in spec.constraints]
+        for index in constraint_indices:
+            result = self.model_check_property(spec.constraints[index])
+            results[index] = result
+            if short_evaluation and result.sat is False:
+                break
+        spec_result = paynt.verification.property_result.SpecificationResult()
+        spec_result.constraints_result = paynt.verification.property_result.ConstraintsResult(results)
+
+        if spec.has_optimality and not (short_evaluation and spec_result.constraints_result.sat is False):
+            spec_result.optimality_result = self.model_check_property(spec.optimality)
+        return spec_result
+
+
+
 class SubMdp(Mdp):
 
     def __init__(self, model, quotient_state_map, quotient_choice_map):

paynt/parser/jani.py

@@ -216,7 +216,7 @@ def construct_edge(self, edge, substitution = None):
         for templ_edge_dest in edge.template_edge.destinations:
             assignments = templ_edge_dest.assignments.clone()
             if substitution is not None:
-                assignments.substitute(substitution,substitute_transcendental_numbers=False)
+                assignments.substitute(substitution)
             templ_edge.add_destination(stormpy.storage.JaniTemplateEdgeDestination(assignments))
 
         new_edge = stormpy.storage.JaniEdge(

paynt/parser/sketch.py

@@ -223,7 +223,7 @@ def export(cls, export, sketch_path, jani_unfolder, explicit_quotient):
     def build_quotient_container(cls, prism, jani_unfolder, explicit_quotient, family, coloring, specification, obs_evaluator, decpomdp_manager):
         if jani_unfolder is not None:
             if prism.model_type == stormpy.storage.PrismModelType.DTMC:
-                quotient_container = paynt.quotient.quotient.DtmcFamilyQuotient(explicit_quotient, family, coloring, specification)
+                quotient_container = paynt.quotient.quotient.Quotient(explicit_quotient, family, coloring, specification)
             elif prism.model_type == stormpy.storage.PrismModelType.MDP:
                 quotient_container = paynt.quotient.mdp_family.MdpFamilyQuotient(explicit_quotient, family, coloring, specification)
             elif prism.model_type == stormpy.storage.PrismModelType.POMDP:

paynt/quotient/decpomdp.py

@@ -105,20 +105,18 @@ def unfold_memory(self):
         self.choice_destinations = payntbind.synthesis.computeChoiceDestinations(self.quotient_mdp)
         logger.debug(f"constructed quotient MDP having {self.quotient_mdp.nr_states} states and {self.quotient_mdp.nr_choices} actions.")
 
-        family, choice_to_hole_options = self.create_coloring()
+        self.family, choice_to_hole_options = self.create_coloring()
 
-        self.coloring = payntbind.synthesis.Coloring(family.family, self.quotient_mdp.nondeterministic_choice_indices, choice_to_hole_options)
+        self.coloring = payntbind.synthesis.Coloring(self.family.family, self.quotient_mdp.nondeterministic_choice_indices, choice_to_hole_options)
 
         # to each hole-option pair a list of actions colored by this combination
-        self.hole_option_to_actions = [[] for hole in range(family.num_holes)]
-        for hole in range(family.num_holes):
-            self.hole_option_to_actions[hole] = [[] for option in family.hole_options(hole)]
+        self.hole_option_to_actions = [[] for hole in range(self.family.num_holes)]
+        for hole in range(self.family.num_holes):
+            self.hole_option_to_actions[hole] = [[] for option in self.family.hole_options(hole)]
         for choice in range(self.quotient_mdp.nr_choices):
             for hole,option in choice_to_hole_options[choice]:
                 self.hole_option_to_actions[hole][option].append(choice)
 
-        self.design_space = paynt.family.family.DesignSpace(family)
-
 
     def create_coloring(self):
         # short aliases