fixed some bugs and enabled markov automaton model checking from cli

Former-commit-id: 91b689d817

src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp

@@ -46,7 +46,17 @@ namespace storm {
             std::unique_ptr<CheckResult> rightResultPointer = this->check(pathFormula.getRightSubformula());
             ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult();
 
-            std::vector<ValueType> result = storm::modelchecker::helper::SparseMarkovAutomatonCslHelper<ValueType>::computeBoundedUntilProbabilities(checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), this->getModel().getExitRates(), this->getModel().getMarkovianStates(), rightResult.getTruthValuesVector(), pathFormula.getIntervalBounds(), *minMaxLinearEquationSolverFactory);
+            double lowerBound = 0;
+            double upperBound = 0;
+            if (!pathFormula.hasDiscreteTimeBound()) {
+                std::pair<double, double> const& intervalBounds =  pathFormula.getIntervalBounds();
+                lowerBound = intervalBounds.first;
+                upperBound = intervalBounds.second;
+            } else {
+                upperBound = pathFormula.getDiscreteTimeBound();
+            }
+            
+            std::vector<ValueType> result = storm::modelchecker::helper::SparseMarkovAutomatonCslHelper<ValueType>::computeBoundedUntilProbabilities(checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), this->getModel().getExitRates(), this->getModel().getMarkovianStates(), rightResult.getTruthValuesVector(), std::make_pair(lowerBound, upperBound), *minMaxLinearEquationSolverFactory);
             return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(std::move(result)));
         }
                 

src/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp

@@ -32,6 +32,7 @@ namespace storm {
 
             template<typename ValueType>
             void SparseMarkovAutomatonCslHelper<ValueType>::computeBoundedReachabilityProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::vector<ValueType> const& exitRates, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& goalStates, storm::storage::BitVector const& markovianNonGoalStates, storm::storage::BitVector const& probabilisticNonGoalStates, std::vector<ValueType>& markovianNonGoalValues, std::vector<ValueType>& probabilisticNonGoalValues, ValueType delta, uint_fast64_t numberOfSteps, storm::utility::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory) {
+                
                 // Start by computing four sparse matrices:
                 // * a matrix aMarkovian with all (discretized) transitions from Markovian non-goal states to all Markovian non-goal states.
                 // * a matrix aMarkovianToProbabilistic with all (discretized) transitions from Markovian non-goal states to all probabilistic non-goal states.
@@ -116,10 +117,10 @@ namespace storm {
                 storm::utility::vector::addVectors(bProbabilistic, bProbabilisticFixed, bProbabilistic);
                 solver->solveEquationSystem(dir, probabilisticNonGoalValues, bProbabilistic, &multiplicationResultScratchMemory, &aProbabilisticScratchMemory);
             }
-            
 
             template<typename ValueType>
             std::vector<ValueType> SparseMarkovAutomatonCslHelper<ValueType>::computeBoundedUntilProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::vector<ValueType> const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, std::pair<double, double> const& boundsPair, storm::utility::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory) {
+
                 uint_fast64_t numberOfStates = transitionMatrix.getRowGroupCount();
                 
                 // 'Unpack' the bounds to make them more easily accessible.

src/models/sparse/MarkovAutomaton.cpp

@@ -15,7 +15,7 @@ namespace storm {
                                                         std::vector<ValueType> const& exitRates,
                                                         std::unordered_map<std::string, RewardModelType> const& rewardModels,
                                                         boost::optional<std::vector<LabelSet>> const& optionalChoiceLabeling)
-            : NondeterministicModel<ValueType, RewardModelType>(storm::models::ModelType::MarkovAutomaton, transitionMatrix, stateLabeling, rewardModels, optionalChoiceLabeling), markovianStates(markovianStates), exitRates(exitRates), closed(false) {
+            : NondeterministicModel<ValueType, RewardModelType>(storm::models::ModelType::MarkovAutomaton, transitionMatrix, stateLabeling, rewardModels, optionalChoiceLabeling), markovianStates(markovianStates), exitRates(exitRates), closed(this->checkIsClosed()) {
                 this->turnRatesToProbabilities();
             }
             
@@ -26,7 +26,7 @@ namespace storm {
                                                         std::vector<ValueType> const& exitRates,
                                                         std::unordered_map<std::string, RewardModelType>&& rewardModels,
                                                         boost::optional<std::vector<LabelSet>>&& optionalChoiceLabeling)
-            : NondeterministicModel<ValueType, RewardModelType>(storm::models::ModelType::MarkovAutomaton, std::move(transitionMatrix), std::move(stateLabeling), std::move(rewardModels), std::move(optionalChoiceLabeling)), markovianStates(markovianStates), exitRates(std::move(exitRates)), closed(false) {
+            : NondeterministicModel<ValueType, RewardModelType>(storm::models::ModelType::MarkovAutomaton, std::move(transitionMatrix), std::move(stateLabeling), std::move(rewardModels), std::move(optionalChoiceLabeling)), markovianStates(markovianStates), exitRates(std::move(exitRates)), closed(this->checkIsClosed()) {
                 this->turnRatesToProbabilities();
             }
             
@@ -97,21 +97,19 @@ namespace storm {
                     // Now copy over all choices that need to be kept.
                     uint_fast64_t currentChoice = 0;
                     for (uint_fast64_t state = 0; state < this->getNumberOfStates(); ++state) {
-                        // If the state is a hybrid state, closing it will make it a probabilistic state, so we remove the Markovian marking.
-                        if (this->isHybridState(state)) {
-                            this->markovianStates.set(state, false);
-                        }
-                        
                         // Record the new beginning of choices of this state.
                         newTransitionMatrixBuilder.newRowGroup(currentChoice);
-                        
-                        // If we are currently treating a hybrid state, we need to skip its first choice.
+
+                        // If the state is a hybrid state, closing it will make it a probabilistic state, so we remove the Markovian marking.
+                        // Additionally, we need to remember whether we need to skip the first choice of the state when
+                        // we assemble the new transition matrix.
+                        uint_fast64_t offset = 0;
                         if (this->isHybridState(state)) {
-                            // Remove the Markovian state marking.
                             this->markovianStates.set(state, false);
+                            offset = 1;
                         }
                         
-                        for (uint_fast64_t row = this->getTransitionMatrix().getRowGroupIndices()[state] + (this->isHybridState(state) ? 1 : 0); row < this->getTransitionMatrix().getRowGroupIndices()[state + 1]; ++row) {
+                        for (uint_fast64_t row = this->getTransitionMatrix().getRowGroupIndices()[state] + offset; row < this->getTransitionMatrix().getRowGroupIndices()[state + 1]; ++row) {
                             for (auto const& entry : this->getTransitionMatrix().getRow(row)) {
                                 newTransitionMatrixBuilder.addNextValue(currentChoice, entry.getColumn(), entry.getValue());
                             }
@@ -216,12 +214,22 @@ namespace storm {
             template <typename ValueType, typename RewardModelType>
             void MarkovAutomaton<ValueType, RewardModelType>::turnRatesToProbabilities() {
                 for (auto state : this->markovianStates) {
-                    for (auto& transition : this->getTransitionMatrix().getRowGroup(state)) {
+                    for (auto& transition : this->getTransitionMatrix().getRow(this->getTransitionMatrix().getRowGroupIndices()[state])) {
                         transition.setValue(transition.getValue() / this->exitRates[state]);
                     }
                 }
             }
             
+            template <typename ValueType, typename RewardModelType>
+            bool MarkovAutomaton<ValueType, RewardModelType>::checkIsClosed() const {
+                for (auto state : markovianStates) {
+                    if (this->getTransitionMatrix().getRowGroupSize(state) > 1) {
+                        return false;
+                    }
+                }
+                return true;
+            }
+            
             template class MarkovAutomaton<double>;
 //            template class MarkovAutomaton<float>;
             

src/models/sparse/MarkovAutomaton.h

@@ -140,6 +140,11 @@ namespace storm {
                  */
                 void turnRatesToProbabilities();
                 
+                /*!
+                 * Checks whether the automaton is closed by actually looking at the transition information.
+                 */
+                bool checkIsClosed() const;
+                
                 // A bit vector representing the set of Markovian states.
                 storm::storage::BitVector markovianStates;
                 

src/parser/MarkovAutomatonSparseTransitionParser.cpp

@@ -6,6 +6,7 @@
 #include "src/exceptions/FileIoException.h"
 #include "src/parser/MappedFile.h"
 #include "src/utility/cstring.h"
+#include "src/utility/constants.h"
 #include "src/utility/macros.h"
 
 namespace storm {
@@ -152,6 +153,16 @@ namespace storm {
                     }
                 } while (!encounteredEOF && !encounteredNewDistribution);
             }
+            
+            // If there are some states with indices that are behind the last source for which no transition was specified,
+            // we need to reserve some space for introducing self-loops later.
+            if (!dontFixDeadlocks) {
+                result.numberOfNonzeroEntries += result.highestStateIndex - lastsource;
+                result.numberOfChoices += result.highestStateIndex - lastsource;
+            } else {
+                STORM_LOG_ERROR("Found deadlock states (e.g. " << lastsource + 1 << ") during parsing. Please fix them or set the appropriate flag.");
+                throw storm::exceptions::WrongFormatException() << "Found deadlock states (e.g. " << lastsource + 1 << ") during parsing. Please fix them or set the appropriate flag.";
+            }
 
             return result;
         }
@@ -259,6 +270,21 @@ namespace storm {
 
                 ++currentChoice;
             }
+            
+            // If there are some states with indices that are behind the last source for which no transition was specified,
+            // we need to insert the self-loops now. Note that we assume all these states to be Markovian.
+            if (!dontFixDeadlocks) {
+                for (uint_fast64_t index = lastsource + 1; index <= firstPassResult.highestStateIndex; ++index) {
+                    result.markovianStates.set(index, true);
+                    result.exitRates[index] = storm::utility::one<ValueType>();
+                    result.transitionMatrixBuilder.newRowGroup(currentChoice);
+                    result.transitionMatrixBuilder.addNextValue(currentChoice, index, storm::utility::one<ValueType>());
+                    ++currentChoice;
+                }
+            } else {
+                STORM_LOG_ERROR("Found deadlock states (e.g. " << lastsource + 1 << ") during parsing. Please fix them or set the appropriate flag.");
+                throw storm::exceptions::WrongFormatException() << "Found deadlock states (e.g. " << lastsource + 1 << ") during parsing. Please fix them or set the appropriate flag.";
+            }
 
             return result;
         }

src/utility/storm.h

@@ -59,6 +59,7 @@
 #include "src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h"
 #include "src/modelchecker/csl/SparseCtmcCslModelChecker.h"
 #include "src/modelchecker/csl/HybridCtmcCslModelChecker.h"
+#include "src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h"
 #include "src/modelchecker/results/ExplicitQualitativeCheckResult.h"
 #include "src/modelchecker/results/SymbolicQualitativeCheckResult.h"
 
@@ -295,6 +296,16 @@ namespace storm {
 
             storm::modelchecker::SparseCtmcCslModelChecker<storm::models::sparse::Ctmc<ValueType>> modelchecker(*ctmc);
             result = modelchecker.check(task);
+        } else if (model->getType() == storm::models::ModelType::MarkovAutomaton) {
+            std::shared_ptr<storm::models::sparse::MarkovAutomaton<ValueType>> ma = model->template as<storm::models::sparse::MarkovAutomaton<ValueType>>();
+            
+            // Close the MA, if it is not already closed.
+            if (!ma->isClosed()) {
+                ma->close();
+            }
+            
+            storm::modelchecker::SparseMarkovAutomatonCslModelChecker<storm::models::sparse::MarkovAutomaton<ValueType>> modelchecker(*ma);
+            result = modelchecker.check(task);
         }
         return result;