From d507eab7f38003d652c17e18ec5eccd86a87645a Mon Sep 17 00:00:00 2001 From: Mavo Date: Tue, 9 Feb 2016 09:42:57 +0100 Subject: [PATCH] Build Markov Automaton instead of CTMC Former-commit-id: 26c299ad345d562542841ae288c80cdc693e238c --- src/builder/ExplicitDFTModelBuilder.cpp | 41 +++++++++++++++---------- src/builder/ExplicitDFTModelBuilder.h | 13 +++++--- src/storage/dft/DFTBuilder.h | 9 ++---- src/storm-dyftee.cpp | 18 +++++------ 4 files changed, 45 insertions(+), 36 deletions(-) diff --git a/src/builder/ExplicitDFTModelBuilder.cpp b/src/builder/ExplicitDFTModelBuilder.cpp index 8fab93b8b..d4de53d64 100644 --- a/src/builder/ExplicitDFTModelBuilder.cpp +++ b/src/builder/ExplicitDFTModelBuilder.cpp @@ -1,5 +1,5 @@ #include "src/builder/ExplicitDFTModelBuilder.h" -#include +#include #include #include #include @@ -7,13 +7,13 @@ namespace storm { namespace builder { - template - ExplicitDFTModelBuilder::ModelComponents::ModelComponents() : transitionMatrix(), stateLabeling(), rewardModels(), choiceLabeling() { + template + ExplicitDFTModelBuilder::ModelComponents::ModelComponents() : transitionMatrix(), stateLabeling(), markovianStates(), exitRates(), choiceLabeling() { // Intentionally left empty. } - template - std::shared_ptr> ExplicitDFTModelBuilder::buildCTMC() { + template + std::shared_ptr> ExplicitDFTModelBuilder::buildMA() { // Initialize DFTStatePointer state = std::make_shared>(mDft, newIndex++); mStates.findOrAdd(state->status(), state); @@ -21,15 +21,17 @@ namespace storm { std::queue stateQueue; stateQueue.push(state); - bool deterministicModel = true; + bool deterministicModel = false; + ModelComponents modelComponents; + std::vector tmpMarkovianStates; storm::storage::SparseMatrixBuilder transitionMatrixBuilder(0, 0, 0, false, !deterministicModel, 0); // Begin model generation - exploreStates(stateQueue, transitionMatrixBuilder); + exploreStates(stateQueue, transitionMatrixBuilder, tmpMarkovianStates, modelComponents.exitRates); STORM_LOG_DEBUG("Generated " << mStates.size() << " states"); - // Build CTMC - ModelComponents modelComponents; + // Build Markov Automaton + modelComponents.markovianStates = storm::storage::BitVector(mStates.size(), tmpMarkovianStates); // Build transition matrix modelComponents.transitionMatrix = transitionMatrixBuilder.build(); STORM_LOG_DEBUG("TransitionMatrix: " << std::endl << modelComponents.transitionMatrix); @@ -65,15 +67,17 @@ namespace storm { } } - std::shared_ptr> model; - model = std::shared_ptr>(new storm::models::sparse::Ctmc(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling))); + std::shared_ptr> model = std::make_shared>(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), std::move(modelComponents.markovianStates), std::move(modelComponents.exitRates)); model->printModelInformationToStream(std::cout); return model; } - template - void ExplicitDFTModelBuilder::exploreStates(std::queue& stateQueue, storm::storage::SparseMatrixBuilder& transitionMatrixBuilder) { + template + void ExplicitDFTModelBuilder::exploreStates(std::queue& stateQueue, storm::storage::SparseMatrixBuilder& transitionMatrixBuilder, std::vector& markovianStates, std::vector& exitRates) { + assert(exitRates.empty()); + assert(markovianStates.empty()); + // TODO Matthias: set Markovian states std::map outgoingTransitions; while (!stateQueue.empty()) { @@ -90,6 +94,8 @@ namespace storm { if (mDft.hasFailed(state) || mDft.isFailsafe(state)) { transitionMatrixBuilder.addNextValue(state->getId(), state->getId(), storm::utility::one()); STORM_LOG_TRACE("Added self loop for " << state->getId()); + exitRates.push_back(storm::utility::one()); + assert(exitRates.size()-1 == state->getId()); // No further exploration required continue; } else { @@ -169,20 +175,23 @@ namespace storm { } // end while failing BE // Add all transitions + ValueType exitRate = storm::utility::zero(); for (auto it = outgoingTransitions.begin(); it != outgoingTransitions.end(); ++it) { transitionMatrixBuilder.addNextValue(state->getId(), it->first, it->second); + exitRate += it->second; } + exitRates.push_back(exitRate); + assert(exitRates.size()-1 == state->getId()); } // end while queue } // Explicitly instantiate the class. - template class ExplicitDFTModelBuilder, uint32_t>; + template class ExplicitDFTModelBuilder; #ifdef STORM_HAVE_CARL - template class ExplicitDFTModelBuilder, uint32_t>; - template class ExplicitDFTModelBuilder, uint32_t>; + template class ExplicitDFTModelBuilder; #endif } // namespace builder diff --git a/src/builder/ExplicitDFTModelBuilder.h b/src/builder/ExplicitDFTModelBuilder.h index ed02e60d4..edb2e1a94 100644 --- a/src/builder/ExplicitDFTModelBuilder.h +++ b/src/builder/ExplicitDFTModelBuilder.h @@ -16,7 +16,7 @@ namespace storm { namespace builder { - template, typename IndexType = uint32_t> + template class ExplicitDFTModelBuilder { using DFTElementPointer = std::shared_ptr>; @@ -33,8 +33,11 @@ namespace storm { // The state labeling. storm::models::sparse::StateLabeling stateLabeling; - // The reward models associated with the model. - std::unordered_map> rewardModels; + // The Markovian states. + storm::storage::BitVector markovianStates; + + // The exit rates. + std::vector exitRates; // A vector that stores a labeling for each choice. boost::optional>> choiceLabeling; @@ -50,10 +53,10 @@ namespace storm { // 2^nrBE is upper bound for state space } - std::shared_ptr> buildCTMC(); + std::shared_ptr> buildMA(); private: - void exploreStates(std::queue& stateQueue, storm::storage::SparseMatrixBuilder& transitionMatrixBuilder); + void exploreStates(std::queue& stateQueue, storm::storage::SparseMatrixBuilder& transitionMatrixBuilder, std::vector& markovianStates, std::vector& exitRates); }; } diff --git a/src/storage/dft/DFTBuilder.h b/src/storage/dft/DFTBuilder.h index 8fc65b0b5..9297d90cf 100644 --- a/src/storage/dft/DFTBuilder.h +++ b/src/storage/dft/DFTBuilder.h @@ -69,15 +69,12 @@ namespace storm { } for (size_t i = 1; i < children.size(); ++i) { - // TODO Matthias: better code - std::stringstream stream; - stream << name << "_" << i; - std::string s = stream.str(); - if(mElements.count(s) != 0) { + std::string nameFdep = name + "_" + std::to_string(i); + if(mElements.count(nameFdep) != 0) { // Element with that name already exists. return false; } - DFTDependencyPointer element = std::make_shared>(mNextId++, s, trigger, children[i], storm::utility::one()); + DFTDependencyPointer element = std::make_shared>(mNextId++, nameFdep, trigger, children[i], storm::utility::one()); mElements[element->name()] = element; mDependencies.push_back(element); } diff --git a/src/storm-dyftee.cpp b/src/storm-dyftee.cpp index 4986469e7..a86347e3b 100644 --- a/src/storm-dyftee.cpp +++ b/src/storm-dyftee.cpp @@ -6,7 +6,7 @@ #include "utility/storm.h" /*! - * Load DFT from filename, build corresponding CTMC and check against given property. + * Load DFT from filename, build corresponding Markov Automaton and check against given property. * * @param filename Path to DFT file in Galileo format. * @param property PCTC formula capturing the property to check. @@ -19,21 +19,21 @@ void analyzeDFT(std::string filename, std::string property) { storm::storage::DFT dft = parser.parseDFT(filename); std::cout << "Built data structure" << std::endl; - // Building CTMC - std::cout << "Building CTMC..." << std::endl; + // Building Markov Automaton + std::cout << "Building Markov Automaton..." << std::endl; storm::builder::ExplicitDFTModelBuilder builder(dft); - std::shared_ptr> model = builder.buildCTMC(); - std::cout << "Built CTMC" << std::endl; + std::shared_ptr> model = builder.buildMA(); + std::cout << "Built Markov Automaton" << std::endl; // Model checking std::cout << "Model checking..." << std::endl; std::vector> formulas = storm::parseFormulasForExplicit(property); assert(formulas.size() == 1); - std::unique_ptr resultCtmc(storm::verifySparseModel(model, formulas[0])); - assert(resultCtmc); + std::unique_ptr resultMA(storm::verifySparseModel(model, formulas[0])); + assert(resultMA); std::cout << "Result: "; - resultCtmc->filter(storm::modelchecker::ExplicitQualitativeCheckResult(model->getInitialStates())); - std::cout << *resultCtmc << std::endl; + resultMA->filter(storm::modelchecker::ExplicitQualitativeCheckResult(model->getInitialStates())); + std::cout << *resultMA << std::endl; } /*!