sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

Disable unnecessary output for DFT model checking

tempestpy_adaptions
Matthias Volk 7 years ago
parent
a03f9c80d2
commit
6fa88b1c14
4 changed files with 37 additions and 33 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 4
      src/storm-dft-cli/storm-dft.cpp
  2. 16
      src/storm-dft/api/storm-dft.h
  3. 48
      src/storm-dft/modelchecker/dft/DFTModelChecker.cpp
  4. 2
      src/test/storm-dft/api/DftModelCheckerTest.cpp

4
src/storm-dft-cli/storm-dft.cpp
View File

@ -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);
}
}

16
src/storm-dft/api/storm-dft.h
View File

@ -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;
}

48
src/storm-dft/modelchecker/dft/DFTModelChecker.cpp
View File

@ -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;
}

2
src/test/storm-dft/api/DftModelCheckerTest.cpp
View File

@ -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]);
}

Write Preview
Loading…
Cancel
Save