pomdps

src/storm/api/builder.h

@@ -10,6 +10,7 @@
 #include "storm/models/sparse/Dtmc.h"
 #include "storm/models/sparse/Ctmc.h"
 #include "storm/models/sparse/Mdp.h"
+#include "storm/models/sparse/Pomdp.h"
 #include "storm/models/sparse/MarkovAutomaton.h"
 #include "storm/models/sparse/StochasticTwoPlayerGame.h"
 #include "storm/models/sparse/StandardRewardModel.h"
@@ -104,6 +105,8 @@ namespace storm {
                     return std::make_shared<storm::models::sparse::Mdp<ValueType, RewardModelType>>(std::move(components));
                 case storm::models::ModelType::MarkovAutomaton:
                     return std::make_shared<storm::models::sparse::MarkovAutomaton<ValueType, RewardModelType>>(std::move(components));
+                case storm::models::ModelType::Pomdp:
+                    return std::make_shared<storm::models::sparse::Pomdp<ValueType, RewardModelType>>(std::move(components));
                 case storm::models::ModelType::S2pg:
                     return std::make_shared<storm::models::sparse::StochasticTwoPlayerGame<ValueType, RewardModelType>>(std::move(components));
             }

src/storm/models/sparse/Mdp.cpp

@@ -13,27 +13,29 @@ namespace storm {
 
             template <typename ValueType, typename RewardModelType>
             Mdp<ValueType, RewardModelType>::Mdp(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::models::sparse::StateLabeling const& stateLabeling,
-                                  std::unordered_map<std::string, RewardModelType> const& rewardModels)
-                    : Mdp<ValueType, RewardModelType>(storm::storage::sparse::ModelComponents<ValueType, RewardModelType>(transitionMatrix, stateLabeling, rewardModels)) {
+                                  std::unordered_map<std::string, RewardModelType> const& rewardModels, ModelType type)
+                    : Mdp<ValueType, RewardModelType>(storm::storage::sparse::ModelComponents<ValueType, RewardModelType>(transitionMatrix, stateLabeling, rewardModels), type) {
                 // Intentionally left empty
             }
             
             template <typename ValueType, typename RewardModelType>
             Mdp<ValueType, RewardModelType>::Mdp(storm::storage::SparseMatrix<ValueType>&& transitionMatrix, storm::models::sparse::StateLabeling&& stateLabeling,
-                                  std::unordered_map<std::string, RewardModelType>&& rewardModels)
-                    : Mdp<ValueType, RewardModelType>(storm::storage::sparse::ModelComponents<ValueType, RewardModelType>(std::move(transitionMatrix), std::move(stateLabeling), std::move(rewardModels))) {
+                                  std::unordered_map<std::string, RewardModelType>&& rewardModels, ModelType type)
+                    : Mdp<ValueType, RewardModelType>(storm::storage::sparse::ModelComponents<ValueType, RewardModelType>(std::move(transitionMatrix), std::move(stateLabeling), std::move(rewardModels)), type) {
                 // Intentionally left empty
             }
             
             template <typename ValueType, typename RewardModelType>
-            Mdp<ValueType, RewardModelType>::Mdp(storm::storage::sparse::ModelComponents<ValueType, RewardModelType> const& components)
-                    : NondeterministicModel<ValueType, RewardModelType>(storm::models::ModelType::Mdp, components) {
+            Mdp<ValueType, RewardModelType>::Mdp(storm::storage::sparse::ModelComponents<ValueType, RewardModelType> const& components, ModelType type)
+                    : NondeterministicModel<ValueType, RewardModelType>(type, components) {
+                assert(type == storm::models::ModelType::Mdp || type == storm::models::ModelType::Pomdp);
                 // Intentionally left empty
             }
             
            template <typename ValueType, typename RewardModelType>
-            Mdp<ValueType, RewardModelType>::Mdp(storm::storage::sparse::ModelComponents<ValueType, RewardModelType>&& components)
-                    : NondeterministicModel<ValueType, RewardModelType>(storm::models::ModelType::Mdp, std::move(components)) {
+            Mdp<ValueType, RewardModelType>::Mdp(storm::storage::sparse::ModelComponents<ValueType, RewardModelType>&& components, ModelType type)
+                    : NondeterministicModel<ValueType, RewardModelType>(type, std::move(components)) {
+               assert(type == storm::models::ModelType::Mdp || type == storm::models::ModelType::Pomdp);
                 // Intentionally left empty
             }
    

src/storm/models/sparse/Mdp.h

@@ -24,7 +24,7 @@ namespace storm {
                  */
                 Mdp(storm::storage::SparseMatrix<ValueType> const& transitionMatrix,
                     storm::models::sparse::StateLabeling const& stateLabeling,
-                    std::unordered_map<std::string, RewardModelType> const& rewardModels = std::unordered_map<std::string, RewardModelType>());
+                    std::unordered_map<std::string, RewardModelType> const& rewardModels = std::unordered_map<std::string, RewardModelType>(), ModelType type = ModelType::Mdp);
                 
                 /*!
                  * Constructs a model by moving the given data.
@@ -35,15 +35,15 @@ namespace storm {
                  */
                 Mdp(storm::storage::SparseMatrix<ValueType>&& transitionMatrix,
                     storm::models::sparse::StateLabeling&& stateLabeling,
-                    std::unordered_map<std::string, RewardModelType>&& rewardModels = std::unordered_map<std::string, RewardModelType>());
+                    std::unordered_map<std::string, RewardModelType>&& rewardModels = std::unordered_map<std::string, RewardModelType>(), ModelType type = ModelType::Mdp);
                 
                 /*!
                  * Constructs a model from the given data.
                  *
                  * @param components The components for this model.
                  */
-                Mdp(storm::storage::sparse::ModelComponents<ValueType, RewardModelType> const& components);
-                Mdp(storm::storage::sparse::ModelComponents<ValueType, RewardModelType>&& components);
+                Mdp(storm::storage::sparse::ModelComponents<ValueType, RewardModelType> const& components, ModelType type = ModelType::Mdp);
+                Mdp(storm::storage::sparse::ModelComponents<ValueType, RewardModelType>&& components, ModelType type = ModelType::Mdp);
                 
                 Mdp(Mdp<ValueType, RewardModelType> const& other) = default;
                 Mdp& operator=(Mdp<ValueType, RewardModelType> const& other) = default;

src/storm/models/sparse/Model.cpp

@@ -56,7 +56,7 @@ namespace storm {
                     STORM_LOG_THROW(stateCount == this->getTransitionMatrix().getRowCount(), storm::exceptions::IllegalArgumentException, "Can not create deterministic model: Number of rows of transition matrix does not match state count.");
                     STORM_LOG_THROW(stateCount == this->getTransitionMatrix().getColumnCount(), storm::exceptions::IllegalArgumentException, "Can not create deterministic model: Number of columns of transition matrix does not match state count.");
                     STORM_LOG_ERROR_COND(!components.player1Matrix.is_initialized(), "Player 1 matrix given for a model that is no stochastic game (will be ignored).");
-                } else if (this->isOfType(ModelType::Mdp) || this->isOfType(ModelType::MarkovAutomaton)) {
+                } else if (this->isOfType(ModelType::Mdp) || this->isOfType(ModelType::MarkovAutomaton) || this->isOfType(ModelType::Pomdp)) {
                     STORM_LOG_THROW(stateCount == this->getTransitionMatrix().getRowGroupCount(), storm::exceptions::IllegalArgumentException, "Can not create nondeterministic model: Number of row groups of transition matrix does not match state count.");
                     STORM_LOG_THROW(stateCount == this->getTransitionMatrix().getColumnCount(), storm::exceptions::IllegalArgumentException, "Can not create nondeterministic model: Number of columns of transition matrix does not match state count.");
                     STORM_LOG_ERROR_COND(!components.player1Matrix.is_initialized(), "Player 1 matrix given for a model that is no stochastic game (will be ignored).");

src/storm/models/sparse/Pomdp.cpp

@@ -5,22 +5,22 @@ namespace storm {
         namespace sparse {
 
             template <typename ValueType, typename RewardModelType>
-            Pomdp<ValueType, RewardModelType>::Pomdp(storm::storage::SparseMatrix<ValueType> const &transitionMatrix, storm::models::sparse::StateLabeling const &stateLabeling, std::unordered_map <std::string, RewardModelType> const &rewardModels) : Mdp<ValueType, RewardModelType>(transitionMatrix, stateLabeling, rewardModels) {
+            Pomdp<ValueType, RewardModelType>::Pomdp(storm::storage::SparseMatrix<ValueType> const &transitionMatrix, storm::models::sparse::StateLabeling const &stateLabeling, std::unordered_map <std::string, RewardModelType> const &rewardModels) : Mdp<ValueType, RewardModelType>(transitionMatrix, stateLabeling, rewardModels, storm::models::ModelType::Pomdp) {
                 // Intentionally left blank.
             }
 
             template <typename ValueType, typename RewardModelType>
-            Pomdp<ValueType, RewardModelType>::Pomdp(storm::storage::SparseMatrix<ValueType> &&transitionMatrix, storm::models::sparse::StateLabeling &&stateLabeling, std::unordered_map <std::string, RewardModelType> &&rewardModels) : Mdp<ValueType, RewardModelType>(transitionMatrix, stateLabeling, rewardModels) {
+            Pomdp<ValueType, RewardModelType>::Pomdp(storm::storage::SparseMatrix<ValueType> &&transitionMatrix, storm::models::sparse::StateLabeling &&stateLabeling, std::unordered_map <std::string, RewardModelType> &&rewardModels) : Mdp<ValueType, RewardModelType>(transitionMatrix, stateLabeling, rewardModels, storm::models::ModelType::Pomdp) {
                 // Intentionally left empty.
             }
 
             template <typename ValueType, typename RewardModelType>
-            Pomdp<ValueType, RewardModelType>::Pomdp(storm::storage::sparse::ModelComponents<ValueType, RewardModelType> const &components) : Mdp<ValueType, RewardModelType>(components) {
+            Pomdp<ValueType, RewardModelType>::Pomdp(storm::storage::sparse::ModelComponents<ValueType, RewardModelType> const &components) : Mdp<ValueType, RewardModelType>(components, storm::models::ModelType::Pomdp) {
 
             }
 
             template <typename ValueType, typename RewardModelType>
-            Pomdp<ValueType, RewardModelType>::Pomdp(storm::storage::sparse::ModelComponents<ValueType, RewardModelType> &&components): Mdp<ValueType, RewardModelType>(components) {
+            Pomdp<ValueType, RewardModelType>::Pomdp(storm::storage::sparse::ModelComponents<ValueType, RewardModelType> &&components): Mdp<ValueType, RewardModelType>(components, storm::models::ModelType::Pomdp) {
 
             }
 

src/storm/parser/PrismParser.cpp

@@ -145,7 +145,7 @@ namespace storm {
             initialStatesConstruct = (qi::lit("init") > expression_ > qi::lit("endinit"))[qi::_pass = phoenix::bind(&PrismParser::addInitialStatesConstruct, phoenix::ref(*this), qi::_1, qi::_r1)];
             initialStatesConstruct.name("initial construct");
 
-            observablesConstruct = (qi::lit("observables") > +(identifier)> qi::lit("endobservables"));
+            observablesConstruct = (qi::lit("observables") > (identifier % qi::lit(",") )> qi::lit("endobservables"))[phoenix::bind(&PrismParser::createObservablesList, phoenix::ref(*this), qi::_1)];
             observablesConstruct.name("observables construct");
             
             systemCompositionConstruct = (qi::lit("system") > parallelComposition > qi::lit("endsystem"))[phoenix::bind(&PrismParser::addSystemCompositionConstruct, phoenix::ref(*this), qi::_1, qi::_r1)];
@@ -534,7 +534,11 @@ namespace storm {
                     }
                 }
             }
-            bool observable = false; // TODO
+            bool observable = this->observables.count(variableName) > 0;
+            if(observable) {
+                this->observables.erase(variableName);
+                std::cout << variableName << " is observable." << std::endl;
+            }
             return storm::prism::BooleanVariable(manager->getVariable(variableName), initialValueExpression, observable, this->getFilename());
         }
         
@@ -551,9 +555,19 @@ namespace storm {
                     }
                 }
             }
-            bool observable = false; // TODO
+            bool observable = this->observables.count(variableName) > 0;
+            if(observable) {
+                this->observables.erase(variableName);
+                std::cout << variableName << " is observable." << std::endl;
+            }
+
             return storm::prism::IntegerVariable(manager->getVariable(variableName), lowerBoundExpression, upperBoundExpression, initialValueExpression, observable, this->getFilename());
         }
+
+        void PrismParser::createObservablesList(std::vector<std::string> const& observables) {
+            this->observables.insert(observables.begin(), observables.end());
+            // We need this list to be filled in both runs.
+        }
         
         storm::prism::Module PrismParser::createModule(std::string const& moduleName, std::vector<storm::prism::BooleanVariable> const& booleanVariables, std::vector<storm::prism::IntegerVariable> const& integerVariables, std::vector<storm::prism::Command> const& commands, GlobalProgramInformation& globalProgramInformation) const {
             globalProgramInformation.moduleToIndexMap[moduleName] = globalProgramInformation.modules.size();

src/storm/parser/PrismParser.h

@@ -161,7 +161,7 @@ namespace storm {
              */
             std::string const& getFilename() const;
 
-            std::vector<std::string> observables;
+            mutable std::set<std::string> observables;
 
             // A function used for annotating the entities with their position.
             phoenix::function<PositionAnnotation> annotate;
@@ -282,7 +282,9 @@ namespace storm {
             storm::prism::Module createModule(std::string const& moduleName, std::vector<storm::prism::BooleanVariable> const& booleanVariables, std::vector<storm::prism::IntegerVariable> const& integerVariables, std::vector<storm::prism::Command> const& commands, GlobalProgramInformation& globalProgramInformation) const;
             storm::prism::Module createRenamedModule(std::string const& newModuleName, std::string const& oldModuleName, std::map<std::string, std::string> const& renaming, GlobalProgramInformation& globalProgramInformation) const;
             storm::prism::Program createProgram(GlobalProgramInformation const& globalProgramInformation) const;
-            
+            void createObservablesList(std::vector<std::string> const& observables);
+
+
             void removeInitialConstruct(GlobalProgramInformation& globalProgramInformation) const;
             
             // An error handler function.