From 102602dea251e76a5247c367401717030718752e Mon Sep 17 00:00:00 2001 From: sjunges Date: Fri, 19 Feb 2016 15:29:27 +0100 Subject: [PATCH] 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."); }