From 8a8aca006234d557640c0bf8ccf5855fb614455c Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Sat, 10 Sep 2016 11:46:22 +0200
Subject: [PATCH] explicit reward model building for JANI working from cli

Former-commit-id: 22b4dbcdbf8f330a87f0e09ccf89d2fc49b4855e [formerly 4edbdf42075482783112564a9b03936ef5d692ea]
Former-commit-id: e93b8bf1a0d4658afadd11b2b1248cbfe760ccfa
---
 src/generator/JaniNextStateGenerator.cpp | 93 ++++++++++++++++++------
 src/generator/JaniNextStateGenerator.h   | 11 ++-
 src/generator/NextStateGenerator.cpp     | 12 +++
 src/generator/NextStateGenerator.h       |  3 +
 src/storage/SymbolicModelDescription.cpp | 11 +++
 src/storage/SymbolicModelDescription.h   |  2 +
 6 files changed, 108 insertions(+), 24 deletions(-)

diff --git a/src/generator/JaniNextStateGenerator.cpp b/src/generator/JaniNextStateGenerator.cpp
index 859257931..c0ae75160 100644
--- a/src/generator/JaniNextStateGenerator.cpp
+++ b/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
diff --git a/src/generator/JaniNextStateGenerator.h b/src/generator/JaniNextStateGenerator.h
index f3202a569..d9932f60a 100644
--- a/src/generator/JaniNextStateGenerator.h
+++ b/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;
         };
         
     }
diff --git a/src/generator/NextStateGenerator.cpp b/src/generator/NextStateGenerator.cpp
index 9c1eefbd5..fccf7b783 100644
--- a/src/generator/NextStateGenerator.cpp
+++ b/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.
diff --git a/src/generator/NextStateGenerator.h b/src/generator/NextStateGenerator.h
index 30a4157cd..553e7871d 100644
--- a/src/generator/NextStateGenerator.h
+++ b/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;
diff --git a/src/storage/SymbolicModelDescription.cpp b/src/storage/SymbolicModelDescription.cpp
index 8d30575b7..adb1e2afc 100644
--- a/src/storage/SymbolicModelDescription.cpp
+++ b/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);
diff --git a/src/storage/SymbolicModelDescription.h b/src/storage/SymbolicModelDescription.h
index 77da92d82..cd08f9ba0 100644
--- a/src/storage/SymbolicModelDescription.h
+++ b/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: