commit to switch workplace

Former-commit-id: da2d6f8af3 [formerly f2157cac64]
Former-commit-id: 1b7b4b6496

src/builder/DdJaniModelBuilder.cpp

@@ -261,7 +261,7 @@ namespace storm {
                 storm::dd::Bdd<Type> globalVariableRanges = result.manager->getBddOne();
                 for (auto const& variable : this->model.getGlobalVariables()) {
                     // Only create the variable if it's non-transient.
-                    if (variable.isTransientVariable()) {
+                    if (variable.isTransient()) {
                         continue;
                     }
                     
@@ -284,7 +284,7 @@ namespace storm {
                     // Then create variables for the variables of the automaton.
                     for (auto const& variable : automaton.getVariables()) {
                         // Only create the variable if it's non-transient.
-                        if (variable.isTransientVariable()) {
+                        if (variable.isTransient()) {
                             continue;
                         }
                         

src/generator/JaniNextStateGenerator.cpp

@@ -11,6 +11,7 @@
 #include "src/utility/solver.h"
 #include "src/exceptions/InvalidSettingsException.h"
 #include "src/exceptions/WrongFormatException.h"
+#include "src/exceptions/InvalidArgumentException.h"
 
 namespace storm {
     namespace generator {
@@ -21,11 +22,38 @@ namespace storm {
         }
         
         template<typename ValueType, typename StateType>
-        JaniNextStateGenerator<ValueType, StateType>::JaniNextStateGenerator(storm::jani::Model const& model, NextStateGeneratorOptions const& options, bool flag) : NextStateGenerator<ValueType, StateType>(model.getExpressionManager(), VariableInformation(model), options), model(model) {
+        JaniNextStateGenerator<ValueType, StateType>::JaniNextStateGenerator(storm::jani::Model const& model, NextStateGeneratorOptions const& options, bool flag) : NextStateGenerator<ValueType, StateType>(model.getExpressionManager(), VariableInformation(model), options), model(model), rewardVariables() {
             STORM_LOG_THROW(model.hasDefaultComposition(), storm::exceptions::WrongFormatException, "The explicit next-state generator currently does not support custom system compositions.");
-            STORM_LOG_THROW(!this->options.isBuildAllRewardModelsSet() && this->options.getRewardModelNames().empty(), storm::exceptions::InvalidSettingsException, "The explicit next-state generator currently does not support building reward models.");
+            STORM_LOG_THROW(!model.hasNonGlobalTransientVariable(), storm::exceptions::InvalidSettingsException, "The explicit next-state generator currently does not support automata-local transient variables.");
             STORM_LOG_THROW(!this->options.isBuildChoiceLabelsSet(), storm::exceptions::InvalidSettingsException, "JANI next-state generator cannot generate choice labels.");
             
+            if (this->options.isBuildAllRewardModelsSet()) {
+                for (auto const& variable : model.getGlobalVariables()) {
+                    if (variable.isTransient()) {
+                        rewardVariables.push_back(variable.getExpressionVariable());
+                    }
+                }
+            } else {
+                // Extract the reward models from the program based on the names we were given.
+                for (auto const& rewardModelName : this->options.getRewardModelNames()) {
+                    auto const& globalVariables = model.getGlobalVariables();
+                    if (globalVariables.hasVariable(rewardModelName)) {
+                        rewardVariables.push_back(globalVariables.getVariable(rewardModelName).getExpressionVariable());
+                    } else {
+                        STORM_LOG_THROW(rewardModelName.empty(), storm::exceptions::InvalidArgumentException, "Cannot build unknown reward model '" << rewardModelName << "'.");
+                        STORM_LOG_THROW(globalVariables.getNumberOfTransientVariables() == 1, storm::exceptions::InvalidArgumentException, "Reference to standard reward model is ambiguous.");
+                        STORM_LOG_THROW(this->program.getNumberOfRewardModels() > 0, storm::exceptions::InvalidArgumentException, "Reference to standard reward model is invalid, because there is no reward model.");
+                    }
+                }
+                
+                // If no reward model was yet added, but there was one that was given in the options, we try to build
+                // standard reward model.
+                if (rewardModels.empty() && !this->options.getRewardModelNames().empty()) {
+                    rewardModels.push_back(this->program.getRewardModel(0));
+                }
+            }
+
+            
             // 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()) {

src/generator/JaniNextStateGenerator.h

@@ -91,6 +91,10 @@ namespace storm {
             
             /// The model used for the generation of next states.
             storm::jani::Model model;
+            
+            // The transient variables of reward models that need to be considered.
+            std::vector<storm::expressions::Variable> rewardVariables;
+
         };
         
     }

src/parser/JaniParser.cpp

@@ -571,7 +571,7 @@ namespace storm {
                     STORM_LOG_THROW(transientValueEntry.count("ref") == 1, storm::exceptions::InvalidJaniException, "Transient values in location " << locName << " need exactly one ref that is assigned to");
                     STORM_LOG_THROW(transientValueEntry.count("value") == 1, storm::exceptions::InvalidJaniException, "Transient values in location " << locName << " need exactly one assigned value");
                     storm::jani::Variable const& lhs = getLValue(transientValueEntry.at("ref"), parentModel.getGlobalVariables(), automaton.getVariables(), "LHS of assignment in location " + locName + " (automaton '" + name + "')");
-                    STORM_LOG_THROW(lhs.isTransientVariable(), storm::exceptions::InvalidJaniException, "Assigned non-transient variable " + lhs.getName() + " in location " + locName + " (automaton: '" + name + "')");
+                    STORM_LOG_THROW(lhs.isTransient(), storm::exceptions::InvalidJaniException, "Assigned non-transient variable " + lhs.getName() + " in location " + locName + " (automaton: '" + name + "')");
                     storm::expressions::Expression rhs = parseExpression(transientValueEntry.at("value"), "Assignment of variable " + lhs.getName() + " in location " + locName + " (automaton: '" + name + "')");
                     transientAssignments.emplace_back(lhs, rhs);
                 }

src/storage/jani/Assignment.cpp

@@ -28,7 +28,7 @@ namespace storm  {
         }
         
         bool Assignment::isTransientAssignment() const {
-            return this->variable.get().isTransientVariable();
+            return this->variable.get().isTransient();
         }
         
         void Assignment::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) {

src/storage/jani/Automaton.cpp

@@ -97,6 +97,10 @@ namespace storm {
             return variables;
         }
         
+        bool Automaton::hasTransientVariable() const {
+            return variables.hasTransientVariable();
+        }
+        
         bool Automaton::hasLocation(std::string const& name) const {
             return locationToIndex.find(name) != locationToIndex.end();
         }

src/storage/jani/Automaton.h

@@ -135,6 +135,11 @@ namespace storm {
              */
             VariableSet const& getVariables() const;
             
+            /*!
+             * Retrieves whether this automaton has a transient variable.
+             */
+            bool hasTransientVariable() const;
+            
             /*!
              * Retrieves whether the automaton has a location with the given name.
              */

src/storage/jani/Model.cpp

@@ -143,6 +143,23 @@ namespace storm {
             return globalVariables;
         }
         
+        bool Model::hasGlobalVariable(std::string const& name) const {
+            return globalVariables.hasVariable(name);
+        }
+        
+        Variable const& Model::getGlobalVariable(std::string const& name) const {
+            return globalVariables.getVariable(name);
+        }
+        
+        bool Model::hasNonGlobalTransientVariable() const {
+            for (auto const& automaton : automata) {
+                if (automaton.hasTransientVariable()) {
+                    return true;
+                }
+            }
+            return false;
+        }
+        
         storm::expressions::ExpressionManager& Model::getExpressionManager() {
             return *expressionManager;
         }

src/storage/jani/Model.h

@@ -141,6 +141,21 @@ namespace storm {
              * Retrieves the variables of this automaton.
              */
             VariableSet const& getGlobalVariables() const;
+
+            /*!
+             * Retrieves whether this model has a global variable with the given name.
+             */
+            bool hasGlobalVariable(std::string const& name) const;
+            
+            /*!
+             * Retrieves the global variable with the given name if one exists.
+             */
+            Variable const& getGlobalVariable(std::string const& name) const;
+            
+            /*!
+             * Retrieves whether this model has a non-global transient variable.
+             */
+            bool hasNonGlobalTransientVariable() const;
             
             /*!
              * Retrieves the manager responsible for the expressions in the JANI model.

src/storage/jani/Variable.cpp

@@ -40,7 +40,7 @@ namespace storm {
             return false;
         }
         
-        bool Variable::isTransientVariable() const {
+        bool Variable::isTransient() const {
             return transient;
         }
 

src/storage/jani/Variable.h

@@ -61,7 +61,7 @@ namespace storm {
             virtual bool isUnboundedIntegerVariable() const;
             virtual bool isRealVariable() const;
 
-            virtual bool isTransientVariable() const;
+            virtual bool isTransient() const;
             
             // Methods to get the variable as a different type.
             BooleanVariable& asBooleanVariable();

src/storage/jani/VariableSet.cpp

@@ -158,6 +158,15 @@ namespace storm {
             return variableToVariable.find(variable) != variableToVariable.end();
         }
         
+        bool VariableSet::hasTransientVariable() const {
+            for (auto const& variable : variables) {
+                if (variable->isTransient()) {
+                    return true;
+                }
+            }
+            return false;
+        }
+        
         bool VariableSet::containsBooleanVariable() const {
             return !booleanVariables.empty();
         }
@@ -176,7 +185,7 @@ namespace storm {
         
         bool VariableSet::containsNonTransientRealVariables() const {
             for (auto const& variable : realVariables) {
-                if (!variable->isTransientVariable()) {
+                if (!variable->isTransient()) {
                     std::cout << "var " << variable->getName() << "is non-transient " << std::endl;
                     return true;
                 }

src/storage/jani/VariableSet.h

@@ -148,6 +148,11 @@ namespace storm {
              */
             Variable const& getVariable(storm::expressions::Variable const& variable) const;
 
+            /*!
+             * Retrieves whether this variable set contains a transient variable.
+             */
+            bool hasTransientVariable() const;
+            
             /*!
              * Retrieves an iterator to the variables in this set.
              */