more work on symbolic JANI model building

Former-commit-id: e57913f1a0

src/builder/DdJaniModelBuilder.cpp

@@ -15,6 +15,10 @@
 #include "src/storage/dd/Bdd.h"
 #include "src/adapters/AddExpressionAdapter.h"
 
+#include "src/models/symbolic/Dtmc.h"
+#include "src/models/symbolic/Ctmc.h"
+#include "src/models/symbolic/Mdp.h"
+
 #include "src/utility/macros.h"
 #include "src/utility/jani.h"
 #include "src/exceptions/InvalidArgumentException.h"
@@ -412,8 +416,6 @@ namespace storm {
             return result;
         }
         
-        static int c = 0;
-        
         // A class that is responsible for performing the actual composition.
         template <storm::dd::DdType Type, typename ValueType>
         class AutomatonComposer : public storm::jani::CompositionVisitor {
@@ -704,7 +706,18 @@ namespace storm {
         }
         
         template <storm::dd::DdType Type, typename ValueType>
-        storm::dd::Add<Type, ValueType> createGlobalTransitionRelation(storm::jani::Model const& model, AutomatonDd<Type, ValueType> const& automatonDd, CompositionVariables<Type, ValueType> const& variables) {
+        struct SystemDd {
+            SystemDd(storm::dd::Add<Type, ValueType> const& transitionsDd, storm::dd::Add<Type, ValueType> const& stateActionDd, uint64_t numberOfNondeterminismVariables = 0) : transitionsDd(transitionsDd), stateActionDd(stateActionDd), numberOfNondeterminismVariables(numberOfNondeterminismVariables) {
+                // Intentionally left empty.
+            }
+            
+            storm::dd::Add<Type, ValueType> transitionsDd;
+            storm::dd::Add<Type, ValueType> stateActionDd;
+            uint64_t numberOfNondeterminismVariables;
+        };
+        
+        template <storm::dd::DdType Type, typename ValueType>
+        SystemDd<Type, ValueType> buildSystemDd(storm::jani::Model const& model, AutomatonDd<Type, ValueType> const& automatonDd, CompositionVariables<Type, ValueType> const& variables) {
             // If the model is an MDP, we need to encode the nondeterminism using additional variables.
             if (model.getModelType() == storm::jani::ModelType::MDP) {
                 // Determine how many nondeterminism variables we need.
@@ -735,6 +748,8 @@ namespace storm {
                     
                     result += edgesForAction * encodeAction<Type, ValueType>(actionIndexToVariableIndex.at(action.first), actionVariables, variables);
                 }
+                
+                return SystemDd<Type, ValueType>(result, result.sumAbstract(variables.columnMetaVariables), numberOfNondeterminismVariables);
             } else if (model.getModelType() == storm::jani::ModelType::DTMC || model.getModelType() == storm::jani::ModelType::CTMC) {
                 // Simply add all actions, but make sure to include the missing global variable identities.
                 storm::dd::Add<Type, ValueType> result = variables.manager->template getAddZero<ValueType>();
@@ -743,25 +758,95 @@ namespace storm {
                         result += edge.transitionsDd * computeMissingGlobalVariableIdentities(edge, variables);
                     }
                 }
-                return result;
+                
+                return SystemDd<Type, ValueType>(result, result.sumAbstract(variables.columnMetaVariables));
+            }
+
+            STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Illegal model type.");
+        }
+        
+        template <storm::dd::DdType Type, typename ValueType>
+        struct ModelComponents {
+            storm::dd::Bdd<Type> reachableStates;
+            storm::dd::Bdd<Type> initialStates;
+            storm::dd::Add<Type, ValueType> transitionMatrix;
+            std::unordered_map<std::string, storm::models::symbolic::StandardRewardModel<Type, ValueType>> rewardModels;
+        };
+        
+        template <storm::dd::DdType Type, typename ValueType>
+        std::shared_ptr<storm::models::symbolic::Model<Type, ValueType>> createModel(storm::jani::ModelType const& modelType, CompositionVariables<Type, ValueType> const& variables, ModelComponents<Type, ValueType> const& modelComponents) {
+            if (modelType == storm::jani::ModelType::DTMC) {
+                return std::shared_ptr<storm::models::symbolic::Model<Type, ValueType>>(new storm::models::symbolic::Dtmc<Type, ValueType>(variables.manager, modelComponents.reachableStates, modelComponents.initialStates, modelComponents.transitionMatrix, variables.rowMetaVariables, variables.rowExpressionAdapter, variables.columnMetaVariables, variables.columnExpressionAdapter, variables.rowColumnMetaVariablePairs, std::map<std::string, storm::expressions::Expression>(), modelComponents.rewardModels));
+            } else if (modelType == storm::jani::ModelType::CTMC) {
+                return std::shared_ptr<storm::models::symbolic::Model<Type, ValueType>>(new storm::models::symbolic::Ctmc<Type, ValueType>(variables.manager, modelComponents.reachableStates, modelComponents.initialStates, modelComponents.transitionMatrix, variables.rowMetaVariables, variables.rowExpressionAdapter, variables.columnMetaVariables, variables.columnExpressionAdapter, variables.rowColumnMetaVariablePairs, std::map<std::string, storm::expressions::Expression>(), modelComponents.rewardModels));
+            } else if (modelType == storm::jani::ModelType::MDP) {
+                return std::shared_ptr<storm::models::symbolic::Model<Type, ValueType>>(new storm::models::symbolic::Mdp<Type, ValueType>(variables.manager, modelComponents.reachableStates, modelComponents.initialStates, modelComponents.transitionMatrix, variables.rowMetaVariables, variables.rowExpressionAdapter, variables.columnMetaVariables, variables.columnExpressionAdapter, variables.rowColumnMetaVariablePairs, variables.allNondeterminismVariables, std::map<std::string, storm::expressions::Expression>(), modelComponents.rewardModels));
             } else {
-                STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Illegal model type.");
+                STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Invalid model type.");
             }
-            return storm::dd::Add<Type, ValueType>();
+
+        }
+        
+        template <storm::dd::DdType Type, typename ValueType>
+        void postprocessSystemDd(storm::jani::Model const& model, SystemDd<Type, ValueType>& system, CompositionVariables<Type, ValueType> const& variables, typename DdJaniModelBuilder<Type, ValueType>::Options const& options) {
+            // For DTMCs, we normalize each row to 1 (to account for non-determinism).
+            if (model.getModelType() == storm::jani::ModelType::DTMC) {
+                system.transitionsDd = system.transitionsDd / system.stateActionDd;
+            }
+            
+            
+            // If we were asked to treat some states as terminal states, we cut away their transitions now.
+            if (options.terminalStates || options.negatedTerminalStates) {
+                std::map<storm::expressions::Variable, storm::expressions::Expression> constantsSubstitution = model.getConstantsSubstitution();
+                
+                storm::dd::Bdd<Type> terminalStatesBdd = variables.manager->getBddZero();
+                if (options.terminalStates) {
+                    storm::expressions::Expression terminalExpression = options.terminalStates.get().substitute(constantsSubstitution);
+                    STORM_LOG_TRACE("Making the states satisfying " << terminalExpression << " terminal.");
+                    terminalStatesBdd = variables.rowExpressionAdapter->translateExpression(terminalExpression).toBdd();
+                }
+                if (options.negatedTerminalStates) {
+                    storm::expressions::Expression negatedTerminalExpression = options.negatedTerminalStates.get().substitute(constantsSubstitution);
+                    STORM_LOG_TRACE("Making the states *not* satisfying " << negatedTerminalExpression << " terminal.");
+                    terminalStatesBdd |= !variables.rowExpressionAdapter->translateExpression(negatedTerminalExpression).toBdd();
+                }
+                
+                system.transitionMatrix *= (!terminalStatesBdd).template toAdd<ValueType>();
+            }
+        }
+        
+        template <storm::dd::DdType Type, typename ValueType>
+        storm::dd::Bdd<Type> computeInitial(storm::jani::Model const& model, CompositionVariables<Type, ValueType> const& variables) {
+            storm::dd::Bdd<Type> initialStates = variables.rowExpressionAdapter->translateExpression( generationInfo.program.getInitialConstruct().getInitialStatesExpression()).toBdd();
+            
+            for (auto const& metaVariable : generationInfo.rowMetaVariables) {
+                initialStates &= generationInfo.manager->getRange(metaVariable);
+            }
+            
+            return initialStates;
         }
         
         template <storm::dd::DdType Type, typename ValueType>
         std::shared_ptr<storm::models::symbolic::Model<Type, ValueType>> DdJaniModelBuilder<Type, ValueType>::translate() {
+            // Create all necessary variables.
             CompositionVariableCreator<Type, ValueType> variableCreator(*this->model);
             CompositionVariables<Type, ValueType> variables = variableCreator.create();
             
+            // Compose the automata to a single automaton.
             AutomatonComposer<Type, ValueType> composer(*this->model, variables);
-            AutomatonDd<Type, ValueType> system = composer.compose();
+            AutomatonDd<Type, ValueType> globalAutomaton = composer.compose();
+            
+            // Combine the edges of the single automaton to the full system DD.
+            SystemDd<Type, ValueType> system = buildSystemDd(*this->model, globalAutomaton, variables);
+
+            // Postprocess the system. This modifies the systemDd in place.
+            postprocessSystemDd(*this->model, system, variables, options);
+            
             
-            storm::dd::Add<Type, ValueType> transitions = createGlobalTransitionRelation(*this->model, system, variables);
+            ModelComponents<Type, ValueType> modelComponents;
+    
             
-            // FIXME
-            return nullptr;
+            return createModel(this->model->getModelType(), variables, modelComponents);
         }
         
         template class DdJaniModelBuilder<storm::dd::DdType::CUDD, double>;

src/storage/jani/Automaton.cpp

@@ -180,5 +180,17 @@ namespace storm {
             return edges.size();
         }
 
+        bool Automaton::hasInitialStatesExpression() const {
+            return initialStatesExpression.isInitialized();
+        }
+        
+        storm::expressions::Expression const& Automaton::getInitialStatesExpression() const {
+            return initialStatesExpression;
+        }
+        
+        void Automaton::setInitialStatesExpression(storm::expressions::Expression const& initialStatesExpression) {
+            this->initialStatesExpression = initialStatesExpression;
+        }
+        
     }
 }

src/storage/jani/Automaton.h

@@ -210,6 +210,21 @@ namespace storm {
              */
             uint64_t getNumberOfEdges() const;
 
+            /*!
+             * Retrieves whether there is an expression defining the legal initial values of the automaton's variables.
+             */
+            bool hasInitialStatesExpression() const;
+            
+            /*!
+             * Retrieves the expression defining the legal initial values of the automaton's variables.
+             */
+            storm::expressions::Expression const& getInitialStatesExpression() const;
+            
+            /*!
+             * Sets the expression defining the legal initial values of the automaton's variables.
+             */
+            void setInitialStatesExpression(storm::expressions::Expression const& initialStatesExpression);
+            
         private:
             /// The name of the automaton.
             std::string name;
@@ -232,6 +247,9 @@ namespace storm {
 
             /// The index of the initial location.
             uint64_t initialLocationIndex;
+            
+            // The expression characterizing the legal initial values of the variables of the automaton.
+            storm::expressions::Expression initialStatesExpression;
         };
         
     }

src/storage/jani/BooleanVariable.cpp

@@ -3,7 +3,7 @@
 namespace storm {
     namespace jani {
         
-        BooleanVariable::BooleanVariable(std::string const& name, storm::expressions::Variable const& variable, storm::expressions::Expression const& initialValue) : Variable(name, variable, initialValue) {
+        BooleanVariable::BooleanVariable(std::string const& name, storm::expressions::Variable const& variable) : Variable(name, variable) {
             // Intentionally left empty.
         }
         

src/storage/jani/BooleanVariable.h

@@ -10,7 +10,7 @@ namespace storm {
             /*!
              * Creates a boolean variable.
              */
-            BooleanVariable(std::string const& name, storm::expressions::Variable const& variable, storm::expressions::Expression const& initialValue = storm::expressions::Expression());
+            BooleanVariable(std::string const& name, storm::expressions::Variable const& variable);
             
             virtual bool isBooleanVariable() const;
         };

src/storage/jani/BoundedIntegerVariable.cpp

@@ -3,7 +3,7 @@
 namespace storm {
     namespace jani {
         
-        BoundedIntegerVariable::BoundedIntegerVariable(std::string const& name, storm::expressions::Variable const& variable, storm::expressions::Expression const& lowerBound, storm::expressions::Expression const& upperBound, storm::expressions::Expression const& initialValue) : Variable(name, variable, initialValue), lowerBound(lowerBound), upperBound(upperBound) {
+        BoundedIntegerVariable::BoundedIntegerVariable(std::string const& name, storm::expressions::Variable const& variable, storm::expressions::Expression const& lowerBound, storm::expressions::Expression const& upperBound) : Variable(name, variable), lowerBound(lowerBound), upperBound(upperBound) {
             // Intentionally left empty.
         }
         

src/storage/jani/BoundedIntegerVariable.h

@@ -11,7 +11,7 @@ namespace storm {
             /*!
              * Creates a bounded integer variable.
              */
-            BoundedIntegerVariable(std::string const& name, storm::expressions::Variable const& variable, storm::expressions::Expression const& lowerBound, storm::expressions::Expression const& upperBound, storm::expressions::Expression const& initialValue = storm::expressions::Expression());
+            BoundedIntegerVariable(std::string const& name, storm::expressions::Variable const& variable, storm::expressions::Expression const& lowerBound, storm::expressions::Expression const& upperBound);
             
             /*!
              * Retrieves the expression defining the lower bound of the variable.

src/storage/jani/Model.cpp

@@ -281,24 +281,27 @@ namespace storm {
             }
             
             // Substitute constants in all global variables.
-            for (auto& variable : result.getGlobalVariables()) {
-                variable.setInitialValue(variable.getInitialValue().substitute(constantSubstitution));
-            }
             for (auto& variable : result.getGlobalVariables().getBoundedIntegerVariables()) {
                 variable.setLowerBound(variable.getLowerBound().substitute(constantSubstitution));
                 variable.setUpperBound(variable.getUpperBound().substitute(constantSubstitution));
             }
             
+            // Substitute constants in initial states expression.
+            if (this->hasInitialStatesExpression()) {
+                result.setInitialStatesExpression(this->getInitialStatesExpression().substitute(constantSubstitution));
+            }
+            
             // Substitute constants in variables of automata and their edges.
             for (auto& automaton : result.getAutomata()) {
-                for (auto& variable : automaton.getVariables()) {
-                    variable.setInitialValue(variable.getInitialValue().substitute(constantSubstitution));
-                }
                 for (auto& variable : automaton.getVariables().getBoundedIntegerVariables()) {
                     variable.setLowerBound(variable.getLowerBound().substitute(constantSubstitution));
                     variable.setUpperBound(variable.getUpperBound().substitute(constantSubstitution));
                 }
                 
+                if (automaton.hasInitialStatesExpression()) {
+                    automaton.setInitialStatesExpression(automaton.getInitialStatesExpression().substitute(constantSubstitution));
+                }
+                
                 for (auto& edge : automaton.getEdges()) {
                     edge.setGuard(edge.getGuard().substitute(constantSubstitution));
                     if (edge.hasRate()) {
@@ -316,6 +319,40 @@ namespace storm {
             return result;
         }
         
+        std::map<storm::expressions::Variable, storm::expressions::Expression> Model::getConstantsSubstitution() const {
+            std::map<storm::expressions::Variable, storm::expressions::Expression> result;
+            
+            for (auto const& constant : constants) {
+                if (constant.isDefined()) {
+                    result.emplace(constant.getExpressionVariable(), constant.getExpression());
+                }
+            }
+            
+            return result;
+        }
+        
+        bool Model::hasInitialStatesExpression() const {
+            return initialStatesExpression.isInitialized();
+        }
+     
+        storm::expressions::Expression Model::getInitialStatesExpression(bool includeAutomataInitialStatesExpressions) const {
+            STORM_LOG_THROW(globalVariables.empty() || this->hasInitialStatesExpression(), storm::exceptions::InvalidOperationException, "Cannot retrieve global initial states expression, because there is none.");
+            storm::expressions::Expression result = this->hasInitialStatesExpression() ? initialStatesExpression : expressionManager->boolean(true);
+            if (includeAutomataInitialStatesExpressions) {
+                for (auto const& automaton : automata) {
+                    STORM_LOG_THROW(automaton.getVariables().empty() || automaton.hasInitialStatesExpression(), storm::exceptions::InvalidOperationException, "Cannot retrieve initial states expression from automaton '" << automaton.getName() << "', because there is none.");
+                    if (!automaton.getVariables().empty()) {
+                        result = result && automaton.getInitialStatesExpression();
+                    }
+                }
+            }
+            return result;
+        }
+        
+        void Model::setInitialStatesExpression(storm::expressions::Expression const& initialStatesExpression) {
+            this->initialStatesExpression = initialStatesExpression;
+        }
+        
         bool Model::checkValidity(bool logdbg) const {
             // TODO switch to exception based return value.
             

src/storage/jani/Model.h

@@ -219,6 +219,30 @@ namespace storm {
              */
             Model substituteConstants() const;
             
+            /*!
+             * Retrieves a mapping from expression variables associated with defined constants of the model to their
+             * (the constants') defining expression.
+             */
+            std::map<storm::expressions::Variable, storm::expressions::Expression> getConstantsSubstitution() const;
+            
+            /*!
+             * Retrieves whether there is an expression defining the legal initial values of the global variables.
+             */
+            bool hasInitialStatesExpression() const;
+            
+            /*!
+             * Retrieves the expression defining the legal initial values of the variables.
+             *
+             * @param includeAutomataInitialStatesExpressions If set to true, the expression defines the legal initial
+             * states not only for the global variables but also for the variables of each automaton.
+             */
+            storm::expressions::Expression getInitialStatesExpression(bool includeAutomataInitialStatesExpressions = false) const;
+            
+            /*!
+             * Sets the expression defining the legal initial values of the global variables.
+             */
+            void setInitialStatesExpression(storm::expressions::Expression const& initialStatesExpression);
+            
             /*!
              *  Checks if the model is valid JANI, which should be verified before any further operations are applied to a model.
              */
@@ -263,6 +287,9 @@ namespace storm {
             
             /// An expression describing how the system is composed of the automata.
             std::shared_ptr<Composition> composition;
+            
+            // The expression characterizing the legal initial values of the global variables.
+            storm::expressions::Expression initialStatesExpression;
         };
     }
 }

src/storage/jani/UnboundedIntegerVariable.cpp

@@ -3,7 +3,7 @@
 namespace storm {
     namespace jani {
         
-        UnboundedIntegerVariable::UnboundedIntegerVariable(std::string const& name, storm::expressions::Variable const& variable, storm::expressions::Expression const& initialValue) : Variable(name, variable, initialValue) {
+        UnboundedIntegerVariable::UnboundedIntegerVariable(std::string const& name, storm::expressions::Variable const& variable) : Variable(name, variable) {
             // Intentionally left empty.
         }
         

src/storage/jani/UnboundedIntegerVariable.h

@@ -10,7 +10,7 @@ namespace storm {
             /*!
              * Creates an unbounded integer variable.
              */
-            UnboundedIntegerVariable(std::string const& name, storm::expressions::Variable const& variable, storm::expressions::Expression const& initialValue = storm::expressions::Expression());
+            UnboundedIntegerVariable(std::string const& name, storm::expressions::Variable const& variable);
             
             virtual bool isUnboundedIntegerVariable() const override;
         };

src/storage/jani/Variable.cpp

@@ -7,7 +7,7 @@
 namespace storm {
     namespace jani {
         
-        Variable::Variable(std::string const& name, storm::expressions::Variable const& variable, storm::expressions::Expression const& initialValue) : name(name), variable(variable), initialValue(initialValue) {
+        Variable::Variable(std::string const& name, storm::expressions::Variable const& variable) : name(name), variable(variable) {
             // Intentionally left empty.
         }
         
@@ -15,22 +15,10 @@ namespace storm {
             return variable;
         }
 
-        bool Variable::hasInitialValue() const {
-            return initialValue.isInitialized();
-        }
-        
         std::string const& Variable::getName() const {
             return name;
         }
         
-        storm::expressions::Expression const& Variable::getInitialValue() const {
-            return initialValue;
-        }
-        
-        void Variable::setInitialValue(storm::expressions::Expression const& initialValue) {
-            this->initialValue = initialValue;
-        }
-        
         bool Variable::isBooleanVariable() const {
             return false;
         }

src/storage/jani/Variable.h

@@ -18,7 +18,7 @@ namespace storm {
             /*!
              * Creates a new variable.
              */
-            Variable(std::string const& name, storm::expressions::Variable const& variable, storm::expressions::Expression const& initialValue);
+            Variable(std::string const& name, storm::expressions::Variable const& variable);
             
             /*!
              * Retrieves the associated expression variable
@@ -29,22 +29,7 @@ namespace storm {
              * Retrieves the name of the variable.
              */
             std::string const& getName() const;
-            
-            /*!
-             * Retrieves the initial value of the variable.
-             */
-            storm::expressions::Expression const& getInitialValue() const;
-            
-            /*!
-             * Sets a new value as the initial value of the variable.
-             */
-            void setInitialValue(storm::expressions::Expression const& initialValue);
-            
-            /*!
-             * Retrieves whether the variable has an initial value.
-             */
-            bool hasInitialValue() const;
-            
+                        
             // Methods to determine the type of the variable.
             virtual bool isBooleanVariable() const;
             virtual bool isBoundedIntegerVariable() const;
@@ -64,9 +49,6 @@ namespace storm {
             
             // The expression variable associated with this variable.
             storm::expressions::Variable variable;
-            
-            // The expression defining the initial value of the variable.
-            storm::expressions::Expression initialValue;
         };
         
     }

src/storage/jani/VariableSet.cpp

@@ -149,6 +149,10 @@ namespace storm {
             return !unboundedIntegerVariables.empty();
         }
         
+        bool VariableSet::empty() const {
+            return !(containsBooleanVariable() || containsBoundedIntegerVariable() || containsUnboundedIntegerVariables());
+        }
+        
         template class detail::Dereferencer<Variable>;
         template class detail::Dereferencer<BooleanVariable>;
         template class detail::Dereferencer<BoundedIntegerVariable>;

src/storage/jani/VariableSet.h

@@ -167,6 +167,11 @@ namespace storm {
              */
             bool containsUnboundedIntegerVariables() const;
 
+            /*!
+             * Retrieves whether this variable set is empty.
+             */
+            bool empty() const;
+            
         private:
             /// The vector of all variables.
             std::vector<std::shared_ptr<Variable>> variables;