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<ValueType>(*dft, props, faultTreeSettings.useSymmetryReduction(), faultTreeSettings.useModularisation(), !faultTreeSettings.isDisableDC(), faultTreeSettings.getApproximationError());
+ storm::api::analyzeDFTApprox<ValueType>(*dft, props, faultTreeSettings.useSymmetryReduction(), faultTreeSettings.useModularisation(), !faultTreeSettings.isDisableDC(), faultTreeSettings.getApproximationError(), true);
} else {
- storm::api::analyzeDFT<ValueType>(*dft, props, faultTreeSettings.useSymmetryReduction(), faultTreeSettings.useModularisation(), !faultTreeSettings.isDisableDC());
+ storm::api::analyzeDFT<ValueType>(*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 ValueType>
- typename storm::modelchecker::DFTModelChecker<ValueType>::dft_results analyzeDFT(storm::storage::DFT<ValueType> const& dft, std::vector<std::shared_ptr<storm::logic::Formula const>> const& properties, bool symred, bool allowModularisation, bool enableDC) {
+ typename storm::modelchecker::DFTModelChecker<ValueType>::dft_results analyzeDFT(storm::storage::DFT<ValueType> const& dft, std::vector<std::shared_ptr<storm::logic::Formula const>> const& properties, bool symred, bool allowModularisation, bool enableDC, bool printOutput) {
storm::modelchecker::DFTModelChecker<ValueType> modelChecker;
typename storm::modelchecker::DFTModelChecker<ValueType>::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 ValueType>
- typename storm::modelchecker::DFTModelChecker<ValueType>::dft_results analyzeDFTApprox(storm::storage::DFT<ValueType> const& dft, std::vector<std::shared_ptr<storm::logic::Formula const>> const& properties, bool symred, bool allowModularisation, bool enableDC, double approximationError) {
+ typename storm::modelchecker::DFTModelChecker<ValueType>::dft_results analyzeDFTApprox(storm::storage::DFT<ValueType> const& dft, std::vector<std::shared_ptr<storm::logic::Formula const>> const& properties, bool symred, bool allowModularisation, bool enableDC, double approximationError, bool printOutput) {
storm::modelchecker::DFTModelChecker<ValueType> modelChecker;
typename storm::modelchecker::DFTModelChecker<ValueType>::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<storm::models::sparse::Ctmc<ValueType>> 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<ValueType> builder(ft, symmetries, enableDC);
typename storm::builder::ExplicitDFTModelBuilder<ValueType>::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<ValueType> builder(dft, symmetries, enableDC);
typename storm::builder::ExplicitDFTModelBuilder<ValueType>::LabelOptions labeloptions(properties);
builder.buildModel(labeloptions, 0, 0.0);
std::shared_ptr<storm::models::sparse::Model<ValueType>> 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<storm::models::sparse::Ctmc<ValueType>>();
@@ -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<ValueType>(approxResult.first) && !storm::utility::isInfinity<ValueType>(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<ValueType> builder(dft, symmetries, enableDC);
typename storm::builder::ExplicitDFTModelBuilder<ValueType>::LabelOptions labeloptions(properties, storm::settings::getModule<storm::settings::modules::IOSettings>().isExportExplicitSet());
builder.buildModel(labeloptions, 0, 0.0);
std::shared_ptr<storm::models::sparse::Model<ValueType>> 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<storm::settings::modules::GeneralSettings>().isBisimulationSet()) {
bisimulationTimer.start();
- STORM_LOG_INFO("Bisimulation...");
+ STORM_LOG_DEBUG("Bisimulation...");
model = storm::api::performDeterministicSparseBisimulationMinimization<storm::models::sparse::Ctmc<ValueType>>(model->template as<storm::models::sparse::Ctmc<ValueType>>(), properties, storm::storage::BisimulationType::Weak)->template as<storm::models::sparse::Ctmc<ValueType>>();
- 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<ValueType> 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<storm::modelchecker::CheckResult> result(storm::api::verifyWithSparseEngine<ValueType>(model, storm::api::createTask<ValueType>(property, true)));
STORM_LOG_ASSERT(result, "Result does not exist.");
result->filter(storm::modelchecker::ExplicitQualitativeCheckResult(model->getInitialStates()));
ValueType resultValue = result->asExplicitQuantitativeCheckResult<ValueType>().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<storm::storage::DFT<double>> dft = storm::api::loadDFTGalileo<double>(file);
std::string property = "Tmin=? [F \"failed\"]";
std::vector<std::shared_ptr<storm::logic::Formula const>> properties = storm::api::extractFormulasFromProperties(storm::api::parseProperties(property));
- typename storm::modelchecker::DFTModelChecker<double>::dft_results results = storm::api::analyzeDFT<double>(*dft, properties, config.useSR, config.useMod, config.useDC);
+ typename storm::modelchecker::DFTModelChecker<double>::dft_results results = storm::api::analyzeDFT<double>(*dft, properties, config.useSR, config.useMod, config.useDC, false);
return boost::get<double>(results[0]);
}