diff --git a/src/core/core.cpp b/src/core/core.cpp index 7abecbf29..ba5e900a1 100644 --- a/src/core/core.cpp +++ b/src/core/core.cpp @@ -115,68 +115,79 @@ std::shared_ptr> buildSymbolic } } +template +void define_build_sparse_model_defs(py::module& m) { + std::string type; + std::string desc; + if constexpr (std::is_same_v) { + type = ""; + desc = ""; + } else if constexpr (std::is_same_v) { + type = "exact_"; + desc = ""; + } else if constexpr (std::is_same_v) { + type = "parametric_"; + desc = "parametric "; + } else if constexpr (std::is_same_v) { + type = "interval_"; + desc = "interval "; + } else if constexpr (std::is_same_v) { + type = "exact_interval_"; + desc = "exact interval "; + } + + m.def( + ("_build_sparse_" + type + "model_from_symbolic_description").c_str(), &buildSparseModel, + ("Build the " + desc + "model in sparse representation" + (std::is_same_v ? " with exact number representation" : "")) + .c_str(), + py::arg("model_description"), py::arg("formulas") = std::vector>()); + m.def( + ("build_sparse_" + type + "model_with_options").c_str(), &buildSparseModelWithOptions, + ("Build the " + desc + "model in sparse representation" + (std::is_same_v ? " with exact number representation" : "")) + .c_str(), + py::arg("model_description"), py::arg("options")); + m.def(("_build_sparse_" + type + "model_from_drn").c_str(), &storm::api::buildExplicitDRNModel, + ("Build the " + desc + "model from DRN" + (std::is_same_v ? " (parametric)" : "")).c_str(), py::arg("file"), + py::arg("options") = storm::parser::DirectEncodingParserOptions()); + + 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"), + py::arg("formulas") = std::vector>()); + 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") = ""); + 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::class_>(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>()); + 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::class_>(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); + } +} + void define_build(py::module& m) { py::class_(m, "DirectEncodingParserOptions", "Options for the .drn parser") .def(py::init<>(), "initialise") .def_readwrite("build_choice_labels", &storm::parser::DirectEncodingParserOptions::buildChoiceLabeling, "Build with choice labels"); // Build model - m.def("_build_sparse_model_from_symbolic_description", &buildSparseModel, "Build the model in sparse representation", py::arg("model_description"), - py::arg("formulas") = std::vector>()); - m.def("_build_sparse_exact_model_from_symbolic_description", &buildSparseModel, - "Build the model in sparse representation with exact number representation", py::arg("model_description"), - py::arg("formulas") = std::vector>()); - m.def("_build_sparse_parametric_model_from_symbolic_description", &buildSparseModel, - "Build the parametric model in sparse representation", py::arg("model_description"), - py::arg("formulas") = std::vector>()); - m.def("_build_sparse_interval_model_from_symbolic_description", &buildSparseModel, "Build the interval model in sparse representation", - py::arg("model_description"), py::arg("formulas") = std::vector>()); - m.def("_build_sparse_exact_interval_model_from_symbolic_description", &buildSparseModel, - "Build the exact interval model in sparse representation", py::arg("model_description"), - py::arg("formulas") = std::vector>()); - m.def("build_sparse_model_with_options", &buildSparseModelWithOptions, "Build the model in sparse representation", py::arg("model_description"), - py::arg("options")); - m.def("build_sparse_exact_model_with_options", &buildSparseModelWithOptions, - "Build the model in sparse representation with exact number representation", py::arg("model_description"), py::arg("options")); - m.def("build_sparse_parametric_model_with_options", &buildSparseModelWithOptions, "Build the model in sparse representation", - py::arg("model_description"), py::arg("options")); - m.def("build_sparse_interval_model_with_options", &buildSparseModelWithOptions, "Build the interval model in sparse representation", - py::arg("model_description"), py::arg("options")); - m.def("build_sparse_exact_interval_model_with_options", &buildSparseModelWithOptions, - "Build the exact interval model in sparse representation", py::arg("model_description"), py::arg("options")); - m.def("_build_symbolic_model_from_symbolic_description", &buildSymbolicModel, - "Build the model in symbolic representation", py::arg("model_description"), - py::arg("formulas") = std::vector>()); - 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>()); - m.def("_build_sparse_model_from_drn", &storm::api::buildExplicitDRNModel, "Build the model from DRN", py::arg("file"), - py::arg("options") = storm::parser::DirectEncodingParserOptions()); - m.def("_build_sparse_exact_model_from_drn", &storm::api::buildExplicitDRNModel, "Build the model from DRN", py::arg("file"), - py::arg("options") = storm::parser::DirectEncodingParserOptions()); - m.def("_build_sparse_parametric_model_from_drn", &storm::api::buildExplicitDRNModel, "Build the parametric model from DRN", - py::arg("file"), py::arg("options") = storm::parser::DirectEncodingParserOptions()); - m.def("_build_sparse_interval_model_from_drn", &storm::api::buildExplicitDRNModel, "Build the interval model from DRN", py::arg("file"), - py::arg("options") = storm::parser::DirectEncodingParserOptions()); - m.def("_build_sparse_exact_interval_model_from_drn", &storm::api::buildExplicitDRNModel, "Build the exact interval model from DRN", - py::arg("file"), py::arg("options") = storm::parser::DirectEncodingParserOptions()); - 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") = ""); - - 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); - 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); - 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::class_>(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"); - - py::class_>(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"); + define_build_sparse_model_defs(m); + define_build_sparse_model_defs(m); + define_build_sparse_model_defs(m); + define_build_sparse_model_defs(m); + define_build_sparse_model_defs(m); py::class_>(m, "ExplicitStateLookup", "Lookup model for states") .def( @@ -240,6 +251,32 @@ void exportDRN(std::shared_ptr> model, s storm::api::exportSparseModelAsDrn(model, file, options); } +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()); +} + void define_export(py::module& m) { py::class_(m, "DirectEncodingExporterOptions") .def(py::init<>()) @@ -247,14 +284,9 @@ void define_export(py::module& m) { .def_readwrite("outputPrecision", &storm::io::DirectEncodingExporterOptions::outputPrecision); // Export - m.def("_export_to_drn", &exportDRN, "Export model in DRN format", py::arg("model"), py::arg("file"), - py::arg("options") = storm::io::DirectEncodingExporterOptions()); - m.def("_export_to_drn_interval", &exportDRN, "Export model in DRN format", py::arg("model"), py::arg("file"), - py::arg("options") = storm::io::DirectEncodingExporterOptions()); - m.def("_export_exact_to_drn_interval", &exportDRN, "Export model in DRN format", py::arg("model"), py::arg("file"), - py::arg("options") = storm::io::DirectEncodingExporterOptions()); - m.def("_export_exact_to_drn", &exportDRN, "Export model in DRN format", py::arg("model"), py::arg("file"), - py::arg("options") = storm::io::DirectEncodingExporterOptions()); - m.def("_export_parametric_to_drn", &exportDRN, "Export parametric model in DRN format", py::arg("model"), py::arg("file"), - py::arg("options") = storm::io::DirectEncodingExporterOptions()); + define_export_drn(m); + define_export_drn(m); + define_export_drn(m); + define_export_drn(m); + define_export_drn(m); } diff --git a/src/core/modelchecking.cpp b/src/core/modelchecking.cpp index c253b09af..e1fff96ab 100644 --- a/src/core/modelchecking.cpp +++ b/src/core/modelchecking.cpp @@ -154,6 +154,58 @@ void define_check_task(py::module& m, std::string const& name) { "Sets the mode which decides how the uncertainty will be resolved."); } +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") = storm::Environment()); + m.def("_model_checking_sparse_engine", &modelCheckingSparseEngine, "Perform model checking using the sparse engine", py::arg("model"), + py::arg("task"), py::arg("environment") = storm::Environment()); + m.def("_model_checking_dd_engine", &modelCheckingDdEngine, "Perform model checking using the dd engine", + py::arg("model"), py::arg("task"), py::arg("environment") = storm::Environment()); + m.def("_model_checking_hybrid_engine", &modelCheckingHybridEngine, "Perform model checking using the hybrid engine", + py::arg("model"), py::arg("task"), py::arg("environment") = storm::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") = storm::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"), + py::arg("environment") = storm::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") = storm::Environment()); + m.def("_multi_objective_model_checking_exact", &multiObjectiveModelChecking, "Run multi-objective model checking", + py::arg("model"), py::arg("formula"), py::arg("environment") = storm::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") = storm::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") = storm::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") = storm::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")); + } +} + void define_modelchecking(py::module& m) { py::class_> mchint( m, "ModelCheckerHint", "Information that may accelerate the model checking process"); @@ -171,59 +223,16 @@ void define_modelchecking(py::module& m) { py::overload_cast> const&>(&storm::modelchecker::ExplicitModelCheckerHint::setResultHint), "result_hint"_a); - 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("_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("_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("_compute_expected_number_of_visits_double", &getExpectedNumberOfVisits, py::arg("env"), py::arg("model")); - m.def("_compute_expected_number_of_visits_exact", &getExpectedNumberOfVisits, py::arg("env"), py::arg("model")); - - m.def("_compute_steady_state_distribution_double", &getSteadyStateDistribution, py::arg("env"), py::arg("model")); - m.def("_compute_steady_state_distribution_exact", &getSteadyStateDistribution, py::arg("env"), py::arg("model")); - - // Model checking - m.def("_model_checking_fully_observable", &modelCheckingFullyObservableSparseEngine, py::arg("model"), py::arg("task"), - py::arg("environment") = storm::Environment()); - m.def("_exact_model_checking_fully_observable", &modelCheckingFullyObservableSparseEngine, py::arg("model"), py::arg("task"), - py::arg("environment") = storm::Environment()); - m.def("_model_checking_sparse_engine", &modelCheckingSparseEngine, "Perform model checking using the sparse engine", py::arg("model"), - py::arg("task"), py::arg("environment") = storm::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") = storm::Environment()); - 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") = storm::Environment()); - m.def("_model_checking_dd_engine", &modelCheckingDdEngine, "Perform model checking using the dd engine", - py::arg("model"), py::arg("task"), py::arg("environment") = storm::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") = storm::Environment()); - m.def("_model_checking_hybrid_engine", &modelCheckingHybridEngine, "Perform model checking using the hybrid engine", - py::arg("model"), py::arg("task"), py::arg("environment") = storm::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") = storm::Environment()); + 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"); m.def("check_exact_interval_mdp", &checkRationalIntervalMdp, "Check exact interval MDP"); m.def("compute_all_until_probabilities", &computeAllUntilProbabilities, "Compute forward until probabilities"); m.def("compute_transient_probabilities", &computeTransientProbabilities, "Compute transient probabilities"); - 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_rationalfunc", &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("_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_double", &multiObjectiveModelChecking, "Run multi-objective model checking", py::arg("model"), - py::arg("formula"), py::arg("environment") = storm::Environment()); - m.def("_multi_objective_model_checking_exact", &multiObjectiveModelChecking, "Run multi-objective model checking", py::arg("model"), - py::arg("formula"), py::arg("environment") = storm::Environment()); } template void define_check_task(py::module&, std::string const&); diff --git a/src/core/result.cpp b/src/core/result.cpp index efbc5d8d7..8422c6f49 100644 --- a/src/core/result.cpp +++ b/src/core/result.cpp @@ -26,6 +26,17 @@ std::shared_ptr createFilterSymboli return std::make_unique>(model->getReachableStates(), model->getStates(expr)); } +template +void define_result_as_explicit(py::class_>& checkResult, + std::string const& vtSuffix) { + checkResult.def(("as_explicit" + vtSuffix + "_qualitative").c_str(), + [](storm::modelchecker::CheckResult const& result) { return result.template asExplicitQualitativeCheckResult(); }, + "Convert into explicit qualitative result"); + checkResult.def(("as_explicit" + vtSuffix + "_quantitative").c_str(), + [](storm::modelchecker::CheckResult const& result) { return result.template asExplicitQuantitativeCheckResult(); }, + "Convert into explicit quantitative result"); +} + // Define python bindings void define_result(py::module& m) { // CheckResult @@ -47,30 +58,11 @@ void define_result(py::module& m) { "Flag if result is hybrid quantitative") .def_property_readonly("_pareto_curve", &storm::modelchecker::CheckResult::isParetoCurveCheckResult, "Flag if result is a pareto curve") .def_property_readonly("result_for_all_states", &storm::modelchecker::CheckResult::isResultForAllStates, "Flag if result is for all states") - .def_property_readonly("has_scheduler", &storm::modelchecker::CheckResult::hasScheduler, "Flag if a scheduler is present") - .def( - "as_explicit_qualitative", [](storm::modelchecker::CheckResult const& result) { return result.asExplicitQualitativeCheckResult(); }, - "Convert into explicit qualitative result") - .def( - "as_explicit_exact_qualitative", - [](storm::modelchecker::CheckResult const& result) { return result.asExplicitQualitativeCheckResult(); }, - "Convert into explicit qualitative result") - .def( - "as_explicit_parametric_qualitative", - [](storm::modelchecker::CheckResult const& result) { return result.asExplicitQualitativeCheckResult(); }, - "Convert into explicit qualitative result") - .def( - "as_explicit_quantitative", [](storm::modelchecker::CheckResult const& result) { return result.asExplicitQuantitativeCheckResult(); }, - "Convert into explicit quantitative result") - .def( - "as_explicit_exact_quantitative", - [](storm::modelchecker::CheckResult const& result) { return result.asExplicitQuantitativeCheckResult(); }, - "Convert into explicit quantitative result") - .def( - "as_explicit_parametric_quantitative", - [](storm::modelchecker::CheckResult const& result) { return result.asExplicitQuantitativeCheckResult(); }, - "Convert into explicit quantitative result") - .def("filter", &storm::modelchecker::CheckResult::filter, py::arg("filter"), "Filter the result") + .def_property_readonly("has_scheduler", &storm::modelchecker::CheckResult::hasScheduler, "Flag if a scheduler is present"); + define_result_as_explicit(checkResult, ""); + define_result_as_explicit(checkResult, "_exact"); + define_result_as_explicit(checkResult, "_parametric"); + checkResult.def("filter", &storm::modelchecker::CheckResult::filter, py::arg("filter"), "Filter the result") .def("__str__", [](storm::modelchecker::CheckResult const& result) { std::stringstream stream; result.writeToStream(stream); diff --git a/src/core/transformation.cpp b/src/core/transformation.cpp index 4e0990410..8d64d9102 100644 --- a/src/core/transformation.cpp +++ b/src/core/transformation.cpp @@ -30,19 +30,30 @@ typename storm::transformer::EndComponentEliminator::EndComponentElim return storm::transformer::EndComponentEliminator::transform(matrix, subsystemStates, possibleECRows, addSinkRowStates, addSelfLoopAtSinkStates); } -void define_transformation(py::module& m) { - // Transform model - m.def("_transform_to_sparse_model", &storm::api::transformSymbolicToSparseModel, - "Transform symbolic model into sparse model", py::arg("model"), py::arg("formulae") = std::vector>()); - m.def("_transform_to_sparse_parametric_model", &storm::api::transformSymbolicToSparseModel, - "Transform symbolic parametric model into sparse parametric model", py::arg("model"), - py::arg("formulae") = std::vector>()); +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_discrete_time_model", &transformContinuousToDiscreteTimeSparseModel, "Transform continuous time model to discrete time model", - py::arg("model"), py::arg("formulae") = std::vector>()); - m.def("_transform_to_discrete_time_parametric_model", &transformContinuousToDiscreteTimeSparseModel, - "Transform parametric continuous time model to parametric discrete time model", py::arg("model"), + 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::class_(m, "SubsystemBuilderOptions", "Options for constructing the subsystem") .def(py::init<>()) @@ -59,11 +70,6 @@ void define_transformation(py::module& m) { .value("MERGE_LABELS", storm::transformer::EliminationLabelBehavior::MergeLabels) .value("DELETE_LABELS", storm::transformer::EliminationLabelBehavior::DeleteLabels) .finalize(); - - m.def("_eliminate_non_markovian_chains", &storm::api::eliminateNonMarkovianChains, "Eliminate chains of non-Markovian states in Markov automaton.", - py::arg("ma"), py::arg("formulae"), py::arg("label_behavior")); - m.def("_eliminate_non_markovian_chains_parametric", &storm::api::eliminateNonMarkovianChains, - "Eliminate chains of non-Markovian states in Markov automaton.", py::arg("ma"), py::arg("formulae"), py::arg("label_behavior")); } template diff --git a/src/mod_pars.cpp b/src/mod_pars.cpp index 84f053a5d..6e5c3851d 100644 --- a/src/mod_pars.cpp +++ b/src/mod_pars.cpp @@ -13,6 +13,8 @@ PYBIND11_MODULE(_pars, m) { define_pars(m); define_pla(m); - define_model_instantiator(m); - define_model_instantiation_checker(m); + define_model_instantiator(m); + define_model_instantiator(m); + define_model_instantiation_checker(m); + define_model_instantiation_checker(m); } diff --git a/src/mod_storage.cpp b/src/mod_storage.cpp index f0cdc3f30..cbbfca22e 100644 --- a/src/mod_storage.cpp +++ b/src/mod_storage.cpp @@ -30,7 +30,8 @@ PYBIND11_MODULE(_storage, m) { #endif define_bitvector(m); - define_dd(m, "Sylvan"); + auto ddSylvan = define_dd(m, "Sylvan"); + define_dd_typed(m, "Sylvan", "_Double", ddSylvan); define_dd_nt(m); define_model(m); define_sparse_model(m, ""); diff --git a/src/pars/model_instantiator.cpp b/src/pars/model_instantiator.cpp index a0e9ad70f..8cfffdaa4 100644 --- a/src/pars/model_instantiator.cpp +++ b/src/pars/model_instantiator.cpp @@ -30,156 +30,96 @@ using MarkovAutomaton = storm::models::sparse::MarkovAutomaton; using namespace storm::modelchecker; -// Model instantiator -void define_model_instantiator(py::module& m) { - py::class_, Dtmc>>(m, "PDtmcInstantiator", "Instantiate PDTMCs to DTMCs") - .def(py::init>(), "parametric model"_a) - .def("instantiate", &storm::utility::ModelInstantiator, Dtmc>::instantiate, - "Instantiate model with given parameter values"); - - py::class_, Mdp>>(m, "PMdpInstantiator", "Instantiate PMDPs to MDPs") - .def(py::init>(), "parametric model"_a) - .def("instantiate", &storm::utility::ModelInstantiator, Mdp>::instantiate, - "Instantiate model with given parameter values"); - - py::class_, Ctmc>>(m, "PCtmcInstantiator", "Instantiate PCTMCs to CTMCs") - .def(py::init>(), "parametric model"_a) - .def("instantiate", &storm::utility::ModelInstantiator, Ctmc>::instantiate, - "Instantiate model with given parameter values"); - - py::class_, MarkovAutomaton>>(m, "PMaInstantiator", - "Instantiate PMAs to MAs") - .def(py::init>(), "parametric model"_a) - .def("instantiate", &storm::utility::ModelInstantiator, MarkovAutomaton>::instantiate, - "Instantiate model with given parameter values"); - - py::class_, Dtmc>>(m, "PartialPDtmcInstantiator", - "Instantiate PDTMCs to DTMCs") - .def(py::init>(), "parametric model"_a) - .def("instantiate", &storm::utility::ModelInstantiator, Dtmc>::instantiate, - "Instantiate model with given parameter values"); - - py::class_, Mdp>>(m, "PartialPMdpInstantiator", - "Instantiate PMDPs to MDPs") - .def(py::init>(), "parametric model"_a) - .def("instantiate", &storm::utility::ModelInstantiator, Mdp>::instantiate, - "Instantiate model with given parameter values"); - - py::class_, Ctmc>>(m, "PartialPCtmcInstantiator", - "Instantiate PCTMCs to CTMCs") - .def(py::init>(), "parametric model"_a) - .def("instantiate", &storm::utility::ModelInstantiator, Ctmc>::instantiate, +// Helper: define typed ModelInstantiator class +template +void define_typed_instantiator(py::module& m, const char* pyName, const char* pyDesc) { + py::class_>(m, pyName, pyDesc) + .def(py::init(), "parametric model"_a) + .def("instantiate", &storm::utility::ModelInstantiator::instantiate, "Instantiate model with given parameter values"); +} - py::class_, MarkovAutomaton>>( - m, "PartialPMaInstantiator", "Instantiate PMAs to MAs") - .def(py::init>(), "parametric model"_a) - .def("instantiate", &storm::utility::ModelInstantiator, MarkovAutomaton>::instantiate, - "Instantiate model with given parameter values"); +template +void define_model_instantiator(py::module& m) { + std::string prefix; + if constexpr (std::is_same_v) { + prefix = ""; + } else if constexpr (std::is_same_v) { + prefix = "Partial"; + } + + define_typed_instantiator, Dtmc>(m, (prefix + "PDtmcInstantiator").c_str(), "Instantiate PDTMCs to DTMCs"); + define_typed_instantiator, Mdp>(m, (prefix + "PMdpInstantiator").c_str(), "Instantiate PMDPs to MDPs"); + define_typed_instantiator, Ctmc>(m, (prefix + "PCtmcInstantiator").c_str(), "Instantiate PCTMCs to CTMCs"); + define_typed_instantiator, MarkovAutomaton>(m, (prefix + "PMaInstantiator").c_str(), + "Instantiate PMAs to MAs"); } -void define_model_instantiation_checker(py::module& m) { - py::class_, double>, - std::shared_ptr, double>>> - bpdtmcinstchecker(m, "_PDtmcInstantiationCheckerBase", "Instantiate pDTMCs to DTMCs and immediately check (base)"); - bpdtmcinstchecker.def("specify_formula", &SparseInstantiationModelChecker, double>::specifyFormula, "check_task"_a); - - py::class_, double>, - std::shared_ptr, double>>>( - m, "PDtmcInstantiationChecker", "Instantiate pDTMCs to DTMCs and immediately check", bpdtmcinstchecker) - .def(py::init>(), "parametric model"_a) - .def( - "check", - [](SparseDtmcInstantiationModelChecker, double>& sdimc, storm::Environment const& env, - storm::utility::parametric::Valuation const& val) -> std::shared_ptr { return sdimc.check(env, val); }, - "env"_a, "instantiation"_a) - .def("set_graph_preserving", &SparseDtmcInstantiationModelChecker, double>::setInstantiationsAreGraphPreserving, - "value"_a); - - py::class_, storm::RationalNumber>, - std::shared_ptr, storm::RationalNumber>>> - bpdtmcexactinstchecker(m, "_PDtmcExactInstantiationCheckerBase", "Instantiate pDTMCs to exact DTMCs and immediately check (base)"); - bpdtmcexactinstchecker.def("specify_formula", &SparseInstantiationModelChecker, storm::RationalNumber>::specifyFormula, - "check_task"_a); - - py::class_, storm::RationalNumber>, - std::shared_ptr, storm::RationalNumber>>>( - m, "PDtmcExactInstantiationChecker", "Instantiate pDTMCs to exact DTMCs and immediately check", bpdtmcexactinstchecker) - .def(py::init>(), "parametric model"_a) - .def( - "check", - [](SparseDtmcInstantiationModelChecker, storm::RationalNumber>& sdimc, storm::Environment const& env, - storm::utility::parametric::Valuation const& val) -> std::shared_ptr { return sdimc.check(env, val); }, - "env"_a, "instantiation"_a) - .def("set_graph_preserving", - &SparseDtmcInstantiationModelChecker, storm::RationalNumber>::setInstantiationsAreGraphPreserving, "value"_a); - - py::class_, double>, - std::shared_ptr, double>>> - bpmdpinstchecker(m, "_PMdpInstantiationCheckerBase", "Instantiate pMDPs to MDPs and immediately check (base)"); - bpmdpinstchecker.def("specify_formula", &SparseInstantiationModelChecker, double>::specifyFormula, "check_task"_a); - - py::class_, double>, - std::shared_ptr, double>>>( - m, "PMdpInstantiationChecker", "Instantiate PMDP to MDPs and immediately check", bpmdpinstchecker) - .def(py::init>(), "parametric model"_a) +// Trait: maps (ModelType, ResultType) to the specific checker class +template +struct instantiation_checker; + +template +struct instantiation_checker, ResultType> { + using type = SparseDtmcInstantiationModelChecker, ResultType>; +}; + +template +struct instantiation_checker, ResultType> { + using type = SparseMdpInstantiationModelChecker, ResultType>; +}; + +template +struct instantiation_checker, ResultType> { + using type = SparseCtmcInstantiationModelChecker, ResultType>; +}; + +// Helper: define typed base + derived instantiation checker pair +template +void define_typed_checker(py::module& m, const char* baseName, const char* baseDesc, const char* derivedName, const char* derivedDesc) { + using CheckerType = typename instantiation_checker::type; + using BaseChecker = SparseInstantiationModelChecker; + auto base = py::class_>(m, baseName, baseDesc); + base.def("specify_formula", &BaseChecker::specifyFormula, "check_task"_a); + + py::class_>(m, derivedName, derivedDesc, base) + .def(py::init(), "parametric model"_a) .def( "check", - [](SparseMdpInstantiationModelChecker, double>& sdimc, storm::Environment const& env, - storm::utility::parametric::Valuation const& val) -> std::shared_ptr { return sdimc.check(env, val); }, + [](CheckerType& c, storm::Environment const& env, + storm::utility::parametric::Valuation const& val) -> std::shared_ptr { return c.check(env, val); }, "env"_a, "instantiation"_a) - .def("set_graph_preserving", &SparseMdpInstantiationModelChecker, double>::setInstantiationsAreGraphPreserving, "value"_a); - - py::class_, storm::RationalNumber>, - std::shared_ptr, storm::RationalNumber>>> - bpmdpexactinstchecker(m, "_PMdpExactInstantiationCheckerBase", "Instantiate pMDPs to exact MDPs and immediately check (base)"); - bpmdpexactinstchecker.def("specify_formula", &SparseInstantiationModelChecker, storm::RationalNumber>::specifyFormula, - "check_task"_a); - - py::class_, storm::RationalNumber>, - std::shared_ptr, storm::RationalNumber>>>( - m, "PMdpExactInstantiationChecker", "Instantiate PMDP to exact MDPs and immediately check", bpmdpexactinstchecker) - .def(py::init>(), "parametric model"_a) - .def( - "check", - [](SparseMdpInstantiationModelChecker, storm::RationalNumber>& sdimc, storm::Environment const& env, - storm::utility::parametric::Valuation const& val) -> std::shared_ptr { return sdimc.check(env, val); }, - "env"_a, "instantiation"_a) - .def("set_graph_preserving", - &SparseMdpInstantiationModelChecker, storm::RationalNumber>::setInstantiationsAreGraphPreserving, "value"_a); - - py::class_, double>, - std::shared_ptr, double>>> - bpctmcinstchecker(m, "_PCtmcInstantiationCheckerBase", "Instantiate pCTMCs to CTMCs and immediately check (base)"); - bpctmcinstchecker.def("specify_formula", &SparseInstantiationModelChecker, double>::specifyFormula, "check_task"_a); - - py::class_, double>, - std::shared_ptr, double>>>( - m, "PCtmcInstantiationChecker", "Instantiate pCTMCs to CTMCs and immediately check", bpctmcinstchecker) - .def(py::init>(), "parametric model"_a) - .def( - "check", - [](SparseCtmcInstantiationModelChecker, double>& scimc, storm::Environment const& env, - storm::utility::parametric::Valuation const& val) -> std::shared_ptr { return scimc.check(env, val); }, - "env"_a, "instantiation"_a) - .def("set_graph_preserving", &SparseCtmcInstantiationModelChecker, double>::setInstantiationsAreGraphPreserving, - "value"_a); - - py::class_, storm::RationalNumber>, - std::shared_ptr, storm::RationalNumber>>> - bpctmcexactinstchecker(m, "_PCtmcExactInstantiationCheckerBase", "Instantiate pCTMCs to exact CTMCs and immediately check (base)"); - bpctmcexactinstchecker.def("specify_formula", &SparseInstantiationModelChecker, storm::RationalNumber>::specifyFormula, - "check_task"_a); - - py::class_, storm::RationalNumber>, - std::shared_ptr, storm::RationalNumber>>>( - m, "PCtmcExactInstantiationChecker", "Instantiate pCTMCs to exact CTMCs and immediately check", bpctmcexactinstchecker) - .def(py::init>(), "parametric model"_a) - .def( - "check", - [](SparseCtmcInstantiationModelChecker, storm::RationalNumber>& scimc, storm::Environment const& env, - storm::utility::parametric::Valuation const& val) -> std::shared_ptr { return scimc.check(env, val); }, - "env"_a, "instantiation"_a) - .def("set_graph_preserving", - &SparseCtmcInstantiationModelChecker, storm::RationalNumber>::setInstantiationsAreGraphPreserving, "value"_a); + .def("set_graph_preserving", &CheckerType::setInstantiationsAreGraphPreserving, "value"_a); } + +template +void define_model_instantiation_checker(py::module& m) { + std::string exactStr, exactDesc; + if constexpr (std::is_same_v) { + exactStr = ""; + exactDesc = ""; + } else if constexpr (std::is_same_v) { + exactStr = "Exact"; + exactDesc = "exact "; + } + + // Dtmc + define_typed_checker, ValueType>( + m, ("_PDtmc" + exactStr + "InstantiationCheckerBase").c_str(), ("Instantiate pDTMCs to " + exactDesc + "DTMCs and immediately check (base)").c_str(), + ("PDtmc" + exactStr + "InstantiationChecker").c_str(), ("Instantiate pDTMCs to " + exactDesc + "DTMCs and immediately check").c_str()); + + // Mdp + define_typed_checker, ValueType>( + m, ("_PMdp" + exactStr + "InstantiationCheckerBase").c_str(), ("Instantiate pMDPs to " + exactDesc + "MDPs and immediately check (base)").c_str(), + ("PMdp" + exactStr + "InstantiationChecker").c_str(), ("Instantiate PMDP to " + exactDesc + "MDPs and immediately check").c_str()); + + // Ctmc + define_typed_checker, ValueType>( + m, ("_PCtmc" + exactStr + "InstantiationCheckerBase").c_str(), ("Instantiate pCTMCs to " + exactDesc + "CTMCs and immediately check (base)").c_str(), + ("PCtmc" + exactStr + "InstantiationChecker").c_str(), ("Instantiate pCTMCs to " + exactDesc + "CTMCs and immediately check").c_str()); +} + +template void define_model_instantiator(py::module&); +template void define_model_instantiator(py::module&); +template void define_model_instantiation_checker(py::module&); +template void define_model_instantiation_checker(py::module&); diff --git a/src/pars/model_instantiator.h b/src/pars/model_instantiator.h index c61a6eee7..f29e125a1 100644 --- a/src/pars/model_instantiator.h +++ b/src/pars/model_instantiator.h @@ -2,5 +2,8 @@ #include "src/pars/common.h" +template void define_model_instantiator(py::module& m); + +template void define_model_instantiation_checker(py::module& m); diff --git a/src/storage/dd.cpp b/src/storage/dd.cpp index 0419dd78c..201cc4e54 100644 --- a/src/storage/dd.cpp +++ b/src/storage/dd.cpp @@ -9,7 +9,7 @@ #include "src/helpers.h" template -void define_dd(py::module& m, std::string const& libstring) { +py::class_> define_dd(py::module& m, std::string const& libstring) { py::class_> ddMetaVariable(m, (std::string("DdMetaVariable_") + libstring).c_str()); ddMetaVariable.def("compute_indices", &storm::dd::DdMetaVariable::getIndices, py::arg("sorted") = true); ddMetaVariable.def_property_readonly("name", &storm::dd::DdMetaVariable::getName); @@ -30,13 +30,18 @@ void define_dd(py::module& m, std::string const& libstring) { py::class_> bdd(m, (std::string("Bdd_") + libstring).c_str(), "Bdd", dd); bdd.def("to_expression", &storm::dd::Bdd::toExpression, py::arg("expression_manager")); - py::class_> add(m, (std::string("Add_") + libstring + "_Double").c_str(), "Add", dd); + return dd; +} + +template +void define_dd_typed(py::module& m, std::string const& libstring, std::string const& valueSuffix, py::class_> const& dd) { + py::class_> add(m, (std::string("Add_") + libstring + valueSuffix).c_str(), "Add", dd); add.def( - "__iter__", [](const storm::dd::Add& s) { return py::make_iterator(s.begin(), s.end()); }, + "__iter__", [](const storm::dd::Add& s) { return py::make_iterator(s.begin(), s.end()); }, py::keep_alive<0, 1>() /* Essential: keep object alive while iterator exists */); - py::class_> addIterator(m, (std::string("AddIterator_") + libstring + "_Double").c_str(), "AddIterator"); - addIterator.def("get", [](const storm::dd::AddIterator& it) { return *it; }); + py::class_> addIterator(m, (std::string("AddIterator_") + libstring + valueSuffix).c_str(), "AddIterator"); + addIterator.def("get", [](const storm::dd::AddIterator& it) { return *it; }); } void define_dd_nt(py::module& m) { @@ -47,4 +52,6 @@ void define_dd_nt(py::module& m) { .finalize(); } -template void define_dd(py::module& m, std::string const& libstring); \ No newline at end of file +template py::class_> define_dd(py::module& m, std::string const& libstring); +template void define_dd_typed(py::module&, std::string const&, std::string const&, + py::class_> const&); \ No newline at end of file diff --git a/src/storage/dd.h b/src/storage/dd.h index 0938a06f7..f66021eb3 100644 --- a/src/storage/dd.h +++ b/src/storage/dd.h @@ -1,9 +1,13 @@ #pragma once +#include #include #include "src/common.h" template -void define_dd(py::module& m, std::string const& libname); -void define_dd_nt(py::module& m); \ No newline at end of file +py::class_> define_dd(py::module& m, std::string const& libname); +template +void define_dd_typed(py::module& m, std::string const& libstring, std::string const& valueSuffix, py::class_> const& dd); + +void define_dd_nt(py::module& m); diff --git a/src/storage/memorystructure.cpp b/src/storage/memorystructure.cpp index ba8117c1b..5fa4800a9 100644 --- a/src/storage/memorystructure.cpp +++ b/src/storage/memorystructure.cpp @@ -7,29 +7,27 @@ #include #include +template +void define_memorystructure_product_each(py::class_>& memoryStructure, + py::class_& reverseData, std::string const& vtSuffix) { + memoryStructure.def( + ("_product_model" + vtSuffix).c_str(), + [](storm::storage::MemoryStructure& ms, storm::models::sparse::Model const& sparseModel) { return ms.product(sparseModel); }); + reverseData.def(("_reverse_scheduler" + vtSuffix).c_str(), + &storm::storage::SparseModelMemoryProductReverseData::createMemorySchedulerFromProductScheduler, py::arg("product_scheduler")); +} + void define_memorystructure_untyped(py::module& m) { typedef storm::storage::MemoryStructure MemoryStructure; py::class_> memoryStructure(m, "MemoryStructure"); memoryStructure.def("product", [](MemoryStructure& ms, MemoryStructure const& memModel) { return ms.product(memModel); }); - memoryStructure.def("_product_model_double", - [](MemoryStructure& ms, storm::models::sparse::Model const& sparseModel) { return ms.product(sparseModel); }); - memoryStructure.def("_product_model_exact", - [](MemoryStructure& ms, storm::models::sparse::Model const& sparseModel) { return ms.product(sparseModel); }); - memoryStructure.def("_product_model_parametric", - [](MemoryStructure& ms, storm::models::sparse::Model const& sparseModel) { return ms.product(sparseModel); }); memoryStructure.def_property_readonly("nr_states", &MemoryStructure::getNumberOfStates); memoryStructure.def_property_readonly("state_labeling", &MemoryStructure::getStateLabeling); py::class_ memoryProductReverseData(m, "SparseModelMemoryProductReverseData"); - memoryProductReverseData.def("_reverse_scheduler_double", - &storm::storage::SparseModelMemoryProductReverseData::createMemorySchedulerFromProductScheduler, - py::arg("product_scheduler")); - memoryProductReverseData.def("_reverse_scheduler_exact", - &storm::storage::SparseModelMemoryProductReverseData::createMemorySchedulerFromProductScheduler, - py::arg("product_scheduler")); - memoryProductReverseData.def("_reverse_scheduler_parametric", - &storm::storage::SparseModelMemoryProductReverseData::createMemorySchedulerFromProductScheduler, - py::arg("product_scheduler")); + define_memorystructure_product_each(memoryStructure, memoryProductReverseData, "_double"); + define_memorystructure_product_each(memoryStructure, memoryProductReverseData, "_exact"); + define_memorystructure_product_each(memoryStructure, memoryProductReverseData, "_parametric"); } template diff --git a/src/storage/model.cpp b/src/storage/model.cpp index 021c08e1d..6d71cfe95 100644 --- a/src/storage/model.cpp +++ b/src/storage/model.cpp @@ -91,6 +91,52 @@ storm::models::sparse::StateLabeling& getLabeling(SparseModel& model) return model.getStateLabeling(); } +template +void define_model_as_sparse(py::class_>& modelBase) { + std::string prefix; + if constexpr (std::is_same_v) + prefix = ""; + else if constexpr (std::is_same_v) + prefix = "exact_"; + else if constexpr (std::is_same_v) + prefix = "i"; + else if constexpr (std::is_same_v) + prefix = "exact_i"; + else if constexpr (std::is_same_v) + prefix = "p"; + + modelBase.def(("_as_sparse_" + prefix + "dtmc").c_str(), [](ModelBase& m) { return m.template as>(); }, "Get model as sparse DTMC"); + modelBase.def(("_as_sparse_" + prefix + "mdp").c_str(), [](ModelBase& m) { return m.template as>(); }, "Get model as sparse MDP"); + modelBase.def(("_as_sparse_" + prefix + "pomdp").c_str(), [](ModelBase& m) { return m.template as>(); }, + "Get model as sparse POMDP"); + modelBase.def(("_as_sparse_" + prefix + "ctmc").c_str(), [](ModelBase& m) { return m.template as>(); }, "Get model as sparse CTMC"); + modelBase.def(("_as_sparse_" + prefix + "ma").c_str(), [](ModelBase& m) { return m.template as>(); }, + "Get model as sparse MA"); + modelBase.def(("_as_sparse_" + prefix + "smg").c_str(), [](ModelBase& m) { return m.template as>(); }, "Get model as sparse SMG"); +} + +template +void define_model_as_symbolic(py::class_>& modelBase) { + std::string prefix; + if constexpr (std::is_same_v) + prefix = ""; + else if constexpr (std::is_same_v) + prefix = "exact_"; + else if constexpr (std::is_same_v) + prefix = "p"; + else + return; + + modelBase.def(("_as_symbolic_" + prefix + "dtmc").c_str(), [](ModelBase& m) { return m.template as>(); }, + "Get model as symbolic DTMC"); + modelBase.def(("_as_symbolic_" + prefix + "mdp").c_str(), [](ModelBase& m) { return m.template as>(); }, + "Get model as symbolic MDP"); + modelBase.def(("_as_symbolic_" + prefix + "ctmc").c_str(), [](ModelBase& m) { return m.template as>(); }, + "Get model as symbolic CTMC"); + modelBase.def(("_as_symbolic_" + prefix + "ma").c_str(), + [](ModelBase& m) { return m.template as>(); }, "Get model as symbolic MA"); +} + // Bindings for general models void define_model(py::module& m) { // ModelType @@ -116,117 +162,15 @@ void define_model(py::module& m) { .def_property_readonly("is_sparse_model", &ModelBase::isSparseModel, "Flag whether the model is stored as a sparse model") .def_property_readonly("is_symbolic_model", &ModelBase::isSymbolicModel, "Flag whether the model is stored using decision diagrams") .def_property_readonly("is_discrete_time_model", &ModelBase::isDiscreteTimeModel, "Flag whether the model is a discrete time model") - .def_property_readonly("is_nondeterministic_model", &ModelBase::isNondeterministicModel, "Flag whether the model contains nondeterminism") - .def( - "_as_sparse_dtmc", [](ModelBase& modelbase) { return modelbase.as>(); }, "Get model as sparse DTMC") - .def( - "_as_sparse_exact_dtmc", [](ModelBase& modelbase) { return modelbase.as>(); }, "Get model as sparse exact DTMC") - .def( - "_as_sparse_idtmc", [](ModelBase& modelbase) { return modelbase.as>(); }, "Get model as sparse interval DTMC") - .def( - "_as_sparse_pdtmc", [](ModelBase& modelbase) { return modelbase.as>(); }, "Get model as sparse parametric DTMC") - .def( - "_as_sparse_idtmc", [](ModelBase& modelbase) { return modelbase.as>(); }, "Get model as sparse interval DTMC") - .def( - "_as_sparse_exact_idtmc", [](ModelBase& modelbase) { return modelbase.as>(); }, - "Get model as sparse exact interval DTMC") - .def( - "_as_sparse_mdp", [](ModelBase& modelbase) { return modelbase.as>(); }, "Get model as sparse MDP") - .def( - "_as_sparse_exact_mdp", [](ModelBase& modelbase) { return modelbase.as>(); }, "Get model as sparse exact MDP") - .def( - "_as_sparse_imdp", [](ModelBase& modelbase) { return modelbase.as>(); }, "Get model as sparse interval MDP") - .def( - "_as_sparse_exact_imdp", [](ModelBase& modelbase) { return modelbase.as>(); }, - "Get model as sparse exact interval MDP") - .def( - "_as_sparse_pmdp", [](ModelBase& modelbase) { return modelbase.as>(); }, "Get model as sparse parametric MDP") - .def( - "_as_sparse_pomdp", [](ModelBase& modelbase) { return modelbase.as>(); }, "Get model as sparse POMDP") - .def( - "_as_sparse_ipomdp", [](ModelBase& modelbase) { return modelbase.as>(); }, "Get model as sparse interval POMDP") - .def( - "_as_sparse_exact_ipomdp", [](ModelBase& modelbase) { return modelbase.as>(); }, - "Get model as sparse interval exact POMDP") - .def( - "_as_sparse_exact_pomdp", [](ModelBase& modelbase) { return modelbase.as>(); }, - "Get model as sparse exact POMDP") - .def( - "_as_sparse_ppomdp", [](ModelBase& modelbase) { return modelbase.as>(); }, - "Get model as sparse parametric POMDP") - .def( - "_as_sparse_ctmc", [](ModelBase& modelbase) { return modelbase.as>(); }, "Get model as sparse CTMC") - .def( - "_as_sparse_exact_ctmc", [](ModelBase& modelbase) { return modelbase.as>(); }, "Get model as sparse exact CTMC") - .def( - "_as_sparse_ictmc", [](ModelBase& modelbase) { return modelbase.as>(); }, "Get model as sparse interval CTMC") - .def( - "_as_sparse_exact_ictmc", [](ModelBase& modelbase) { return modelbase.as>(); }, - "Get model as sparse exact interval CTMC") - .def( - "_as_sparse_pctmc", [](ModelBase& modelbase) { return modelbase.as>(); }, "Get model as sparse parametric CTMC") - .def( - "_as_sparse_ma", [](ModelBase& modelbase) { return modelbase.as>(); }, "Get model as sparse MA") - .def( - "_as_sparse_exact_ma", [](ModelBase& modelbase) { return modelbase.as>(); }, - "Get model as sparse exact MA") - .def( - "_as_sparse_ima", [](ModelBase& modelbase) { return modelbase.as>(); }, "Get model as sparse interval MA") - .def( - "_as_sparse_exact_ima", [](ModelBase& modelbase) { return modelbase.as>(); }, - "Get model as sparse exact interval MA") - .def( - "_as_sparse_pma", [](ModelBase& modelbase) { return modelbase.as>(); }, - "Get model as sparse parametric MA") - .def( - "_as_sparse_smg", [](ModelBase& modelbase) { return modelbase.as>(); }, "Get model as sparse SMG") - .def( - "_as_sparse_exact_smg", [](ModelBase& modelbase) { return modelbase.as>(); }, "Get model as sparse exact SMG") - .def( - "_as_sparse_ismg", [](ModelBase& modelbase) { return modelbase.as>(); }, "Get model as sparse interval SMG") - .def( - "_as_sparse_exact_ismg", [](ModelBase& modelbase) { return modelbase.as>(); }, - "Get model as sparse exact interval SMG") - .def( - "_as_sparse_psmg", [](ModelBase& modelbase) { return modelbase.as>(); }, "Get model as sparse parametric SMG") - .def( - "_as_symbolic_dtmc", [](ModelBase& modelbase) { return modelbase.as>(); }, - "Get model as symbolic DTMC") - .def( - "_as_symbolic_exact_dtmc", [](ModelBase& modelbase) { return modelbase.as>(); }, - "Get model as symbolic exact DTMC") - .def( - "_as_symbolic_pdtmc", [](ModelBase& modelbase) { return modelbase.as>(); }, - "Get model as symbolic parametric DTMC") - .def( - "_as_symbolic_mdp", [](ModelBase& modelbase) { return modelbase.as>(); }, - "Get model as symbolic MDP") - .def( - "_as_symbolic_exact_mdp", [](ModelBase& modelbase) { return modelbase.as>(); }, - "Get model as symbolic exact MDP") - .def( - "_as_symbolic_pmdp", [](ModelBase& modelbase) { return modelbase.as>(); }, - "Get model as symbolic parametric MDP") - .def( - "_as_symbolic_ctmc", [](ModelBase& modelbase) { return modelbase.as>(); }, - "Get model as symbolic CTMC") - .def( - "_as_symbolic_exact_ctmc", [](ModelBase& modelbase) { return modelbase.as>(); }, - "Get model as symbolic exact CTMC") - .def( - "_as_symbolic_pctmc", [](ModelBase& modelbase) { return modelbase.as>(); }, - "Get model as symbolic parametric CTMC") - .def( - "_as_symbolic_ma", [](ModelBase& modelbase) { return modelbase.as>(); }, - "Get model as symbolic MA") - .def( - "_as_symbolic_exact_ma", - [](ModelBase& modelbase) { return modelbase.as>(); }, - "Get model as symbolic exact MA") - .def( - "_as_symbolic_pma", - [](ModelBase& modelbase) { return modelbase.as>(); }, - "Get model as symbolic parametric MA"); + .def_property_readonly("is_nondeterministic_model", &ModelBase::isNondeterministicModel, "Flag whether the model contains nondeterminism"); + define_model_as_sparse(modelBase); + define_model_as_sparse(modelBase); + define_model_as_sparse(modelBase); + define_model_as_sparse(modelBase); + define_model_as_sparse(modelBase); + define_model_as_symbolic(modelBase); + define_model_as_symbolic(modelBase); + define_model_as_symbolic(modelBase); } // Bindings for sparse models