diff --git a/src/storm-dft/api/storm-dft.h b/src/storm-dft/api/storm-dft.h index 136e8bfb4..ca4c7588d 100644 --- a/src/storm-dft/api/storm-dft.h +++ b/src/storm-dft/api/storm-dft.h @@ -69,7 +69,7 @@ namespace storm { typename storm::modelchecker::DFTModelChecker::dft_results analyzeDFT(storm::storage::DFT const& dft, std::vector> const& properties, bool symred, bool allowModularisation, bool enableDC, bool printOutput) { - storm::modelchecker::DFTModelChecker modelChecker; + storm::modelchecker::DFTModelChecker modelChecker(printOutput); typename storm::modelchecker::DFTModelChecker::dft_results results = modelChecker.check(dft, properties, symred, allowModularisation, enableDC, 0.0); if (printOutput) { modelChecker.printTimings(); @@ -95,7 +95,7 @@ namespace storm { typename storm::modelchecker::DFTModelChecker::dft_results analyzeDFTApprox(storm::storage::DFT const& dft, std::vector> const& properties, bool symred, bool allowModularisation, bool enableDC, double approximationError, bool printOutput) { - storm::modelchecker::DFTModelChecker modelChecker; + storm::modelchecker::DFTModelChecker modelChecker(printOutput); typename storm::modelchecker::DFTModelChecker::dft_results results = modelChecker.check(dft, properties, symred, allowModularisation, enableDC, approximationError); if (printOutput) { diff --git a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp index 658ed75c6..d96aacfc4 100644 --- a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp +++ b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp @@ -348,9 +348,13 @@ namespace storm { 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); explorationTimer.stop(); + // Print model information + if (printInfo) { + model->printModelInformationToStream(std::cout); + } + // Export the model if required // TODO move this outside of the model checker? if (ioSettings.isExportExplicitSet()) { diff --git a/src/storm-dft/modelchecker/dft/DFTModelChecker.h b/src/storm-dft/modelchecker/dft/DFTModelChecker.h index 6da5d5aaa..cf05cbb8f 100644 --- a/src/storm-dft/modelchecker/dft/DFTModelChecker.h +++ b/src/storm-dft/modelchecker/dft/DFTModelChecker.h @@ -25,7 +25,7 @@ namespace storm { /*! * Constructor. */ - DFTModelChecker() { + DFTModelChecker(bool printOutput) : printInfo(printOutput) { } /*! @@ -58,6 +58,8 @@ namespace storm { private: + bool printInfo; + // Timing values storm::utility::Stopwatch buildingTimer; storm::utility::Stopwatch explorationTimer;