Structure for MA to CTMC

Former-commit-id: 6dee4cec3c

src/builder/ExplicitDFTModelBuilder.cpp

@@ -73,20 +73,20 @@ namespace storm {
             }
 
             std::shared_ptr<storm::models::sparse::Model<ValueType>> model;
-            if (deterministic) {
-                // Turn the probabilities into rates by multiplying each row with the exit rate of the state.
-                // TODO Matthias: avoid transforming back and forth
-                storm::storage::SparseMatrix<ValueType> rateMatrix(modelComponents.transitionMatrix);
-                for (uint_fast64_t row = 0; row < rateMatrix.getRowCount(); ++row) {
+            // Turn the probabilities into rates by multiplying each row with the exit rate of the state.
+            // TODO Matthias: avoid transforming back and forth
+            storm::storage::SparseMatrix<ValueType> rateMatrix(modelComponents.transitionMatrix);
+            for (uint_fast64_t row = 0; row < rateMatrix.getRowCount(); ++row) {
+                if (modelComponents.markovianStates.get(row)) {
                     for (auto& entry : rateMatrix.getRow(row)) {
                         entry.setValue(entry.getValue() * modelComponents.exitRates[row]);
                     }
                 }
-
+            }
+            if (deterministic) {
                 model = std::make_shared<storm::models::sparse::Ctmc<ValueType>>(std::move(rateMatrix), std::move(modelComponents.stateLabeling));
             } else {
-                model = std::make_shared<storm::models::sparse::MarkovAutomaton<ValueType>>(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), std::move(modelComponents.markovianStates), std::move(modelComponents.exitRates));
-
+                model = std::make_shared<storm::models::sparse::MarkovAutomaton<ValueType>>(std::move(rateMatrix), std::move(modelComponents.stateLabeling), std::move(modelComponents.markovianStates), std::move(modelComponents.exitRates));
             }
             model->printModelInformationToStream(std::cout);
             return model;

src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp

@@ -30,7 +30,7 @@ namespace storm {
         template<typename SparseMarkovAutomatonModelType>
         bool SparseMarkovAutomatonCslModelChecker<SparseMarkovAutomatonModelType>::canHandle(CheckTask<storm::logic::Formula> const& checkTask) const {
             storm::logic::Formula const& formula = checkTask.getFormula();
-            return formula.isCslStateFormula() || formula.isCslPathFormula() || (formula.isRewardPathFormula() && formula.isReachabilityRewardFormula());
+            return formula.isCslStateFormula() || formula.isCslPathFormula() || (formula.isRewardPathFormula() && formula.isReachabilityRewardFormula()) || formula.isExpectedTimeOperatorFormula();
         }
         
         template<typename SparseMarkovAutomatonModelType>

src/models/sparse/MarkovAutomaton.cpp

@@ -3,6 +3,8 @@
 #include "src/exceptions/InvalidArgumentException.h"
 #include "src/utility/constants.h"
 #include "src/adapters/CarlAdapter.h"
+#include "src/storage/FlexibleSparseMatrix.h"
+#include "src/models/sparse/Dtmc.h"
 
 namespace storm {
     namespace models {
@@ -217,6 +219,29 @@ namespace storm {
                 }
             }
             
+            template <typename ValueType, typename RewardModelType>
+            bool MarkovAutomaton<ValueType, RewardModelType>::hasOnlyTrivialNondeterminism() const {
+                // Check every state
+                for (uint_fast64_t state = 0; state < this->getNumberOfStates(); ++state) {
+                    // Get number of choices in current state
+                    uint_fast64_t numberChoices = this->getTransitionMatrix().getRowGroupIndices()[state + 1] - this->getTransitionMatrix().getRowGroupIndices()[state];
+                    if (isMarkovianState(state)) {
+                        assert(numberChoices == 1);
+                    }
+                    if (numberChoices > 1) {
+                        assert(isProbabilisticState(state));
+                        return false;
+                    }
+                }
+                return true;
+            }
+            
+            template <typename ValueType, typename RewardModelType>
+            std::shared_ptr<storm::models::sparse::Ctmc<ValueType, RewardModelType>> MarkovAutomaton<ValueType, RewardModelType>::convertToCTMC() {
+                assert(false)
+            }
+
+            
             template class MarkovAutomaton<double>;
 //            template class MarkovAutomaton<float>;
             

src/models/sparse/MarkovAutomaton.h

@@ -2,6 +2,7 @@
 #define STORM_MODELS_SPARSE_MARKOVAUTOMATON_H_
 
 #include "src/models/sparse/NondeterministicModel.h"
+#include "src/models/sparse/Ctmc.h"
 #include "src/utility/OsDetection.h"
 
 namespace storm {
@@ -121,6 +122,10 @@ namespace storm {
                  */
                 void close();
                 
+                bool hasOnlyTrivialNondeterminism() const;
+                
+                std::shared_ptr<storm::models::sparse::Ctmc<ValueType, RewardModelType>> convertToCTMC();
+                
                 virtual void writeDotToStream(std::ostream& outStream, bool includeLabeling = true, storm::storage::BitVector const* subsystem = nullptr, std::vector<ValueType> const* firstValue = nullptr, std::vector<ValueType> const* secondValue = nullptr, std::vector<uint_fast64_t> const* stateColoring = nullptr, std::vector<std::string> const* colors = nullptr, std::vector<uint_fast64_t>* scheduler = nullptr, bool finalizeOutput = true) const;
                 
                 std::size_t getSizeInBytes() const;

src/utility/storm.h

@@ -277,6 +277,8 @@ namespace storm {
                 storm::modelchecker::SparseDtmcEliminationModelChecker<storm::models::sparse::Dtmc<ValueType>> modelchecker2(*dtmc);
                 if (modelchecker2.canHandle(task)) {
                     result = modelchecker2.check(task);
+                } else {
+                    STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "The property " << *formula << " is not supported on DTMCs.");
                 }
             }
         } else if (model->getType() == storm::models::ModelType::Mdp) {
@@ -300,9 +302,15 @@ namespace storm {
             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>>();
-
-            storm::modelchecker::SparseMarkovAutomatonCslModelChecker<storm::models::sparse::MarkovAutomaton<ValueType>> modelchecker(*ma);
-            result = modelchecker.check(task);
+            if (ma->hasOnlyTrivialNondeterminism()) {
+                // Markov automaton can be converted into CTMC
+                std::shared_ptr<storm::models::sparse::Ctmc<ValueType>> ctmc = ma->convertToCTMC();
+                storm::modelchecker::SparseCtmcCslModelChecker<storm::models::sparse::Ctmc<ValueType>> modelchecker(*ctmc);
+                result = modelchecker.check(task);
+            } else {
+                storm::modelchecker::SparseMarkovAutomatonCslModelChecker<storm::models::sparse::MarkovAutomaton<ValueType>> modelchecker(*ma);
+                result = modelchecker.check(task);
+            }
         } else {
             STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "The model type " << model->getType() << " is not supported.");
         }