From 6fa88b1c14e68c49f64ca55b59bf3a1d9b68ffb0 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Mon, 26 Mar 2018 11:14:00 +0200 Subject: [PATCH] Disable unnecessary output for DFT model checking --- src/storm-dft-cli/storm-dft.cpp | 4 +- src/storm-dft/api/storm-dft.h | 16 ++++--- .../modelchecker/dft/DFTModelChecker.cpp | 48 +++++++++---------- .../storm-dft/api/DftModelCheckerTest.cpp | 2 +- 4 files changed, 37 insertions(+), 33 deletions(-) diff --git a/src/storm-dft-cli/storm-dft.cpp b/src/storm-dft-cli/storm-dft.cpp index f051570dc..9923330d0 100644 --- a/src/storm-dft-cli/storm-dft.cpp +++ b/src/storm-dft-cli/storm-dft.cpp @@ -107,9 +107,9 @@ void processOptions() { // Carry out the actual analysis if (faultTreeSettings.isApproximationErrorSet()) { // Approximate analysis - storm::api::analyzeDFTApprox(*dft, props, faultTreeSettings.useSymmetryReduction(), faultTreeSettings.useModularisation(), !faultTreeSettings.isDisableDC(), faultTreeSettings.getApproximationError()); + storm::api::analyzeDFTApprox(*dft, props, faultTreeSettings.useSymmetryReduction(), faultTreeSettings.useModularisation(), !faultTreeSettings.isDisableDC(), faultTreeSettings.getApproximationError(), true); } else { - storm::api::analyzeDFT(*dft, props, faultTreeSettings.useSymmetryReduction(), faultTreeSettings.useModularisation(), !faultTreeSettings.isDisableDC()); + storm::api::analyzeDFT(*dft, props, faultTreeSettings.useSymmetryReduction(), faultTreeSettings.useModularisation(), !faultTreeSettings.isDisableDC(), true); } } diff --git a/src/storm-dft/api/storm-dft.h b/src/storm-dft/api/storm-dft.h index 003c03f14..db6d7b3e4 100644 --- a/src/storm-dft/api/storm-dft.h +++ b/src/storm-dft/api/storm-dft.h @@ -53,11 +53,13 @@ namespace storm { * @return Result. */ template - typename storm::modelchecker::DFTModelChecker::dft_results analyzeDFT(storm::storage::DFT const& dft, std::vector> const& properties, bool symred, bool allowModularisation, bool enableDC) { + 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; typename storm::modelchecker::DFTModelChecker::dft_results results = modelChecker.check(dft, properties, symred, allowModularisation, enableDC, 0.0); - modelChecker.printTimings(); - modelChecker.printResults(); + if (printOutput) { + modelChecker.printTimings(); + modelChecker.printResults(); + } return results; } @@ -75,11 +77,13 @@ namespace storm { * @return Result. */ template - typename storm::modelchecker::DFTModelChecker::dft_results analyzeDFTApprox(storm::storage::DFT const& dft, std::vector> const& properties, bool symred, bool allowModularisation, bool enableDC, double approximationError) { + 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; typename storm::modelchecker::DFTModelChecker::dft_results results = modelChecker.check(dft, properties, symred, allowModularisation, enableDC, approximationError); - modelChecker.printTimings(); - modelChecker.printResults(); + if (printOutput) { + modelChecker.printTimings(); + modelChecker.printResults(); + } return results; } diff --git a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp index c3e7996c7..31ba6789d 100644 --- a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp +++ b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp @@ -176,7 +176,7 @@ namespace storm { bool firstTime = true; std::shared_ptr> composedModel; for (auto const ft : dfts) { - STORM_LOG_INFO("Building Model via parallel composition..."); + STORM_LOG_DEBUG("Building Model via parallel composition..."); explorationTimer.start(); // Find symmetries @@ -185,12 +185,12 @@ namespace storm { if(symred) { auto colouring = ft.colourDFT(); symmetries = ft.findSymmetries(colouring); - STORM_LOG_INFO("Found " << symmetries.groups.size() << " symmetries."); + STORM_LOG_DEBUG("Found " << symmetries.groups.size() << " symmetries."); STORM_LOG_TRACE("Symmetries: " << std::endl << symmetries); } // Build a single CTMC - STORM_LOG_INFO("Building Model..."); + STORM_LOG_DEBUG("Building Model..."); storm::builder::ExplicitDFTModelBuilder builder(ft, symmetries, enableDC); typename storm::builder::ExplicitDFTModelBuilder::LabelOptions labeloptions(properties); builder.buildModel(labeloptions, 0, 0.0); @@ -226,7 +226,7 @@ namespace storm { } } - composedModel->printModelInformationToStream(std::cout); + //composedModel->printModelInformationToStream(std::cout); return composedModel; } else { // No composition was possible @@ -237,17 +237,17 @@ namespace storm { if(symred) { auto colouring = dft.colourDFT(); symmetries = dft.findSymmetries(colouring); - STORM_LOG_INFO("Found " << symmetries.groups.size() << " symmetries."); + STORM_LOG_DEBUG("Found " << symmetries.groups.size() << " symmetries."); STORM_LOG_TRACE("Symmetries: " << std::endl << symmetries); } // Build a single CTMC - STORM_LOG_INFO("Building Model..."); + STORM_LOG_DEBUG("Building Model..."); storm::builder::ExplicitDFTModelBuilder builder(dft, symmetries, enableDC); typename storm::builder::ExplicitDFTModelBuilder::LabelOptions labeloptions(properties); builder.buildModel(labeloptions, 0, 0.0); std::shared_ptr> model = builder.getModel(); - model->printModelInformationToStream(std::cout); + //model->printModelInformationToStream(std::cout); explorationTimer.stop(); STORM_LOG_THROW(model->isOfType(storm::models::ModelType::Ctmc), storm::exceptions::NotSupportedException, "Parallel composition only applicable for CTMCs"); return model->template as>(); @@ -264,7 +264,7 @@ namespace storm { if(symred) { auto colouring = dft.colourDFT(); symmetries = dft.findSymmetries(colouring); - STORM_LOG_INFO("Found " << symmetries.groups.size() << " symmetries."); + STORM_LOG_DEBUG("Found " << symmetries.groups.size() << " symmetries."); STORM_LOG_TRACE("Symmetries: " << std::endl << symmetries); } @@ -292,7 +292,7 @@ namespace storm { if (iteration > 0) { explorationTimer.start(); } - STORM_LOG_INFO("Building model..."); + STORM_LOG_DEBUG("Building model..."); // TODO Matthias refine model using existing model and MC results builder.buildModel(labeloptions, iteration, approximationError); explorationTimer.stop(); @@ -301,10 +301,10 @@ namespace storm { // TODO Matthias: possible to do bisimulation on approximated model and not on concrete one? // Build model for lower bound - STORM_LOG_INFO("Getting model for lower bound..."); + STORM_LOG_DEBUG("Getting model for lower bound..."); model = builder.getModelApproximation(true, !probabilityFormula); // We only output the info from the lower bound as the info for the upper bound is the same - model->printModelInformationToStream(std::cout); + //model->printModelInformationToStream(std::cout); buildingTimer.stop(); // Check lower bounds @@ -314,7 +314,7 @@ namespace storm { approxResult.first = newResult[0]; // Build model for upper bound - STORM_LOG_INFO("Getting model for upper bound..."); + STORM_LOG_DEBUG("Getting model for upper bound..."); buildingTimer.start(); model = builder.getModelApproximation(false, !probabilityFormula); buildingTimer.stop(); @@ -326,25 +326,25 @@ namespace storm { ++iteration; STORM_LOG_ASSERT(comparator.isLess(approxResult.first, approxResult.second) || comparator.isEqual(approxResult.first, approxResult.second), "Under-approximation " << approxResult.first << " is greater than over-approximation " << approxResult.second); - STORM_LOG_INFO("Result after iteration " << iteration << ": (" << std::setprecision(10) << approxResult.first << ", " << approxResult.second << ")"); + //STORM_LOG_INFO("Result after iteration " << iteration << ": (" << std::setprecision(10) << approxResult.first << ", " << approxResult.second << ")"); totalTimer.stop(); printTimings(); totalTimer.start(); STORM_LOG_THROW(!storm::utility::isInfinity(approxResult.first) && !storm::utility::isInfinity(approxResult.second), storm::exceptions::NotSupportedException, "Approximation does not work if result might be infinity."); } while (!isApproximationSufficient(approxResult.first, approxResult.second, approximationError, probabilityFormula)); - STORM_LOG_INFO("Finished approximation after " << iteration << " iteration" << (iteration > 1 ? "s." : ".")); + //STORM_LOG_INFO("Finished approximation after " << iteration << " iteration" << (iteration > 1 ? "s." : ".")); dft_results results; results.push_back(approxResult); return results; } else { // Build a single Markov Automaton - STORM_LOG_INFO("Building Model..."); + STORM_LOG_DEBUG("Building Model..."); storm::builder::ExplicitDFTModelBuilder builder(dft, symmetries, enableDC); typename storm::builder::ExplicitDFTModelBuilder::LabelOptions labeloptions(properties, storm::settings::getModule().isExportExplicitSet()); 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 @@ -373,15 +373,15 @@ namespace storm { // Bisimulation if (model->isOfType(storm::models::ModelType::Ctmc) && storm::settings::getModule().isBisimulationSet()) { bisimulationTimer.start(); - STORM_LOG_INFO("Bisimulation..."); + STORM_LOG_DEBUG("Bisimulation..."); model = storm::api::performDeterministicSparseBisimulationMinimization>(model->template as>(), properties, storm::storage::BisimulationType::Weak)->template as>(); - STORM_LOG_INFO("No. states (Bisimulation): " << model->getNumberOfStates()); - STORM_LOG_INFO("No. transitions (Bisimulation): " << model->getNumberOfTransitions()); + STORM_LOG_DEBUG("No. states (Bisimulation): " << model->getNumberOfStates()); + STORM_LOG_DEBUG("No. transitions (Bisimulation): " << model->getNumberOfTransitions()); bisimulationTimer.stop(); } // Check the model - STORM_LOG_INFO("Model checking..."); + STORM_LOG_DEBUG("Model checking..."); modelCheckingTimer.start(); std::vector results; @@ -390,18 +390,18 @@ namespace storm { for (auto property : properties) { singleModelCheckingTimer.reset(); singleModelCheckingTimer.start(); - STORM_PRINT_AND_LOG("Model checking property " << *property << " ..." << std::endl); + //STORM_PRINT_AND_LOG("Model checking property " << *property << " ..." << std::endl); std::unique_ptr result(storm::api::verifyWithSparseEngine(model, storm::api::createTask(property, true))); STORM_LOG_ASSERT(result, "Result does not exist."); result->filter(storm::modelchecker::ExplicitQualitativeCheckResult(model->getInitialStates())); ValueType resultValue = result->asExplicitQuantitativeCheckResult().getValueMap().begin()->second; - STORM_PRINT_AND_LOG("Result (initial states): " << resultValue << std::endl); + //STORM_PRINT_AND_LOG("Result (initial states): " << resultValue << std::endl); results.push_back(resultValue); singleModelCheckingTimer.stop(); - STORM_PRINT_AND_LOG("Time for model checking: " << singleModelCheckingTimer << "." << std::endl); + //STORM_PRINT_AND_LOG("Time for model checking: " << singleModelCheckingTimer << "." << std::endl); } modelCheckingTimer.stop(); - STORM_LOG_INFO("Model checking done."); + STORM_LOG_DEBUG("Model checking done."); return results; } diff --git a/src/test/storm-dft/api/DftModelCheckerTest.cpp b/src/test/storm-dft/api/DftModelCheckerTest.cpp index 902108018..5db58d60d 100644 --- a/src/test/storm-dft/api/DftModelCheckerTest.cpp +++ b/src/test/storm-dft/api/DftModelCheckerTest.cpp @@ -65,7 +65,7 @@ namespace { std::shared_ptr> dft = storm::api::loadDFTGalileo(file); std::string property = "Tmin=? [F \"failed\"]"; std::vector> properties = storm::api::extractFormulasFromProperties(storm::api::parseProperties(property)); - typename storm::modelchecker::DFTModelChecker::dft_results results = storm::api::analyzeDFT(*dft, properties, config.useSR, config.useMod, config.useDC); + typename storm::modelchecker::DFTModelChecker::dft_results results = storm::api::analyzeDFT(*dft, properties, config.useSR, config.useMod, config.useDC, false); return boost::get(results[0]); }