Further work on symbolic CTMC generation.

Former-commit-id: 81f2efb98c

src/builder/DdPrismModelBuilder.cpp

@@ -1,6 +1,7 @@
 #include "src/builder/DdPrismModelBuilder.h"
 
 #include "src/models/symbolic/Dtmc.h"
+#include "src/models/symbolic/Ctmc.h"
 #include "src/models/symbolic/Mdp.h"
 
 #include "src/storage/dd/CuddDd.h"
@@ -171,6 +172,7 @@ namespace storm {
             if (!commandDds.empty()) {
                 switch (generationInfo.program.getModelType()){
                     case storm::prism::Program::ModelType::DTMC:
+                    case storm::prism::Program::ModelType::CTMC:
                         result = combineCommandsToActionDTMC(generationInfo, commandDds);
                         break;
                     case storm::prism::Program::ModelType::MDP:
@@ -193,7 +195,9 @@ namespace storm {
             for (auto const& commandDd : commandDds) {
                 // Check for overlapping guards.
                 temporary = commandDd.guardDd * allGuards;
-                STORM_LOG_WARN_COND(temporary.isZero(), "Guard of a command overlaps with previous guards.");
+                
+                // Issue a warning if there are overlapping guards in a non-CTMC model.
+                STORM_LOG_WARN_COND(temporary.isZero() || generationInfo.program.getModelType() == storm::prism::Program::ModelType::CTMC, "Guard of a command overlaps with previous guards.");
                 
                 allGuards += commandDd.guardDd;
                 allCommands += commandDd.guardDd * commandDd.transitionsDd;
@@ -325,7 +329,7 @@ namespace storm {
             storm::dd::Add<Type> action1Extended = action1.transitionsDd * identityDd2;
             storm::dd::Add<Type> action2Extended = action2.transitionsDd * identityDd1;
 
-            if (generationInfo.program.getModelType() == storm::prism::Program::ModelType::DTMC) {
+            if (generationInfo.program.getModelType() == storm::prism::Program::ModelType::DTMC || generationInfo.program.getModelType() == storm::prism::Program::ModelType::CTMC) {
                 return ActionDecisionDiagram(action1.guardDd + action2.guardDd, action1Extended + action2Extended, 0);
             } else if (generationInfo.program.getModelType() == storm::prism::Program::ModelType::MDP) {
                 if (action1.transitionsDd.isZero()) {
@@ -432,7 +436,7 @@ namespace storm {
                 }
 
                 return result;
-            } else if (generationInfo.program.getModelType() == storm::prism::Program::ModelType::DTMC) {
+            } else if (generationInfo.program.getModelType() == storm::prism::Program::ModelType::DTMC || generationInfo.program.getModelType() == storm::prism::Program::ModelType::CTMC) {
                 // Simply add all actions.
                 storm::dd::Add<Type> result = module.independentAction.transitionsDd;
                 for (auto const& synchronizingAction : module.synchronizingActionToDecisionDiagramMap) {
@@ -673,6 +677,8 @@ namespace storm {
             
             if (program.getModelType() == storm::prism::Program::ModelType::DTMC) {
                 return std::shared_ptr<storm::models::symbolic::Model<Type>>(new storm::models::symbolic::Dtmc<Type>(generationInfo.manager, reachableStates, initialStates, transitionMatrix, generationInfo.rowMetaVariables, generationInfo.rowExpressionAdapter, generationInfo.columnMetaVariables, generationInfo.columnExpressionAdapter, generationInfo.rowColumnMetaVariablePairs, labelToExpressionMapping, stateAndTransitionRewards ? stateAndTransitionRewards.get().first : boost::optional<storm::dd::Add<Type>>(), stateAndTransitionRewards ? stateAndTransitionRewards.get().second : boost::optional<storm::dd::Add<Type>>()));
+            } else if (program.getModelType() == storm::prism::Program::ModelType::CTMC) {
+                return std::shared_ptr<storm::models::symbolic::Model<Type>>(new storm::models::symbolic::Ctmc<Type>(generationInfo.manager, reachableStates, initialStates, transitionMatrix, generationInfo.rowMetaVariables, generationInfo.rowExpressionAdapter, generationInfo.columnMetaVariables, generationInfo.columnExpressionAdapter, generationInfo.rowColumnMetaVariablePairs, labelToExpressionMapping, stateAndTransitionRewards ? stateAndTransitionRewards.get().first : boost::optional<storm::dd::Add<Type>>(), stateAndTransitionRewards ? stateAndTransitionRewards.get().second : boost::optional<storm::dd::Add<Type>>()));
             } else if (program.getModelType() == storm::prism::Program::ModelType::MDP) {
                 return std::shared_ptr<storm::models::symbolic::Model<Type>>(new storm::models::symbolic::Mdp<Type>(generationInfo.manager, reachableStates, initialStates, transitionMatrix, generationInfo.rowMetaVariables, generationInfo.rowExpressionAdapter, generationInfo.columnMetaVariables, generationInfo.columnExpressionAdapter, generationInfo.rowColumnMetaVariablePairs, generationInfo.allNondeterminismVariables, labelToExpressionMapping, stateAndTransitionRewards ? stateAndTransitionRewards.get().first : boost::optional<storm::dd::Add<Type>>(), stateAndTransitionRewards ? stateAndTransitionRewards.get().second : boost::optional<storm::dd::Add<Type>>()));
             } else {

src/models/symbolic/Ctmc.cpp

@@ -0,0 +1,29 @@
+#include "src/models/symbolic/Ctmc.h"
+
+namespace storm {
+    namespace models {
+        namespace symbolic {
+            
+            template<storm::dd::DdType Type>
+            Ctmc<Type>::Ctmc(std::shared_ptr<storm::dd::DdManager<Type>> manager,
+                             storm::dd::Bdd<Type> reachableStates,
+                             storm::dd::Bdd<Type> initialStates,
+                             storm::dd::Add<Type> transitionMatrix,
+                             std::set<storm::expressions::Variable> const& rowVariables,
+                             std::shared_ptr<storm::adapters::AddExpressionAdapter<Type>> rowExpressionAdapter,
+                             std::set<storm::expressions::Variable> const& columnVariables,
+                             std::shared_ptr<storm::adapters::AddExpressionAdapter<Type>> columnExpressionAdapter,
+                             std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& rowColumnMetaVariablePairs,
+                             std::map<std::string, storm::expressions::Expression> labelToExpressionMap,
+                             boost::optional<storm::dd::Add<Type>> const& optionalStateRewardVector,
+                             boost::optional<storm::dd::Add<Type>> const& optionalTransitionRewardMatrix)
+            : DeterministicModel<Type>(storm::models::ModelType::Ctmc, manager, reachableStates, initialStates, transitionMatrix, rowVariables, rowExpressionAdapter, columnVariables, columnExpressionAdapter, rowColumnMetaVariablePairs, labelToExpressionMap, optionalStateRewardVector, optionalTransitionRewardMatrix) {
+                // Intentionally left empty.
+            }
+            
+            // Explicitly instantiate the template class.
+            template class Ctmc<storm::dd::DdType::CUDD>;
+            
+        } // namespace symbolic
+    } // namespace models
+} // namespace storm

src/models/symbolic/Ctmc.h

@@ -0,0 +1,61 @@
+#ifndef STORM_MODELS_SYMBOLIC_CTMC_H_
+#define STORM_MODELS_SYMBOLIC_CTMC_H_
+
+#include "src/models/symbolic/DeterministicModel.h"
+#include "src/utility/OsDetection.h"
+
+namespace storm {
+    namespace models {
+        namespace symbolic {
+            
+            /*!
+             * This class represents a continuous-time Markov chain.
+             */
+            template<storm::dd::DdType Type>
+            class Ctmc : public DeterministicModel<Type> {
+            public:
+                Ctmc(Ctmc<Type> const& other) = default;
+                Ctmc& operator=(Ctmc<Type> const& other) = default;
+                
+#ifndef WINDOWS
+                Ctmc(Ctmc<Type>&& other) = default;
+                Ctmc& operator=(Ctmc<Type>&& other) = default;
+#endif
+                
+                /*!
+                 * Constructs a model from the given data.
+                 *
+                 * @param manager The manager responsible for the decision diagrams.
+                 * @param reachableStates A DD representing the reachable states.
+                 * @param initialStates A DD representing the initial states of the model.
+                 * @param transitionMatrix The matrix representing the transitions in the model.
+                 * @param rowVariables The set of row meta variables used in the DDs.
+                 * @param rowExpressionAdapter An object that can be used to translate expressions in terms of the row
+                 * meta variables.
+                 * @param columVariables The set of column meta variables used in the DDs.
+                 * @param columnExpressionAdapter An object that can be used to translate expressions in terms of the
+                 * column meta variables.
+                 * @param rowColumnMetaVariablePairs All pairs of row/column meta variables.
+                 * @param labelToExpressionMap A mapping from label names to their defining expressions.
+                 * @param optionalStateRewardVector The reward values associated with the states.
+                 * @param optionalTransitionRewardMatrix The reward values associated with the transitions of the model.
+                 */
+                Ctmc(std::shared_ptr<storm::dd::DdManager<Type>> manager,
+                     storm::dd::Bdd<Type> reachableStates,
+                     storm::dd::Bdd<Type> initialStates,
+                     storm::dd::Add<Type> transitionMatrix,
+                     std::set<storm::expressions::Variable> const& rowVariables,
+                     std::shared_ptr<storm::adapters::AddExpressionAdapter<Type>> rowExpressionAdapter,
+                     std::set<storm::expressions::Variable> const& columnVariables,
+                     std::shared_ptr<storm::adapters::AddExpressionAdapter<Type>> columnExpressionAdapter,
+                     std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& rowColumnMetaVariablePairs,
+                     std::map<std::string, storm::expressions::Expression> labelToExpressionMap = std::map<std::string, storm::expressions::Expression>(),
+                     boost::optional<storm::dd::Add<Type>> const& optionalStateRewardVector = boost::optional<storm::dd::Dd<Type>>(),
+                     boost::optional<storm::dd::Add<Type>> const& optionalTransitionRewardMatrix = boost::optional<storm::dd::Dd<Type>>());
+            };
+            
+        } // namespace symbolic
+    } // namespace models
+} // namespace storm
+
+#endif /* STORM_MODELS_SYMBOLIC_CTMC_H_ */

src/models/symbolic/Model.cpp

@@ -138,7 +138,17 @@ namespace storm {
                 out << "Model type: \t" << this->getType() << " (symbolic)" << std::endl;
                 out << "States: \t" << this->getNumberOfStates() << " (" << reachableStates.getNodeCount() << " nodes)" << std::endl;
                 out << "Transitions: \t" << this->getNumberOfTransitions() << " (" << transitionMatrix.getNodeCount() << " nodes)" << std::endl;
-                out << "Variables: \t" << "rows: " << this->rowVariables.size() << ", columns: " << this->columnVariables.size() << std::endl;
+                
+                uint_fast64_t rowVariableCount = 0;
+                for (auto const& metaVariable : this->rowVariables) {
+                    rowVariableCount += this->getManager().getMetaVariable(metaVariable).getNumberOfDdVariables();
+                }
+                uint_fast64_t columnVariableCount = 0;
+                for (auto const& metaVariable : this->columnVariables) {
+                    columnVariableCount += this->getManager().getMetaVariable(metaVariable).getNumberOfDdVariables();
+                }
+                
+                out << "Variables: \t" << "rows: " << this->rowVariables.size() << "(" << rowVariableCount << " dd variables)" << ", columns: " << this->columnVariables.size() << "(" << columnVariableCount << " dd variables)" << std::endl;
                 out << "Labels: \t" << this->labelToExpressionMap.size() << std::endl;
                 for (auto const& label : labelToExpressionMap) {
                     out << "   * " << label.first << std::endl;