From c25889bc3ee94876c329eafb26fcdcb0e61179ed Mon Sep 17 00:00:00 2001 From: sjunges Date: Fri, 19 Feb 2016 13:57:38 +0100 Subject: [PATCH 1/2] minor Former-commit-id: 1a746c86f203a21c3b613850c556af7a28f56cf6 --- src/storage/dft/DFT.cpp | 10 ++++++++++ src/storage/dft/DFT.h | 1 + src/storage/dft/DFTElements.h | 2 ++ 3 files changed, 13 insertions(+) diff --git a/src/storage/dft/DFT.cpp b/src/storage/dft/DFT.cpp index d56166f60..a52cf8984 100644 --- a/src/storage/dft/DFT.cpp +++ b/src/storage/dft/DFT.cpp @@ -172,11 +172,21 @@ namespace storm { return ISD; } + template + std::vector DFT::immediateFailureCauses(size_t index) const { + if(isGate(index)) { + + } else { + return {index}; + } + } + template DFTColouring DFT::colourDFT() const { return DFTColouring(*this); } + template DFTIndependentSymmetries DFT::findSymmetries(DFTColouring const& colouring) const { std::vector vec; diff --git a/src/storage/dft/DFT.h b/src/storage/dft/DFT.h index 1583cc8d5..61f286619 100644 --- a/src/storage/dft/DFT.h +++ b/src/storage/dft/DFT.h @@ -232,6 +232,7 @@ namespace storm { DFTIndependentSymmetries findSymmetries(DFTColouring const& colouring) const; + std::vector immediateFailureCauses(size_t index) const; private: std::pair, std::vector> getSortedParentAndOutDepIds(size_t index) const; diff --git a/src/storage/dft/DFTElements.h b/src/storage/dft/DFTElements.h index c352bd38e..1a3c5b512 100644 --- a/src/storage/dft/DFTElements.h +++ b/src/storage/dft/DFTElements.h @@ -173,6 +173,8 @@ namespace storm { } virtual void extendSpareModule(std::set& elementsInModule) const; + + // virtual void extendImmediateFailureCausePathEvents(std::set& ) const; virtual size_t nrChildren() const = 0; From 102602dea251e76a5247c367401717030718752e Mon Sep 17 00:00:00 2001 From: sjunges Date: Fri, 19 Feb 2016 15:29:27 +0100 Subject: [PATCH 2/2] some refactoring Former-commit-id: 90be99f04d7736718e19986a2d02d9815813e889 --- src/builder/ExplicitDFTModelBuilder.cpp | 29 ++++++++++++++++++------- src/builder/ExplicitDFTModelBuilder.h | 10 ++++++++- src/storm-dyftee.cpp | 3 ++- src/utility/storm.h | 21 ++++++++++-------- 4 files changed, 44 insertions(+), 19 deletions(-) diff --git a/src/builder/ExplicitDFTModelBuilder.cpp b/src/builder/ExplicitDFTModelBuilder.cpp index a7284cb9c..08b6f4026 100644 --- a/src/builder/ExplicitDFTModelBuilder.cpp +++ b/src/builder/ExplicitDFTModelBuilder.cpp @@ -56,7 +56,7 @@ namespace storm { template - std::shared_ptr> ExplicitDFTModelBuilder::buildModel() { + std::shared_ptr> ExplicitDFTModelBuilder::buildModel(LabelOptions const& labelOpts) { // Initialize DFTStatePointer state = std::make_shared>(mDft, *mStateGenerationInfo, newIndex++); mStates.findOrAdd(state->status(), state); @@ -89,25 +89,32 @@ namespace storm { modelComponents.stateLabeling.addLabel("init"); modelComponents.stateLabeling.addLabelToState("init", 0); // Label all states corresponding to their status (failed, failsafe, failed BE) - modelComponents.stateLabeling.addLabel("failed"); - modelComponents.stateLabeling.addLabel("failsafe"); + if(labelOpts.buildFailLabel) { + modelComponents.stateLabeling.addLabel("failed"); + } + if(labelOpts.buildFailSafeLabel) { + modelComponents.stateLabeling.addLabel("failsafe"); + } + // Collect labels for all BE std::vector>> basicElements = mDft.getBasicElements(); for (std::shared_ptr> elem : basicElements) { - modelComponents.stateLabeling.addLabel(elem->name() + "_fail"); + if(labelOpts.beLabels.count(elem->name()) > 0) { + modelComponents.stateLabeling.addLabel(elem->name() + "_fail"); + } } for (auto const& stateVectorPair : mStates) { DFTStatePointer state = stateVectorPair.second; - if (mDft.hasFailed(state)) { + if (labelOpts.buildFailLabel && mDft.hasFailed(state)) { modelComponents.stateLabeling.addLabelToState("failed", state->getId()); } - if (mDft.isFailsafe(state)) { + if (labelOpts.buildFailSafeLabel && mDft.isFailsafe(state)) { modelComponents.stateLabeling.addLabelToState("failsafe", state->getId()); }; // Set fail status for each BE for (std::shared_ptr> elem : basicElements) { - if (state->hasFailed(elem->id())) { + if (labelOpts.beLabels.count(elem->name()) > 0 && state->hasFailed(elem->id()) ) { modelComponents.stateLabeling.addLabelToState(elem->name() + "_fail", state->getId()); } } @@ -129,7 +136,13 @@ namespace storm { } model = std::make_shared>(std::move(rateMatrix), std::move(modelComponents.stateLabeling)); } else { - model = std::make_shared>(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), std::move(modelComponents.markovianStates), std::move(modelComponents.exitRates), true); + std::shared_ptr> ma = std::make_shared>(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), std::move(modelComponents.markovianStates), std::move(modelComponents.exitRates), true); + if (ma->hasOnlyTrivialNondeterminism()) { + // Markov automaton can be converted into CTMC + model = ma->convertToCTMC(); + } else { + model = ma; + } } model->printModelInformationToStream(std::cout); diff --git a/src/builder/ExplicitDFTModelBuilder.h b/src/builder/ExplicitDFTModelBuilder.h index eacf2568c..40e0c2a8c 100644 --- a/src/builder/ExplicitDFTModelBuilder.h +++ b/src/builder/ExplicitDFTModelBuilder.h @@ -44,15 +44,23 @@ namespace storm { boost::optional>> choiceLabeling; }; + + storm::storage::DFT const& mDft; std::shared_ptr mStateGenerationInfo; storm::storage::BitVectorHashMap mStates; size_t newIndex = 0; public: + struct LabelOptions { + bool buildFailLabel = true; + bool buildFailSafeLabel = false; + std::set beLabels = {}; + }; + ExplicitDFTModelBuilder(storm::storage::DFT const& dft); - std::shared_ptr> buildModel(); + std::shared_ptr> buildModel(LabelOptions const& labelOpts); private: bool exploreStates(std::queue& stateQueue, storm::storage::SparseMatrixBuilder& transitionMatrixBuilder, std::vector& markovianStates, std::vector& exitRates); diff --git a/src/storm-dyftee.cpp b/src/storm-dyftee.cpp index 7b7cea029..805ef7570 100644 --- a/src/storm-dyftee.cpp +++ b/src/storm-dyftee.cpp @@ -32,7 +32,8 @@ void analyzeDFT(std::string filename, std::string property, bool symred = false) // Building Markov Automaton std::cout << "Building Model..." << std::endl; storm::builder::ExplicitDFTModelBuilder builder(dft); - std::shared_ptr> model = builder.buildModel(); + typename storm::builder::ExplicitDFTModelBuilder::LabelOptions labeloptions; // TODO initialize this with the formula + std::shared_ptr> model = builder.buildModel(labeloptions); std::cout << "Built Model" << std::endl; // Model checking diff --git a/src/utility/storm.h b/src/utility/storm.h index f737b318e..5d02405fa 100644 --- a/src/utility/storm.h +++ b/src/utility/storm.h @@ -196,6 +196,15 @@ namespace storm { template std::shared_ptr preprocessModel(std::shared_ptr model, std::vector> const& formulas) { + if(model->getType() == storm::models::ModelType::MarkovAutomaton && model->isSparseModel()) { + std::shared_ptr> ma = model->template as>(); + if (ma->hasOnlyTrivialNondeterminism()) { + // Markov automaton can be converted into CTMC + model = ma->convertToCTMC(); + + } + } + if (model->isSparseModel() && storm::settings::generalSettings().isBisimulationSet()) { storm::storage::BisimulationType bisimType = storm::storage::BisimulationType::Strong; if (storm::settings::bisimulationSettings().isWeakBisimulationSet()) { @@ -205,6 +214,7 @@ namespace storm { STORM_LOG_THROW(model->isSparseModel(), storm::exceptions::InvalidSettingsException, "Bisimulation minimization is currently only available for sparse models."); return performBisimulationMinimization(model->template as>(), formulas, bisimType); } + return model; } @@ -302,15 +312,8 @@ namespace storm { result = modelchecker.check(task); } else if (model->getType() == storm::models::ModelType::MarkovAutomaton) { std::shared_ptr> ma = model->template as>(); - if (ma->hasOnlyTrivialNondeterminism()) { - // Markov automaton can be converted into CTMC - std::shared_ptr> ctmc = ma->convertToCTMC(); - storm::modelchecker::SparseCtmcCslModelChecker> modelchecker(*ctmc); - result = modelchecker.check(task); - } else { - storm::modelchecker::SparseMarkovAutomatonCslModelChecker> modelchecker(*ma); - result = modelchecker.check(task); - } + storm::modelchecker::SparseMarkovAutomatonCslModelChecker> modelchecker(*ma); + result = modelchecker.check(task); } else { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "The model type " << model->getType() << " is not supported."); }