From 852afd17186bd3fd92e532575246b8b965d0d122 Mon Sep 17 00:00:00 2001 From: dehnert Date: Wed, 22 Jun 2016 13:11:54 +0200 Subject: [PATCH] fixed crowds models to work with exact arithmetic. fixed dynamic state priority queue implementation. added setting to use dedicated elimination-based model checker instead of regular model checker (+ elimination solver) Former-commit-id: 1b0802ff05c2b6c9bc99baf833d1e177cc2a73ad --- examples/dtmc/crowds/crowds10_5.pm | 10 ++-- examples/dtmc/crowds/crowds15_5.pm | 8 ++-- examples/dtmc/crowds/crowds20_5.pm | 8 ++-- examples/dtmc/crowds/crowds5_5.pm | 8 ++-- src/settings/Option.cpp | 8 ++-- src/settings/modules/EliminationSettings.cpp | 10 +++- src/settings/modules/EliminationSettings.h | 8 ++++ .../EliminationLinearEquationSolver.cpp | 20 ++------ .../DynamicStatePriorityQueue.cpp | 34 ++++++-------- .../DynamicStatePriorityQueue.h | 7 ++- src/utility/solver.h | 7 +-- src/utility/storm.h | 46 +++++++++++-------- 12 files changed, 92 insertions(+), 82 deletions(-) diff --git a/examples/dtmc/crowds/crowds10_5.pm b/examples/dtmc/crowds/crowds10_5.pm index 752b3f9bb..2dfdfdc3a 100644 --- a/examples/dtmc/crowds/crowds10_5.pm +++ b/examples/dtmc/crowds/crowds10_5.pm @@ -1,12 +1,12 @@ dtmc // probability of forwarding -const double PF = 0.8; -const double notPF = .2; // must be 1-PF +const double PF = 4/5; +const double notPF = 1/5; // must be 1-PF // probability that a crowd member is bad -const double badC = .167; +const double badC = 167/1000; // probability that a crowd member is good -const double goodC = 0.833; +const double goodC = 833/1000; // Total number of protocol runs to analyze const int TotalRuns = 5; // size of the crowd @@ -77,4 +77,4 @@ endmodule label "observe0Greater1" = observe0 > 1; label "observeIGreater1" = observe1 > 1 | observe2 > 1 | observe3 > 1 | observe4 > 1 | observe5 > 1 | observe6 > 1 | observe7 > 1 | observe8 > 1 | observe9 > 1; -label "observeOnlyTrueSender" = observe0 > 1 & observe1 <= 1 & observe2 <= 1 & observe3 <= 1 & observe4 <= 1 & observe5 <= 1 & observe6 <= 1 & observe7 <= 1 & observe8 <= 1 & observe9 <= 1; \ No newline at end of file +label "observeOnlyTrueSender" = observe0 > 1 & observe1 <= 1 & observe2 <= 1 & observe3 <= 1 & observe4 <= 1 & observe5 <= 1 & observe6 <= 1 & observe7 <= 1 & observe8 <= 1 & observe9 <= 1; diff --git a/examples/dtmc/crowds/crowds15_5.pm b/examples/dtmc/crowds/crowds15_5.pm index 95ab8a910..31ffefc0f 100644 --- a/examples/dtmc/crowds/crowds15_5.pm +++ b/examples/dtmc/crowds/crowds15_5.pm @@ -1,12 +1,12 @@ dtmc // probability of forwarding -const double PF = 0.8; -const double notPF = 0.2; // must be 1-PF +const double PF = 4/5; +const double notPF = 1/5; // must be 1-PF // probability that a crowd member is bad -const double badC = 0.167; +const double badC = 167/1000; // probability that a crowd member is good -const double goodC = 0.833; +const double goodC = 833/1000; // Total number of protocol runs to analyze const int TotalRuns = 5; // size of the crowd diff --git a/examples/dtmc/crowds/crowds20_5.pm b/examples/dtmc/crowds/crowds20_5.pm index 1809c22d7..ffe4c9a4f 100644 --- a/examples/dtmc/crowds/crowds20_5.pm +++ b/examples/dtmc/crowds/crowds20_5.pm @@ -1,12 +1,12 @@ dtmc // probability of forwarding -const double PF = 0.8; -const double notPF = 0.2; // must be 1-PF +const double PF = 4/5; +const double notPF = 1/5; // must be 1-PF // probability that a crowd member is bad -const double badC = 0.167; +const double badC = 167/1000; // probability that a crowd member is good -const double goodC = 0.833; +const double goodC = 833/1000; // Total number of protocol runs to analyze const int TotalRuns = 5; // size of the crowd diff --git a/examples/dtmc/crowds/crowds5_5.pm b/examples/dtmc/crowds/crowds5_5.pm index 60bdaa7ea..be995c528 100644 --- a/examples/dtmc/crowds/crowds5_5.pm +++ b/examples/dtmc/crowds/crowds5_5.pm @@ -1,12 +1,12 @@ dtmc // probability of forwarding -const double PF = 0.8; -const double notPF = .2; // must be 1-PF +const double PF = 4/5; +const double notPF = 1/5; // must be 1-PF // probability that a crowd member is bad -const double badC = .167; +const double badC = 167/1000; // probability that a crowd member is good -const double goodC = 0.833; +const double goodC = 833/1000; // Total number of protocol runs to analyze const int TotalRuns = 5; // size of the crowd diff --git a/src/settings/Option.cpp b/src/settings/Option.cpp index cba074b58..b5701e63c 100644 --- a/src/settings/Option.cpp +++ b/src/settings/Option.cpp @@ -116,11 +116,11 @@ namespace storm { STORM_LOG_THROW(!longName.empty(), storm::exceptions::IllegalArgumentException, "Unable to construct option with empty name."); STORM_LOG_THROW(!moduleName.empty(), storm::exceptions::IllegalArgumentException, "Unable to construct option with empty module name."); - bool longNameContainsNonAlpha = std::find_if(longName.begin(), longName.end(), [](char c) { return !(std::isalpha(c) || std::isdigit(c)); }) != longName.end(); - STORM_LOG_THROW(!longNameContainsNonAlpha, storm::exceptions::IllegalArgumentException, "Unable to construct option with illegal long name '" << longName << "'."); + bool longNameContainsIllegalCharacter = std::find_if(longName.begin(), longName.end(), [](char c) { return !(std::isalpha(c) || std::isdigit(c) || c == '-' || c == '_'); }) != longName.end(); + STORM_LOG_THROW(!longNameContainsIllegalCharacter, storm::exceptions::IllegalArgumentException, "Unable to construct option with illegal long name '" << longName << "'."); - bool shortNameContainsNonAlpha = std::find_if(shortName.begin(), shortName.end(), [](char c) { return !(std::isalpha(c) || std::isdigit(c)); }) != shortName.end(); - STORM_LOG_THROW(!shortNameContainsNonAlpha, storm::exceptions::IllegalArgumentException, "Unable to construct option with illegal short name '" << shortName << "'."); + bool shortNameContainsIllegalCharacter = std::find_if(shortName.begin(), shortName.end(), [](char c) { return !(std::isalpha(c) || std::isdigit(c) || c == 'c' || c == '_'); }) != shortName.end(); + STORM_LOG_THROW(!shortNameContainsIllegalCharacter, storm::exceptions::IllegalArgumentException, "Unable to construct option with illegal short name '" << shortName << "'."); // Then index all arguments. for (auto const& argument : arguments) { diff --git a/src/settings/modules/EliminationSettings.cpp b/src/settings/modules/EliminationSettings.cpp index 4c26ae0b5..db973ce41 100644 --- a/src/settings/modules/EliminationSettings.cpp +++ b/src/settings/modules/EliminationSettings.cpp @@ -10,15 +10,16 @@ namespace storm { namespace settings { namespace modules { - const std::string EliminationSettings::moduleName = "sparseelim"; + const std::string EliminationSettings::moduleName = "elimination"; const std::string EliminationSettings::eliminationMethodOptionName = "method"; const std::string EliminationSettings::eliminationOrderOptionName = "order"; const std::string EliminationSettings::entryStatesLastOptionName = "entrylast"; const std::string EliminationSettings::maximalSccSizeOptionName = "sccsize"; + const std::string EliminationSettings::useDedicatedModelCheckerOptionName = "use-dedicated-mc"; EliminationSettings::EliminationSettings() : ModuleSettings(moduleName) { std::vector orders = {"fw", "fwrev", "bw", "bwrev", "rand", "spen", "dpen", "regex"}; - this->addOption(storm::settings::OptionBuilder(moduleName, eliminationOrderOptionName, true, "The order that is to be used for the elimination techniques. Available are {fw, fwrev, bw, bwrev, rand, spen, dpen}.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the order in which states are chosen for elimination.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(orders)).setDefaultValueString("fwrev").build()).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, eliminationOrderOptionName, true, "The order that is to be used for the elimination techniques. Available are {fw, fwrev, bw, bwrev, rand, spen, dpen, regex}.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the order in which states are chosen for elimination.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(orders)).setDefaultValueString("fwrev").build()).build()); std::vector methods = {"state", "hybrid"}; this->addOption(storm::settings::OptionBuilder(moduleName, eliminationMethodOptionName, true, "The elimination technique to use. Available are {state, hybrid}.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the elimination technique to use.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(methods)).setDefaultValueString("state").build()).build()); @@ -26,6 +27,7 @@ namespace storm { this->addOption(storm::settings::OptionBuilder(moduleName, entryStatesLastOptionName, true, "Sets whether the entry states are eliminated last.").build()); this->addOption(storm::settings::OptionBuilder(moduleName, maximalSccSizeOptionName, true, "Sets the maximal size of the SCCs for which state elimination is applied.") .addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("maxsize", "The maximal size of an SCC on which state elimination is applied.").setDefaultValueUnsignedInteger(20).setIsOptional(true).build()).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, useDedicatedModelCheckerOptionName, true, "Sets whether to use the dedicated model elimination checker (only DTMCs).").build()); } EliminationSettings::EliminationMethod EliminationSettings::getEliminationMethod() const { @@ -69,6 +71,10 @@ namespace storm { uint_fast64_t EliminationSettings::getMaximalSccSize() const { return this->getOption(maximalSccSizeOptionName).getArgumentByName("maxsize").getValueAsUnsignedInteger(); } + + bool EliminationSettings::isUseDedicatedModelCheckerSet() const { + return this->getOption(useDedicatedModelCheckerOptionName).getHasOptionBeenSet(); + } } // namespace modules } // namespace settings } // namespace storm \ No newline at end of file diff --git a/src/settings/modules/EliminationSettings.h b/src/settings/modules/EliminationSettings.h index 22c53daac..239b33795 100644 --- a/src/settings/modules/EliminationSettings.h +++ b/src/settings/modules/EliminationSettings.h @@ -54,6 +54,13 @@ namespace storm { * @return The maximal size of an SCC on which state elimination is to be directly applied. */ uint_fast64_t getMaximalSccSize() const; + + /*! + * Retrieves whether the dedicated model checker is to be used instead of the general on. + * + * @return True iff the option was set. + */ + bool isUseDedicatedModelCheckerSet() const; const static std::string moduleName; @@ -62,6 +69,7 @@ namespace storm { const static std::string eliminationOrderOptionName; const static std::string entryStatesLastOptionName; const static std::string maximalSccSizeOptionName; + const static std::string useDedicatedModelCheckerOptionName; }; } // namespace modules diff --git a/src/solver/EliminationLinearEquationSolver.cpp b/src/solver/EliminationLinearEquationSolver.cpp index 01c91531d..4a4321ef9 100644 --- a/src/solver/EliminationLinearEquationSolver.cpp +++ b/src/solver/EliminationLinearEquationSolver.cpp @@ -27,11 +27,13 @@ namespace storm { void EliminationLinearEquationSolver::solveEquationSystem(std::vector& x, std::vector const& b, std::vector* multiplyResult) const { STORM_LOG_WARN_COND(multiplyResult == nullptr, "Providing scratch memory will not improve the performance of this solver."); + STORM_LOG_DEBUG("Solving equation system using elimination."); + // We need to revert the transformation into an equation system matrix, because the elimination procedure // and the distance computation is based on the probability matrix instead. storm::storage::SparseMatrix transitionMatrix(A); transitionMatrix.convertToEquationSystem(); - storm::storage::SparseMatrix backwardTransitions = A.transpose(); + storm::storage::SparseMatrix backwardTransitions = transitionMatrix.transpose(); // Initialize the solution to the right-hand side of the equation system. x = b; @@ -52,28 +54,14 @@ namespace storm { std::shared_ptr priorityQueue = createStatePriorityQueue(distanceBasedPriorities, flexibleMatrix, flexibleBackwardTransitions, b, storm::storage::BitVector(x.size(), true)); -// std::cout << "intermediate:" << std::endl; -// std::cout << "flexibleMatrix:" << std::endl; -// std::cout << flexibleMatrix << std::endl; -// std::cout << "backward:" << std::endl; -// std::cout << flexibleBackwardTransitions << std::endl; - // Create a state eliminator to perform the actual elimination. PrioritizedStateEliminator eliminator(flexibleMatrix, flexibleBackwardTransitions, priorityQueue, x); - std::cout << "eliminating" << std::endl; + // Eliminate all states. while (priorityQueue->hasNext()) { auto state = priorityQueue->pop(); eliminator.eliminateState(state, false); } - -// std::cout << "output:" << std::endl; -// std::cout << "x:" << std::endl; -// for (auto const& e : x) { -// std::cout << e << std::endl; -// } - - std::cout << "done" << std::endl; } template diff --git a/src/solver/stateelimination/DynamicStatePriorityQueue.cpp b/src/solver/stateelimination/DynamicStatePriorityQueue.cpp index afff0b7a3..ec2c4fe3f 100644 --- a/src/solver/stateelimination/DynamicStatePriorityQueue.cpp +++ b/src/solver/stateelimination/DynamicStatePriorityQueue.cpp @@ -10,15 +10,11 @@ namespace storm { namespace stateelimination { template - DynamicStatePriorityQueue::DynamicStatePriorityQueue(std::vector> const& sortedStatePenaltyPairs, storm::storage::FlexibleSparseMatrix const& transitionMatrix, storm::storage::FlexibleSparseMatrix const& backwardTransitions, std::vector const& oneStepProbabilities, PenaltyFunctionType const& penaltyFunction) : StatePriorityQueue(), transitionMatrix(transitionMatrix), backwardTransitions(backwardTransitions), oneStepProbabilities(oneStepProbabilities), priorityQueue(), stateToPriorityMapping(), penaltyFunction(penaltyFunction) { + DynamicStatePriorityQueue::DynamicStatePriorityQueue(std::vector> const& sortedStatePenaltyPairs, storm::storage::FlexibleSparseMatrix const& transitionMatrix, storm::storage::FlexibleSparseMatrix const& backwardTransitions, std::vector const& oneStepProbabilities, PenaltyFunctionType const& penaltyFunction) : StatePriorityQueue(), transitionMatrix(transitionMatrix), backwardTransitions(backwardTransitions), oneStepProbabilities(oneStepProbabilities), priorityQueue(), stateToPriorityQueueEntry(), penaltyFunction(penaltyFunction) { // Insert all state-penalty pairs into our priority queue. for (auto const& statePenalty : sortedStatePenaltyPairs) { - priorityQueue.insert(priorityQueue.end(), statePenalty); - } - - // Insert all state-penalty pairs into auxiliary mapping. - for (auto const& statePenalty : sortedStatePenaltyPairs) { - stateToPriorityMapping.emplace(statePenalty); + auto it = priorityQueue.insert(priorityQueue.end(), statePenalty); + stateToPriorityQueueEntry.emplace(statePenalty.first, it); } } @@ -33,30 +29,30 @@ namespace storm { STORM_LOG_TRACE("Popping state " << it->first << " with priority " << it->second << "."); storm::storage::sparse::state_type result = it->first; priorityQueue.erase(priorityQueue.begin()); + stateToPriorityQueueEntry.erase(result); return result; } template void DynamicStatePriorityQueue::update(storm::storage::sparse::state_type state) { - // First, we need to find the priority until now. - auto priorityIt = stateToPriorityMapping.find(state); + // First, we need to find the old priority queue entry for the state. + auto priorityQueueEntryIt = stateToPriorityQueueEntry.find(state); // If the priority queue does not store the priority of the given state, we must not update it. - if (priorityIt == stateToPriorityMapping.end()) { + if (priorityQueueEntryIt == stateToPriorityQueueEntry.end()) { return; } - uint_fast64_t lastPriority = priorityIt->second; - + + // Compute the new priority. uint_fast64_t newPriority = penaltyFunction(state, transitionMatrix, backwardTransitions, oneStepProbabilities); - if (lastPriority != newPriority) { - // Erase and re-insert into the priority queue with the new priority. - auto queueIt = priorityQueue.find(std::make_pair(state, lastPriority)); - priorityQueue.erase(queueIt); - priorityQueue.emplace(state, newPriority); + if (priorityQueueEntryIt->second->second != newPriority) { + // Erase and re-insert the entry into priority queue (with the new priority). + priorityQueue.erase(priorityQueueEntryIt->second); + stateToPriorityQueueEntry.erase(priorityQueueEntryIt); - // Finally, update the probability in the mapping. - priorityIt->second = newPriority; + auto newElementIt = priorityQueue.emplace(state, newPriority); + stateToPriorityQueueEntry.emplace(state, newElementIt.first); } } diff --git a/src/solver/stateelimination/DynamicStatePriorityQueue.h b/src/solver/stateelimination/DynamicStatePriorityQueue.h index b5675440b..e1fbc4039 100644 --- a/src/solver/stateelimination/DynamicStatePriorityQueue.h +++ b/src/solver/stateelimination/DynamicStatePriorityQueue.h @@ -35,11 +35,14 @@ namespace storm { virtual std::size_t size() const override; private: + typedef std::set, PriorityComparator> PriorityQueue; + typedef std::unordered_map StatePriorityQueueEntryMap; + storm::storage::FlexibleSparseMatrix const& transitionMatrix; storm::storage::FlexibleSparseMatrix const& backwardTransitions; std::vector const& oneStepProbabilities; - std::set, PriorityComparator> priorityQueue; - std::unordered_map stateToPriorityMapping; + PriorityQueue priorityQueue; + StatePriorityQueueEntryMap stateToPriorityQueueEntry; PenaltyFunctionType penaltyFunction; }; diff --git a/src/utility/solver.h b/src/utility/solver.h index 4791737a8..d61c99442 100644 --- a/src/utility/solver.h +++ b/src/utility/solver.h @@ -34,9 +34,10 @@ namespace storm { class LpSolver; class SmtSolver; - template class NativeLinearEquationSolver; - enum class - NativeLinearEquationSolverSolutionMethod; + template + class NativeLinearEquationSolver; + + enum class NativeLinearEquationSolverSolutionMethod; } namespace storage { diff --git a/src/utility/storm.h b/src/utility/storm.h index e6f7a277c..c33c5cfb5 100644 --- a/src/utility/storm.h +++ b/src/utility/storm.h @@ -21,7 +21,8 @@ #include "src/settings/modules/IOSettings.h" #include "src/settings/modules/BisimulationSettings.h" #include "src/settings/modules/ParametricSettings.h" - +#include "src/settings/modules/EliminationSettings.h" +#include "src/settings/modules/MarkovChainSettings.h" // Formula headers. #include "src/logic/Formulas.h" @@ -263,20 +264,23 @@ namespace storm { template std::unique_ptr verifySparseModel(std::shared_ptr> model, std::shared_ptr const& formula, bool onlyInitialStatesRelevant = false) { - std::unique_ptr result; storm::modelchecker::CheckTask task(*formula, onlyInitialStatesRelevant); if (model->getType() == storm::models::ModelType::Dtmc) { std::shared_ptr> dtmc = model->template as>(); - storm::modelchecker::SparseDtmcPrctlModelChecker> modelchecker(*dtmc); - if (modelchecker.canHandle(task)) { - result = modelchecker.check(task); + if (storm::settings::getModule().getEquationSolver() == storm::solver::EquationSolverType::Elimination && storm::settings::getModule().isUseDedicatedModelCheckerSet()) { + storm::modelchecker::SparseDtmcEliminationModelChecker> modelchecker(*dtmc); + if (modelchecker.canHandle(task)) { + result = modelchecker.check(task); + } else { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "The property " << *formula << " is not supported by the dedicated elimination model checker."); + } } else { - storm::modelchecker::SparseDtmcEliminationModelChecker> modelchecker2(*dtmc); - if (modelchecker2.canHandle(task)) { - result = modelchecker2.check(task); + storm::modelchecker::SparseDtmcPrctlModelChecker> modelchecker(*dtmc); + if (modelchecker.canHandle(task)) { + result = modelchecker.check(task); } else { - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "The property " << *formula << " is not supported on DTMCs."); + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "The property " << *formula << " is not supported."); } } } else if (model->getType() == storm::models::ModelType::Mdp) { @@ -320,16 +324,20 @@ namespace storm { std::unique_ptr result; if (model->getType() == storm::models::ModelType::Dtmc) { std::shared_ptr> dtmc = model->template as>(); - storm::modelchecker::SparseDtmcPrctlModelChecker> modelchecker(*dtmc); - if (modelchecker.canHandle(task)) { - result = modelchecker.check(task); - } else { + + if (storm::settings::getModule().getEquationSolver() == storm::solver::EquationSolverType::Elimination && storm::settings::getModule().isUseDedicatedModelCheckerSet()) { storm::modelchecker::SparseDtmcEliminationModelChecker> modelchecker(*dtmc); - storm::modelchecker::CheckTask task(*formula, onlyInitialStatesRelevant); if (modelchecker.canHandle(task)) { result = modelchecker.check(task); } else { - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "The exact engine currently does not support this property on DTMCs."); + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "The property " << *formula << " is not supported by the dedicated elimination model checker."); + } + } else { + storm::modelchecker::SparseDtmcPrctlModelChecker> modelchecker(*dtmc); + if (modelchecker.canHandle(task)) { + result = modelchecker.check(task); + } else { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "The property " << *formula << " is not supported."); } } } else { @@ -362,20 +370,20 @@ namespace storm { std::unique_ptr result; if (model->getType() == storm::models::ModelType::Dtmc) { std::shared_ptr> dtmc = model->template as>(); - if (storm::settings::getModule().getEquationSolver() == storm::solver::EquationSolverType::Elimination) { + + if (storm::settings::getModule().getEquationSolver() == storm::solver::EquationSolverType::Elimination && storm::settings::getModule().isUseDedicatedModelCheckerSet()) { storm::modelchecker::SparseDtmcEliminationModelChecker> modelchecker(*dtmc); - storm::modelchecker::CheckTask task(*formula, onlyInitialStatesRelevant); if (modelchecker.canHandle(task)) { result = modelchecker.check(task); } else { - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "The parametric engine currently does not support this property on DTMCs."); + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "The property " << *formula << " is not supported by the dedicated elimination model checker."); } } else { storm::modelchecker::SparseDtmcPrctlModelChecker> modelchecker(*dtmc); if (modelchecker.canHandle(task)) { result = modelchecker.check(task); } else { - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "The parametric engine currently does not support this property on DTMCs."); + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "The property " << *formula << " is not supported."); } } } else if (model->getType() == storm::models::ModelType::Mdp) {