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: 1b0802ff05

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

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

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

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

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) {

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<std::string> 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<std::string> 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

src/settings/modules/EliminationSettings.h

@@ -55,6 +55,13 @@ namespace storm {
                  */
                 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;
                 
             private:
@@ -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

src/solver/EliminationLinearEquationSolver.cpp

@@ -27,11 +27,13 @@ namespace storm {
         void EliminationLinearEquationSolver<ValueType>::solveEquationSystem(std::vector<ValueType>& x, std::vector<ValueType> const& b, std::vector<ValueType>* 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<ValueType> transitionMatrix(A);
             transitionMatrix.convertToEquationSystem();
-            storm::storage::SparseMatrix<ValueType> backwardTransitions = A.transpose();
+            storm::storage::SparseMatrix<ValueType> 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<StatePriorityQueue> priorityQueue = createStatePriorityQueue<ValueType>(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<ValueType> 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<typename ValueType>

src/solver/stateelimination/DynamicStatePriorityQueue.cpp

@@ -10,15 +10,11 @@ namespace storm {
         namespace stateelimination {
             
             template<typename ValueType>
-            DynamicStatePriorityQueue<ValueType>::DynamicStatePriorityQueue(std::vector<std::pair<storm::storage::sparse::state_type, uint_fast64_t>> const& sortedStatePenaltyPairs, storm::storage::FlexibleSparseMatrix<ValueType> const& transitionMatrix, storm::storage::FlexibleSparseMatrix<ValueType> const& backwardTransitions, std::vector<ValueType> const& oneStepProbabilities, PenaltyFunctionType const& penaltyFunction) : StatePriorityQueue(), transitionMatrix(transitionMatrix), backwardTransitions(backwardTransitions), oneStepProbabilities(oneStepProbabilities), priorityQueue(), stateToPriorityMapping(), penaltyFunction(penaltyFunction) {
+            DynamicStatePriorityQueue<ValueType>::DynamicStatePriorityQueue(std::vector<std::pair<storm::storage::sparse::state_type, uint_fast64_t>> const& sortedStatePenaltyPairs, storm::storage::FlexibleSparseMatrix<ValueType> const& transitionMatrix, storm::storage::FlexibleSparseMatrix<ValueType> const& backwardTransitions, std::vector<ValueType> 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<typename ValueType>
             void DynamicStatePriorityQueue<ValueType>::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);
                 }
             }
             

src/solver/stateelimination/DynamicStatePriorityQueue.h

@@ -35,11 +35,14 @@ namespace storm {
                 virtual std::size_t size() const override;
                 
             private:
+                typedef std::set<std::pair<storm::storage::sparse::state_type, uint_fast64_t>, PriorityComparator> PriorityQueue;
+                typedef std::unordered_map<storm::storage::sparse::state_type, PriorityQueue::const_iterator> StatePriorityQueueEntryMap;
+                
                 storm::storage::FlexibleSparseMatrix<ValueType> const& transitionMatrix;
                 storm::storage::FlexibleSparseMatrix<ValueType> const& backwardTransitions;
                 std::vector<ValueType> const& oneStepProbabilities;
-                std::set<std::pair<storm::storage::sparse::state_type, uint_fast64_t>, PriorityComparator> priorityQueue;
-                std::unordered_map<storm::storage::sparse::state_type, uint_fast64_t> stateToPriorityMapping;
+                PriorityQueue priorityQueue;
+                StatePriorityQueueEntryMap stateToPriorityQueueEntry;
                 PenaltyFunctionType penaltyFunction;
             };
             

src/utility/solver.h

@@ -34,9 +34,10 @@ namespace storm {
         class LpSolver;
         class SmtSolver;
         
-        template<typename ValueType> class NativeLinearEquationSolver;
-        enum class
-                NativeLinearEquationSolverSolutionMethod;
+        template<typename ValueType>
+        class NativeLinearEquationSolver;
+        
+        enum class NativeLinearEquationSolverSolutionMethod;
     }
 
     namespace storage {

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<typename ValueType>
     std::unique_ptr<storm::modelchecker::CheckResult> verifySparseModel(std::shared_ptr<storm::models::sparse::Model<ValueType>> model, std::shared_ptr<storm::logic::Formula const> const& formula, bool onlyInitialStatesRelevant = false) {
-
         std::unique_ptr<storm::modelchecker::CheckResult> result;
         storm::modelchecker::CheckTask<storm::logic::Formula> task(*formula, onlyInitialStatesRelevant);
         if (model->getType() == storm::models::ModelType::Dtmc) {
             std::shared_ptr<storm::models::sparse::Dtmc<ValueType>> dtmc = model->template as<storm::models::sparse::Dtmc<ValueType>>();
-            storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<ValueType>> modelchecker(*dtmc);
+            if (storm::settings::getModule<storm::settings::modules::MarkovChainSettings>().getEquationSolver() == storm::solver::EquationSolverType::Elimination && storm::settings::getModule<storm::settings::modules::EliminationSettings>().isUseDedicatedModelCheckerSet()) {
+                storm::modelchecker::SparseDtmcEliminationModelChecker<storm::models::sparse::Dtmc<ValueType>> modelchecker(*dtmc);
                 if (modelchecker.canHandle(task)) {
                     result = modelchecker.check(task);
                 } else {
-                storm::modelchecker::SparseDtmcEliminationModelChecker<storm::models::sparse::Dtmc<ValueType>> modelchecker2(*dtmc);
-                if (modelchecker2.canHandle(task)) {
-                    result = modelchecker2.check(task);
+                    STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "The property " << *formula << " is not supported by the dedicated elimination model checker.");
+                }
+            } else {
+                storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<ValueType>> 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<storm::modelchecker::CheckResult> result;
         if (model->getType() == storm::models::ModelType::Dtmc) {
             std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalNumber>> dtmc = model->template as<storm::models::sparse::Dtmc<storm::RationalNumber>>();
-            storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<storm::RationalNumber>> modelchecker(*dtmc);
+
+            if (storm::settings::getModule<storm::settings::modules::MarkovChainSettings>().getEquationSolver() == storm::solver::EquationSolverType::Elimination && storm::settings::getModule<storm::settings::modules::EliminationSettings>().isUseDedicatedModelCheckerSet()) {
+                storm::modelchecker::SparseDtmcEliminationModelChecker<storm::models::sparse::Dtmc<storm::RationalNumber>> modelchecker(*dtmc);
                 if (modelchecker.canHandle(task)) {
                     result = modelchecker.check(task);
                 } else {
-                storm::modelchecker::SparseDtmcEliminationModelChecker<storm::models::sparse::Dtmc<storm::RationalNumber>> modelchecker(*dtmc);
-                storm::modelchecker::CheckTask<storm::logic::Formula> task(*formula, onlyInitialStatesRelevant);
+                    STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "The property " << *formula << " is not supported by the dedicated elimination model checker.");
+                }
+            } else {
+                storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<storm::RationalNumber>> modelchecker(*dtmc);
                 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.");
                 }
             }
         } else {
@@ -362,20 +370,20 @@ namespace storm {
         std::unique_ptr<storm::modelchecker::CheckResult> result;
         if (model->getType() == storm::models::ModelType::Dtmc) {
             std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> dtmc = model->template as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
-            if (storm::settings::getModule<storm::settings::modules::MarkovChainSettings>().getEquationSolver() == storm::solver::EquationSolverType::Elimination) {
+            
+            if (storm::settings::getModule<storm::settings::modules::MarkovChainSettings>().getEquationSolver() == storm::solver::EquationSolverType::Elimination && storm::settings::getModule<storm::settings::modules::EliminationSettings>().isUseDedicatedModelCheckerSet()) {
                 storm::modelchecker::SparseDtmcEliminationModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>> modelchecker(*dtmc);
-                storm::modelchecker::CheckTask<storm::logic::Formula> 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<storm::models::sparse::Dtmc<storm::RationalFunction>> 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) {