diff --git a/src/dft/dft.cpp b/src/dft/dft.cpp index 4c2ca64..587d8c3 100644 --- a/src/dft/dft.cpp +++ b/src/dft/dft.cpp @@ -3,16 +3,21 @@ #include "storm-dft/builder/ExplicitDFTModelBuilderApprox.h" #include "storm/settings/SettingsManager.h" #include "storm-dft/settings/modules/DFTSettings.h" +#include "storm-dft/storage/dft/DFTIsomorphism.h" // Thin wrapper for model building using one formula as argument template -std::shared_ptr> buildModelFromJsonDft(std::string const& jsonDft) { +std::shared_ptr> buildModelFromJsonDft(std::string const& jsonDft, bool symred) { // Build DFT storm::parser::DFTJsonParser parser; storm::storage::DFT dft = parser.parseJson(jsonDft); // Build model std::map>> emptySymmetry; storm::storage::DFTIndependentSymmetries symmetries(emptySymmetry); + if (symred) { + auto colouring = dft.colourDFT(); + symmetries = dft.findSymmetries(colouring); + } storm::builder::ExplicitDFTModelBuilderApprox builder(dft, symmetries, true); typename storm::builder::ExplicitDFTModelBuilderApprox::LabelOptions labeloptions({}, true); builder.buildModel(labeloptions, 0, 0.0); @@ -24,6 +29,6 @@ void define_dft(py::module& m) { storm::settings::addModule(); }, "Initialize Storm-dft"); // Build model - m.def("build_sparse_model_from_json_dft", &buildModelFromJsonDft, "Build the model", py::arg("jsonDft")); - m.def("build_sparse_parametric_model_from_json_dft", &buildModelFromJsonDft, "Build the parametric model", py::arg("jsonDft")); + m.def("build_sparse_model_from_json_dft", &buildModelFromJsonDft, "Build the model", py::arg("jsonDft"), py::arg("symred") = false); + m.def("build_sparse_parametric_model_from_json_dft", &buildModelFromJsonDft, "Build the parametric model", py::arg("jsonDft"), py::arg("symred") = false); }