Merge branch 'future' into gspn

Former-commit-id: 89684bb6b6

src/builder/ExplicitPrismModelBuilder.h

@@ -16,6 +16,7 @@
 #include "src/storage/expressions/ExpressionEvaluator.h"
 #include "src/storage/BitVectorHashMap.h"
 #include "src/logic/Formulas.h"
+#include "src/models/sparse/StateAnnotation.h"
 #include "src/models/sparse/Model.h"
 #include "src/models/sparse/StateLabeling.h"
 #include "src/storage/SparseMatrix.h"
@@ -59,7 +60,7 @@ namespace storm {
             };
             
             // A structure holding information about the reachable state space that can be retrieved from the outside.
-            struct StateInformation {
+            struct StateInformation : public storm::models::sparse::StateAnnotation {
                 /*!
                  * Constructs a state information object for the given number of states.
                  */
@@ -67,6 +68,12 @@ namespace storm {
                 
                 // A mapping from state indices to their variable valuations.
                 std::vector<storm::expressions::SimpleValuation> valuations;
+
+                std::string stateInfo(uint_fast64_t state) const override {
+                    return valuations[state].toString();
+                }
+
+
             };
             
             // A structure storing information about the used variables of the program.
@@ -195,7 +202,7 @@ namespace storm {
                 bool buildAllRewardModels;
                 
                 // A flag that indicates whether or not to store the state information after successfully building the
-                // model. If it is to be preserved, it can be retrieved via the appropriate methods after a successfull
+                // model. If it is to be preserved, it can be retrieved via the appropriate methods after a successful
                 // call to <code>translateProgram</code>.
                 bool buildStateInformation;
                 

src/models/sparse/Mdp.cpp

@@ -2,6 +2,7 @@
 
 #include "src/exceptions/InvalidArgumentException.h"
 #include "src/utility/constants.h"
+#include "src/utility/vector.h"
 #include "src/adapters/CarlAdapter.h"
 
 #include "src/models/sparse/StandardRewardModel.h"
@@ -81,7 +82,13 @@ namespace storm {
                 for (auto const& rewardModel : this->getRewardModels()) {
                     newRewardModels.emplace(rewardModel.first, rewardModel.second.restrictActions(enabledChoices));
                 }
-                return Mdp<ValueType, RewardModelType>(restrictedTransitions, this->getStateLabeling(), newRewardModels, this->getOptionalChoiceLabeling());
+                if(this->hasChoiceLabeling()) {
+                    return Mdp<ValueType, RewardModelType>(restrictedTransitions, this->getStateLabeling(), newRewardModels, boost::optional<std::vector<LabelSet>>(storm::utility::vector::filterVector(this->getChoiceLabeling(), enabledChoices)));
+                } else {
+                    return Mdp<ValueType, RewardModelType>(restrictedTransitions, this->getStateLabeling(), newRewardModels, boost::optional<std::vector<LabelSet>>());
+                }
+
+
             }
 
             template<typename ValueType, typename RewardModelType>

src/models/sparse/StateAnnotation.h

@@ -0,0 +1,16 @@
+#ifndef STORM_STATEANNOTATION_H
+#define STORM_STATEANNOTATION_H
+
+namespace storm {
+    namespace models {
+        namespace sparse {
+            class StateAnnotation {
+            public:
+                virtual std::string stateInfo(uint_fast64_t s) const = 0;
+            };
+        }
+    }
+
+}
+
+#endif //STORM_STATEANNOTATION_H

src/storage/expressions/SimpleValuation.cpp

@@ -110,29 +110,57 @@ namespace storm {
             return "[" + boost::join(assignments, ", ") + "]";
         }
 
-        std::ostream& operator<<(std::ostream& out, SimpleValuation const& valuation) {
-            out << "valuation {" << std::endl;
-            out << valuation.getManager() << std::endl;
-            if (!valuation.booleanValues.empty()) {
-                for (auto const& element : valuation.booleanValues) {
-                    out << element << " ";
+
+        std::string SimpleValuation::toString(bool pretty) const {
+
+
+            std::stringstream sstr;
+            if(pretty) {
+                sstr << "valuation {" << std::endl;
+                for(auto const& e : getManager()) {
+                    sstr << e.first.getName() << "=";
+                    if (e.first.hasBooleanType()) {
+                        sstr << std::boolalpha << this->getBooleanValue(e.first) << std::noboolalpha;
+                    } else if (e.first.hasIntegerType()) {
+                        sstr << this->getIntegerValue(e.first);
+                    } else if (e.first.hasRationalType()) {
+                        sstr << this->getRationalValue(e.first);
+                    } else {
+                        STORM_LOG_THROW(false, storm::exceptions::InvalidTypeException, "Unexpected variable type.");
+                    }
+                    sstr << std::endl;
                 }
-                out << std::endl;
-            }
-            if (!valuation.integerValues.empty()) {
-                for (auto const& element : valuation.integerValues) {
-                    out << element << " ";
+                sstr << "}";
+            } else {
+                sstr << "valuation {" << std::endl;
+                sstr << getManager() << std::endl;
+                if (!booleanValues.empty()) {
+                    for (auto const& element : booleanValues) {
+                        sstr << element << " ";
+                    }
+                    sstr << std::endl;
                 }
-                out << std::endl;
-            }
-            if (!valuation.rationalValues.empty()) {
-                for (auto const& element : valuation.rationalValues) {
-                    out << element << " ";
+                if (!integerValues.empty()) {
+                    for (auto const& element : integerValues) {
+                        sstr << element << " ";
+                    }
+                    sstr << std::endl;
+                }
+                if (!rationalValues.empty()) {
+                    for (auto const& element : rationalValues) {
+                        sstr << element << " ";
+                    }
+                    sstr << std::endl;
                 }
-                out << std::endl;
+                sstr << "}";
             }
-            out << "}" << std::endl;
 
+
+            return sstr.str();
+        }
+        
+        std::ostream& operator<<(std::ostream& out, SimpleValuation const& valuation) {
+            out << valuation.toString(false) << std::endl;
             return out;
         }
         

src/storage/expressions/SimpleValuation.h

@@ -62,6 +62,8 @@ namespace storm {
              */
             virtual std::string toPrettyString(std::set<storm::expressions::Variable> const& selectedVariables) const;
 
+            virtual std::string toString(bool pretty = true) const;
+
             friend std::ostream& operator<<(std::ostream& out, SimpleValuation const& valuation);
             
         private:

src/storage/prism/Program.cpp

@@ -1067,6 +1067,16 @@ namespace storm {
             return Program(manager, this->getModelType(), this->getConstants(), std::vector<storm::prism::BooleanVariable>(), std::vector<storm::prism::IntegerVariable>(), this->getFormulas(), {singleModule}, actionToIndexMap, this->getRewardModels(), false, this->getInitialConstruct(), this->getLabels(), this->getFilename(), 0, true);
         }
 
+        std::unordered_map<uint_fast64_t, std::string> Program::buildCommandIndexToActionNameMap() const {
+            std::unordered_map<uint_fast64_t, std::string> res;
+            for(auto const& m : this->modules) {
+                for(auto const& c : m.getCommands()) {
+                    res.emplace(c.getGlobalIndex(), c.getActionName());
+                }
+            }
+            return res;
+        }
+        
         Command Program::synchronizeCommands(uint_fast64_t newCommandIndex, uint_fast64_t actionIndex, uint_fast64_t firstUpdateIndex, std::string const& actionName, std::vector<std::reference_wrapper<Command const>> const& commands) const {
             // To construct the synchronous product of the commands, we need to store a list of its updates.
             std::vector<storm::prism::Update> newUpdates;

src/storage/prism/Program.h

@@ -444,6 +444,11 @@ namespace storm {
              */
             storm::expressions::ExpressionManager& getManager();
 
+            /*!
+             *
+             */
+            std::unordered_map<uint_fast64_t, std::string> buildCommandIndexToActionNameMap() const;
+            
         private:
             /*!
              * This function builds a command that corresponds to the synchronization of the given list of commands.

src/utility/vector.h

@@ -654,6 +654,17 @@ namespace storm {
 
 				return resultVector;
 			}
+
+            template<typename Type>
+            std::vector<Type> filterVector(std::vector<Type> const& in, storm::storage::BitVector const& filter) {
+                std::vector<Type> result;
+                result.reserve(filter.getNumberOfSetBits());
+                for(auto index : filter) {
+                    result.push_back(in[index]);
+                }
+                assert(result.size() == filter.getNumberOfSetBits());
+                return result;
+            }
         } // namespace vector
     } // namespace utility
 } // namespace storm