diff --git a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp index 2a2a62e14..35367ed3a 100644 --- a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp +++ b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp @@ -342,23 +342,24 @@ namespace storm { return results; } else { // Build a single Markov Automaton + auto ioSettings = storm::settings::getModule(); STORM_LOG_DEBUG("Building Model..."); storm::builder::ExplicitDFTModelBuilder builder(dft, symmetries, enableDC); - typename storm::builder::ExplicitDFTModelBuilder::LabelOptions labeloptions(properties, storm::settings::getModule().isExportExplicitSet()); + typename storm::builder::ExplicitDFTModelBuilder::LabelOptions labeloptions(properties, ioSettings.isExportExplicitSet() || ioSettings.isExportDotSet()); builder.buildModel(labeloptions, 0, 0.0); std::shared_ptr> model = builder.getModel(); - //model->printModelInformationToStream(std::cout); + model->printModelInformationToStream(std::cout); explorationTimer.stop(); // Export the model if required // TODO move this outside of the model checker? - if (storm::settings::getModule().isExportExplicitSet()) { - std::ofstream stream; - storm::utility::openFile(storm::settings::getModule().getExportExplicitFilename(), stream); + if (ioSettings.isExportExplicitSet()) { std::vector parameterNames; // TODO fill parameter names - storm::exporter::explicitExportSparseModel(stream, model, parameterNames); - storm::utility::closeFile(stream); + storm::api::exportSparseModelAsDrn(model, ioSettings.getExportExplicitFilename(), parameterNames); + } + if (ioSettings.isExportDotSet()) { + storm::api::exportSparseModelAsDot(model, ioSettings.getExportDotFilename()); } // Model checking