From e5fd60449830058b3fc95f2097bc03ac29548c7b Mon Sep 17 00:00:00 2001 From: Mavo Date: Mon, 14 Mar 2016 16:42:53 +0100 Subject: [PATCH] Flag for disabling DC propagation Former-commit-id: 1fa850ef266cc00bb51068934823a1ca95ff79da --- src/builder/ExplicitDFTModelBuilder.cpp | 4 ++-- src/builder/ExplicitDFTModelBuilder.h | 3 ++- src/modelchecker/DFTAnalyser.h | 12 ++++++------ src/storm-dyftee.cpp | 11 +++++++---- 4 files changed, 17 insertions(+), 13 deletions(-) diff --git a/src/builder/ExplicitDFTModelBuilder.cpp b/src/builder/ExplicitDFTModelBuilder.cpp index d57dec2e7..f5296a487 100644 --- a/src/builder/ExplicitDFTModelBuilder.cpp +++ b/src/builder/ExplicitDFTModelBuilder.cpp @@ -15,7 +15,7 @@ namespace storm { } template - ExplicitDFTModelBuilder::ExplicitDFTModelBuilder(storm::storage::DFT const& dft, storm::storage::DFTIndependentSymmetries const& symmetries) : mDft(dft), mStates(((mDft.stateVectorSize() / 64) + 1) * 64, INITIAL_BUCKETSIZE) { + ExplicitDFTModelBuilder::ExplicitDFTModelBuilder(storm::storage::DFT const& dft, storm::storage::DFTIndependentSymmetries const& symmetries, bool enableDC) : mDft(dft), mStates(((mDft.stateVectorSize() / 64) + 1) * 64, INITIAL_BUCKETSIZE), enableDC(enableDC) { // stateVectorSize is bound for size of bitvector mStateGenerationInfo = std::make_shared(mDft.buildStateGenerationInfo(symmetries)); @@ -218,7 +218,7 @@ namespace storm { next->checkFailsafe(*newState, queues); } - while (!queues.dontCarePropagationDone()) { + while (enableDC && !queues.dontCarePropagationDone()) { DFTElementPointer next = queues.nextDontCarePropagation(); next->checkDontCareAnymore(*newState, queues); } diff --git a/src/builder/ExplicitDFTModelBuilder.h b/src/builder/ExplicitDFTModelBuilder.h index 7fc343be2..4f1dff514 100644 --- a/src/builder/ExplicitDFTModelBuilder.h +++ b/src/builder/ExplicitDFTModelBuilder.h @@ -55,6 +55,7 @@ namespace storm { std::vector> mPseudoStatesMapping; // vector of (id to concrete state, bitvector) size_t newIndex = 0; bool mergeFailedStates = true; + bool enableDC = true; size_t failedIndex = 0; size_t initialStateIndex = 0; @@ -65,7 +66,7 @@ namespace storm { std::set beLabels = {}; }; - ExplicitDFTModelBuilder(storm::storage::DFT const& dft, storm::storage::DFTIndependentSymmetries const& symmetries); + ExplicitDFTModelBuilder(storm::storage::DFT const& dft, storm::storage::DFTIndependentSymmetries const& symmetries, bool enableDC); std::shared_ptr> buildModel(LabelOptions const& labelOpts); diff --git a/src/modelchecker/DFTAnalyser.h b/src/modelchecker/DFTAnalyser.h index 93bc7c7b1..0bf9d491e 100644 --- a/src/modelchecker/DFTAnalyser.h +++ b/src/modelchecker/DFTAnalyser.h @@ -20,7 +20,7 @@ class DFTAnalyser { std::chrono::duration totalTime = std::chrono::duration::zero(); ValueType checkResult = storm::utility::zero(); public: - void check(storm::storage::DFT dft , std::shared_ptr const& formula, bool symred = true, bool allowModularisation = true) { + void check(storm::storage::DFT dft , std::shared_ptr const& formula, bool symred = true, bool allowModularisation = true, bool enableDC = true) { // Building DFT std::chrono::high_resolution_clock::time_point totalStart = std::chrono::high_resolution_clock::now(); @@ -29,7 +29,7 @@ public: // Optimizing DFT dft = dft.optimize(); std::vector> dfts; - checkResult = checkHelper(dft, formula, symred, allowModularisation); + checkResult = checkHelper(dft, formula, symred, allowModularisation, enableDC); totalTime = std::chrono::high_resolution_clock::now() - totalStart; @@ -37,7 +37,7 @@ public: } private: - ValueType checkHelper(storm::storage::DFT const& dft , std::shared_ptr const& formula, bool symred = true, bool allowModularisation = true) { + ValueType checkHelper(storm::storage::DFT const& dft , std::shared_ptr const& formula, bool symred = true, bool allowModularisation = true, bool enableDC = true) { std::cout << "check helper called" << std::endl; bool invResults = false; std::vector> dfts = {dft}; @@ -67,7 +67,7 @@ private: } if(res.empty()) { // Model based modularisation. - auto const& models = buildMarkovModels(dfts, formula, symred); + auto const& models = buildMarkovModels(dfts, formula, symred, enableDC); for (auto const& model : models) { @@ -98,7 +98,7 @@ private: } - std::vector>> buildMarkovModels(std::vector> const& dfts, std::shared_ptr const& formula, bool symred) { + std::vector>> buildMarkovModels(std::vector> const& dfts, std::shared_ptr const& formula, bool symred, bool enableDC) { std::vector>> models; for(auto& dft : dfts) { std::chrono::high_resolution_clock::time_point buildingStart = std::chrono::high_resolution_clock::now(); @@ -116,7 +116,7 @@ private: // Building Markov Automaton std::cout << "Building Model..." << std::endl; - storm::builder::ExplicitDFTModelBuilder builder(dft, symmetries); + storm::builder::ExplicitDFTModelBuilder builder(dft, symmetries, enableDC); typename storm::builder::ExplicitDFTModelBuilder::LabelOptions labeloptions; // TODO initialize this with the formula std::shared_ptr> model = builder.buildModel(labeloptions); //model->printModelInformationToStream(std::cout); diff --git a/src/storm-dyftee.cpp b/src/storm-dyftee.cpp index f280bbebf..ea0da3a14 100644 --- a/src/storm-dyftee.cpp +++ b/src/storm-dyftee.cpp @@ -11,7 +11,7 @@ * @param property PCTC formula capturing the property to check. */ template -void analyzeDFT(std::string filename, std::string property, bool symred = false, bool allowModularisation = false) { +void analyzeDFT(std::string filename, std::string property, bool symred = false, bool allowModularisation = false, bool enableDC = true) { storm::settings::SettingsManager& manager = storm::settings::mutableManager(); manager.setFromString(""); @@ -22,7 +22,7 @@ void analyzeDFT(std::string filename, std::string property, bool symred = false, assert(formulas.size() == 1); DFTAnalyser analyser; - analyser.check(dft, formulas[0], symred, allowModularisation); + analyser.check(dft, formulas[0], symred, allowModularisation, enableDC); analyser.printTimings(); analyser.printResult(); } @@ -47,6 +47,7 @@ int main(int argc, char** argv) { bool minimal = true; bool allowModular = true; bool enableModularisation = false; + bool disableDC = false; std::string filename = argv[1]; std::string operatorType = ""; std::string targetFormula = ""; @@ -92,6 +93,8 @@ int main(int argc, char** argv) { symred = true; } else if (option == "--modularisation") { enableModularisation = true; + } else if (option == "--disabledc") { + disableDC = true; } else if (option == "--min") { minimal = true; } else if (option == "--max") { @@ -114,8 +117,8 @@ int main(int argc, char** argv) { std::cout << "Running " << (parametric ? "parametric " : "") << "DFT analysis on file " << filename << " with property " << pctlFormula << std::endl; if (parametric) { - analyzeDFT(filename, pctlFormula, symred, allowModular && enableModularisation ); + analyzeDFT(filename, pctlFormula, symred, allowModular && enableModularisation, !disableDC ); } else { - analyzeDFT(filename, pctlFormula, symred, allowModular && enableModularisation); + analyzeDFT(filename, pctlFormula, symred, allowModular && enableModularisation, !disableDC); } }