explicit reward model building for JANI working from cli

Former-commit-id: 22b4dbcdbf [formerly 4edbdf4207]
Former-commit-id: e93b8bf1a0

src/generator/JaniNextStateGenerator.cpp

@@ -53,6 +53,9 @@ namespace storm {
                 }
             }
             
+            // Build the information structs for the reward models.
+            buildRewardModelInformation();
+            
             // If there are terminal states we need to handle, we now need to translate all labels to expressions.
             if (this->options.hasTerminalStates()) {
                 for (auto const& expressionOrLabelAndBool : this->options.getTerminalStates()) {
@@ -309,25 +312,6 @@ namespace storm {
             return result;
         }
         
-        template<typename ValueType, typename StateType>
-        void JaniNextStateGenerator<ValueType, StateType>::performTransientAssignments(storm::jani::detail::ConstAssignments const& transientAssignments, std::function<void (ValueType const&)> const& callback) {
-            auto rewardVariableIt = rewardVariables.begin();
-            auto rewardVariableIte = rewardVariables.end();
-            for (auto const& assignment : transientAssignments) {
-                while (rewardVariableIt != rewardVariableIte && *rewardVariableIt < assignment.getExpressionVariable()) {
-                    callback(storm::utility::zero<ValueType>());
-                    ++rewardVariableIt;
-                }
-                if (rewardVariableIt == rewardVariableIte) {
-                    break;
-                }
-                if (*rewardVariableIt == assignment.getExpressionVariable()) {
-                    callback(ValueType(this->evaluator.asRational(assignment.getAssignedExpression())));
-                    ++rewardVariableIt;
-                }
-            }
-        }
-        
         template<typename ValueType, typename StateType>
         std::vector<Choice<ValueType>> JaniNextStateGenerator<ValueType, StateType>::getSilentActionChoices(std::vector<uint64_t> const& locations, CompressedState const& state, StateToIdCallback stateToIdCallback) {
             std::vector<Choice<ValueType>> result;
@@ -537,13 +521,12 @@ namespace storm {
         
         template<typename ValueType, typename StateType>
         std::size_t JaniNextStateGenerator<ValueType, StateType>::getNumberOfRewardModels() const {
-            return 0;
+            return rewardVariables.size();
         }
         
         template<typename ValueType, typename StateType>
         RewardModelInformation JaniNextStateGenerator<ValueType, StateType>::getRewardModelInformation(uint64_t const& index) const {
-            STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Cannot retrieve reward model information.");
-            return RewardModelInformation("", false, false, false);
+            return rewardModelInformation[index];
         }
         
         template<typename ValueType, typename StateType>
@@ -551,6 +534,72 @@ namespace storm {
             return NextStateGenerator<ValueType, StateType>::label(states, initialStateIndices, deadlockStateIndices, {});
         }
         
+        template<typename ValueType, typename StateType>
+        void JaniNextStateGenerator<ValueType, StateType>::performTransientAssignments(storm::jani::detail::ConstAssignments const& transientAssignments, std::function<void (ValueType const&)> const& callback) {
+            auto rewardVariableIt = rewardVariables.begin();
+            auto rewardVariableIte = rewardVariables.end();
+            for (auto const& assignment : transientAssignments) {
+                while (rewardVariableIt != rewardVariableIte && *rewardVariableIt < assignment.getExpressionVariable()) {
+                    callback(storm::utility::zero<ValueType>());
+                    ++rewardVariableIt;
+                }
+                if (rewardVariableIt == rewardVariableIte) {
+                    break;
+                }
+                if (*rewardVariableIt == assignment.getExpressionVariable()) {
+                    callback(ValueType(this->evaluator.asRational(assignment.getAssignedExpression())));
+                    ++rewardVariableIt;
+                }
+            }
+        }
+        
+        template<typename ValueType, typename StateType>
+        void JaniNextStateGenerator<ValueType, StateType>::buildRewardModelInformation() {
+            // Prepare all reward model information structs.
+            for (auto const& variable : rewardVariables) {
+                rewardModelInformation.emplace_back(variable.getName(), false, false, false);
+            }
+            
+            // Then fill them.
+            for (auto const& automaton : model.getAutomata()) {
+                for (auto const& location : automaton.getLocations()) {
+                    auto rewardVariableIt = rewardVariables.begin();
+                    auto rewardVariableIte = rewardVariables.end();
+                    
+                    for (auto const& assignment : location.getAssignments().getTransientAssignments()) {
+                        while (rewardVariableIt != rewardVariableIte && *rewardVariableIt < assignment.getExpressionVariable()) {
+                            ++rewardVariableIt;
+                        }
+                        if (rewardVariableIt == rewardVariableIte) {
+                            break;
+                        }
+                        if (*rewardVariableIt == assignment.getExpressionVariable()) {
+                            rewardModelInformation[std::distance(rewardVariables.begin(), rewardVariableIt)].setHasStateRewards();
+                            ++rewardVariableIt;
+                        }
+                    }
+                }
+
+                for (auto const& edge : automaton.getEdges()) {
+                    auto rewardVariableIt = rewardVariables.begin();
+                    auto rewardVariableIte = rewardVariables.end();
+                    
+                    for (auto const& assignment : edge.getAssignments().getTransientAssignments()) {
+                        while (rewardVariableIt != rewardVariableIte && *rewardVariableIt < assignment.getExpressionVariable()) {
+                            ++rewardVariableIt;
+                        }
+                        if (rewardVariableIt == rewardVariableIte) {
+                            break;
+                        }
+                        if (*rewardVariableIt == assignment.getExpressionVariable()) {
+                            rewardModelInformation[std::distance(rewardVariables.begin(), rewardVariableIt)].setHasStateActionRewards();
+                            ++rewardVariableIt;
+                        }
+                    }
+                }
+            }
+        }
+        
         template class JaniNextStateGenerator<double>;
 
 #ifdef STORM_HAVE_CARL

src/generator/JaniNextStateGenerator.h

@@ -95,12 +95,19 @@ namespace storm {
              */
             void performTransientAssignments(storm::jani::detail::ConstAssignments const& transientAssignments, std::function<void (ValueType const&)> const& callback);
             
+            /*!
+             * Builds the information structs for the reward models.
+             */
+            void buildRewardModelInformation();
+            
             /// The model used for the generation of next states.
             storm::jani::Model model;
             
-            // The transient variables of reward models that need to be considered.
+            /// The transient variables of reward models that need to be considered.
             std::vector<storm::expressions::Variable> rewardVariables;
             
+            /// A vector storing information about the corresponding reward models (variables).
+            std::vector<RewardModelInformation> rewardModelInformation;
         };
         
     }

src/generator/NextStateGenerator.cpp

@@ -211,6 +211,18 @@ namespace storm {
             return transitionRewards;
         }
         
+        void RewardModelInformation::setHasStateRewards() {
+            stateRewards = true;
+        }
+        
+        void RewardModelInformation::setHasStateActionRewards() {
+            stateActionRewards = true;
+        }
+        
+        void RewardModelInformation::setHasTransitionRewards() {
+            transitionRewards = true;
+        }
+        
         template<typename ValueType, typename StateType>
         NextStateGenerator<ValueType, StateType>::NextStateGenerator(storm::expressions::ExpressionManager const& expressionManager, VariableInformation const& variableInformation, NextStateGeneratorOptions const& options) : options(options), expressionManager(expressionManager.getSharedPointer()), variableInformation(variableInformation), evaluator(expressionManager), state(nullptr) {
             // Intentionally left empty.

src/generator/NextStateGenerator.h

@@ -148,6 +148,9 @@ namespace storm {
             bool hasStateActionRewards() const;
             bool hasTransitionRewards() const;
             
+            void setHasStateRewards();
+            void setHasStateActionRewards();
+            void setHasTransitionRewards();
         private:
             std::string name;
             bool stateRewards;

src/storage/SymbolicModelDescription.cpp

@@ -47,6 +47,17 @@ namespace storm {
             return boost::get<storm::prism::Program>(modelDescription.get());
         }
         
+        void SymbolicModelDescription::toJani(bool makeVariablesGlobal) {
+            if (this->isJaniModel()) {
+                return;
+            }
+            if (this->isPrismProgram()) {
+                modelDescription = this->asPrismProgram().toJani(makeVariablesGlobal);
+            } else {
+                STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Cannot transform model description to the JANI format.");
+            }
+        }
+        
         void SymbolicModelDescription::preprocess(std::string const& constantDefinitionString) {
             if (this->isJaniModel()) {
                 std::map<storm::expressions::Variable, storm::expressions::Expression> substitution = storm::utility::jani::parseConstantDefinitionString(this->asJaniModel(), constantDefinitionString);

src/storage/SymbolicModelDescription.h

@@ -24,6 +24,8 @@ namespace storm {
             storm::jani::Model const& asJaniModel() const;
             storm::prism::Program const& asPrismProgram() const;
             
+            void toJani(bool makeVariablesGlobal = true);
+            
             void preprocess(std::string const& constantDefinitionString = "");
             
         private: