first version of rewards for JANI models (explicit next-state generator only)

Former-commit-id: b2b0638427 [formerly c763581e06]
Former-commit-id: a032da1cff

src/adapters/DereferenceIteratorAdapter.h

@@ -25,11 +25,11 @@ namespace storm {
                 // Intentionally left empty.
             }
             
-            iterator begin() {
+            iterator begin() const {
                 return boost::make_transform_iterator(it, Dereferencer<value_type>());
             }
             
-            iterator end() {
+            iterator end() const {
                 return boost::make_transform_iterator(ite, Dereferencer<value_type>());
             }
             

src/generator/JaniNextStateGenerator.cpp

@@ -52,7 +52,6 @@ namespace storm {
                     rewardVariables.push_back(globalVariables.getTransientVariables().front()->getExpressionVariable());
                 }
             }
-
             
             // If there are terminal states we need to handle, we now need to translate all labels to expressions.
             if (this->options.hasTerminalStates()) {
@@ -202,11 +201,6 @@ namespace storm {
         CompressedState JaniNextStateGenerator<ValueType, StateType>::applyUpdate(CompressedState const& state, storm::jani::EdgeDestination const& destination) {
             CompressedState newState(state);
             
-            // NOTE: the following process assumes that the assignments of the destination are ordered in such a way
-            // that the assignments to boolean variables precede the assignments to all integer variables and that
-            // within the types, the assignments to variables are ordered (in ascending order) by the expression variables.
-            // This is guaranteed for JANI models, by sorting the assignments as soon as an edge destination is created.
-            
             auto assignmentIt = destination.getNonTransientAssignments().begin();
             auto assignmentIte = destination.getNonTransientAssignments().end();
             
@@ -242,6 +236,22 @@ namespace storm {
             // Prepare the result, in case we return early.
             StateBehavior<ValueType, StateType> result;
             
+            // Retrieve the locations from the state.
+            std::vector<uint64_t> locations = getLocations(*this->state);
+
+            // First, construct the state rewards, as we may return early if there are no choices later and we already
+            // need the state rewards then.
+            std::vector<ValueType> stateRewards(this->rewardVariables.size(), storm::utility::zero<ValueType>());
+            uint64_t automatonIndex = 0;
+            for (auto const& automaton : model.getAutomata()) {
+                uint64_t currentLocationIndex = locations[automatonIndex];
+                storm::jani::Location const& location = automaton.getLocation(currentLocationIndex);
+                auto valueIt = stateRewards.begin();
+                performTransientAssignments(location.getAssignments().getTransientAssignments(), [&valueIt] (ValueType const& value) { *valueIt += value; ++valueIt; } );
+                ++automatonIndex;
+            }
+            result.addStateRewards(std::move(stateRewards));
+            
             // If a terminal expression was set and we must not expand this state, return now.
             if (!this->terminalStates.empty()) {
                 for (auto const& expressionBool : this->terminalStates) {
@@ -251,9 +261,6 @@ namespace storm {
                 }
             }
             
-            // Retrieve the locations from the state.
-            std::vector<uint64_t> locations = getLocations(*this->state);
-            
             // Get all choices for the state.
             std::vector<Choice<ValueType>> allChoices = getSilentActionChoices(locations, *this->state, stateToIdCallback);
             std::vector<Choice<ValueType>> allLabeledChoices = getNonsilentActionChoices(locations, *this->state, stateToIdCallback);
@@ -302,6 +309,25 @@ 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;
@@ -339,6 +365,9 @@ namespace storm {
                         probabilitySum += probability;
                     }
                     
+                    // Create the state-action reward for the newly created choice.
+                    performTransientAssignments(edge.getAssignments().getTransientAssignments(), [&choice] (ValueType const& value) { choice.addChoiceReward(value); } );
+
                     // Check that the resulting distribution is in fact a distribution.
                     STORM_LOG_THROW(!this->isDiscreteTimeModel() || this->comparator.isOne(probabilitySum), storm::exceptions::WrongFormatException, "Probabilities do not sum to one for edge (actually sum to " << probabilitySum << ").");
                 }

src/generator/JaniNextStateGenerator.h

@@ -89,6 +89,12 @@ namespace storm {
              */
             void checkGlobalVariableWritesValid(std::vector<std::vector<storm::jani::Edge const*>> const& enabledEdges) const;
             
+            /*!
+             * Treats the given transient assignments by calling the callback function whenever a transient assignment
+             * to one of the reward variables of this generator is performed.
+             */
+            void performTransientAssignments(storm::jani::detail::ConstAssignments const& transientAssignments, std::function<void (ValueType const&)> const& callback);
+            
             /// The model used for the generation of next states.
             storm::jani::Model model;
             

src/generator/StateBehavior.cpp

@@ -20,6 +20,11 @@ namespace storm {
             stateRewards.push_back(stateReward);
         }
         
+        template<typename ValueType, typename StateType>
+        void StateBehavior<ValueType, StateType>::addStateRewards(std::vector<ValueType>&& stateRewards) {
+            this->stateRewards = std::move(stateRewards);
+        }
+        
         template<typename ValueType, typename StateType>
         void StateBehavior<ValueType, StateType>::setExpanded(bool newValue) {
             this->expanded = newValue;

src/generator/StateBehavior.h

@@ -25,7 +25,12 @@ namespace storm {
              * Adds the given state reward to the behavior of the state.
              */
             void addStateReward(ValueType const& stateReward);
-            
+
+            /*!
+             * Adds the given state rewards to the behavior of the state.
+             */
+            void addStateRewards(std::vector<ValueType>&& stateRewards);
+
             /*!
              * Sets whether the state was expanded.
              */

src/storage/SymbolicModelDescription.cpp

@@ -0,0 +1,9 @@
+//
+//  SymbolicModelDescription.cpp
+//  storm
+//
+//  Created by Christian Dehnert on 09/09/16.
+//
+//
+
+#include "SymbolicModelDescription.hpp"

src/storage/SymbolicModelDescription.h

@@ -0,0 +1,14 @@
+//
+//  SymbolicModelDescription.hpp
+//  storm
+//
+//  Created by Christian Dehnert on 09/09/16.
+//
+//
+
+#ifndef SymbolicModelDescription_hpp
+#define SymbolicModelDescription_hpp
+
+#include <stdio.h>
+
+#endif /* SymbolicModelDescription_hpp */

src/storage/jani/Edge.cpp

@@ -8,7 +8,7 @@
 namespace storm {
     namespace jani {
         
-        Edge::Edge(uint64_t sourceLocationIndex, uint64_t actionIndex, boost::optional<storm::expressions::Expression> const& rate, storm::expressions::Expression const& guard, std::vector<EdgeDestination> destinations) : sourceLocationIndex(sourceLocationIndex), actionIndex(actionIndex), rate(rate), guard(guard), destinations(destinations) {
+        Edge::Edge(uint64_t sourceLocationIndex, uint64_t actionIndex, boost::optional<storm::expressions::Expression> const& rate, storm::expressions::Expression const& guard, std::vector<EdgeDestination> destinations) : sourceLocationIndex(sourceLocationIndex), actionIndex(actionIndex), rate(rate), guard(guard), destinations(destinations), assignments(), writtenGlobalVariables() {
             // Intentionally left empty.
         }
         
@@ -52,8 +52,8 @@ namespace storm {
             destinations.push_back(destination);
         }
         
-        OrderedAssignments const& Edge::getTransientAssignments() const {
-            return transientAssignments;
+        OrderedAssignments const& Edge::getAssignments() const {
+            return assignments;
         }
         
         void Edge::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) {
@@ -61,7 +61,7 @@ namespace storm {
             if (this->hasRate()) {
                 this->setRate(this->getRate().substitute(substitution));
             }
-            for (auto& assignment : this->getTransientAssignments()) {
+            for (auto& assignment : this->getAssignments()) {
                 assignment.substitute(substitution);
             }
             for (auto& destination : this->getDestinations()) {
@@ -81,7 +81,7 @@ namespace storm {
         
         bool Edge::addTransientAssignment(Assignment const& assignment) {
             STORM_LOG_THROW(assignment.isTransient(), storm::exceptions::InvalidArgumentException, "Must not add non-transient assignment to location.");
-            return transientAssignments.add(assignment);
+            return assignments.add(assignment);
         }
         
         void Edge::liftTransientDestinationAssignments() {

src/storage/jani/Edge.h

@@ -91,9 +91,9 @@ namespace storm {
             bool addTransientAssignment(Assignment const& assignment);
             
             /*!
-             * Retrieves the transient assignments of this edge.
+             * Retrieves the assignments of this edge.
              */
-            OrderedAssignments const& getTransientAssignments() const;
+            OrderedAssignments const& getAssignments() const;
 
             /*!
              * Finds the transient assignments common to all destinations and lifts them to the edge. Afterwards, these
@@ -118,8 +118,8 @@ namespace storm {
             /// The destinations of this edge.
             std::vector<EdgeDestination> destinations;
             
-            /// The transient assignments made when taking this edge.
-            OrderedAssignments transientAssignments;
+            /// The assignments made when taking this edge.
+            OrderedAssignments assignments;
             
             /// A set of global variables that is written by at least one of the edge's destinations. This set is
             /// initialized by the call to <code>finalize</code>.

src/storage/jani/Location.cpp

@@ -7,7 +7,7 @@
 namespace storm {
     namespace jani {
         
-        Location::Location(std::string const& name, std::vector<Assignment> const& transientAssignments) : name(name), transientAssignments(transientAssignments) {
+        Location::Location(std::string const& name, std::vector<Assignment> const& transientAssignments) : name(name), assignments(transientAssignments) {
             // Intentionally left empty.
         }
         
@@ -15,13 +15,13 @@ namespace storm {
             return name;
         }
         
-        OrderedAssignments const& Location::getTransientAssignments() const {
-            return transientAssignments;
+        OrderedAssignments const& Location::getAssignments() const {
+            return assignments;
         }
         
         void Location::addTransientAssignment(storm::jani::Assignment const& assignment) {
             STORM_LOG_THROW(assignment.isTransient(), storm::exceptions::InvalidArgumentException, "Must not add non-transient assignment to location.");
-            transientAssignments.add(assignment);
+            assignments.add(assignment);
         }
         
         void Location::checkValid() const {

src/storage/jani/Location.h

@@ -25,9 +25,9 @@ namespace storm {
             std::string const& getName() const;
             
             /*!
-             * Retrieves the transient assignments of this location.
+             * Retrieves the assignments of this location.
              */
-            OrderedAssignments const& getTransientAssignments() const;
+            OrderedAssignments const& getAssignments() const;
             
             /*!
              * Adds the given transient assignment to this location.
@@ -44,7 +44,7 @@ namespace storm {
             std::string name;
             
             /// The transient assignments made in this location.
-            OrderedAssignments transientAssignments;
+            OrderedAssignments assignments;
         };
         
     }