real transient variables and assignments are now added in PRISM to JANI transformation

Former-commit-id: 45ccd46071 [formerly a8d1de9c6a]
Former-commit-id: 6aa6dbae52

src/builder/DdJaniModelBuilder.cpp

@@ -188,11 +188,15 @@ namespace storm {
                 this->model.getSystemComposition().accept(*this, boost::none);
                 STORM_LOG_THROW(automata.size() == this->model.getNumberOfAutomata(), storm::exceptions::InvalidArgumentException, "Cannot build symbolic model from JANI model whose system composition refers to a subset of automata.");
                 
-                // Then, check that the model does not contain unbounded integer variables.
+                // Then, check that the model does not contain unbounded integer or non-transient real variables.
                 STORM_LOG_THROW(!this->model.getGlobalVariables().containsUnboundedIntegerVariables(), storm::exceptions::InvalidArgumentException, "Cannot build symbolic model from JANI model that contains global unbounded integer variables.");
                 for (auto const& automaton : this->model.getAutomata()) {
                     STORM_LOG_THROW(!automaton.getVariables().containsUnboundedIntegerVariables(), storm::exceptions::InvalidArgumentException, "Cannot build symbolic model from JANI model that contains unbounded integer variables in automaton '" << automaton.getName() << "'.");
                 }
+                STORM_LOG_THROW(!this->model.getGlobalVariables().containsNonTransientRealVariables(), storm::exceptions::InvalidArgumentException, "Cannot build symbolic model from JANI model that contains global non-transient real variables.");
+                for (auto const& automaton : this->model.getAutomata()) {
+                    STORM_LOG_THROW(!automaton.getVariables().containsNonTransientRealVariables(), storm::exceptions::InvalidArgumentException, "Cannot build symbolic model from JANI model that contains non-transient real variables in automaton '" << automaton.getName() << "'.");
+                }
                 
                 // Based on this assumption, we create the variables.
                 return createVariables();
@@ -256,6 +260,11 @@ namespace storm {
                 // Create global variables.
                 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()) {
+                        continue;
+                    }
+                    
                     createVariable(variable, result);
                     globalVariableRanges &= result.manager->getRange(result.variableToRowMetaVariableMap->at(variable.getExpressionVariable()));
                 }
@@ -274,6 +283,11 @@ 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()) {
+                            continue;
+                        }
+                        
                         createVariable(variable, result);
                         identity &= result.variableToIdentityMap.at(variable.getExpressionVariable()).toBdd();
                         range &= result.manager->getRange(result.variableToRowMetaVariableMap->at(variable.getExpressionVariable()));
@@ -391,7 +405,7 @@ namespace storm {
             
             // Iterate over all assignments (boolean and integer) and build the DD for it.
             std::set<storm::expressions::Variable> assignedVariables;
-            for (auto const& assignment : destination.getAssignments()) {
+            for (auto const& assignment : destination.getNonTransientAssignments()) {
                 // Record the variable as being written.
                 STORM_LOG_TRACE("Assigning to variable " << variables.variableToRowMetaVariableMap->at(assignment.getExpressionVariable()).getName());
                 assignedVariables.insert(assignment.getExpressionVariable());

src/generator/JaniNextStateGenerator.cpp

@@ -179,8 +179,8 @@ namespace storm {
             // 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.getAssignments().begin();
-            auto assignmentIte = destination.getAssignments().end();
+            auto assignmentIt = destination.getNonTransientAssignments().begin();
+            auto assignmentIte = destination.getNonTransientAssignments().end();
             
             // Iterate over all boolean assignments and carry them out.
             auto boolIt = this->variableInformation.booleanVariables.begin();

src/storage/jani/Assignment.cpp

@@ -31,6 +31,10 @@ namespace storm  {
             return this->variable.get().isTransientVariable();
         }
         
+        void Assignment::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) {
+            this->setAssignedExpression(this->getAssignedExpression().substitute(substitution));
+        }
+        
         std::ostream& operator<<(std::ostream& stream, Assignment const& assignment) {
             stream << assignment.getVariable().getName() << " := " << assignment.getAssignedExpression();
             return stream;

src/storage/jani/Assignment.h

@@ -37,6 +37,11 @@ namespace storm {
              */
             void setAssignedExpression(storm::expressions::Expression const& expression);
 
+            /*!
+             * Substitutes all variables in all expressions according to the given substitution.
+             */
+            void substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution);
+            
             /**
              * Retrieves whether the assignment assigns to a transient variable.
              */

src/storage/jani/Automaton.cpp

@@ -108,7 +108,11 @@ namespace storm {
         Location const& Automaton::getLocation(uint64_t index) const {
             return locations[index];
         }
-        
+
+        Location& Automaton::getLocation(uint64_t index) {
+            return locations[index];
+        }
+
         uint64_t Automaton::addLocation(Location const& location) {
             STORM_LOG_THROW(!this->hasLocation(location.getName()), storm::exceptions::WrongFormatException, "Cannot add location with name '" << location.getName() << "', because a location with this name already exists.");
             locationToIndex.emplace(location.getName(), locations.size());
@@ -358,6 +362,18 @@ namespace storm {
             return result;
         }
         
+        void Automaton::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) {
+            for (auto& variable : this->getVariables().getBoundedIntegerVariables()) {
+                variable.substitute(substitution);
+            }
+            
+            this->setInitialStatesRestriction(this->getInitialStatesRestriction().substitute(substitution));
+            
+            for (auto& edge : this->getEdges()) {
+                edge.substitute(substitution);
+            }
+        }
+        
         void Automaton::finalize(Model const& containingModel) {
             for (auto& edge : edges) {
                 edge.finalize(containingModel);

src/storage/jani/Automaton.h

@@ -158,6 +158,11 @@ namespace storm {
              */
             Location const& getLocation(uint64_t index) const;
             
+            /*!
+             * Retrieves the location with the given index.
+             */
+            Location& getLocation(uint64_t index);
+            
             /*!
              * Adds the given location to the automaton.
              */
@@ -268,6 +273,11 @@ namespace storm {
              */
             std::vector<storm::expressions::Expression> getAllRangeExpressions() const;
             
+            /*!
+             * Substitutes all variables in all expressions according to the given substitution.
+             */
+            void substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution);
+            
             /*!
              * Finalizes the building of this automaton. Subsequent changes to the automaton require another call to this
              * method. Note that this method is invoked by a call to <code>finalize</code> to the containing model.

src/storage/jani/BoundedIntegerVariable.cpp

@@ -21,7 +21,6 @@ namespace storm {
             // Intentionally left empty.
         }
 
-
         storm::expressions::Expression const& BoundedIntegerVariable::getLowerBound() const {
             return lowerBound;
         }
@@ -46,6 +45,12 @@ namespace storm {
             return true;
         }
         
+        void BoundedIntegerVariable::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) {
+            Variable::substitute(substitution);
+            this->setLowerBound(this->getLowerBound().substitute(substitution));
+            this->setUpperBound(this->getUpperBound().substitute(substitution));
+        }
+        
         std::shared_ptr<BoundedIntegerVariable> makeBoundedIntegerVariable(std::string const& name, storm::expressions::Variable const& variable, boost::optional<storm::expressions::Expression> initValue, bool transient, boost::optional<storm::expressions::Expression> lowerBound, boost::optional<storm::expressions::Expression> upperBound) {
             STORM_LOG_THROW(lowerBound && upperBound, storm::exceptions::NotImplementedException, "Jani Bounded Integer variables (for now) have to be bounded from both sides");
             if (initValue) {

src/storage/jani/BoundedIntegerVariable.h

@@ -52,6 +52,11 @@ namespace storm {
             
             virtual bool isBoundedIntegerVariable() const override;
 
+            /*!
+             * Substitutes all variables in all expressions according to the given substitution.
+             */
+            virtual void substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) override;
+            
         private:
             // The expression defining the lower bound of the variable.
             storm::expressions::Expression lowerBound;

src/storage/jani/Edge.cpp

@@ -49,6 +49,27 @@ namespace storm {
             destinations.push_back(destination);
         }
         
+        std::vector<Assignment>& Edge::getTransientAssignments() {
+            return transientAssignments;
+        }
+        
+        std::vector<Assignment> const& Edge::getTransientAssignments() const {
+            return transientAssignments;
+        }
+        
+        void Edge::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) {
+            this->setGuard(this->getGuard().substitute(substitution));
+            if (this->hasRate()) {
+                this->setRate(this->getRate().substitute(substitution));
+            }
+            for (auto& assignment : this->getTransientAssignments()) {
+                assignment.substitute(substitution);
+            }
+            for (auto& destination : this->getDestinations()) {
+                destination.substitute(substitution);
+            }
+        }
+        
         void Edge::finalize(Model const& containingModel) {
             for (auto const& destination : getDestinations()) {
                 for (auto const& assignment : destination.getAssignments()) {

src/storage/jani/Edge.h

@@ -64,6 +64,21 @@ namespace storm {
              */
             void addDestination(EdgeDestination const& destination);
             
+            /*!
+             * Retrieves the transient assignments of this edge.
+             */
+            std::vector<Assignment>& getTransientAssignments();
+            
+            /*!
+             * Retrieves the transient assignments of this edge.
+             */
+            std::vector<Assignment> const& getTransientAssignments() const;
+            
+            /*!
+             * Substitutes all variables in all expressions according to the given substitution.
+             */
+            void substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution);
+            
             /*!
              * Finalizes the building of this edge. Subsequent changes to the edge require another call to this
              * method. Note that this method is invoked by a call to <code>finalize</code> to the containing model.

src/storage/jani/EdgeDestination.cpp

@@ -72,6 +72,19 @@ namespace storm {
             return transientAssignments;
         }
         
+        void EdgeDestination::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) {
+            this->setProbability(this->getProbability().substitute(substitution));
+            for (auto& assignment : this->getAssignments()) {
+                assignment.substitute(substitution);
+            }
+            for (auto& assignment : this->getTransientAssignments()) {
+                assignment.substitute(substitution);
+            }
+            for (auto& assignment : this->getNonTransientAssignments()) {
+                assignment.substitute(substitution);
+            }
+        }
+        
         bool EdgeDestination::hasAssignment(Assignment const& assignment) const {
             for (auto const& containedAssignment : assignments) {
                 if (containedAssignment == assignment) {

src/storage/jani/EdgeDestination.h

@@ -66,6 +66,11 @@ namespace storm {
              */
             std::vector<Assignment> const& getTransientAssignments() const;
 
+            /*!
+             * Substitutes all variables in all expressions according to the given substitution.
+             */
+            void substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution);
+            
             /*!
              * Retrieves whether this assignment is made when choosing this destination.
              *

src/storage/jani/Location.cpp

@@ -18,6 +18,10 @@ namespace storm {
             return transientAssignments;
         }
         
+        void Location::addTransientAssignment(storm::jani::Assignment const& assignment) {
+            transientAssignments.push_back(assignment);
+        }
+        
         void Location::checkValid() const {
             for(auto const& assignment : transientAssignments) {
                 STORM_LOG_THROW(assignment.isTransientAssignment(), storm::exceptions::InvalidJaniException, "Only transient assignments are allowed in locations.");

src/storage/jani/Location.h

@@ -29,6 +29,11 @@ namespace storm {
              */
             std::vector<Assignment> const& getTransientAssignments() const;
             
+            /*!
+             * Adds the given transient assignment to this location.
+             */
+            void addTransientAssignment(storm::jani::Assignment const& assignment);
+            
             /*!
              * Checks whether the location is valid, that is, whether the assignments are indeed all transient assignments.
              */

src/storage/jani/Model.cpp

@@ -310,9 +310,7 @@ namespace storm {
             
             // Substitute constants in all global variables.
             for (auto& variable : result.getGlobalVariables().getBoundedIntegerVariables()) {
-                variable.setInitExpression(variable.getInitExpression().substitute(constantSubstitution));
-                variable.setLowerBound(variable.getLowerBound().substitute(constantSubstitution));
-                variable.setUpperBound(variable.getUpperBound().substitute(constantSubstitution));
+                variable.substitute(constantSubstitution);
             }
             
             // Substitute constants in initial states expression.
@@ -320,26 +318,7 @@ namespace storm {
             
             // Substitute constants in variables of automata and their edges.
             for (auto& automaton : result.getAutomata()) {
-                for (auto& variable : automaton.getVariables().getBoundedIntegerVariables()) {
-                    variable.setInitExpression(variable.getInitExpression().substitute(constantSubstitution));
-                    variable.setLowerBound(variable.getLowerBound().substitute(constantSubstitution));
-                    variable.setUpperBound(variable.getUpperBound().substitute(constantSubstitution));
-                }
-                
-                automaton.setInitialStatesRestriction(automaton.getInitialStatesExpression().substitute(constantSubstitution));
-                
-                for (auto& edge : automaton.getEdges()) {
-                    edge.setGuard(edge.getGuard().substitute(constantSubstitution));
-                    if (edge.hasRate()) {
-                        edge.setRate(edge.getRate().substitute(constantSubstitution));
-                    }
-                    for (auto& destination : edge.getDestinations()) {
-                        destination.setProbability(destination.getProbability().substitute(constantSubstitution));
-                        for (auto& assignment : destination.getAssignments()) {
-                            assignment.setAssignedExpression(assignment.getAssignedExpression().substitute(constantSubstitution));
-                        }
-                    }
-                }
+                automaton.substitute(constantSubstitution);
             }
             
             return result;

src/storage/jani/Variable.cpp

@@ -16,7 +16,6 @@ namespace storm {
             // Intentionally left empty.
         }
 
-
         storm::expressions::Variable const& Variable::getExpressionVariable() const {
             return variable;
         }
@@ -89,5 +88,11 @@ namespace storm {
             return static_cast<RealVariable const&>(*this);
         }
         
+        void Variable::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) {
+            if (this->hasInitExpression()) {
+                this->setInitExpression(this->getInitExpression().substitute(substitution));
+            }
+        }
+        
     }
 }

src/storage/jani/Variable.h

@@ -73,6 +73,11 @@ namespace storm {
             RealVariable& asRealVariable();
             RealVariable const& asRealVariable() const;
             
+            /*!
+             * Substitutes all variables in all expressions according to the given substitution.
+             */
+            virtual void substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution);
+            
         private:
             // The name of the variable.
             std::string name;

src/storage/jani/VariableSet.cpp

@@ -174,6 +174,16 @@ namespace storm {
             return !realVariables.empty();
         }
         
+        bool VariableSet::containsNonTransientRealVariables() const {
+            for (auto const& variable : realVariables) {
+                if (!variable->isTransientVariable()) {
+                    std::cout << "var " << variable->getName() << "is non-transient " << std::endl;
+                    return true;
+                }
+            }
+            return false;
+        }
+        
         bool VariableSet::empty() const {
             return !(containsBooleanVariable() || containsBoundedIntegerVariable() || containsUnboundedIntegerVariables());
         }

src/storage/jani/VariableSet.h

@@ -184,10 +184,15 @@ namespace storm {
             bool containsUnboundedIntegerVariables() const;
 
             /*!
-             * Retrieves whether the set of variables contains an unbounded integer variable.
+             * Retrieves whether the set of variables contains a real variable.
              */
             bool containsRealVariables() const;
 
+            /*!
+             * Retrieves whether the set of variables contains a non-transient real variable.
+             */
+            bool containsNonTransientRealVariables() const;
+            
             /*!
              * Retrieves whether this variable set is empty.
              */

src/storage/prism/ToJaniConverter.cpp

@@ -6,6 +6,9 @@
 #include "src/storage/prism/CompositionToJaniVisitor.h"
 #include "src/storage/jani/Model.h"
 
+#include "src/utility/macros.h"
+#include "src/exceptions/NotImplementedException.h"
+
 namespace storm {
     namespace prism {
         
@@ -91,8 +94,53 @@ namespace storm {
                 }
             }
             
+            // Go through the reward models and construct assignments to the transient variables that are to be added to
+            // edges and transient assignments that are added to the locations.
+            std::map<uint_fast64_t, std::vector<storm::jani::Assignment>> transientEdgeAssignments;
+            std::vector<storm::jani::Assignment> transientLocationAssignments;
+            for (auto const& rewardModel : program.getRewardModels()) {
+                auto newExpressionVariable = manager->declareRationalVariable(rewardModel.getName().empty() ? "default" : rewardModel.getName());
+                storm::jani::RealVariable const& newTransientVariable = janiModel.addVariable(storm::jani::RealVariable(rewardModel.getName(), newExpressionVariable, true));
+                
+                if (rewardModel.hasStateRewards()) {
+                    storm::expressions::Expression transientLocationExpression;
+                    for (auto const& stateReward : rewardModel.getStateRewards()) {
+                        storm::expressions::Expression rewardTerm = stateReward.getStatePredicateExpression().isTrue() ? stateReward.getRewardValueExpression() : storm::expressions::ite(stateReward.getStatePredicateExpression(), stateReward.getRewardValueExpression(), manager->rational(0));
+                        if (transientLocationExpression.isInitialized()) {
+                            transientLocationExpression = transientLocationExpression + rewardTerm;
+                        } else {
+                            transientLocationExpression = rewardTerm;
+                        }
+                    }
+                    transientLocationAssignments.emplace_back(newTransientVariable, transientLocationExpression);
+                }
+                
+                std::map<uint_fast64_t, storm::expressions::Expression> actionIndexToExpression;
+                for (auto const& actionReward : rewardModel.getStateActionRewards()) {
+                    storm::expressions::Expression rewardTerm = actionReward.getStatePredicateExpression().isTrue() ? actionReward.getRewardValueExpression() : storm::expressions::ite(actionReward.getStatePredicateExpression(), actionReward.getRewardValueExpression(), manager->rational(0));
+                    auto it = actionIndexToExpression.find(janiModel.getActionIndex(actionReward.getActionName()));
+                    if (it != actionIndexToExpression.end()) {
+                        it->second = it->second + rewardTerm;
+                    } else {
+                        actionIndexToExpression[janiModel.getActionIndex(actionReward.getActionName())] = rewardTerm;
+                    }
+                }
+                
+                for (auto const& entry : actionIndexToExpression) {
+                    auto it = transientEdgeAssignments.find(entry.first);
+                    if (it != transientEdgeAssignments.end()) {
+                        it->second.push_back(storm::jani::Assignment(newTransientVariable, entry.second));
+                    } else {
+                        std::vector<storm::jani::Assignment> assignments = {storm::jani::Assignment(newTransientVariable, entry.second)};
+                        transientEdgeAssignments.emplace(entry.first, assignments);
+                    }
+                }
+                STORM_LOG_THROW(!rewardModel.hasTransitionRewards(), storm::exceptions::NotImplementedException, "Transition reward translation currently not implemented.");
+            }
+            
             // Now create the separate JANI automata from the modules of the PRISM program. While doing so, we use the
             // previously built mapping to make variables global that are read by more than one module.
+            bool firstModule = true;
             for (auto const& module : program.getModules()) {
                 storm::jani::Automaton automaton(module.getName());
                 for (auto const& variable : module.getIntegerVariables()) {
@@ -124,8 +172,16 @@ namespace storm {
                 automaton.setInitialStatesRestriction(manager->boolean(true));
                 
                 // Create a single location that will have all the edges.
-                uint64_t onlyLocation = automaton.addLocation(storm::jani::Location("l"));
-                automaton.addInitialLocation(onlyLocation);
+                uint64_t onlyLocationIndex = automaton.addLocation(storm::jani::Location("l"));
+                automaton.addInitialLocation(onlyLocationIndex);
+                
+                // If we are translating the first module, we need to add the transient assignments to the location.
+                if (firstModule) {
+                    storm::jani::Location& onlyLocation = automaton.getLocation(onlyLocationIndex);
+                    for (auto const& assignment : transientLocationAssignments) {
+                        onlyLocation.addTransientAssignment(assignment);
+                    }
+                }
                 
                 for (auto const& command : module.getCommands()) {
                     boost::optional<storm::expressions::Expression> rateExpression;
@@ -147,20 +203,29 @@ namespace storm {
                         }
                         
                         if (rateExpression) {
-                            destinations.push_back(storm::jani::EdgeDestination(onlyLocation, manager->integer(1) / rateExpression.get(), assignments));
+                            destinations.push_back(storm::jani::EdgeDestination(onlyLocationIndex, manager->integer(1) / rateExpression.get(), assignments));
                         } else {
-                            destinations.push_back(storm::jani::EdgeDestination(onlyLocation, update.getLikelihoodExpression(), assignments));
+                            destinations.push_back(storm::jani::EdgeDestination(onlyLocationIndex, update.getLikelihoodExpression(), assignments));
                         }
                     }
-                    automaton.addEdge(storm::jani::Edge(onlyLocation, janiModel.getActionIndex(command.getActionName()), rateExpression, command.getGuardExpression(), destinations));
+                    
+                    // Create the edge object so we can add transient assignments.
+                    storm::jani::Edge newEdge(onlyLocationIndex, janiModel.getActionIndex(command.getActionName()), rateExpression, command.getGuardExpression(), destinations);
+                    
+                    // Then add the transient assignments for the rewards.
+                    auto transientEdgeAssignmentsToAdd = transientEdgeAssignments.find(janiModel.getActionIndex(command.getActionName()));
+                    if (transientEdgeAssignmentsToAdd != transientEdgeAssignments.end()) {
+                        for (auto const& assignment : transientEdgeAssignmentsToAdd->second) {
+                            newEdge.addTransientAssignment(assignment);
+                        }
+                    }
+                    
+                    // Finally add the constructed edge.
+                    automaton.addEdge(newEdge);
                 }
                 
                 janiModel.addAutomaton(automaton);
-            }
-            
-            // Translate the reward models.
-            for (auto const& rewardModel : program.getRewardModels()) {
-                
+                firstModule = false;
             }
             
             // Create an initial state restriction if there was an initial construct in the program.