diff --git a/examples/building_models/04-building-models.py b/examples/building_models/04-building-models.py index f014420647..b5434701aa 100644 --- a/examples/building_models/04-building-models.py +++ b/examples/building_models/04-building-models.py @@ -37,7 +37,7 @@ def permissive_policy(state_valuation, action_index): cond3 = json.loads(str(state_valuation.to_json()))["x1"] < 40 return cond1 or (cond2 and cond3) - constructor = stormpy.make_sparse_model_builder(prism_program, options, stormpy.StateValuationFunctionActionMaskDouble(permissive_policy)) + constructor = stormpy.make_sparse_model_builder(prism_program, options, stormpy.StateValuationFunctionActionMask[float](permissive_policy)) model = constructor.build() print(model) diff --git a/lib/stormpy/__init__.py b/lib/stormpy/__init__.py index bf4d45755d..575a03179f 100644 --- a/lib/stormpy/__init__.py +++ b/lib/stormpy/__init__.py @@ -7,6 +7,64 @@ from .logic import * from . import exceptions +from ._template import ( + TemplateClass as _TemplateClass, + TemplateParameter as _TemplateParameter, + deduce_default as _deduce_default, + deduce_from_object as _deduce_from_object, +) + +# src/core/core.cpp +ExplicitModelBuilderOptions = _TemplateClass("stormpy.ExplicitModelBuilderOptions", _core, parameters=("ValueType",), deduce=_deduce_default(float)) +ExplicitModelBuilder = _TemplateClass("stormpy.ExplicitModelBuilder", _core, parameters=("ValueType",)) +ActionMask = _TemplateClass("stormpy.ActionMask", _core, parameters=("ValueType",)) +StateValuationFunctionActionMask = _TemplateClass("stormpy.StateValuationFunctionActionMask", _core, parameters=("ValueType",), deduce=_deduce_default(float)) + +# src/core/modelchecking.cpp +CheckTask = _TemplateClass("stormpy.CheckTask", _core, parameters=("ValueType",), deduce=_deduce_default(float)) +ExplicitModelCheckerHint = _TemplateClass("stormpy.ExplicitModelCheckerHint", _core, parameters=("ValueType",), deduce=_deduce_default(float)) + +# src/core/result.cpp +ExplicitQualitativeCheckResult = _TemplateClass("stormpy.ExplicitQualitativeCheckResult", _core, parameters=("ValueType",)) +SymbolicQualitativeCheckResult = _TemplateClass("stormpy.SymbolicQualitativeCheckResult", _core, parameters=(_TemplateParameter("DdType", kind="value"),)) +QuantitativeCheckResult = _TemplateClass("stormpy.QuantitativeCheckResult", _core, parameters=("ValueType",)) +ExplicitQuantitativeCheckResult = _TemplateClass("stormpy.ExplicitQuantitativeCheckResult", _core, parameters=("ValueType",), deduce=_deduce_default(float)) +SymbolicQuantitativeCheckResult = _TemplateClass( + "stormpy.SymbolicQuantitativeCheckResult", _core, parameters=(_TemplateParameter("DdType", kind="value"), "ValueType") +) +HybridQuantitativeCheckResult = _TemplateClass( + "stormpy.HybridQuantitativeCheckResult", _core, parameters=(_TemplateParameter("DdType", kind="value"), "ValueType") +) +ParetoCurveCheckResult = _TemplateClass("stormpy.ParetoCurveCheckResult", _core, parameters=("ValueType",)) +ExplicitParetoCurveCheckResult = _TemplateClass("stormpy.ExplicitParetoCurveCheckResult", _core, parameters=("ValueType",)) + +# src/core/simulator.cpp +DiscreteTimeSparseModelSimulator = _TemplateClass( + "stormpy.DiscreteTimeSparseModelSimulator", _core, parameters=("ValueType",), deduce=_deduce_from_object(storage.parameters_of_model, keyword="model") +) +DiscreteTimePrismProgramSimulator = _TemplateClass("stormpy.DiscreteTimePrismProgramSimulator", _core, parameters=("ValueType",), deduce=_deduce_default(float)) + +# src/core/multiobjective.cpp +WeightedObjectiveMdpModelChecker = _TemplateClass("stormpy.WeightedObjectiveMdpModelChecker", _core, parameters=("ValueType",)) + +# src/core/transformation.cpp +SubsystemBuilderReturnType = _TemplateClass("stormpy.SubsystemBuilderReturnType", _core, parameters=("ValueType",)) +EndComponentEliminatorReturnType = _TemplateClass("stormpy.EndComponentEliminatorReturnType", _core, parameters=("ValueType",)) +AddUncertainty = _TemplateClass( + "stormpy.AddUncertainty", _core, parameters=("ValueType",), deduce=_deduce_from_object(storage.parameters_of_model, keyword="model") +) + +# src/core/analysis.cpp +ConstraintCollector = _TemplateClass( + "stormpy.ConstraintCollector", _core, parameters=("ValueType",), deduce=_deduce_from_object(storage.parameters_of_model, keyword="model") +) + +# src/core/counterexample.cpp +SMTCounterExampleGeneratorStats = _TemplateClass("stormpy.SMTCounterExampleGeneratorStats", _core, parameters=("ValueType",), deduce=_deduce_default(float)) +SMTCounterExampleGeneratorOptions = _TemplateClass("stormpy.SMTCounterExampleGeneratorOptions", _core, parameters=("ValueType",), deduce=_deduce_default(float)) +SMTCounterExampleGenerator = _TemplateClass("stormpy.SMTCounterExampleGenerator", _core, parameters=("ValueType",)) +SMTCounterExampleInput = _TemplateClass("stormpy.SMTCounterExampleInput", _core, parameters=("ValueType",)) + from enum import Enum try: @@ -384,10 +442,7 @@ def perform_sparse_bisimulation(model, properties, bisimulation_type, graph_pres :return: Model after bisimulation. """ formulae = [(prop.raw_formula if isinstance(prop, Property) else prop) for prop in properties] - if model.supports_parameters: - return _core._perform_parametric_bisimulation(model, formulae, bisimulation_type, graph_preserving, tolerance) - else: - return _core._perform_bisimulation(model, formulae, bisimulation_type, graph_preserving, tolerance) + return _core._perform_bisimulation(model, formulae, bisimulation_type, graph_preserving, tolerance) def perform_symbolic_bisimulation(model, properties, quotient_format=stormpy.QuotientFormat.DD, bisimulation_options=stormpy.BisimulationOptionsDd()): @@ -401,10 +456,7 @@ def perform_symbolic_bisimulation(model, properties, quotient_format=stormpy.Quo """ formulae = [(prop.raw_formula if isinstance(prop, Property) else prop) for prop in properties] bisimulation_type = BisimulationType.STRONG - if model.supports_parameters: - return _core._perform_symbolic_parametric_bisimulation(model, formulae, bisimulation_type, quotient_format, bisimulation_options) - else: - return _core._perform_symbolic_bisimulation(model, formulae, bisimulation_type, quotient_format, bisimulation_options) + return _core._perform_symbolic_bisimulation(model, formulae, bisimulation_type, quotient_format, bisimulation_options) def model_checking(model, property, only_initial_states=False, extract_scheduler=False, force_fully_observable=False, environment=Environment()): @@ -445,56 +497,25 @@ def check_model_sparse(model, property, only_initial_states=False, extract_sched :return: Model checking result. :rtype: CheckResult """ - if isinstance(property, Property): - formula = property.raw_formula - else: - formula = property - + formula = property.raw_formula if isinstance(property, Property) else property if model.is_partially_observable: - if force_fully_observable: - # Note that casting a model to a fully observable model wont work with python/pybind, so we actually have other access points - if model.supports_parameters: - raise NotImplementedError("Model checking of partially observable models is not supported for parametric models.") - elif model.supports_uncertainty: - raise NotImplementedError("Model checking of partially observable models is not supported for interval models.") - elif model.is_exact: - task = _core.ExactCheckTask(formula, only_initial_states) - task.set_produce_schedulers(extract_scheduler) - if hint: - task.set_hint(hint) - return _core._exact_model_checking_fully_observable(model, task, environment=environment) - else: - task = _core.CheckTask(formula, only_initial_states) - task.set_produce_schedulers(extract_scheduler) - if hint: - task.set_hint(hint) - return _core._model_checking_fully_observable(model, task, environment=environment) - else: + if not force_fully_observable: raise RuntimeError("Model checking of partially observable models is handled via dedicated methods, unless the force fully-observable is set.") - - if model.supports_parameters: - task = _core.ParametricCheckTask(formula, only_initial_states) - task.set_produce_schedulers(extract_scheduler) - if hint: - task.set_hint(hint) - return _core._parametric_model_checking_sparse_engine(model, task, environment=environment) - else: - if model.is_exact: - if formula.is_multi_objective_formula: - return _core._multi_objective_model_checking_exact(model, formula, environment=environment) - task = _core.ExactCheckTask(formula, only_initial_states) - task.set_produce_schedulers(extract_scheduler) - if hint: - task.set_hint(hint) - return _core._exact_model_checking_sparse_engine(model, task, environment=environment) - else: - if formula.is_multi_objective_formula: - return _core._multi_objective_model_checking_double(model, formula, environment=environment) - task = _core.CheckTask(formula, only_initial_states) - task.set_produce_schedulers(extract_scheduler) - if hint: - task.set_hint(hint) - return _core._model_checking_sparse_engine(model, task, environment=environment) + if model.supports_parameters: + raise NotImplementedError("Model checking of partially observable models is not supported for parametric models.") + if model.supports_uncertainty: + raise NotImplementedError("Model checking of partially observable models is not supported for interval models.") + elif model.supports_uncertainty: + raise NotImplementedError("Model checking of interval models is handled via dedicated methods.") + elif formula.is_multi_objective_formula and not model.supports_parameters: + return _core._multi_objective_model_checking(model, formula, environment=environment) + task = CheckTask[storage.parameters_of_model(model)](formula, only_initial_states) + task.set_produce_schedulers(extract_scheduler) + if hint: + task.set_hint(hint) + if model.is_partially_observable: + return _core._model_checking_fully_observable(model, task, environment=environment) + return _core._model_checking_sparse_engine(model, task, environment=environment) def check_model_dd(model, property, only_initial_states=False, environment=Environment()): @@ -506,17 +527,10 @@ def check_model_dd(model, property, only_initial_states=False, environment=Envir :return: Model checking result. :rtype: CheckResult """ - if isinstance(property, Property): - formula = property.raw_formula - else: - formula = property - - if model.supports_parameters: - task = _core.ParametricCheckTask(formula, only_initial_states) - return _core._parametric_model_checking_dd_engine(model, task, environment=environment) - else: - task = _core.CheckTask(formula, only_initial_states) - return _core._model_checking_dd_engine(model, task, environment=environment) + formula = property.raw_formula if isinstance(property, Property) else property + value_type = RationalFunction if model.supports_parameters else (Rational if model.is_exact else float) + task = CheckTask[value_type](formula, only_initial_states) + return _core._model_checking_dd_engine(model, task, environment=environment) def check_model_hybrid(model, property, only_initial_states=False, environment=Environment()): @@ -528,17 +542,10 @@ def check_model_hybrid(model, property, only_initial_states=False, environment=E :return: Model checking result. :rtype: CheckResult """ - if isinstance(property, Property): - formula = property.raw_formula - else: - formula = property - - if model.supports_parameters: - task = _core.ParametricCheckTask(formula, only_initial_states) - return _core._parametric_model_checking_hybrid_engine(model, task, environment=environment) - else: - task = _core.CheckTask(formula, only_initial_states) - return _core._model_checking_hybrid_engine(model, task, environment=environment) + formula = property.raw_formula if isinstance(property, Property) else property + value_type = RationalFunction if model.supports_parameters else (Rational if model.is_exact else float) + task = CheckTask[value_type](formula, only_initial_states) + return _core._model_checking_hybrid_engine(model, task, environment=environment) def set_state_valuations(model, new_state_valuations): @@ -566,10 +573,7 @@ def transform_to_sparse_model(model): :param model: Symbolic model. :return: Sparse model. """ - if model.supports_parameters: - return _core._transform_to_sparse_parametric_model(model) - else: - return _core._transform_to_sparse_model(model) + return _core._transform_to_sparse_model(model) def transform_to_discrete_time_model(model, properties): @@ -580,10 +584,7 @@ def transform_to_discrete_time_model(model, properties): :return: Tuple (Discrete-time model, converted properties). """ formulae = [(prop.raw_formula if isinstance(prop, Property) else prop) for prop in properties] - if model.supports_parameters: - return _core._transform_to_discrete_time_parametric_model(model, formulae) - else: - return _core._transform_to_discrete_time_model(model, formulae) + return _core._transform_to_discrete_time_model(model, formulae) def eliminate_non_markovian_chains(ma, properties, label_behavior): @@ -595,10 +596,7 @@ def eliminate_non_markovian_chains(ma, properties, label_behavior): :return: Tuple (converted MA, converted properties). """ formulae = [(prop.raw_formula if isinstance(prop, Property) else prop) for prop in properties] - if ma.supports_parameters: - return _core._eliminate_non_markovian_chains_parametric(ma, formulae, label_behavior) - else: - return _core._eliminate_non_markovian_chains(ma, formulae, label_behavior) + return _core._eliminate_non_markovian_chains(ma, formulae, label_behavior) def prob01min_states(model, eventually_formula): @@ -630,28 +628,19 @@ def compute_prob01_states(model, phi_states, psi_states): if model.model_type != ModelType.DTMC: raise stormpy.exceptions.StormError("Prob 01 is only defined for DTMCs -- model must be a DTMC") - if model.supports_parameters: - return _core._compute_prob01states_rationalfunc(model, phi_states, psi_states) - else: - return _core._compute_prob01states_double(model, phi_states, psi_states) + return _core._compute_prob01states(model, phi_states, psi_states) def compute_prob01min_states(model, phi_states, psi_states): if model.model_type == ModelType.DTMC: return compute_prob01_states(model, phi_states, psi_states) - if model.supports_parameters: - return _core._compute_prob01states_min_rationalfunc(model, phi_states, psi_states) - else: - return _core._compute_prob01states_min_double(model, phi_states, psi_states) + return _core._compute_prob01states_min(model, phi_states, psi_states) def compute_prob01max_states(model, phi_states, psi_states): if model.model_type == ModelType.DTMC: return compute_prob01_states(model, phi_states, psi_states) - if model.supports_parameters: - return _core._compute_prob01states_max_rationalfunc(model, phi_states, psi_states) - else: - return _core._compute_prob01states_max_double(model, phi_states, psi_states) + return _core._compute_prob01states_max(model, phi_states, psi_states) def topological_sort(model, forward=True, initial=[]): @@ -662,13 +651,10 @@ def topological_sort(model, forward=True, initial=[]): :param initial: a list of states :return: A topological sort of the states """ + if not model.is_sparse_model: + raise NotImplementedError("Topological sorting is only supported for sparse models.") matrix = model.transition_matrix if forward else model.backward_transition_matrix - if isinstance(model, storage.SparseModel[stormpy.RationalFunction]): - return storage._storage._topological_sort_rf(matrix, initial) - elif isinstance(model, storage.SparseModel[float]): - return storage._storage._topological_sort_double(matrix, initial) - else: - raise stormpy.exceptions.StormError("Unknown kind of model.") + return storage._storage._topological_sort(matrix, initial) def get_reachable_states(model, initial_states, constraint_states, target_states, maximal_steps=None, choice_filter=None): @@ -683,11 +669,7 @@ def get_reachable_states(model, initial_states, constraint_states, target_states :param choice_filter: :return: """ - if model.supports_parameters: - return _core._get_reachable_states_rf(model, initial_states, constraint_states, target_states, maximal_steps, choice_filter) - if model.is_exact: - return _core._get_reachable_states_exact(model, initial_states, constraint_states, target_states, maximal_steps, choice_filter) - return _core._get_reachable_states_double(model, initial_states, constraint_states, target_states, maximal_steps, choice_filter) + return _core._get_reachable_states(model, initial_states, constraint_states, target_states, maximal_steps, choice_filter) def compute_expected_number_of_visits(environment, model): @@ -700,9 +682,7 @@ def compute_expected_number_of_visits(environment, model): """ if model.supports_parameters: raise NotImplementedError("Expected number of visits is not implemented for parametric models") - if model.is_exact: - return _core._compute_expected_number_of_visits_exact(environment, model) - return _core._compute_expected_number_of_visits_double(environment, model) + return _core._compute_expected_number_of_visits(environment, model) def compute_steady_state_distribution(environment, model): @@ -715,9 +695,7 @@ def compute_steady_state_distribution(environment, model): """ if model.supports_parameters: raise NotImplementedError("Steady-state distribution is not implemented for parametric models") - if model.is_exact: - return _core._compute_steady_state_distribution_exact(environment, model) - return _core._compute_steady_state_distribution_double(environment, model) + return _core._compute_steady_state_distribution(environment, model) def construct_submodel(model, states, actions, keep_unreachable_states=True, options=SubsystemBuilderOptions()): @@ -730,15 +708,7 @@ def construct_submodel(model, states, actions, keep_unreachable_states=True, opt :param options: An options object of type SubsystemBuilderOptions :return: A model with fewer states/actions """ - if model.supports_parameters: - return _core._construct_subsystem_RatFunc(model, states, actions, keep_unreachable_states, options) - if model.supports_uncertainty: - if model.is_exact: - return _core._construct_subsystem_RationalInterval(model, states, actions, keep_unreachable_states, options) - return _core._construct_subsystem_Interval(model, states, actions, keep_unreachable_states, options) - if model.is_exact: - return _core._construct_subsystem_Exact(model, states, actions, keep_unreachable_states, options) - return _core._construct_subsystem_Double(model, states, actions, keep_unreachable_states, options) + return _core._construct_subsystem(model, states, actions, keep_unreachable_states, options) def make_weighted_objective_mdp_model_checker(environment, model, formula, compute_scheduler): @@ -752,9 +722,7 @@ def make_weighted_objective_mdp_model_checker(environment, model, formula, compu """ if model.supports_parameters or model.supports_uncertainty: raise ValueError("Parameters and intervals are not supported.") - if model.is_exact: - return _core._make_weighted_objective_mdp_model_checker_Exact(environment, model, formula, compute_scheduler) - return _core._make_weighted_objective_mdp_model_checker_Double(environment, model, formula, compute_scheduler) + return _core._make_weighted_objective_mdp_model_checker(environment, model, formula, compute_scheduler) def eliminate_ECs(matrix, subsystem, possible_ecs, add_sink_row_states, add_self_loop_at_sink_states=False): @@ -775,17 +743,7 @@ def eliminate_ECs(matrix, subsystem, possible_ecs, add_sink_row_states, add_self assert matrix.nr_columns == subsystem.size(), "subsystem vector should have an entry for every state." assert matrix.nr_rows == possible_ecs.size(), "possible_ecs vector should have an entry for every row." assert matrix.nr_columns == add_sink_row_states.size(), "add_sink_row_states vector should have an entry for every state." - - if isinstance(matrix, storage.SparseMatrix[stormpy.RationalInterval]): - return _core._eliminate_end_components_RationalInterval(matrix, subsystem, possible_ecs, add_sink_row_states, add_self_loop_at_sink_states) - elif isinstance(matrix, storage.SparseMatrix[stormpy.Interval]): - return _core._eliminate_end_components_Interval(matrix, subsystem, possible_ecs, add_sink_row_states, add_self_loop_at_sink_states) - elif isinstance(matrix, storage.SparseMatrix[stormpy.Rational]): - return _core._eliminate_end_components_Exact(matrix, subsystem, possible_ecs, add_sink_row_states, add_self_loop_at_sink_states) - elif isinstance(matrix, storage.SparseMatrix[float]): - return _core._eliminate_end_components_Double(matrix, subsystem, possible_ecs, add_sink_row_states, add_self_loop_at_sink_states) - else: - raise TypeError(f"eliminate_ECs: unsupported matrix type {type(matrix)}") + return _core._eliminate_end_components(matrix, subsystem, possible_ecs, add_sink_row_states, add_self_loop_at_sink_states) def parse_properties(properties, context=None, filters=None): @@ -819,14 +777,6 @@ def export_to_drn(model, file, options=DirectEncodingExporterOptions()): :param options: DirectEncodingExporterOptions :return: """ - if model.supports_parameters: - return _core._export_parametric_to_drn(model, file, options) - if model.supports_uncertainty and model.is_exact: - return _core._export_exact_to_drn_interval(model, file, options) - if model.supports_uncertainty: - return _core._export_to_drn_interval(model, file, options) - if model.is_exact: - return _core._export_exact_to_drn(model, file, options) return _core._export_to_drn(model, file, options) diff --git a/lib/stormpy/simulator.py b/lib/stormpy/simulator.py index bc9658b8c0..293d74d150 100644 --- a/lib/stormpy/simulator.py +++ b/lib/stormpy/simulator.py @@ -105,10 +105,7 @@ class SparseSimulator(Simulator): def __init__(self, model, seed=None): super().__init__(seed) self._model = model - if self._model.is_exact: - self._engine = stormpy._core._DiscreteTimeSparseModelSimulatorExact(model) - else: - self._engine = stormpy._core._DiscreteTimeSparseModelSimulatorDouble(model) + self._engine = stormpy.DiscreteTimeSparseModelSimulator(model) if seed is not None: self._engine.set_seed(seed) self._state_valuations = None @@ -234,7 +231,7 @@ def __init__(self, program, seed=None, options=stormpy.BuilderOptions()): super().__init__(seed) self._program = program # TODO support exact arithmetic here - self._engine = stormpy._core._DiscreteTimePrismProgramSimulatorDouble(program, options) + self._engine = stormpy.DiscreteTimePrismProgramSimulator[float](program, options) if seed is not None: self._engine.set_seed(seed) self.set_full_observability(self._program.model_type != stormpy.storage.PrismModelType.POMDP) diff --git a/lib/stormpy/storage/__init__.py b/lib/stormpy/storage/__init__.py index 531b556e9d..5dab6240ad 100644 --- a/lib/stormpy/storage/__init__.py +++ b/lib/stormpy/storage/__init__.py @@ -55,45 +55,50 @@ deduce=_deduce_from_object(SparseMatrix.parameters_of, keyword="transition_matrix", default=(float,)), ) + # src/storage/model.cpp -_model_parameters = lambda source: SparseMatrix.parameters_of(source.transition_matrix) +def parameters_of_model(model): + """Return the value-type parameter of a sparse model or model components.""" + + return SparseMatrix.parameters_of(model.transition_matrix) + SparseModel = TemplateClass("stormpy.storage.SparseModel", _storage, parameters=("ValueType",), deduce=_deduce_default(float)) SparseDtmc = TemplateClass( "stormpy.storage.SparseDtmc", _storage, parameters=("ValueType",), - deduce=_deduce_from_object(_model_parameters, keyword=("components", "other_model")), + deduce=_deduce_from_object(parameters_of_model, keyword=("components", "other_model")), ) SparseMdp = TemplateClass( "stormpy.storage.SparseMdp", _storage, parameters=("ValueType",), - deduce=_deduce_from_object(_model_parameters, keyword=("components", "other_model")), + deduce=_deduce_from_object(parameters_of_model, keyword=("components", "other_model")), ) SparsePomdp = TemplateClass( "stormpy.storage.SparsePomdp", _storage, parameters=("ValueType",), - deduce=_deduce_from_object(_model_parameters, keyword=("components", "other_model")), + deduce=_deduce_from_object(parameters_of_model, keyword=("components", "other_model")), ) SparseCtmc = TemplateClass( "stormpy.storage.SparseCtmc", _storage, parameters=("ValueType",), - deduce=_deduce_from_object(_model_parameters, keyword=("components", "other_model")), + deduce=_deduce_from_object(parameters_of_model, keyword=("components", "other_model")), ) SparseMA = TemplateClass( "stormpy.storage.SparseMA", _storage, parameters=("ValueType",), - deduce=_deduce_from_object(_model_parameters, keyword=("components", "other_model")), + deduce=_deduce_from_object(parameters_of_model, keyword=("components", "other_model")), ) SparseSmg = TemplateClass( "stormpy.storage.SparseSmg", _storage, parameters=("ValueType",), - deduce=_deduce_from_object(_model_parameters, keyword=("components", "other_model")), + deduce=_deduce_from_object(parameters_of_model, keyword=("components", "other_model")), ) SparseRewardModel = TemplateClass("stormpy.storage.SparseRewardModel", _storage, parameters=("ValueType",), deduce=_deduce_default(float)) SymbolicModel = TemplateClass("stormpy.storage.SymbolicModel", _storage, parameters=(_TemplateParameter("DdType", kind="value"), "ValueType")) @@ -108,7 +113,7 @@ "stormpy.storage.MaximalEndComponentDecomposition", _storage, parameters=("ValueType",), - deduce=_deduce_from_object(_model_parameters, keyword="model"), + deduce=_deduce_from_object(parameters_of_model, keyword="model"), ) # src/storage/memorystructure.cpp @@ -116,7 +121,7 @@ "stormpy.storage.MemoryStructureBuilder", _storage, parameters=("ValueType",), - deduce=_deduce_from_object(_model_parameters, keyword="model", position=1), + deduce=_deduce_from_object(parameters_of_model, keyword="model", position=1), ) MemoryStructureProduct = TemplateClass("stormpy.storage.MemoryStructureProduct", _storage, parameters=("ValueType",), deduce=_deduce_default(float)) diff --git a/src/core/analysis.cpp b/src/core/analysis.cpp index c942f229ad..3e2736eee9 100644 --- a/src/core/analysis.cpp +++ b/src/core/analysis.cpp @@ -2,10 +2,13 @@ #include +#include "src/binding_type_index.h" + // Define python bindings void define_graph_constraints(py::module& m) { // ConstraintCollector - py::classh>(m, "ConstraintCollector", "Collector for constraints on parametric Markov chains") + stormpy::bindings::bindTemplateClass>( + m, "ConstraintCollector", stormpy::bindings::typeIndex(), "Collector for constraints on parametric Markov chains") .def(py::init const&>(), py::arg("model")) .def_property_readonly("wellformed_constraints", &storm::analysis::ConstraintCollector::getWellformedConstraints, "Get the constraints ensuring a wellformed model") diff --git a/src/core/bisimulation.cpp b/src/core/bisimulation.cpp index 5ce9be5e7b..e2eddd3647 100644 --- a/src/core/bisimulation.cpp +++ b/src/core/bisimulation.cpp @@ -17,11 +17,11 @@ void define_bisimulation(py::module& m) { // Bisimulation m.def("_perform_bisimulation", &storm::api::performBisimulationMinimization, "Perform bisimulation", py::arg("model"), py::arg("formulas"), py::arg("bisimulation_type"), py::arg("graph_preserving"), py::arg("tolerance")); - m.def("_perform_parametric_bisimulation", &storm::api::performBisimulationMinimization, "Perform bisimulation on parametric model", + m.def("_perform_bisimulation", &storm::api::performBisimulationMinimization, "Perform bisimulation on parametric model", py::arg("model"), py::arg("formulas"), py::arg("bisimulation_type"), py::arg("graph_preserving"), py::arg("tolerance")); m.def("_perform_symbolic_bisimulation", &performBisimulationMinimization, "Perform bisimulation", py::arg("model"), py::arg("formulas"), py::arg("bisimulation_type"), py::arg("quotient_format"), py::arg("bisimulation_options")); - m.def("_perform_symbolic_parametric_bisimulation", &performBisimulationMinimization, + m.def("_perform_symbolic_bisimulation", &performBisimulationMinimization, "Perform bisimulation on parametric model", py::arg("model"), py::arg("formulas"), py::arg("bisimulation_type"), py::arg("quotient_format"), py::arg("bisimulation_options")); diff --git a/src/core/core.cpp b/src/core/core.cpp index 6f3c022421..69c711e2cc 100644 --- a/src/core/core.cpp +++ b/src/core/core.cpp @@ -15,6 +15,8 @@ #include #include +#include "src/binding_type_index.h" + void define_core(py::module& m) { // Init m.def( @@ -103,30 +105,35 @@ std::shared_ptr> buildSymbolic } } +template +void define_explicit_model_builder(py::module& m, std::string const& name) { + m.def(name.c_str(), &storm::api::makeExplicitModelBuilder, "Construct a builder instance", py::arg("model_description"), py::arg("options"), + py::arg("action_mask") = nullptr, py::arg("exploration_options") = typename storm::builder::ExplicitModelBuilder::Options()); + + stormpy::bindings::bindTemplateClass>(m, "ExplicitModelBuilder", stormpy::bindings::typeIndex(), + "Model builder for sparse models") + .def("build", &storm::builder::ExplicitModelBuilder::build, "Build the model", py::call_guard()) + .def("export_lookup", &storm::builder::ExplicitModelBuilder::exportExplicitStateLookup, "Export a lookup model"); +} + template void define_build_sparse_model_defs(py::module& m) { std::string type; - std::string classType; std::string desc; if constexpr (std::is_same_v) { type = ""; - classType = ""; desc = ""; } else if constexpr (std::is_same_v) { type = "exact_"; - classType = "Exact"; desc = ""; } else if constexpr (std::is_same_v) { type = "parametric_"; - classType = "Parametric"; desc = "parametric "; } else if constexpr (std::is_same_v) { type = "interval_"; - classType = "Interval"; desc = "interval "; } else if constexpr (std::is_same_v) { type = "exact_interval_"; - classType = "ExactInterval"; desc = "exact interval "; } @@ -144,8 +151,8 @@ void define_build_sparse_model_defs(py::module& m) { ("Build the " + desc + "model from DRN" + (std::is_same_v ? " (parametric)" : "")).c_str(), py::arg("file"), py::arg("options") = storm::parser::DirectEncodingParserOptions()); - py::classh::Options>(m, ("Explicit" + classType + "ModelBuilderOptions").c_str(), - "Options for the explicit model builder") + stormpy::bindings::bindTemplateClass::Options>( + m, "ExplicitModelBuilderOptions", stormpy::bindings::typeIndex(), "Options for the explicit model builder") .def(py::init<>(), "Create") .def_readwrite("exploration_order", &storm::builder::ExplicitModelBuilder::Options::explorationOrder, "The order in which to explore the model") @@ -154,33 +161,18 @@ void define_build_sparse_model_defs(py::module& m) { .def_readwrite("exploration_state_limit", &storm::builder::ExplicitModelBuilder::Options::explorationStateLimit, "If set, no further states will be explored once the given number is exceeded."); - if constexpr (std::is_same_v) { - m.def("_build_symbolic_model_from_symbolic_description", &buildSymbolicModel, - "Build the model in symbolic representation", py::arg("model_description"), + define_explicit_model_builder(m, "make_sparse_model_builder" + type); + + if constexpr (!storm::IsIntervalType) { + m.def(("_build_symbolic_" + type + "model_from_symbolic_description").c_str(), &buildSymbolicModel, + ("Build the " + desc + "model in symbolic representation").c_str(), py::arg("model_description"), py::arg("formulas") = std::vector>(), py::arg("environment")); + } + + if constexpr (std::is_same_v) { m.def("build_sparse_model_from_explicit", &storm::api::buildExplicitModel, "Build the model model from explicit input", py::arg("transition_file"), py::arg("labeling_file"), py::arg("state_reward_file") = "", py::arg("transition_reward_file") = "", py::arg("choice_labeling_file") = "", py::arg("options") = storm::parser::ExplicitModelParserOptions()); - m.def("make_sparse_model_builder", &storm::api::makeExplicitModelBuilder, "Construct a builder instance", py::arg("model_description"), - py::arg("options"), py::arg("action_mask") = nullptr, - py::arg("exploration_options") = typename storm::builder::ExplicitModelBuilder::Options()); - py::classh>(m, "ExplicitModelBuilder", "Model builder for sparse models") - .def("build", &storm::builder::ExplicitModelBuilder::build, "Build the model", py::call_guard()) - .def("export_lookup", &storm::builder::ExplicitModelBuilder::exportExplicitStateLookup, "Export a lookup model"); - } else if constexpr (std::is_same_v) { - m.def("_build_symbolic_parametric_model_from_symbolic_description", &buildSymbolicModel, - "Build the parametric model in symbolic representation", py::arg("model_description"), - py::arg("formulas") = std::vector>(), py::arg("environment")); - m.def("make_sparse_model_builder_parametric", &storm::api::makeExplicitModelBuilder, "Construct a builder instance", - py::arg("model_description"), py::arg("options"), py::arg("action_mask") = nullptr, - py::arg("exploration_options") = typename storm::builder::ExplicitModelBuilder::Options()); - py::classh>(m, "ExplicitParametricModelBuilder", "Model builder for sparse models") - .def("build", &storm::builder::ExplicitModelBuilder::build, "Build the model", py::call_guard()) - .def("export_lookup", &storm::builder::ExplicitModelBuilder::exportExplicitStateLookup, "Export a lookup model"); - } else if constexpr (std::is_same_v) { - m.def("make_sparse_model_builder_exact", &storm::api::makeExplicitModelBuilder, "Construct a builder instance", - py::arg("model_description"), py::arg("options"), py::arg("action_mask") = nullptr, - py::arg("exploration_options") = typename storm::builder::ExplicitModelBuilder::Options()); } } @@ -242,9 +234,11 @@ void define_build(py::module& m) { .def("set_build_all_reward_models", &storm::builder::BuilderOptions::setBuildAllRewardModels, "Build with all reward models", py::arg("new_value") = true); - py::classh> actionmask(m, "ActionMaskDouble"); - py::classh> actfuncmask(m, "StateValuationFunctionActionMaskDouble", actionmask); - actfuncmask.def(py::init>(), py::arg("f")); + auto actionmask = + stormpy::bindings::bindTemplateClass>(m, "ActionMask", stormpy::bindings::typeIndex(), "Mask for actions"); + stormpy::bindings::bindTemplateClass>( + m, "StateValuationFunctionActionMask", stormpy::bindings::typeIndex(), "Action mask based on state valuations", actionmask) + .def(py::init>(), py::arg("f")); } void define_optimality_type(py::module& m) { @@ -270,28 +264,8 @@ void exportDRN(std::shared_ptr> model, s template void define_export_drn(py::module& m) { - std::string prefix; - std::string suffix; - if constexpr (std::is_same_v) { - prefix = ""; - suffix = ""; - } else if constexpr (std::is_same_v) { - prefix = "_exact"; - suffix = ""; - } else if constexpr (std::is_same_v) { - prefix = "_parametric"; - suffix = ""; - } else if constexpr (std::is_same_v) { - prefix = ""; - suffix = "_interval"; - } else if constexpr (std::is_same_v) { - prefix = "_exact"; - suffix = "_interval"; - } - - m.def(("_export" + prefix + "_to_drn" + suffix).c_str(), &exportDRN, - ("Export " + (std::is_same_v ? std::string("parametric ") : std::string()) + "model in DRN format").c_str(), - py::arg("model"), py::arg("file"), py::arg("options") = storm::io::DirectEncodingExporterOptions()); + m.def("_export_to_drn", &exportDRN, "Export model in DRN format", py::arg("model"), py::arg("file"), + py::arg("options") = storm::io::DirectEncodingExporterOptions()); } void define_export(py::module& m) { diff --git a/src/core/counterexample.cpp b/src/core/counterexample.cpp index 50d79a6b9b..7b7767fe98 100644 --- a/src/core/counterexample.cpp +++ b/src/core/counterexample.cpp @@ -3,6 +3,8 @@ #include #include +#include "src/binding_type_index.h" + using namespace storm::counterexamples; // Define python bindings @@ -37,7 +39,8 @@ void define_counterexamples(py::module& m) { using CexGeneratorStats = SMTMinimalLabelSetGenerator::GeneratorStats; - py::classh(m, "SMTCounterExampleGeneratorStats", "Stats for highlevel counterexample generation") + stormpy::bindings::bindTemplateClass(m, "SMTCounterExampleGeneratorStats", stormpy::bindings::typeIndex(), + "Stats for highlevel counterexample generation") .def(py::init<>()) .def_readonly("analysis_time", &CexGeneratorStats::analysisTime) .def_readonly("setup_time", &CexGeneratorStats::setupTime) @@ -47,7 +50,8 @@ void define_counterexamples(py::module& m) { .def_readonly("iterations", &CexGeneratorStats::iterations); using CexGeneratorOptions = SMTMinimalLabelSetGenerator::Options; - py::classh(m, "SMTCounterExampleGeneratorOptions", "Options for highlevel counterexample generation") + stormpy::bindings::bindTemplateClass(m, "SMTCounterExampleGeneratorOptions", stormpy::bindings::typeIndex(), + "Options for highlevel counterexample generation") .def(py::init<>()) .def_readwrite("check_threshold_feasible", &CexGeneratorOptions::checkThresholdFeasible) .def_readwrite("encode_reachability", &CexGeneratorOptions::encodeReachability) @@ -57,7 +61,8 @@ void define_counterexamples(py::module& m) { .def_readwrite("maximum_counterexamples", &CexGeneratorOptions::maximumCounterexamples) .def_readwrite("continue_after_first_counterexample", &CexGeneratorOptions::continueAfterFirstCounterexampleUntil) .def_readwrite("maximum_iterations_after_counterexample", &CexGeneratorOptions::maximumExtraIterations); - py::classh>(m, "SMTCounterExampleGenerator", "Highlevel Counterexample Generator with SMT as backend") + stormpy::bindings::bindTemplateClass>(m, "SMTCounterExampleGenerator", stormpy::bindings::typeIndex(), + "Highlevel Counterexample Generator with SMT as backend") .def_static("precompute", &SMTMinimalLabelSetGenerator::precompute, "Precompute input for counterexample generation", py::arg("env"), py::arg("symbolic_model"), py::arg("model"), py::arg("formula")) .def_static("build", &SMTMinimalLabelSetGenerator::computeCounterexampleLabelSet, "Compute counterexample", py::arg("env"), py::arg("stats"), @@ -66,7 +71,8 @@ void define_counterexamples(py::module& m) { ; using CexInput = SMTMinimalLabelSetGenerator::CexInput; - py::classh(m, "SMTCounterExampleInput", "Precomputed input for counterexample generation") + stormpy::bindings::bindTemplateClass(m, "SMTCounterExampleInput", stormpy::bindings::typeIndex(), + "Precomputed input for counterexample generation") .def("add_reward_and_threshold", &CexInput::addRewardThresholdCombination, "add another reward structure and threshold", py::arg("reward_name"), py::arg("threshold")); } diff --git a/src/core/modelchecking.cpp b/src/core/modelchecking.cpp index 072781877d..63d213fa0e 100644 --- a/src/core/modelchecking.cpp +++ b/src/core/modelchecking.cpp @@ -11,6 +11,7 @@ #include #include +#include "src/binding_type_index.h" #include "src/core/result.h" template @@ -141,11 +142,10 @@ storm::storage::BitVector getReachableStates(storm::models::sparse::Model -void define_check_task(py::module& m, std::string const& name) { +void define_check_task(py::module& m) { // CheckTask - py::classh>(m, name.c_str(), "Task for model checking") + stormpy::bindings::bindTemplateClass>(m, "CheckTask", stormpy::bindings::typeIndex(), "Task for model checking") .def(py::init(), py::arg("formula"), py::arg("only_initial_states") = false) .def("set_produce_schedulers", &CheckTask::setProduceSchedulers, "Set whether schedulers should be produced (if possible)", py::arg("produce_schedulers") = true) @@ -155,60 +155,34 @@ void define_check_task(py::module& m, std::string const& name) { } template -void define_modelchecking_mdefs(py::module& m) { - if constexpr (std::is_same_v) { - m.def("_get_reachable_states_double", &getReachableStates, py::arg("model"), py::arg("initial_states"), py::arg("constraint_states"), - py::arg("target_states"), py::arg("maximal_steps") = boost::none, py::arg("choice_filter") = boost::none); - m.def("_compute_expected_number_of_visits_double", &getExpectedNumberOfVisits, py::arg("env"), py::arg("model")); - m.def("_compute_steady_state_distribution_double", &getSteadyStateDistribution, py::arg("env"), py::arg("model")); - m.def("_model_checking_fully_observable", &modelCheckingFullyObservableSparseEngine, py::arg("model"), py::arg("task"), py::arg("environment")); - m.def("_model_checking_sparse_engine", &modelCheckingSparseEngine, "Perform model checking using the sparse engine", py::arg("model"), - py::arg("task"), py::arg("environment")); - m.def("_model_checking_dd_engine", &modelCheckingDdEngine, "Perform model checking using the dd engine", - py::arg("model"), py::arg("task"), py::arg("environment")); - m.def("_model_checking_hybrid_engine", &modelCheckingHybridEngine, "Perform model checking using the hybrid engine", - py::arg("model"), py::arg("task"), py::arg("environment")); - m.def("_compute_prob01states_double", &computeProb01, "Compute prob-0-1 states", py::arg("model"), py::arg("phi_states"), - py::arg("psi_states")); - m.def("_compute_prob01states_min_double", &computeProb01min, "Compute prob-0-1 states (min)", py::arg("model"), py::arg("phi_states"), - py::arg("psi_states")); - m.def("_compute_prob01states_max_double", &computeProb01max, "Compute prob-0-1 states (max)", py::arg("model"), py::arg("phi_states"), - py::arg("psi_states")); - m.def("_multi_objective_model_checking_double", &multiObjectiveModelChecking, "Run multi-objective model checking", py::arg("model"), - py::arg("formula"), py::arg("environment")); - } else if constexpr (std::is_same_v) { - m.def("_get_reachable_states_exact", &getReachableStates, py::arg("model"), py::arg("initial_states"), - py::arg("constraint_states"), py::arg("target_states"), py::arg("maximal_steps") = boost::none, py::arg("choice_filter") = boost::none); - m.def("_compute_expected_number_of_visits_exact", &getExpectedNumberOfVisits, py::arg("env"), py::arg("model")); - m.def("_compute_steady_state_distribution_exact", &getSteadyStateDistribution, py::arg("env"), py::arg("model")); - m.def("_exact_model_checking_fully_observable", &modelCheckingFullyObservableSparseEngine, py::arg("model"), py::arg("task"), +void define_modelchecking_typed(py::module& m) { + m.def("_get_reachable_states", &getReachableStates, py::arg("model"), py::arg("initial_states"), py::arg("constraint_states"), + py::arg("target_states"), py::arg("maximal_steps") = boost::none, py::arg("choice_filter") = boost::none); + m.def("_model_checking_sparse_engine", &modelCheckingSparseEngine, "Perform model checking using the sparse engine", py::arg("model"), + py::arg("task"), py::arg("environment")); + if constexpr (std::is_same_v || std::is_same_v) { + m.def("_compute_expected_number_of_visits", &getExpectedNumberOfVisits, py::arg("env"), py::arg("model")); + m.def("_compute_steady_state_distribution", &getSteadyStateDistribution, py::arg("env"), py::arg("model")); + m.def("_model_checking_fully_observable", &modelCheckingFullyObservableSparseEngine, py::arg("model"), py::arg("task"), py::arg("environment")); - m.def("_exact_model_checking_sparse_engine", &modelCheckingSparseEngine, "Perform model checking using the sparse engine", - py::arg("model"), py::arg("task"), py::arg("environment")); - m.def("_multi_objective_model_checking_exact", &multiObjectiveModelChecking, "Run multi-objective model checking", - py::arg("model"), py::arg("formula"), py::arg("environment")); - } else if constexpr (std::is_same_v) { - m.def("_get_reachable_states_rf", &getReachableStates, py::arg("model"), py::arg("initial_states"), - py::arg("constraint_states"), py::arg("target_states"), py::arg("maximal_steps") = boost::none, py::arg("choice_filter") = boost::none); - m.def("_parametric_model_checking_sparse_engine", &modelCheckingSparseEngine, - "Perform parametric model checking using the sparse engine", py::arg("model"), py::arg("task"), py::arg("environment")); - m.def("_parametric_model_checking_dd_engine", &modelCheckingDdEngine, - "Perform parametric model checking using the dd engine", py::arg("model"), py::arg("task"), py::arg("environment")); - m.def("_parametric_model_checking_hybrid_engine", &modelCheckingHybridEngine, - "Perform parametric model checking using the hybrid engine", py::arg("model"), py::arg("task"), py::arg("environment")); - m.def("_compute_prob01states_rationalfunc", &computeProb01, "Compute prob-0-1 states", py::arg("model"), py::arg("phi_states"), - py::arg("psi_states")); - m.def("_compute_prob01states_min_rationalfunc", &computeProb01min, "Compute prob-0-1 states (min)", py::arg("model"), - py::arg("phi_states"), py::arg("psi_states")); - m.def("_compute_prob01states_max_rationalfunc", &computeProb01max, "Compute prob-0-1 states (max)", py::arg("model"), - py::arg("phi_states"), py::arg("psi_states")); + m.def("_multi_objective_model_checking", &multiObjectiveModelChecking, "Run multi-objective model checking", py::arg("model"), + py::arg("formula"), py::arg("environment")); } + m.def("_model_checking_dd_engine", &modelCheckingDdEngine, "Perform model checking using the dd engine", + py::arg("model"), py::arg("task"), py::arg("environment")); + m.def("_model_checking_hybrid_engine", &modelCheckingHybridEngine, "Perform model checking using the hybrid engine", + py::arg("model"), py::arg("task"), py::arg("environment")); + m.def("_compute_prob01states", &computeProb01, "Compute prob-0-1 states", py::arg("model"), py::arg("phi_states"), py::arg("psi_states")); + m.def("_compute_prob01states_min", &computeProb01min, "Compute prob-0-1 states (min)", py::arg("model"), py::arg("phi_states"), + py::arg("psi_states")); + m.def("_compute_prob01states_max", &computeProb01max, "Compute prob-0-1 states (max)", py::arg("model"), py::arg("phi_states"), + py::arg("psi_states")); } void define_modelchecking(py::module& m) { py::classh mchint(m, "ModelCheckerHint", "Information that may accelerate the model checking process"); - py::classh>(m, "ExplicitModelCheckerHintDouble", - "Information that may accelerate an explicit state model checker", mchint) + stormpy::bindings::bindTemplateClass>( + m, "ExplicitModelCheckerHint", stormpy::bindings::typeIndex(), "Information that may accelerate an explicit state model checker", mchint) .def(py::init<>()) .def("set_scheduler_hint", py::overload_cast> const&>( @@ -221,10 +195,6 @@ void define_modelchecking(py::module& m) { py::overload_cast> const&>(&storm::modelchecker::ExplicitModelCheckerHint::setResultHint), "result_hint"_a); - define_modelchecking_mdefs(m); - define_modelchecking_mdefs(m); - define_modelchecking_mdefs(m); - m.def("check_interval_dtmc", &checkIntervalDtmc, "Check interval DTMC"); m.def("check_exact_interval_dtmc", &checkRationalIntervalDtmc, "Check exact interval DTMC"); m.def("check_interval_mdp", &checkIntervalMdp, "Check interval MDP"); @@ -233,6 +203,10 @@ void define_modelchecking(py::module& m) { m.def("compute_transient_probabilities", &computeTransientProbabilities, "Compute transient probabilities"); } -template void define_check_task(py::module&, std::string const&); -template void define_check_task(py::module&, std::string const&); -template void define_check_task(py::module&, std::string const&); \ No newline at end of file +template void define_check_task(py::module&); +template void define_check_task(py::module&); +template void define_check_task(py::module&); + +template void define_modelchecking_typed(py::module&); +template void define_modelchecking_typed(py::module&); +template void define_modelchecking_typed(py::module&); diff --git a/src/core/modelchecking.h b/src/core/modelchecking.h index ffe2139307..8211c34dea 100644 --- a/src/core/modelchecking.h +++ b/src/core/modelchecking.h @@ -3,6 +3,8 @@ #include "src/core/common.h" template -void define_check_task(py::module& m, std::string const& name); +void define_check_task(py::module& m); +template +void define_modelchecking_typed(py::module& m); void define_modelchecking(py::module& m); diff --git a/src/core/multiobjective.cpp b/src/core/multiobjective.cpp index 606a75e9fc..a0c21afa15 100644 --- a/src/core/multiobjective.cpp +++ b/src/core/multiobjective.cpp @@ -9,6 +9,8 @@ #include #include +#include "src/binding_type_index.h" + // Helper class to avoid that we also need to bind the preprocessing. template std::pair>>, @@ -22,12 +24,13 @@ makeWeightedObjectiveMDPModelChecker(storm::Environment const& env, storm::model } template -void define_multiobjective(py::module& m, std::string const& vtSuffix) { - m.def(("_make_weighted_objective_mdp_model_checker_" + vtSuffix).c_str(), &makeWeightedObjectiveMDPModelChecker, py::arg("env"), - py::arg("model"), py::arg("formula"), py::arg("compute_scheduler") = false); +void define_multiobjective(py::module& m) { + m.def("_make_weighted_objective_mdp_model_checker", &makeWeightedObjectiveMDPModelChecker, py::arg("env"), py::arg("model"), py::arg("formula"), + py::arg("compute_scheduler") = false); using PcaaWeightVectorChecker = storm::modelchecker::multiobjective::PcaaWeightVectorChecker>; - py::classh weightedObjectiveMdpModelChecker(m, ("WeightedObjectiveMdpModelChecker" + vtSuffix).c_str()); + auto weightedObjectiveMdpModelChecker = stormpy::bindings::bindTemplateClass( + m, "WeightedObjectiveMdpModelChecker", stormpy::bindings::typeIndex(), "Model checker for weighted multi-objective queries"); weightedObjectiveMdpModelChecker.def("check", &PcaaWeightVectorChecker::check, py::arg("env"), py::arg("weight_vector")) .def("get_achievable_point", &PcaaWeightVectorChecker::getAchievablePoint) .def("get_optimal_weighted_sum", &PcaaWeightVectorChecker::getOptimalWeightedSum, @@ -36,5 +39,5 @@ void define_multiobjective(py::module& m, std::string const& vtSuffix) { .def("set_weighted_precision", &PcaaWeightVectorChecker::setWeightedPrecision, py::arg("value"), "A smaller value means a higher precision."); } -template void define_multiobjective(py::module&, std::string const&); -template void define_multiobjective(py::module&, std::string const&); +template void define_multiobjective(py::module&); +template void define_multiobjective(py::module&); diff --git a/src/core/multiobjective.h b/src/core/multiobjective.h index 8e4f3ef1d5..5ed00fb526 100644 --- a/src/core/multiobjective.h +++ b/src/core/multiobjective.h @@ -3,4 +3,4 @@ #include "src/core/common.h" template -void define_multiobjective(py::module& m, std::string const& vtSuffix); +void define_multiobjective(py::module& m); diff --git a/src/core/result.cpp b/src/core/result.cpp index 55368c39b4..aad93c2f78 100644 --- a/src/core/result.cpp +++ b/src/core/result.cpp @@ -10,6 +10,8 @@ #include #include +#include "src/binding_type_index.h" + template std::shared_ptr createFilterInitialStatesSparse(std::shared_ptr> model) { return std::make_unique>(model->getInitialStates()); @@ -72,16 +74,18 @@ void define_result(py::module& m) { py::classh qualitativeCheckResult(m, "_QualitativeCheckResult", "Abstract class for qualitative model checking results", checkResult); - py::classh>( - m, "SymbolicQualitativeCheckResult", "Symbolic qualitative model checking result", qualitativeCheckResult) + stormpy::bindings::bindTemplateClass>( + m, "SymbolicQualitativeCheckResult", stormpy::bindings::typeIndex(), "Symbolic qualitative model checking result", + qualitativeCheckResult) .def("get_truth_values", &storm::modelchecker::SymbolicQualitativeCheckResult::getTruthValuesVector, "Get Dd representing the truth values"); } template -void define_typed_result(py::module& m, std::string const& vtSuffix) { - py::classh, storm::modelchecker::QualitativeCheckResult>( - m, ("Explicit" + vtSuffix + "QualitativeCheckResult").c_str(), "Explicit qualitative model checking result") +void define_typed_result(py::module& m) { + auto const index = stormpy::bindings::typeIndex(); + stormpy::bindings::bindTemplateClass, storm::modelchecker::QualitativeCheckResult>( + m, "ExplicitQualitativeCheckResult", index, "Explicit qualitative model checking result") .def( "at", [](storm::modelchecker::ExplicitQualitativeCheckResult const& result, storm::storage::sparse::state_type state) { @@ -93,8 +97,9 @@ void define_typed_result(py::module& m, std::string const& vtSuffix) { .def_property_readonly( "scheduler", [](storm::modelchecker::ExplicitQualitativeCheckResult const& res) { return res.getScheduler(); }, "Get scheduler"); - py::classh, storm::modelchecker::CheckResult> quantitativeCheckResult( - m, ("_" + vtSuffix + "QuantitativeCheckResult").c_str(), "Abstract class for quantitative model checking results"); + auto quantitativeCheckResult = + stormpy::bindings::bindTemplateClass, storm::modelchecker::CheckResult>( + m, "QuantitativeCheckResult", index, "Abstract class for quantitative model checking results"); quantitativeCheckResult .def_property_readonly( "min", [](storm::modelchecker::QuantitativeCheckResult const& res) { return storm::utility::narrow(res.getMin()); }, @@ -103,8 +108,8 @@ void define_typed_result(py::module& m, std::string const& vtSuffix) { "max", [](storm::modelchecker::QuantitativeCheckResult const& res) { return storm::utility::narrow(res.getMax()); }, "Maximal value"); - py::classh>(m, ("Explicit" + vtSuffix + "QuantitativeCheckResult").c_str(), - "Explicit quantitative model checking result", quantitativeCheckResult) + stormpy::bindings::bindTemplateClass>( + m, "ExplicitQuantitativeCheckResult", index, "Explicit quantitative model checking result", quantitativeCheckResult) .def(py::init>(), py::arg("values")) .def( "at", @@ -118,37 +123,39 @@ void define_typed_result(py::module& m, std::string const& vtSuffix) { .def_property_readonly( "scheduler", [](storm::modelchecker::ExplicitQuantitativeCheckResult const& res) { return res.getScheduler(); }, "get scheduler"); - py::classh>( - m, ("Symbolic" + vtSuffix + "QuantitativeCheckResult").c_str(), "Symbolic quantitative model checking result", quantitativeCheckResult) + stormpy::bindings::bindTemplateClass>( + m, "SymbolicQuantitativeCheckResult", stormpy::bindings::typeIndex(), + "Symbolic quantitative model checking result", quantitativeCheckResult) .def("clone", [](storm::modelchecker::SymbolicQuantitativeCheckResult const& dd) { return dd.clone()->template asSymbolicQuantitativeCheckResult(); }) .def("get_values", &storm::modelchecker::SymbolicQuantitativeCheckResult::getValueVector); - py::classh>( - m, ("Hybrid" + vtSuffix + "QuantitativeCheckResult").c_str(), "Hybrid quantitative model checking result", quantitativeCheckResult) + stormpy::bindings::bindTemplateClass>( + m, "HybridQuantitativeCheckResult", stormpy::bindings::typeIndex(), "Hybrid quantitative model checking result", + quantitativeCheckResult) .def("get_values", &storm::modelchecker::HybridQuantitativeCheckResult::getExplicitValueVector, "Get model checking result values for all states"); if constexpr (std::is_same_v || std::is_same_v) { - py::classh, storm::modelchecker::CheckResult> pccheckresult( - m, (vtSuffix + "ParetoCurveCheckResult").c_str(), "Result for multiobjective model checking"); + auto pccheckresult = stormpy::bindings::bindTemplateClass, storm::modelchecker::CheckResult>( + m, "ParetoCurveCheckResult", index, "Result for multiobjective model checking"); pccheckresult.def("get_underapproximation", &storm::modelchecker::ParetoCurveCheckResult::getUnderApproximation) .def("get_overapproximation", &storm::modelchecker::ParetoCurveCheckResult::getOverApproximation); - py::classh> epccheckresult( - m, ("Explicit" + vtSuffix + "ParetoCurveCheckResult").c_str(), "Result for explicit multiobjective model checking", pccheckresult); + stormpy::bindings::bindTemplateClass>( + m, "ExplicitParetoCurveCheckResult", index, "Result for explicit multiobjective model checking", pccheckresult); - m.def(("create_filter_symbolic" + vtSuffix).c_str(), &createFilterSymbolic, + m.def("create_filter_symbolic", &createFilterSymbolic, "Creates a filter for the given states and a symbolic model", py::arg("model"), py::arg("states")); - m.def(("create_filter_initial_states_sparse" + vtSuffix).c_str(), &createFilterInitialStatesSparse, - "Create a filter for the initial states on a sparse model", py::arg("model")); - m.def(("create_filter_initial_states_symbolic" + vtSuffix).c_str(), &createFilterInitialStatesSymbolic, + m.def("create_filter_initial_states_sparse", &createFilterInitialStatesSparse, "Create a filter for the initial states on a sparse model", + py::arg("model")); + m.def("create_filter_initial_states_symbolic", &createFilterInitialStatesSymbolic, "Create a filter for the initial states on a symbolic model", py::arg("model")); } } -template void define_typed_result(py::module& m, std::string const& vtSuffix); -template void define_typed_result(py::module& m, std::string const& vtSuffix); -template void define_typed_result(py::module& m, std::string const& vtSuffix); +template void define_typed_result(py::module& m); +template void define_typed_result(py::module& m); +template void define_typed_result(py::module& m); diff --git a/src/core/result.h b/src/core/result.h index fbf70ad2f0..f2a3912c2a 100644 --- a/src/core/result.h +++ b/src/core/result.h @@ -5,4 +5,4 @@ void define_result(py::module& m); template -void define_typed_result(py::module& m, std::string const& vtSuffix); +void define_typed_result(py::module& m); diff --git a/src/core/simulator.cpp b/src/core/simulator.cpp index 3af41e9717..22774ac763 100644 --- a/src/core/simulator.cpp +++ b/src/core/simulator.cpp @@ -4,13 +4,15 @@ #include #include +#include "src/binding_type_index.h" + template using PLSim = storm::simulator::DiscreteTimePrismProgramSimulator; template -void define_sparse_model_simulator(py::module& m, std::string const& vtSuffix) { - py::classh> dtsmsd(m, ("_DiscreteTimeSparseModelSimulator" + vtSuffix).c_str(), - "Simulator for sparse discrete-time models in memory (for ValueType)"); +void define_sparse_model_simulator(py::module& m) { + auto dtsmsd = stormpy::bindings::bindTemplateClass>( + m, "DiscreteTimeSparseModelSimulator", stormpy::bindings::typeIndex(), "Simulator for sparse discrete-time models in memory"); dtsmsd.def(py::init const&>()); dtsmsd.def("set_seed", &storm::simulator::DiscreteTimeSparseModelSimulator::setSeed, py::arg("seed")); dtsmsd.def("step", &storm::simulator::DiscreteTimeSparseModelSimulator::step, py::arg("action")); @@ -21,9 +23,9 @@ void define_sparse_model_simulator(py::module& m, std::string const& vtSuffix) { } template -void define_prism_program_simulator(py::module& m, std::string const& vtSuffix) { - py::classh> dtpps(m, ("_DiscreteTimePrismProgramSimulator" + vtSuffix).c_str(), - "Simulator for prism programs"); +void define_prism_program_simulator(py::module& m) { + auto dtpps = stormpy::bindings::bindTemplateClass>( + m, "DiscreteTimePrismProgramSimulator", stormpy::bindings::typeIndex(), "Simulator for prism programs"); dtpps.def(py::init(), py::arg("program"), py::arg("options")); dtpps.def("set_seed", &storm::simulator::DiscreteTimePrismProgramSimulator::setSeed, py::arg("seed")); dtpps.def("step", &storm::simulator::DiscreteTimePrismProgramSimulator::step, py::arg("action_index"), @@ -56,7 +58,7 @@ void define_prism_program_simulator(py::module& m, std::string const& vtSuffix) "Get names of the rewards provided by the simulator"); } -template void define_sparse_model_simulator(py::module& m, std::string const& vtSuffix); -template void define_sparse_model_simulator(py::module& m, std::string const& vtSuffix); +template void define_sparse_model_simulator(py::module& m); +template void define_sparse_model_simulator(py::module& m); -template void define_prism_program_simulator(py::module& m, std::string const& vtSuffix); +template void define_prism_program_simulator(py::module& m); diff --git a/src/core/simulator.h b/src/core/simulator.h index e110777f04..ca05908043 100644 --- a/src/core/simulator.h +++ b/src/core/simulator.h @@ -3,7 +3,7 @@ #include "src/core/common.h" template -void define_sparse_model_simulator(py::module& m, std::string const& vtSuffix); +void define_sparse_model_simulator(py::module& m); template -void define_prism_program_simulator(py::module& m, std::string const& vtSuffix); \ No newline at end of file +void define_prism_program_simulator(py::module& m); \ No newline at end of file diff --git a/src/core/transformation.cpp b/src/core/transformation.cpp index e71d62aa6e..12ffb636f0 100644 --- a/src/core/transformation.cpp +++ b/src/core/transformation.cpp @@ -7,6 +7,8 @@ #include #include +#include "src/binding_type_index.h" + // Thin wrappers. template storm::transformer::SubsystemBuilderReturnType constructSubsystem(storm::models::sparse::Model const& originalModel, @@ -30,31 +32,7 @@ typename storm::transformer::EndComponentEliminator::EndComponentElim return storm::transformer::EndComponentEliminator::transform(matrix, subsystemStates, possibleECRows, addSinkRowStates, addSelfLoopAtSinkStates); } -template -void define_transformation_mdef(py::module& m) { - std::string type, desc; - if constexpr (std::is_same_v) { - type = ""; - desc = ""; - } else if constexpr (std::is_same_v) { - type = "_parametric"; - desc = "parametric "; - } - - m.def(("_transform_to_sparse" + type + "_model").c_str(), &storm::api::transformSymbolicToSparseModel, - ("Transform symbolic " + desc + "model into sparse " + desc + "model").c_str(), py::arg("model"), - py::arg("formulae") = std::vector>()); - m.def(("_transform_to_discrete_time" + type + "_model").c_str(), &transformContinuousToDiscreteTimeSparseModel, - ("Transform " + desc + "continuous time model to " + desc + "discrete time model").c_str(), py::arg("model"), - py::arg("formulae") = std::vector>()); - m.def(("_eliminate_non_markovian_chains" + type).c_str(), &storm::api::eliminateNonMarkovianChains, - "Eliminate chains of non-Markovian states in Markov automaton.", py::arg("ma"), py::arg("formulae"), py::arg("label_behavior")); -} - void define_transformation(py::module& m) { - define_transformation_mdef(m); - define_transformation_mdef(m); - py::classh(m, "SubsystemBuilderOptions", "Options for constructing the subsystem") .def(py::init<>()) .def_readwrite("check_transitions_outside", &storm::transformer::SubsystemBuilderOptions::checkTransitionsOutside) @@ -73,9 +51,23 @@ void define_transformation(py::module& m) { } template -void define_transformation_typed(py::module& m, std::string const& vtSuffix) { - py::classh>(m, ("SubsystemBuilderReturnType" + vtSuffix).c_str(), - "Result of the construction of a subsystem") +void define_transformation_typed(py::module& m) { + auto const index = stormpy::bindings::typeIndex(); + if constexpr (!storm::IsIntervalType) { + m.def("_transform_to_sparse_model", &storm::api::transformSymbolicToSparseModel, + "Transform a symbolic model into a sparse model", py::arg("model"), + py::arg("formulae") = std::vector>()); + } + m.def("_transform_to_discrete_time_model", &transformContinuousToDiscreteTimeSparseModel, + "Transform a continuous-time model into a discrete-time model", py::arg("model"), + py::arg("formulae") = std::vector>()); + if constexpr (!storm::IsIntervalType) { + m.def("_eliminate_non_markovian_chains", &storm::api::eliminateNonMarkovianChains, + "Eliminate chains of non-Markovian states in a Markov automaton", py::arg("ma"), py::arg("formulae"), py::arg("label_behavior")); + } + + stormpy::bindings::bindTemplateClass>(m, "SubsystemBuilderReturnType", index, + "Result of the construction of a subsystem") .def_readonly("model", &storm::transformer::SubsystemBuilderReturnType::model, "the submodel") .def_readonly("new_to_old_state_mapping", &storm::transformer::SubsystemBuilderReturnType::newToOldStateIndexMapping, "for each state in result, the state index in the original model") @@ -85,10 +77,10 @@ void define_transformation_typed(py::module& m, std::string const& vtSuffix) { "Actions of the subsystem available in the original system") .def_readonly("deadlock_label", &storm::transformer::SubsystemBuilderReturnType::deadlockLabel, "If set, deadlock states have been introduced and have been assigned this label"); - m.def(("_construct_subsystem_" + vtSuffix).c_str(), &constructSubsystem, "build a subsystem of a sparse model"); + m.def("_construct_subsystem", &constructSubsystem, "build a subsystem of a sparse model"); - py::classh::EndComponentEliminatorReturnType>( - m, ("EndComponentEliminatorReturnType" + vtSuffix).c_str(), "Container for result of endcomponent elimination") + stormpy::bindings::bindTemplateClass::EndComponentEliminatorReturnType>( + m, "EndComponentEliminatorReturnType", index, "Container for result of endcomponent elimination") .def_readonly("matrix", &storm::transformer::EndComponentEliminator::EndComponentEliminatorReturnType::matrix, "The resulting matrix") .def_readonly("new_to_old_row_mapping", &storm::transformer::EndComponentEliminator::EndComponentEliminatorReturnType::newToOldRowMapping, "Index mapping that gives for each row of the new matrix the corresponding row in the original matrix") @@ -97,24 +89,24 @@ void define_transformation_typed(py::module& m, std::string const& vtSuffix) { "For each state of the original matrix (and subsystem) the corresponding state in the result. Removed states are mapped to the EC.") .def_readonly("sink_rows", &storm::transformer::EndComponentEliminator::EndComponentEliminatorReturnType::sinkRows, "Rows that indicate staying in the EC forever"); - m.def(("_eliminate_end_components_" + vtSuffix).c_str(), &eliminateECs, "Eliminate ECs in the subsystem", py::arg("matrix"), - py::arg("subsystem"), py::arg("possible_ec_rows"), py::arg("addSinkRowStates"), py::arg("addSelfLoopAtSinkStates")); + m.def("_eliminate_end_components", &eliminateECs, "Eliminate ECs in the subsystem", py::arg("matrix"), py::arg("subsystem"), + py::arg("possible_ec_rows"), py::arg("addSinkRowStates"), py::arg("addSelfLoopAtSinkStates")); } template -void define_transformation_typed_only_numbers(py::module& m, std::string const& vtSuffix) { - py::classh>(m, ("AddUncertainty" + vtSuffix).c_str(), - "Transform model into interval model with specified uncertainty") +void define_transformation_typed_only_numbers(py::module& m) { + stormpy::bindings::bindTemplateClass>(m, "AddUncertainty", stormpy::bindings::typeIndex(), + "Transform model into interval model with specified uncertainty") .def(py::init> const&>(), py::arg("model")) .def("transform", &storm::transformer::AddUncertainty::transform, "Transform the model", py::arg("additive_uncertainty"), py::arg("minimal_value") = storm::utility::convertNumber(0.0001), py::arg("max_successors") = std::optional{}); } -template void define_transformation_typed(py::module& m, std::string const& vtSuffix); -template void define_transformation_typed(py::module& m, std::string const& vtSuffix); -template void define_transformation_typed(py::module& m, std::string const& vtSuffix); -template void define_transformation_typed(py::module& m, std::string const& vtSuffix); -template void define_transformation_typed(py::module& m, std::string const& vtSuffix); +template void define_transformation_typed(py::module& m); +template void define_transformation_typed(py::module& m); +template void define_transformation_typed(py::module& m); +template void define_transformation_typed(py::module& m); +template void define_transformation_typed(py::module& m); -template void define_transformation_typed_only_numbers(py::module& m, std::string const& vtSuffix); -template void define_transformation_typed_only_numbers(py::module& m, std::string const& vtSuffix); +template void define_transformation_typed_only_numbers(py::module& m); +template void define_transformation_typed_only_numbers(py::module& m); diff --git a/src/core/transformation.h b/src/core/transformation.h index 1fda1d26ad..862ca870da 100644 --- a/src/core/transformation.h +++ b/src/core/transformation.h @@ -4,6 +4,6 @@ void define_transformation(py::module& m); template -void define_transformation_typed(py::module& m, std::string const& suffix); +void define_transformation_typed(py::module& m); template -void define_transformation_typed_only_numbers(py::module& m, std::string const& vtSuffix); +void define_transformation_typed_only_numbers(py::module& m); diff --git a/src/core/valuetype.cpp b/src/core/valuetype.cpp index ca377e3806..31f950c09e 100644 --- a/src/core/valuetype.cpp +++ b/src/core/valuetype.cpp @@ -8,6 +8,7 @@ // Bindings that return a representative value of each Storm C++ ValueType back to Python. // These are used to check that Storm's C++ ValueTypes match stormpy's Python types. void define_value_types(py::module& m) { + m.attr("DdType") = py::module::import("stormpy.storage._storage").attr("DdType"); m.def("_valuetype_double", []() { return storm::utility::one(); }, "Representative value of C++ type 'double'"); m.def( "_valuetype_rationalnumber", []() { return storm::utility::one(); }, "Representative value of C++ type 'storm::RationalNumber'"); diff --git a/src/mod_core.cpp b/src/mod_core.cpp index be567941a3..a1083e692c 100644 --- a/src/mod_core.cpp +++ b/src/mod_core.cpp @@ -32,28 +32,31 @@ PYBIND11_MODULE(_core, m) { define_optimality_type(m); define_export(m); define_result(m); - define_typed_result(m, ""); - define_typed_result(m, "Exact"); - define_typed_result(m, "Parametric"); - define_check_task(m, "CheckTask"); - define_check_task(m, "ExactCheckTask"); - define_check_task(m, "ParametricCheckTask"); + define_typed_result(m); + define_typed_result(m); + define_typed_result(m); + define_check_task(m); + define_check_task(m); + define_check_task(m); + define_modelchecking_typed(m); + define_modelchecking_typed(m); + define_modelchecking_typed(m); define_modelchecking(m); - define_multiobjective(m, "Double"); - define_multiobjective(m, "Exact"); + define_multiobjective(m); + define_multiobjective(m); define_counterexamples(m); define_bisimulation(m); define_input(m); define_graph_constraints(m); define_transformation(m); - define_transformation_typed(m, "Double"); - define_transformation_typed(m, "Exact"); - define_transformation_typed(m, "RatFunc"); - define_transformation_typed(m, "Interval"); - define_transformation_typed(m, "RationalInterval"); - define_transformation_typed_only_numbers(m, "Double"); - define_transformation_typed_only_numbers(m, "Exact"); - define_sparse_model_simulator(m, "Double"); - define_sparse_model_simulator(m, "Exact"); - define_prism_program_simulator(m, "Double"); + define_transformation_typed(m); + define_transformation_typed(m); + define_transformation_typed(m); + define_transformation_typed(m); + define_transformation_typed(m); + define_transformation_typed_only_numbers(m); + define_transformation_typed_only_numbers(m); + define_sparse_model_simulator(m); + define_sparse_model_simulator(m); + define_prism_program_simulator(m); } diff --git a/src/mod_storage.cpp b/src/mod_storage.cpp index 54afb96494..96a2eb5a48 100644 --- a/src/mod_storage.cpp +++ b/src/mod_storage.cpp @@ -47,7 +47,6 @@ PYBIND11_MODULE(_storage, m) { define_sparse_matrix(m); define_sparse_matrix(m); define_sparse_matrix(m); - define_sparse_matrix_nt(m); define_symbolic_model(m); define_symbolic_model(m); define_symbolic_model(m); diff --git a/src/storage/matrix.cpp b/src/storage/matrix.cpp index 33b96d3034..8a57e758d0 100644 --- a/src/storage/matrix.cpp +++ b/src/storage/matrix.cpp @@ -20,19 +20,12 @@ using MatrixEntry = storm::storage::MatrixEntry, ValueTyp using RationalFunction = storm::RationalFunction; using row_index = unsigned int; -void define_sparse_matrix_nt(py::module& m) { - m.def( - "_topological_sort_double", - [](SparseMatrix& matrix, std::vector initial) { return storm::utility::graph::getTopologicalSort(matrix, initial); }, "matrix"_a, - "initial"_a, "get topological sort w.r.t. a transition matrix"); - m.def( - "_topological_sort_rf", - [](SparseMatrix& matrix, std::vector initial) { return storm::utility::graph::getTopologicalSort(matrix, initial); }, - "matrix"_a, "initial"_a, "get topological sort w.r.t. a transition matrix"); -} - template void define_sparse_matrix(py::module& m) { + m.def( + "_topological_sort", + [](SparseMatrix& matrix, std::vector initial) { return storm::utility::graph::getTopologicalSort(matrix, initial); }, "matrix"_a, + "initial"_a, "get topological sort w.r.t. a transition matrix"); auto const index = stormpy::bindings::typeIndex(); // MatrixEntry stormpy::bindings::bindTemplateClass>(m, "SparseMatrixEntry", index, "Entry of sparse matrix") diff --git a/src/storage/matrix.h b/src/storage/matrix.h index 517aa37575..c2fb91a6ba 100644 --- a/src/storage/matrix.h +++ b/src/storage/matrix.h @@ -4,5 +4,3 @@ template void define_sparse_matrix(py::module& m); - -void define_sparse_matrix_nt(py::module& m); diff --git a/src/storage/model.cpp b/src/storage/model.cpp index bbd7037289..4b31e81b6d 100644 --- a/src/storage/model.cpp +++ b/src/storage/model.cpp @@ -416,3 +416,5 @@ template void define_sparse_model(py::module& m); template void define_symbolic_model(py::module& m); template void define_symbolic_model(py::module& m); template void define_symbolic_model(py::module& m); +template void define_symbolic_model(py::module& m); +template void define_symbolic_model(py::module& m); diff --git a/tests/core/test_counterexample.py b/tests/core/test_counterexample.py new file mode 100644 index 0000000000..7b62d45aa0 --- /dev/null +++ b/tests/core/test_counterexample.py @@ -0,0 +1,6 @@ +import stormpy + + +def test_counterexample_options_default(): + options = stormpy.SMTCounterExampleGeneratorOptions() + assert type(options) is stormpy.SMTCounterExampleGeneratorOptions[float] diff --git a/tests/core/test_modelchecking.py b/tests/core/test_modelchecking.py index d33ea923f0..870e7ccdb1 100644 --- a/tests/core/test_modelchecking.py +++ b/tests/core/test_modelchecking.py @@ -1,11 +1,31 @@ +import pytest import stormpy -from helpers.helper import get_example_path +from helpers.helper import build_sparse_model, get_example_path from configurations import spot import math +def test_symbolic_filter_template_and_shared_dd_type(): + program = stormpy.parse_prism_program(get_example_path("dtmc", "die.pm")) + model = stormpy.build_symbolic_model(program) + result = stormpy.create_filter_initial_states_symbolic(model) + + assert stormpy.DdType is stormpy.storage.DdType + assert type(result) is stormpy.SymbolicQualitativeCheckResult[stormpy.DdType.Sylvan] + assert stormpy.Bdd.parameters_of(result.get_truth_values()) == (stormpy.DdType.Sylvan,) + + +@pytest.mark.parametrize("value_type", [float, stormpy.Rational, stormpy.RationalFunction]) +def test_initial_state_filter_overloads(value_type): + model = build_sparse_model(get_example_path("dtmc", "die.pm"), value_type) + result = stormpy.create_filter_initial_states_sparse(model) + + assert type(result) is stormpy.ExplicitQualitativeCheckResult[value_type] + assert result.get_truth_values() == model.initial_states_as_bitvector + + class TestModelChecking: def test_model_checking_prism_dtmc_label(self): program = stormpy.parse_prism_program(get_example_path("dtmc", "die.pm")) @@ -130,7 +150,7 @@ def test_model_checking_exact_interval_dtmc(self): env = stormpy.Environment() env.solver_environment.minmax_solver_environment.method = stormpy.MinMaxMethod.VALUE_ITERATION - task = stormpy.ExactCheckTask(formulas[0].raw_formula, only_initial_states=True) + task = stormpy.CheckTask[stormpy.Rational](formulas[0].raw_formula, only_initial_states=True) task.set_produce_schedulers() # Compute maximal task.set_uncertainty_resolution_mode(stormpy.UncertaintyResolutionMode.MAXIMIZE) @@ -150,7 +170,7 @@ def test_model_checking_exact_interval_mdp(self): env = stormpy.Environment() env.solver_environment.minmax_solver_environment.method = stormpy.MinMaxMethod.VALUE_ITERATION - task = stormpy.ExactCheckTask(formulas[0].raw_formula, only_initial_states=True) + task = stormpy.CheckTask[stormpy.Rational](formulas[0].raw_formula, only_initial_states=True) task.set_produce_schedulers() # Compute maximal robust task.set_uncertainty_resolution_mode(stormpy.UncertaintyResolutionMode.ROBUST) @@ -161,7 +181,7 @@ def test_model_checking_exact_interval_mdp(self): result = stormpy.check_exact_interval_mdp(model, task, env) assert math.isclose(result.at(initial_state), 0.5, rel_tol=1e-4) - task = stormpy.ExactCheckTask(formulas[1].raw_formula, only_initial_states=True) + task = stormpy.CheckTask[stormpy.Rational](formulas[1].raw_formula, only_initial_states=True) task.set_produce_schedulers() # Compute minimal robust task.set_uncertainty_resolution_mode(stormpy.UncertaintyResolutionMode.ROBUST) @@ -287,7 +307,7 @@ def test_model_checking_prism_dd_dtmc(self): assert model.nr_states == 13 assert model.nr_transitions == 20 result = stormpy.check_model_dd(model, formulas[0]) - assert type(result) is stormpy.SymbolicQuantitativeCheckResult + assert type(result) is stormpy.SymbolicQuantitativeCheckResult[stormpy.DdType.Sylvan, float] assert result.min == 0.0 assert result.max == 1.0 filter = stormpy.create_filter_initial_states_symbolic(model) @@ -303,7 +323,7 @@ def test_model_checking_prism_hybrid_dtmc(self): assert model.nr_states == 13 assert model.nr_transitions == 20 result = stormpy.check_model_hybrid(model, formulas[0]) - assert type(result) is stormpy.HybridQuantitativeCheckResult + assert type(result) is stormpy.HybridQuantitativeCheckResult[stormpy.DdType.Sylvan, float] values = result.get_values() assert len(values) == 3 assert math.isclose(values[0], 1 / 6) diff --git a/tests/core/test_transformation.py b/tests/core/test_transformation.py index 47d5efe837..7f7dd13231 100644 --- a/tests/core/test_transformation.py +++ b/tests/core/test_transformation.py @@ -1,9 +1,28 @@ +import pytest import stormpy -from helpers.helper import get_example_path +from helpers.helper import build_sparse_model, get_example_path import math +@pytest.mark.parametrize("value_type", [float, stormpy.Rational, stormpy.RationalFunction, stormpy.Interval, stormpy.RationalInterval]) +def test_subsystem_and_end_component_overloads(value_type, tmp_path): + model = build_sparse_model(get_example_path("dtmc", "die.pm"), value_type) + + states = stormpy.BitVector(model.nr_states, True) + choices = stormpy.BitVector(model.nr_choices, True) + subsystem = stormpy.construct_submodel(model, states, choices) + assert type(subsystem) is stormpy.SubsystemBuilderReturnType[value_type] + assert subsystem.model.nr_states == model.nr_states + result = stormpy.eliminate_ECs(model.transition_matrix, states, choices, states, True) + assert type(result) is stormpy.EndComponentEliminatorReturnType[value_type] + assert result.matrix.nr_columns == model.nr_states + + output = tmp_path / "model.drn" + stormpy.export_to_drn(model, str(output)) + assert f"@nr_states\n{model.nr_states}" in output.read_text() + + class TestTransformation: def test_transform_symbolic_dtmc_to_sparse(self): program = stormpy.parse_prism_program(get_example_path("dtmc", "crowds5_5.pm")) @@ -151,7 +170,7 @@ def test_add_uncertainty_dtmc(self): model = stormpy.build_model(program) assert type(model) is stormpy.SparseDtmc[float] assert model.nr_states == 13 - transformer = stormpy.AddUncertaintyDouble(model) + transformer = stormpy.AddUncertainty[float](model) interval_model = transformer.transform(0.1) assert type(interval_model) is stormpy.SparseDtmc[stormpy.Interval] assert interval_model.nr_states == 13 @@ -165,7 +184,7 @@ def test_add_uncertainty_exact_dtmc(self): program = stormpy.parse_prism_program(get_example_path("dtmc", "die.pm")) model = stormpy.build_sparse_exact_model(program) assert type(model) is stormpy.SparseDtmc[stormpy.Rational] - transformer = stormpy.AddUncertaintyExact(model) + transformer = stormpy.AddUncertainty[stormpy.Rational](model) interval_model = transformer.transform(stormpy.Rational("1/10")) assert type(interval_model) is stormpy.SparseDtmc[stormpy.RationalInterval] assert interval_model.nr_states == model.nr_states diff --git a/tests/helpers/helper.py b/tests/helpers/helper.py index cde009ac65..6b13e583c9 100644 --- a/tests/helpers/helper.py +++ b/tests/helpers/helper.py @@ -8,3 +8,19 @@ def get_example_path(*paths): return os.path.join(example_dir, *paths) + + +def build_sparse_model(path, value_type): + program = stormpy.parse_prism_program(path) + if value_type in (stormpy.Rational, stormpy.RationalInterval): + model = stormpy.build_sparse_exact_model(program) + elif value_type is stormpy.RationalFunction: + model = stormpy.build_parametric_model(program) + else: + model = stormpy.build_model(program) + # The following are hardcoded interval values for testing purposes + if value_type is stormpy.Interval: + model = stormpy.AddUncertainty(model).transform(0.01) + elif value_type is stormpy.RationalInterval: + model = stormpy.AddUncertainty(model).transform(stormpy.Rational("1/100")) + return model diff --git a/tests/pars/test_model_instantiator.py b/tests/pars/test_model_instantiator.py index 0e5c80c126..5176918426 100644 --- a/tests/pars/test_model_instantiator.py +++ b/tests/pars/test_model_instantiator.py @@ -74,12 +74,12 @@ def test_pdtmc_instantiation_checker(self): env = stormpy.Environment() inst_checker = stormpy.pars.ModelInstantiationChecker(env, model) assert type(inst_checker) is stormpy.pars.ModelInstantiationChecker[stormpy.ModelType.DTMC, float] - inst_checker.specify_formula(stormpy.ParametricCheckTask(formulas[0].raw_formula, True)) + inst_checker.specify_formula(stormpy.CheckTask[stormpy.RationalFunction](formulas[0].raw_formula, True)) inst_checker.set_graph_preserving(True) point = {p: stormpy.RationalFunctionCoefficient(1 / 2) for p in parameters} result = inst_checker.check(env, point) - assert isinstance(result, stormpy.ExplicitQuantitativeCheckResult) + assert isinstance(result, stormpy.ExplicitQuantitativeCheckResult[float]) res = result.at(model.initial_states[0]) assert isinstance(res, float) assert math.isclose(res, 29 / 15) @@ -92,12 +92,12 @@ def test_pdtmc_exact_instantiation_checker(self): parameters = model.collect_all_parameters() env = stormpy.Environment() inst_checker = stormpy.pars.ModelInstantiationChecker[stormpy.ModelType.DTMC, stormpy.Rational](env, model) - inst_checker.specify_formula(stormpy.ParametricCheckTask(formulas[0].raw_formula, True)) + inst_checker.specify_formula(stormpy.CheckTask[stormpy.RationalFunction](formulas[0].raw_formula, True)) inst_checker.set_graph_preserving(True) point = {p: stormpy.RationalFunctionCoefficient("1/2") for p in parameters} result = inst_checker.check(env, point) - assert isinstance(result, stormpy.ExplicitExactQuantitativeCheckResult) + assert isinstance(result, stormpy.ExplicitQuantitativeCheckResult[stormpy.Rational]) res = result.at(model.initial_states[0]) assert isinstance(res, stormpy.Rational) assert res == stormpy.Rational("29/15") @@ -110,12 +110,12 @@ def test_pdtmc_exact_instantiation_checker_die(self): parameters = model.collect_all_parameters() env = stormpy.Environment() inst_checker = stormpy.pars.ModelInstantiationChecker[stormpy.ModelType.DTMC, stormpy.Rational](env, model) - inst_checker.specify_formula(stormpy.ParametricCheckTask(formulas[0].raw_formula, True)) + inst_checker.specify_formula(stormpy.CheckTask[stormpy.RationalFunction](formulas[0].raw_formula, True)) inst_checker.set_graph_preserving(True) point = {p: stormpy.RationalFunctionCoefficient("2/5") for p in parameters} result = inst_checker.check(env, point) - assert isinstance(result, stormpy.ExplicitExactQuantitativeCheckResult) + assert isinstance(result, stormpy.ExplicitQuantitativeCheckResult[stormpy.Rational]) res = result.at(model.initial_states[0]) assert isinstance(res, stormpy.Rational) assert res == stormpy.Rational("4/35") diff --git a/tests/pars/test_parametric.py b/tests/pars/test_parametric.py index 8d7dbca8be..0d902dc7ff 100644 --- a/tests/pars/test_parametric.py +++ b/tests/pars/test_parametric.py @@ -66,7 +66,7 @@ def test_parametric_model_checking_dd(self): assert model.model_type == stormpy.ModelType.DTMC assert model.has_parameters result = stormpy.check_model_dd(model, formulas[0]) - assert type(result) is stormpy.SymbolicParametricQuantitativeCheckResult + assert type(result) is stormpy.SymbolicQuantitativeCheckResult[stormpy.DdType.Sylvan, stormpy.RationalFunction] def test_parametric_model_checking_hybrid(self): program = stormpy.parse_prism_program(get_example_path("pdtmc", "parametric_die.pm")) @@ -78,7 +78,7 @@ def test_parametric_model_checking_hybrid(self): assert model.model_type == stormpy.ModelType.DTMC assert model.has_parameters result = stormpy.check_model_hybrid(model, formulas[0]) - assert type(result) is stormpy.HybridParametricQuantitativeCheckResult + assert type(result) is stormpy.HybridQuantitativeCheckResult[stormpy.DdType.Sylvan, stormpy.RationalFunction] values = result.get_values() assert len(values) == 3 diff --git a/tests/storage/test_maximal_end_components.py b/tests/storage/test_maximal_end_components.py index d4377e0606..7b1888b728 100644 --- a/tests/storage/test_maximal_end_components.py +++ b/tests/storage/test_maximal_end_components.py @@ -70,7 +70,7 @@ def test_elimination_interval(self): program = stormpy.parse_prism_program(get_example_path("mdp", "two_dice.nm")) formulas = stormpy.parse_properties_for_prism_program('P=? [ F "two" ]', program) model = stormpy.build_model(program, formulas) - transformer = stormpy.AddUncertaintyDouble(model) + transformer = stormpy.AddUncertainty[float](model) interval_model = transformer.transform(0.01) assert type(interval_model) is stormpy.SparseMdp[stormpy.Interval] subsystem = stormpy.BitVector(interval_model.nr_states, True) @@ -85,7 +85,7 @@ def test_elimination_exact_interval(self): program = stormpy.parse_prism_program(get_example_path("mdp", "two_dice.nm")) formulas = stormpy.parse_properties_for_prism_program('P=? [ F "two" ]', program) model = stormpy.build_sparse_exact_model(program, formulas) - transformer = stormpy.AddUncertaintyExact(model) + transformer = stormpy.AddUncertainty[stormpy.Rational](model) exact_interval_model = transformer.transform(stormpy.Rational("1/100")) assert type(exact_interval_model) is stormpy.SparseMdp[stormpy.RationalInterval] subsystem = stormpy.BitVector(exact_interval_model.nr_states, True) diff --git a/tests/storage/test_model.py b/tests/storage/test_model.py index c7c8bea7dc..039f773749 100644 --- a/tests/storage/test_model.py +++ b/tests/storage/test_model.py @@ -5,6 +5,13 @@ import pytest +def test_parameters_of_model(): + program = stormpy.parse_prism_program(get_example_path("dtmc", "die.pm")) + model = stormpy.build_sparse_exact_model(program) + + assert stormpy.storage.parameters_of_model(model) == (stormpy.Rational,) + + class TestSparseModel: def test_build_dtmc_from_prism_program(self): program = stormpy.parse_prism_program(get_example_path("dtmc", "die.pm"))