diff --git a/src/storm/modelchecker/helper/ltl/SparseLTLHelper.cpp b/src/storm/modelchecker/helper/ltl/SparseLTLHelper.cpp index 7dd5e1367..8182289ce 100644 --- a/src/storm/modelchecker/helper/ltl/SparseLTLHelper.cpp +++ b/src/storm/modelchecker/helper/ltl/SparseLTLHelper.cpp @@ -3,9 +3,6 @@ #include "storm/transformer/DAProductBuilder.h" #include "storm/automata/LTL2DeterministicAutomaton.h" -#include "storm/models/sparse/Dtmc.h" -#include "storm/models/sparse/Mdp.h" - #include "storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h" #include "storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.h" @@ -19,13 +16,13 @@ namespace storm { namespace modelchecker { namespace helper { - template - SparseLTLHelper::SparseLTLHelper(Model const& model, storm::storage::SparseMatrix const& transitionMatrix) : _model(model), _transitionMatrix(transitionMatrix) { + template + SparseLTLHelper::SparseLTLHelper(storm::storage::SparseMatrix const& transitionMatrix, std::size_t numberOfStates) : _transitionMatrix(transitionMatrix), _numberOfStates(numberOfStates) { // Intentionally left empty. } - template - std::vector SparseLTLHelper::computeDAProductProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, storm::automata::DeterministicAutomaton const& da, std::map& apSatSets, bool qualitative) { + template + std::vector SparseLTLHelper::computeDAProductProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, storm::automata::DeterministicAutomaton const& da, std::map& apSatSets, bool qualitative) { STORM_LOG_THROW((!Nondeterministic) || goal.hasDirection() && goal.direction() == OptimizationDirection::Maximize, storm::exceptions::InvalidPropertyException, "Can only compute maximizing probabilties for DA product with MDP"); @@ -44,14 +41,14 @@ namespace storm { statesOfInterest = goal.relevantValues(); } else { // product from all model states - statesOfInterest = storm::storage::BitVector(this->_model.getNumberOfStates(), true); + statesOfInterest = storm::storage::BitVector(this->_numberOfStates, true); } STORM_LOG_INFO("Building "+ (Nondeterministic ? std::string("MDP-DA") : std::string("DTMC-DA")) +"product with deterministic automaton, starting from " << statesOfInterest.getNumberOfSetBits() << " model states..."); storm::transformer::DAProductBuilder productBuilder(da, apLabels); - auto product = productBuilder.build(this->_model, statesOfInterest); + auto product = productBuilder.build(this->_transitionMatrix, statesOfInterest); STORM_LOG_INFO("Product "+ (Nondeterministic ? std::string("MDP-DA") : std::string("DTMC")) +" has " << product->getProductModel().getNumberOfStates() << " states and " << product->getProductModel().getNumberOfTransitions() << " transitions."); @@ -59,7 +56,7 @@ namespace storm { if (storm::settings::getModule().isTraceSet()) { STORM_LOG_TRACE("Writing model to model.dot"); std::ofstream modelDot("model.dot"); - this->_model.writeDotToStream(modelDot); + // this->_model.writeDotToStream(modelDot); // TODO modelDot.close(); STORM_LOG_TRACE("Writing product model to product.dot"); @@ -82,7 +79,7 @@ namespace storm { accepting = storm::modelchecker::helper::SparseMdpPrctlHelper::computeSurelyAcceptingPmaxStates(*product->getAcceptance(), product->getProductModel().getTransitionMatrix(), product->getProductModel().getBackwardTransitions()); if (accepting.empty()) { STORM_LOG_INFO("No accepting states, skipping probability computation."); - std::vector numericResult(this->_model.getNumberOfStates(), storm::utility::zero()); + std::vector numericResult(this->_numberOfStates, storm::utility::zero()); return numericResult; } @@ -108,12 +105,12 @@ namespace storm { if (acceptingBSCCs == 0) { STORM_LOG_INFO("No accepting BSCCs, skipping probability computation."); - std::vector numericResult(this->_model.getNumberOfStates(), storm::utility::zero()); + std::vector numericResult(this->_numberOfStates, storm::utility::zero()); return numericResult; } } - STORM_LOG_INFO("Computing probabilities for reaching accepting BSCCs..."); + STORM_LOG_INFO("Computing probabilities for reaching accepting components..."); storm::storage::BitVector bvTrue(product->getProductModel().getNumberOfStates(), true); @@ -124,8 +121,7 @@ namespace storm { std::vector prodNumericResult; if (Nondeterministic) { - prodNumericResult - = std::move(storm::modelchecker::helper::SparseMdpPrctlHelper::computeUntilProbabilities(env, + prodNumericResult = std::move(storm::modelchecker::helper::SparseMdpPrctlHelper::computeUntilProbabilities(env, std::move(solveGoalProduct), product->getProductModel().getTransitionMatrix(), product->getProductModel().getBackwardTransitions(), @@ -145,13 +141,13 @@ namespace storm { qualitative); } - std::vector numericResult = product->projectToOriginalModel(this->_model, prodNumericResult); + std::vector numericResult = product->projectToOriginalModel(this->_numberOfStates, prodNumericResult); return numericResult; } - template - std::vector SparseLTLHelper::computeLTLProbabilities(Environment const &env, storm::solver::SolveGoal&& goal, storm::logic::Formula const& ltlFormula, std::map& apSatSets) { + template + std::vector SparseLTLHelper::computeLTLProbabilities(Environment const &env, storm::solver::SolveGoal&& goal, storm::logic::Formula const& ltlFormula, std::map& apSatSets) { STORM_LOG_INFO("Resulting LTL path formula: " << ltlFormula); STORM_LOG_INFO(" in prefix format: " << ltlFormula.toPrefixString()); @@ -165,6 +161,7 @@ namespace storm { std::vector numericResult = computeDAProductProbabilities(env, std::move(goal), *da, apSatSets, this->isQualitativeSet()); + // TODO /* if(Nondeterministic && this->getOptimizationDirection()==OptimizationDirection::Minimize) { // compute 1-Pmax[!ltl] @@ -177,13 +174,13 @@ namespace storm { return numericResult; } - template class SparseLTLHelper, false>; - template class SparseLTLHelper, true>; + template class SparseLTLHelper; + template class SparseLTLHelper; #ifdef STORM_HAVE_CARL - template class SparseLTLHelper, false>; - template class SparseLTLHelper, true>; - template class SparseLTLHelper, false>; + template class SparseLTLHelper; + template class SparseLTLHelper; + template class SparseLTLHelper; #endif diff --git a/src/storm/modelchecker/helper/ltl/SparseLTLHelper.h b/src/storm/modelchecker/helper/ltl/SparseLTLHelper.h index 6240fe1b0..42bf322cc 100644 --- a/src/storm/modelchecker/helper/ltl/SparseLTLHelper.h +++ b/src/storm/modelchecker/helper/ltl/SparseLTLHelper.h @@ -1,15 +1,13 @@ #include "storm/modelchecker/helper/SingleValueModelCheckerHelper.h" +#include "storm/automata/DeterministicAutomaton.h" #include "storm/storage/SparseMatrix.h" #include "storm/solver/SolveGoal.h" +#include "storm/models/sparse/Dtmc.h" +#include "storm/models/sparse/Mdp.h" namespace storm { - namespace automata { - // fwd - class DeterministicAutomaton; - } - namespace modelchecker { namespace helper { @@ -18,14 +16,21 @@ namespace storm { * @tparam ValueType the type a value can have * @tparam Nondeterministic true if there is nondeterminism in the Model (MDP) */ - template // todo remove Model + template class SparseLTLHelper: public SingleValueModelCheckerHelper { public: + + /*! + * The type of the product automaton model // todo + */ + using productModelType = typename std::conditional, storm::models::sparse::Dtmc>::type; + + /*! * Initializes the helper for a discrete time (i.e. DTMC, MDP) */ - SparseLTLHelper(Model const& model, storm::storage::SparseMatrix const& transitionMatrix); + SparseLTLHelper(storm::storage::SparseMatrix const& transitionMatrix, std::size_t numberOfSates); /*! @@ -44,7 +49,7 @@ namespace storm { private: storm::storage::SparseMatrix const& _transitionMatrix; - Model const& _model; // todo remove ? + std::size_t _numberOfStates; }; } diff --git a/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp index 64c2eaa05..66b726bce 100644 --- a/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp +++ b/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp @@ -162,7 +162,7 @@ namespace storm { STORM_LOG_INFO("Extracting maximal state formulas and computing satisfaction sets for path formula: " << pathFormula); std::map apSets; - // todo instead: std::map apSets = storm::modelchecker::helper::computeApSets(env, checkTask); + // todo apSets = computeApSets(env, checkTask); for (auto& p : extracted) { STORM_LOG_INFO(" Computing satisfaction set for atomic proposition \"" << p.first << "\" <=> " << *p.second << "..."); @@ -177,7 +177,7 @@ namespace storm { const SparseDtmcModelType& dtmc = this->getModel(); - storm::modelchecker::helper::SparseLTLHelper helper(dtmc, dtmc.getTransitionMatrix()); + storm::modelchecker::helper::SparseLTLHelper helper(dtmc.getTransitionMatrix(), this->getModel().getNumberOfStates()); storm::modelchecker::helper::setInformationFromCheckTaskDeterministic(helper, checkTask, dtmc); std::vector numericResult = helper.computeLTLProbabilities(env, storm::solver::SolveGoal(this->getModel(), checkTask), *ltlFormula, apSets); diff --git a/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp index dbf044910..6f0bc270a 100644 --- a/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp +++ b/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp @@ -219,7 +219,7 @@ namespace storm { const SparseMdpModelType& mdp = this->getModel(); storm::solver::SolveGoal goal(mdp, subTask); - storm::modelchecker::helper::SparseLTLHelper helper(mdp, mdp.getTransitionMatrix()); + storm::modelchecker::helper::SparseLTLHelper helper(mdp.getTransitionMatrix(), this->getModel().getNumberOfStates()); storm::modelchecker::helper::setInformationFromCheckTaskNondeterministic(helper, subTask, mdp); std::vector numericResult = helper.computeLTLProbabilities(env, storm::solver::SolveGoal(this->getModel(), subTask), *ltlFormula, apSets); @@ -233,88 +233,6 @@ namespace storm { return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } - - /* - template - std::vector::ValueType> SparseMdpPrctlModelChecker::computeDAProductProbabilities(Environment const& env, storm::solver::SolveGoal::ValueType>&& goal, storm::automata::DeterministicAutomaton const& da, std::map& apSatSets, bool qualitative) const { - STORM_LOG_THROW(goal.hasDirection() && goal.direction() == OptimizationDirection::Maximize, storm::exceptions::InvalidPropertyException, "Can only compute maximizing probabilties for DA product with MDP"); - - const storm::automata::APSet& apSet = da.getAPSet(); - - std::vector apLabels; - for (const std::string& ap : apSet.getAPs()) { - auto it = apSatSets.find(ap); - STORM_LOG_THROW(it != apSatSets.end(), storm::exceptions::InvalidOperationException, "Deterministic automaton has AP " << ap << ", does not appear in formula"); - - apLabels.push_back(std::move(it->second)); - } - - const SparseMdpModelType& mdp = this->getModel(); - - storm::storage::BitVector statesOfInterest; - if (goal.hasRelevantValues()) { - statesOfInterest = goal.relevantValues(); - } else { - // product from all model states - statesOfInterest = storm::storage::BitVector(mdp.getNumberOfStates(), true); - } - - STORM_LOG_INFO("Building MDP-DA product with deterministic automaton, starting from " << statesOfInterest.getNumberOfSetBits() << " model states..."); - storm::transformer::DAProductBuilder productBuilder(da, apLabels); - auto product = productBuilder.build(mdp, statesOfInterest); - STORM_LOG_INFO("Product MDP has " << product->getProductModel().getNumberOfStates() << " states and " - << product->getProductModel().getNumberOfTransitions() << " transitions."); - - if (storm::settings::getModule().isTraceSet()) { - STORM_LOG_TRACE("Writing model to model.dot"); - std::ofstream modelDot("model.dot"); - mdp.writeDotToStream(modelDot); - modelDot.close(); - - STORM_LOG_TRACE("Writing product model to product.dot"); - std::ofstream productDot("product.dot"); - product->getProductModel().writeDotToStream(productDot); - productDot.close(); - - STORM_LOG_TRACE("Product model mapping:"); - std::stringstream str; - product->printMapping(str); - STORM_LOG_TRACE(str.str()); - } - - STORM_LOG_INFO("Computing accepting end components..."); - storm::storage::BitVector accepting = storm::modelchecker::helper::SparseMdpPrctlHelper::computeSurelyAcceptingPmaxStates(*product->getAcceptance(), product->getProductModel().getTransitionMatrix(), product->getProductModel().getBackwardTransitions()); - if (accepting.empty()) { - STORM_LOG_INFO("No accepting states, skipping probability computation."); - std::vector numericResult(this->getModel().getNumberOfStates(), storm::utility::zero()); - return numericResult; - } - - STORM_LOG_INFO("Computing probabilities for reaching accepting BSCCs..."); - - storm::storage::BitVector bvTrue(product->getProductModel().getNumberOfStates(), true); - - storm::solver::SolveGoal solveGoalProduct(goal); - storm::storage::BitVector soiProduct(product->getStatesOfInterest()); - solveGoalProduct.setRelevantValues(std::move(soiProduct)); - - std::vector prodNumericResult - = std::move(storm::modelchecker::helper::SparseMdpPrctlHelper::computeUntilProbabilities(env, - std::move(solveGoalProduct), - product->getProductModel().getTransitionMatrix(), - product->getProductModel().getBackwardTransitions(), - bvTrue, - accepting, - qualitative, - false // no schedulers (at the moment) - ).values); - - std::vector numericResult = product->projectToOriginalModel(this->getModel(), prodNumericResult); - return numericResult; - } - */ - - template std::unique_ptr SparseMdpPrctlModelChecker::computeConditionalProbabilities(Environment const& env, CheckTask const& checkTask) { storm::logic::ConditionalFormula const& conditionalFormula = checkTask.getFormula(); diff --git a/src/storm/transformer/DAProductBuilder.h b/src/storm/transformer/DAProductBuilder.h index 9e903e058..d90d4b6dc 100644 --- a/src/storm/transformer/DAProductBuilder.h +++ b/src/storm/transformer/DAProductBuilder.h @@ -18,10 +18,15 @@ namespace storm { template typename DAProduct::ptr build(const Model& originalModel, const storm::storage::BitVector& statesOfInterest) const { - typename Product::ptr product = ProductBuilder::buildProduct(originalModel, *this, statesOfInterest); + return build(originalModel.getTransitionMatrix(), statesOfInterest); + } + + template + typename DAProduct::ptr build(const storm::storage::SparseMatrix& originalMatrix, const storm::storage::BitVector& statesOfInterest) const { //todo transition matrix + typename Product::ptr product = ProductBuilder::buildProduct(originalMatrix, *this, statesOfInterest); storm::automata::AcceptanceCondition::ptr prodAcceptance - = da.getAcceptance()->lift(product->getProductModel().getNumberOfStates(), - [&product](std::size_t prodState) {return product->getAutomatonState(prodState);}); + = da.getAcceptance()->lift(product->getProductModel().getNumberOfStates(), + [&product](std::size_t prodState) {return product->getAutomatonState(prodState);}); return typename DAProduct::ptr(new DAProduct(std::move(*product), prodAcceptance)); } diff --git a/src/storm/transformer/Product.h b/src/storm/transformer/Product.h index d0d826d0f..ee037784b 100644 --- a/src/storm/transformer/Product.h +++ b/src/storm/transformer/Product.h @@ -60,7 +60,12 @@ namespace storm { template std::vector projectToOriginalModel(const Model& originalModel, const std::vector& prodValues) { - std::vector origValues(originalModel.getNumberOfStates()); + return projectToOriginalModel(originalModel.getNumberOfStates(), prodValues); + } + + template + std::vector projectToOriginalModel(std::size_t numberOfStates, const std::vector& prodValues) { + std::vector origValues(numberOfStates); for (state_type productState : productModel.getStateLabeling().getStates(productStateOfInterestLabel)) { state_type originalState = getModelState(productState); origValues.at(originalState) = prodValues.at(productState); diff --git a/src/storm/transformer/ProductBuilder.h b/src/storm/transformer/ProductBuilder.h index 32f3a0cea..a82bd2839 100644 --- a/src/storm/transformer/ProductBuilder.h +++ b/src/storm/transformer/ProductBuilder.h @@ -17,8 +17,7 @@ namespace storm { typedef storm::storage::SparseMatrix matrix_type; template - static typename Product::ptr buildProduct(const Model& originalModel, ProductOperator& prodOp, const storm::storage::BitVector& statesOfInterest) { - const matrix_type& originalMatrix = originalModel.getTransitionMatrix(); + static typename Product::ptr buildProduct(const matrix_type& originalMatrix , ProductOperator& prodOp, const storm::storage::BitVector& statesOfInterest) { bool deterministic = originalMatrix.hasTrivialRowGrouping(); typedef storm::storage::sparse::state_type state_type;