From a73c2691b68957b1efa2573c97d2b37bd6e76eb4 Mon Sep 17 00:00:00 2001 From: Alexander Bork Date: Mon, 15 Jul 2019 17:41:37 +0200 Subject: [PATCH] Integration of the new settings in the DFT analysis --- src/storm-dft-cli/storm-dft.cpp | 35 ++-- src/storm-dft/api/storm-dft.h | 9 +- .../builder/ExplicitDFTModelBuilder.cpp | 7 +- .../modelchecker/dft/DFTModelChecker.cpp | 193 +++++++++++++----- .../modelchecker/dft/DFTModelChecker.h | 15 +- src/storm-dft/settings/DftSettings.cpp | 2 + 6 files changed, 177 insertions(+), 84 deletions(-) diff --git a/src/storm-dft-cli/storm-dft.cpp b/src/storm-dft-cli/storm-dft.cpp index 7ce6eadea..1cc9a02e2 100644 --- a/src/storm-dft-cli/storm-dft.cpp +++ b/src/storm-dft-cli/storm-dft.cpp @@ -10,6 +10,7 @@ #include "storm/settings/modules/DebugSettings.h" #include "storm/settings/modules/IOSettings.h" #include "storm/settings/modules/ResourceSettings.h" +#include "storm/settings/modules/TransformationSettings.h" #include "storm/utility/initialize.h" #include "storm-cli-utilities/cli.h" #include "storm-parsers/api/storm-parsers.h" @@ -28,6 +29,7 @@ void processOptions() { storm::settings::modules::FaultTreeSettings const& faultTreeSettings = storm::settings::getModule(); storm::settings::modules::IOSettings const& ioSettings = storm::settings::getModule(); storm::settings::modules::DftGspnSettings const& dftGspnSettings = storm::settings::getModule(); + storm::settings::modules::TransformationSettings const &transformationSettings = storm::settings::getModule(); auto dftTransformator = storm::transformations::dft::DftTransformator(); @@ -55,7 +57,7 @@ void processOptions() { } // Eliminate non-binary dependencies - if (dft->getDependencies().size() > 0) { + if (!dft->getDependencies().empty()) { dft = dftTransformator.transformBinaryFDEPs(*dft); } // Check well-formedness of DFT @@ -81,7 +83,7 @@ void processOptions() { // SMT if (dftIOSettings.isExportToSmt()) { dft = dftTransformator.transformUniqueFailedBe(*dft); - if (dft->getDependencies().size() > 0) { + if (!dft->getDependencies().empty()) { dft = dftTransformator.transformBinaryFDEPs(*dft); } // Export to smtlib2 @@ -91,14 +93,13 @@ void processOptions() { // TODO introduce some flags bool useSMT = false; - bool printOutput = false; uint64_t solverTimeout = 10; #ifdef STORM_HAVE_Z3 if (faultTreeSettings.solveWithSMT()) { useSMT = true; STORM_PRINT("Use SMT for preprocessing" << std::endl) dft = dftTransformator.transformUniqueFailedBe(*dft); - if (dft->getDependencies().size() > 0) { + if (!dft->getDependencies().empty()) { // Making the constantly failed BE unique may introduce non-binary FDEPs dft = dftTransformator.transformBinaryFDEPs(*dft); } @@ -112,25 +113,20 @@ void processOptions() { solverTimeout); preResults.upperBEBound = storm::dft::utility::FailureBoundFinder::getAlwaysFailedBound(*dft, useSMT, solverTimeout); - if (printOutput) { - STORM_PRINT("BE FAILURE BOUNDS" << std::endl << - "========================================" << std::endl << + STORM_LOG_DEBUG("BE FAILURE BOUNDS" << std::endl << "========================================" << std::endl << "Lower bound: " << std::to_string(preResults.lowerBEBound) << std::endl << - "Upper bound: " << std::to_string(preResults.upperBEBound) << std::endl) - } + "Upper bound: " << std::to_string(preResults.upperBEBound) << std::endl); preResults.fdepConflicts = storm::dft::utility::FDEPConflictFinder::getDependencyConflicts(*dft, true, solverTimeout); - if (printOutput) { - STORM_PRINT("========================================" << std::endl << + STORM_LOG_DEBUG("========================================" << std::endl << "FDEP CONFLICTS" << std::endl << "========================================" - << std::endl) - for (auto pair: preResults.fdepConflicts) { - STORM_PRINT("Conflict between " << dft->getElement(pair.first)->name() << " and " - << dft->getElement(pair.second)->name() << std::endl) - } + << std::endl); + for (auto pair: preResults.fdepConflicts) { + STORM_LOG_DEBUG("Conflict between " << dft->getElement(pair.first)->name() << " and " + << dft->getElement(pair.second)->name() << std::endl); } // Set the conflict map of the dft @@ -149,7 +145,7 @@ void processOptions() { #ifdef STORM_HAVE_Z3 if (faultTreeSettings.solveWithSMT()) { // Solve with SMT - STORM_LOG_DEBUG("Running DFT analysis with use of SMT"); + STORM_LOG_DEBUG("Running DFT analysis with use of SMT" << std::endl); // Set dynamic behavior vector storm::api::analyzeDFTSMT(*dft, true); } @@ -263,7 +259,10 @@ void processOptions() { approximationError = faultTreeSettings.getApproximationError(); } storm::api::analyzeDFT(*dft, props, faultTreeSettings.useSymmetryReduction(), faultTreeSettings.useModularisation(), relevantEvents, - faultTreeSettings.isAllowDCForRelevantEvents(), approximationError, faultTreeSettings.getApproximationHeuristic(), true); + faultTreeSettings.isAllowDCForRelevantEvents(), approximationError, + faultTreeSettings.getApproximationHeuristic(), + transformationSettings.isChainEliminationSet(), + transformationSettings.isIgnoreLabelingSet(), true); } } diff --git a/src/storm-dft/api/storm-dft.h b/src/storm-dft/api/storm-dft.h index c9aa6b902..470e3a218 100644 --- a/src/storm-dft/api/storm-dft.h +++ b/src/storm-dft/api/storm-dft.h @@ -81,6 +81,8 @@ namespace storm { * @param allowDCForRelevantEvents If true, Don't Care propagation is allowed even for relevant events. * @param approximationError Allowed approximation error. Value 0 indicates no approximation. * @param approximationHeuristic Heuristic used for state space exploration. + * @param eliminateChains If true, chains of non-Markovian states are elimianted from the resulting MA + * @param ignoreLabeling If true, the labeling of states is ignored during state elimination * @param printOutput If true, model information, timings, results, etc. are printed. * @return Results. */ @@ -88,11 +90,14 @@ namespace storm { typename storm::modelchecker::DFTModelChecker::dft_results analyzeDFT(storm::storage::DFT const& dft, std::vector> const& properties, bool symred = true, bool allowModularisation = true, std::set const& relevantEvents = {}, bool allowDCForRelevantEvents = true, double approximationError = 0.0, - storm::builder::ApproximationHeuristic approximationHeuristic = storm::builder::ApproximationHeuristic::DEPTH, bool printOutput = false) { + storm::builder::ApproximationHeuristic approximationHeuristic = storm::builder::ApproximationHeuristic::DEPTH, + bool eliminateChains = false, bool ignoreLabeling = false, bool printOutput = false) { storm::modelchecker::DFTModelChecker modelChecker(printOutput); typename storm::modelchecker::DFTModelChecker::dft_results results = modelChecker.check(dft, properties, symred, allowModularisation, relevantEvents, allowDCForRelevantEvents, approximationError, - approximationHeuristic); + approximationHeuristic, + eliminateChains, + ignoreLabeling); if (printOutput) { modelChecker.printTimings(); modelChecker.printResults(results); diff --git a/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp b/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp index ad1f5d449..0f3196516 100644 --- a/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp +++ b/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp @@ -652,11 +652,8 @@ namespace storm { maComponents.exitRates = std::move(modelComponents.exitRates); ma = std::make_shared>(std::move(maComponents)); } - if (ma->hasOnlyTrivialNondeterminism()) { - // Markov automaton can be converted into CTMC - // TODO apply transformer to all MAs - model = storm::transformer::NonMarkovianChainTransformer::eliminateNonmarkovianStates( - ma); + if (ma->isConvertibleToCtmc()) { + model = ma->convertToCtmc(); } else { model = ma; } diff --git a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp index eed303311..4af4c28c5 100644 --- a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp +++ b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp @@ -7,6 +7,8 @@ #include "storm/utility/DirectEncodingExporter.h" #include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h" #include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h" +#include "storm/models/ModelType.h" +#include "storm/transformer/NonMarkovianChainTransformer.h" #include "storm-dft/builder/ExplicitDFTModelBuilder.h" #include "storm-dft/storage/dft/DFTIsomorphism.h" @@ -17,7 +19,13 @@ namespace storm { namespace modelchecker { template - typename DFTModelChecker::dft_results DFTModelChecker::check(storm::storage::DFT const& origDft, std::vector> const& properties, bool symred, bool allowModularisation, std::set const& relevantEvents, bool allowDCForRelevantEvents, double approximationError, storm::builder::ApproximationHeuristic approximationHeuristic) { + typename DFTModelChecker::dft_results + DFTModelChecker::check(storm::storage::DFT const &origDft, + std::vector> const &properties, + bool symred, bool allowModularisation, std::set const &relevantEvents, + bool allowDCForRelevantEvents, double approximationError, + storm::builder::ApproximationHeuristic approximationHeuristic, + bool eliminateChains, bool ignoreLabeling) { totalTimer.start(); dft_results results; @@ -30,21 +38,32 @@ namespace storm { // TODO: distinguish for all properties, not only for first one if (properties[0]->isTimeOperatorFormula() && allowModularisation) { // Use parallel composition as modularisation approach for expected time - std::shared_ptr> model = buildModelViaComposition(dft, properties, symred, true, relevantEvents); + std::shared_ptr> model = buildModelViaComposition(dft, + properties, + symred, true, + relevantEvents); // Model checking std::vector resultsValue = checkModel(model, properties); for (ValueType result : resultsValue) { results.push_back(result); } } else { - results = checkHelper(dft, properties, symred, allowModularisation, relevantEvents, allowDCForRelevantEvents, approximationError, approximationHeuristic); + results = checkHelper(dft, properties, symred, allowModularisation, relevantEvents, + allowDCForRelevantEvents, approximationError, approximationHeuristic, + eliminateChains, ignoreLabeling); } totalTimer.stop(); return results; } template - typename DFTModelChecker::dft_results DFTModelChecker::checkHelper(storm::storage::DFT const& dft, property_vector const& properties, bool symred, bool allowModularisation, std::set const& relevantEvents, bool allowDCForRelevantEvents, double approximationError, storm::builder::ApproximationHeuristic approximationHeuristic) { + typename DFTModelChecker::dft_results + DFTModelChecker::checkHelper(storm::storage::DFT const &dft, + property_vector const &properties, bool symred, + bool allowModularisation, std::set const &relevantEvents, + bool allowDCForRelevantEvents, double approximationError, + storm::builder::ApproximationHeuristic approximationHeuristic, + bool eliminateChains, bool ignoreLabeling) { STORM_LOG_TRACE("Check helper called"); std::vector> dfts; bool invResults = false; @@ -52,7 +71,7 @@ namespace storm { size_t nrM = 0; // K out of M // Try modularisation - if(allowModularisation) { + if (allowModularisation) { switch (dft.topLevelType()) { case storm::storage::DFTElementType::AND: STORM_LOG_TRACE("top modularisation called AND"); @@ -73,9 +92,10 @@ namespace storm { STORM_LOG_TRACE("top modularisation called VOT"); dfts = dft.topModularisation(); STORM_LOG_TRACE("Modularisation into " << dfts.size() << " submodules."); - nrK = std::static_pointer_cast const>(dft.getTopLevelGate())->threshold(); + nrK = std::static_pointer_cast const>( + dft.getTopLevelGate())->threshold(); nrM = dfts.size(); - if(nrK <= nrM/2) { + if (nrK <= nrM / 2) { nrK -= 1; invResults = true; } @@ -87,7 +107,7 @@ namespace storm { } // Perform modularisation - if(dfts.size() > 1) { + if (dfts.size() > 1) { STORM_LOG_TRACE("Recursive CHECK Call"); // TODO: compute simultaneously dft_results results; @@ -97,39 +117,42 @@ namespace storm { } else { // Recursively call model checking std::vector res; - for(auto const ft : dfts) { + for (auto const ft : dfts) { // TODO: allow approximation in modularisation - dft_results ftResults = checkHelper(ft, {property}, symred, true, relevantEvents, allowDCForRelevantEvents, 0.0); + dft_results ftResults = checkHelper(ft, {property}, symred, true, relevantEvents, + allowDCForRelevantEvents, 0.0); STORM_LOG_ASSERT(ftResults.size() == 1, "Wrong number of results"); res.push_back(boost::get(ftResults[0])); } // Combine modularisation results - STORM_LOG_TRACE("Combining all results... K=" << nrK << "; M=" << nrM << "; invResults=" << (invResults?"On":"Off")); + STORM_LOG_TRACE("Combining all results... K=" << nrK << "; M=" << nrM << "; invResults=" + << (invResults ? "On" : "Off")); ValueType result = storm::utility::zero(); - int limK = invResults ? -1 : nrM+1; + int limK = invResults ? -1 : nrM + 1; int chK = invResults ? -1 : 1; // WARNING: there is a bug for computing permutations with more than 32 elements - STORM_LOG_THROW(res.size() < 32, storm::exceptions::NotSupportedException, "Permutations work only for < 32 elements"); - for(int cK = nrK; cK != limK; cK += chK ) { + STORM_LOG_THROW(res.size() < 32, storm::exceptions::NotSupportedException, + "Permutations work only for < 32 elements"); + for (int cK = nrK; cK != limK; cK += chK) { STORM_LOG_ASSERT(cK >= 0, "ck negative."); size_t permutation = smallestIntWithNBitsSet(static_cast(cK)); do { - STORM_LOG_TRACE("Permutation="<() - result; } results.push_back(result); @@ -138,19 +161,25 @@ namespace storm { return results; } else { // No modularisation was possible - return checkDFT(dft, properties, symred, relevantEvents, allowDCForRelevantEvents, approximationError, approximationHeuristic); + return checkDFT(dft, properties, symred, relevantEvents, allowDCForRelevantEvents, approximationError, + approximationHeuristic, eliminateChains, ignoreLabeling); } } template - std::shared_ptr> DFTModelChecker::buildModelViaComposition(storm::storage::DFT const& dft, property_vector const& properties, bool symred, bool allowModularisation, std::set const& relevantEvents, bool allowDCForRelevantEvents) { + std::shared_ptr> + DFTModelChecker::buildModelViaComposition(storm::storage::DFT const &dft, + property_vector const &properties, bool symred, + bool allowModularisation, + std::set const &relevantEvents, + bool allowDCForRelevantEvents) { // TODO: use approximation? STORM_LOG_TRACE("Build model via composition"); std::vector> dfts; bool isAnd = true; // Try modularisation - if(allowModularisation) { + if (allowModularisation) { switch (dft.topLevelType()) { case storm::storage::DFTElementType::AND: STORM_LOG_TRACE("top modularisation called AND"); @@ -174,7 +203,7 @@ namespace storm { } // Perform modularisation via parallel composition - if(dfts.size() > 1) { + if (dfts.size() > 1) { STORM_LOG_TRACE("Recursive CHECK Call"); bool firstTime = true; std::shared_ptr> composedModel; @@ -185,7 +214,7 @@ namespace storm { // Find symmetries std::map>> emptySymmetry; storm::storage::DFTIndependentSymmetries symmetries(emptySymmetry); - if(symred) { + if (symred) { auto colouring = ft.colourDFT(); symmetries = ft.findSymmetries(colouring); STORM_LOG_DEBUG("Found " << symmetries.groups.size() << " symmetries."); @@ -194,29 +223,37 @@ namespace storm { // Build a single CTMC STORM_LOG_DEBUG("Building Model..."); - storm::builder::ExplicitDFTModelBuilder builder(ft, symmetries, relevantEvents, allowDCForRelevantEvents); + storm::builder::ExplicitDFTModelBuilder builder(ft, symmetries, relevantEvents, + allowDCForRelevantEvents); builder.buildModel(0, 0.0); std::shared_ptr> model = builder.getModel(); explorationTimer.stop(); - STORM_LOG_THROW(model->isOfType(storm::models::ModelType::Ctmc), storm::exceptions::NotSupportedException, "Parallel composition only applicable for CTMCs"); + STORM_LOG_THROW(model->isOfType(storm::models::ModelType::Ctmc), + storm::exceptions::NotSupportedException, + "Parallel composition only applicable for CTMCs"); std::shared_ptr> ctmc = model->template as>(); // Apply bisimulation to new CTMC bisimulationTimer.start(); - ctmc = storm::api::performDeterministicSparseBisimulationMinimization>(ctmc, properties, storm::storage::BisimulationType::Weak)->template as>(); + ctmc = storm::api::performDeterministicSparseBisimulationMinimization>( + ctmc, properties, + storm::storage::BisimulationType::Weak)->template as>(); bisimulationTimer.stop(); if (firstTime) { composedModel = ctmc; firstTime = false; } else { - composedModel = storm::builder::ParallelCompositionBuilder::compose(composedModel, ctmc, isAnd); + composedModel = storm::builder::ParallelCompositionBuilder::compose(composedModel, + ctmc, isAnd); } // Apply bisimulation to parallel composition bisimulationTimer.start(); - composedModel = storm::api::performDeterministicSparseBisimulationMinimization>(composedModel, properties, storm::storage::BisimulationType::Weak)->template as>(); + composedModel = storm::api::performDeterministicSparseBisimulationMinimization>( + composedModel, properties, + storm::storage::BisimulationType::Weak)->template as>(); bisimulationTimer.stop(); STORM_LOG_DEBUG("No. states (Composed): " << composedModel->getNumberOfStates()); @@ -236,7 +273,7 @@ namespace storm { // Find symmetries std::map>> emptySymmetry; storm::storage::DFTIndependentSymmetries symmetries(emptySymmetry); - if(symred) { + if (symred) { auto colouring = dft.colourDFT(); symmetries = dft.findSymmetries(colouring); STORM_LOG_DEBUG("Found " << symmetries.groups.size() << " symmetries."); @@ -245,24 +282,33 @@ namespace storm { // Build a single CTMC STORM_LOG_DEBUG("Building Model..."); - storm::builder::ExplicitDFTModelBuilder builder(dft, symmetries, relevantEvents, allowDCForRelevantEvents); + storm::builder::ExplicitDFTModelBuilder builder(dft, symmetries, relevantEvents, + allowDCForRelevantEvents); builder.buildModel(0, 0.0); std::shared_ptr> model = builder.getModel(); //model->printModelInformationToStream(std::cout); explorationTimer.stop(); - STORM_LOG_THROW(model->isOfType(storm::models::ModelType::Ctmc), storm::exceptions::NotSupportedException, "Parallel composition only applicable for CTMCs"); + STORM_LOG_THROW(model->isOfType(storm::models::ModelType::Ctmc), + storm::exceptions::NotSupportedException, + "Parallel composition only applicable for CTMCs"); return model->template as>(); } } template - typename DFTModelChecker::dft_results DFTModelChecker::checkDFT(storm::storage::DFT const& dft, property_vector const& properties, bool symred, std::set const& relevantEvents, bool allowDCForRelevantEvents, double approximationError, storm::builder::ApproximationHeuristic approximationHeuristic) { + typename DFTModelChecker::dft_results + DFTModelChecker::checkDFT(storm::storage::DFT const &dft, + property_vector const &properties, bool symred, + std::set const &relevantEvents, bool allowDCForRelevantEvents, + double approximationError, + storm::builder::ApproximationHeuristic approximationHeuristic, + bool eliminateChains, bool ignoreLabeling) { explorationTimer.start(); // Find symmetries std::map>> emptySymmetry; storm::storage::DFTIndependentSymmetries symmetries(emptySymmetry); - if(symred) { + if (symred) { auto colouring = dft.colourDFT(); symmetries = dft.findSymmetries(colouring); STORM_LOG_DEBUG("Found " << symmetries.groups.size() << " symmetries."); @@ -273,10 +319,12 @@ namespace storm { // Comparator for checking the error of the approximation storm::utility::ConstantsComparator comparator; // Build approximate Markov Automata for lower and upper bound - approximation_result approxResult = std::make_pair(storm::utility::zero(), storm::utility::zero()); + approximation_result approxResult = std::make_pair(storm::utility::zero(), + storm::utility::zero()); std::shared_ptr> model; std::vector newResult; - storm::builder::ExplicitDFTModelBuilder builder(dft, symmetries, relevantEvents, allowDCForRelevantEvents); + storm::builder::ExplicitDFTModelBuilder builder(dft, symmetries, relevantEvents, + allowDCForRelevantEvents); // TODO: compute approximation for all properties simultaneously? std::shared_ptr property = properties[0]; @@ -285,7 +333,9 @@ namespace storm { } bool probabilityFormula = property->isProbabilityOperatorFormula(); - STORM_LOG_ASSERT((property->isTimeOperatorFormula() && !probabilityFormula) || (!property->isTimeOperatorFormula() && probabilityFormula), "Probability formula not initialized correctly"); + STORM_LOG_ASSERT((property->isTimeOperatorFormula() && !probabilityFormula) || + (!property->isTimeOperatorFormula() && probabilityFormula), + "Probability formula not initialized correctly"); size_t iteration = 0; do { // Iteratively build finer models @@ -310,7 +360,9 @@ namespace storm { // Check lower bounds newResult = checkModel(model, {property}); STORM_LOG_ASSERT(newResult.size() == 1, "Wrong size for result vector."); - STORM_LOG_ASSERT(iteration == 0 || !comparator.isLess(newResult[0], approxResult.first), "New under-approximation " << newResult[0] << " is smaller than old result " << approxResult.first); + STORM_LOG_ASSERT(iteration == 0 || !comparator.isLess(newResult[0], approxResult.first), + "New under-approximation " << newResult[0] << " is smaller than old result " + << approxResult.first); approxResult.first = newResult[0]; // Build model for upper bound @@ -321,17 +373,27 @@ namespace storm { // Check upper bound newResult = checkModel(model, {property}); STORM_LOG_ASSERT(newResult.size() == 1, "Wrong size for result vector."); - STORM_LOG_ASSERT(iteration == 0 || !comparator.isLess(approxResult.second, newResult[0]), "New over-approximation " << newResult[0] << " is greater than old result " << approxResult.second); + STORM_LOG_ASSERT(iteration == 0 || !comparator.isLess(approxResult.second, newResult[0]), + "New over-approximation " << newResult[0] << " is greater than old result " + << approxResult.second); approxResult.second = newResult[0]; ++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_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 << ")"); 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_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." : ".")); dft_results results; @@ -341,9 +403,15 @@ namespace storm { // Build a single Markov Automaton auto ioSettings = storm::settings::getModule(); STORM_LOG_DEBUG("Building Model..."); - storm::builder::ExplicitDFTModelBuilder builder(dft, symmetries, relevantEvents, allowDCForRelevantEvents); + storm::builder::ExplicitDFTModelBuilder builder(dft, symmetries, relevantEvents, + allowDCForRelevantEvents); builder.buildModel(0, 0.0); std::shared_ptr> model = builder.getModel(); + if (eliminateChains && model->isOfType(storm::models::ModelType::MarkovAutomaton)) { + auto ma = std::static_pointer_cast>(model); + model = storm::transformer::NonMarkovianChainTransformer::eliminateNonmarkovianStates(ma, + !ignoreLabeling); + } explorationTimer.stop(); // Print model information @@ -376,12 +444,17 @@ namespace storm { } template - std::vector DFTModelChecker::checkModel(std::shared_ptr>& model, property_vector const& properties) { + std::vector + DFTModelChecker::checkModel(std::shared_ptr> &model, + property_vector const &properties) { // Bisimulation - if (model->isOfType(storm::models::ModelType::Ctmc) && storm::settings::getModule().isBisimulationSet()) { + if (model->isOfType(storm::models::ModelType::Ctmc) && + storm::settings::getModule().isBisimulationSet()) { bisimulationTimer.start(); STORM_LOG_DEBUG("Bisimulation..."); - model = storm::api::performDeterministicSparseBisimulationMinimization>(model->template as>(), properties, storm::storage::BisimulationType::Weak)->template as>(); + model = storm::api::performDeterministicSparseBisimulationMinimization>( + model->template as>(), properties, + storm::storage::BisimulationType::Weak)->template as>(); STORM_LOG_DEBUG("No. states (Bisimulation): " << model->getNumberOfStates()); STORM_LOG_DEBUG("No. transitions (Bisimulation): " << model->getNumberOfTransitions()); bisimulationTimer.stop(); @@ -398,7 +471,9 @@ namespace storm { singleModelCheckingTimer.reset(); singleModelCheckingTimer.start(); //STORM_PRINT_AND_LOG("Model checking property " << *property << " ..." << std::endl); - std::unique_ptr result(storm::api::verifyWithSparseEngine(model, storm::api::createTask(property, true))); + 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; @@ -413,13 +488,15 @@ namespace storm { } template - bool DFTModelChecker::isApproximationSufficient(ValueType , ValueType , double , bool ) { + bool DFTModelChecker::isApproximationSufficient(ValueType, ValueType, double, bool) { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Approximation works only for double."); } template<> - bool DFTModelChecker::isApproximationSufficient(double lowerBound, double upperBound, double approximationError, bool relative) { - STORM_LOG_THROW(!std::isnan(lowerBound) && !std::isnan(upperBound), storm::exceptions::NotSupportedException, "Approximation does not work if result is NaN."); + bool DFTModelChecker::isApproximationSufficient(double lowerBound, double upperBound, + double approximationError, bool relative) { + STORM_LOG_THROW(!std::isnan(lowerBound) && !std::isnan(upperBound), + storm::exceptions::NotSupportedException, "Approximation does not work if result is NaN."); if (relative) { return upperBound - lowerBound <= approximationError; } else { @@ -428,17 +505,17 @@ namespace storm { } template - void DFTModelChecker::printTimings(std::ostream& os) { + void DFTModelChecker::printTimings(std::ostream &os) { os << "Times:" << std::endl; os << "Exploration:\t" << explorationTimer << std::endl; os << "Building:\t" << buildingTimer << std::endl; - os << "Bisimulation:\t" << bisimulationTimer<< std::endl; + os << "Bisimulation:\t" << bisimulationTimer << std::endl; os << "Modelchecking:\t" << modelCheckingTimer << std::endl; os << "Total:\t\t" << totalTimer << std::endl; } template - void DFTModelChecker::printResults(dft_results const& results, std::ostream& os) { + void DFTModelChecker::printResults(dft_results const &results, std::ostream &os) { bool first = true; os << "Result: ["; for (auto result : results) { @@ -453,10 +530,14 @@ namespace storm { } - template class DFTModelChecker; + template + class DFTModelChecker; #ifdef STORM_HAVE_CARL - template class DFTModelChecker; + + template + class DFTModelChecker; + #endif } } diff --git a/src/storm-dft/modelchecker/dft/DFTModelChecker.h b/src/storm-dft/modelchecker/dft/DFTModelChecker.h index 4b4cd4d3d..9b898725a 100644 --- a/src/storm-dft/modelchecker/dft/DFTModelChecker.h +++ b/src/storm-dft/modelchecker/dft/DFTModelChecker.h @@ -55,11 +55,14 @@ namespace storm { * @param allowDCForRelevantEvents If true, Don't Care propagation is allowed even for relevant events. * @param approximationError Error allowed for approximation. Value 0 indicates no approximation. * @param approximationHeuristic Heuristic used for state space exploration. + * @param eliminateChains If true, chains of non-Markovian states are elimianted from the resulting MA + * @param ignoreLabeling If true, the labeling of states is ignored during state elimination * @return Model checking results for the given properties.. */ dft_results check(storm::storage::DFT const& origDft, property_vector const& properties, bool symred = true, bool allowModularisation = true, std::set const& relevantEvents = {}, bool allowDCForRelevantEvents = true, double approximationError = 0.0, - storm::builder::ApproximationHeuristic approximationHeuristic = storm::builder::ApproximationHeuristic::DEPTH); + storm::builder::ApproximationHeuristic approximationHeuristic = storm::builder::ApproximationHeuristic::DEPTH, + bool eliminateChains = false, bool ignoreLabeling = false); /*! * Print timings of all operations to stream. @@ -98,11 +101,14 @@ namespace storm { * @param allowDCForRelevantEvents If true, Don't Care propagation is allowed even for relevant events. * @param approximationError Error allowed for approximation. Value 0 indicates no approximation. * @param approximationHeuristic Heuristic used for approximation. + * @param eliminateChains If true, chains of non-Markovian states are elimianted from the resulting MA + * @param ignoreLabeling If true, the labeling of states is ignored during state elimination * @return Model checking results (or in case of approximation two results for lower and upper bound) */ dft_results checkHelper(storm::storage::DFT const& dft, property_vector const& properties, bool symred, bool allowModularisation, std::set const& relevantEvents, bool allowDCForRelevantEvents = true, double approximationError = 0.0, - storm::builder::ApproximationHeuristic approximationHeuristic = storm::builder::ApproximationHeuristic::DEPTH); + storm::builder::ApproximationHeuristic approximationHeuristic = storm::builder::ApproximationHeuristic::DEPTH, + bool eliminateChains = false, bool ignoreLabeling = false); /*! * Internal helper for building a CTMC from a DFT via parallel composition. @@ -129,12 +135,15 @@ namespace storm { * @param allowDCForRelevantEvents If true, Don't Care propagation is allowed even for relevant events. * @param approximationError Error allowed for approximation. Value 0 indicates no approximation. * @param approximationHeuristic Heuristic used for approximation. + * @param eliminateChains If true, chains of non-Markovian states are elimianted from the resulting MA + * @param ignoreLabeling If true, the labeling of states is ignored during state elimination * * @return Model checking result */ dft_results checkDFT(storm::storage::DFT const& dft, property_vector const& properties, bool symred, std::set const& relevantEvents = {}, bool allowDCForRelevantEvents = true, double approximationError = 0.0, - storm::builder::ApproximationHeuristic approximationHeuristic = storm::builder::ApproximationHeuristic::DEPTH); + storm::builder::ApproximationHeuristic approximationHeuristic = storm::builder::ApproximationHeuristic::DEPTH, + bool eliminateChains = false, bool ignoreLabeling = false); /*! * Check the given markov model for the given properties. diff --git a/src/storm-dft/settings/DftSettings.cpp b/src/storm-dft/settings/DftSettings.cpp index 43f0b0f51..4ff3e2aaf 100644 --- a/src/storm-dft/settings/DftSettings.cpp +++ b/src/storm-dft/settings/DftSettings.cpp @@ -23,6 +23,7 @@ #include "storm-conv/settings/modules/JaniExportSettings.h" #include "storm-gspn/settings/modules/GSPNSettings.h" #include "storm-gspn/settings/modules/GSPNExportSettings.h" +#include "storm/settings/modules/TransformationSettings.h" namespace storm { @@ -37,6 +38,7 @@ namespace storm { storm::settings::addModule(); storm::settings::addModule(); storm::settings::addModule(); + storm::settings::addModule(); storm::settings::addModule(); storm::settings::addModule();