towards support for pomdps in storm

src/storm/builder/ExplicitModelBuilder.cpp

@@ -73,6 +73,8 @@ namespace storm {
                     return storm::utility::builder::buildModelFromComponents(storm::models::ModelType::Ctmc, buildModelComponents());
                 case storm::generator::ModelType::MDP:
                     return storm::utility::builder::buildModelFromComponents(storm::models::ModelType::Mdp, buildModelComponents());
+                case storm::generator::ModelType::POMDP:
+                    return storm::utility::builder::buildModelFromComponents(storm::models::ModelType::Pomdp, buildModelComponents());
                 case storm::generator::ModelType::MA:
                     return storm::utility::builder::buildModelFromComponents(storm::models::ModelType::MarkovAutomaton, buildModelComponents());
                 default:

src/storm/generator/JaniNextStateGenerator.cpp

@@ -134,6 +134,11 @@ namespace storm {
             return model.isDiscreteTimeModel();
         }
 
+        template<typename ValueType, typename StateType>
+        bool JaniNextStateGenerator<ValueType, StateType>::isPartiallyObservable() const {
+            return false;
+        };
+        
         template<typename ValueType, typename StateType>
         uint64_t JaniNextStateGenerator<ValueType, StateType>::getLocation(CompressedState const& state, LocationVariableInformation const& locationVariable) const {
             if (locationVariable.bitWidth == 0) {

src/storm/generator/JaniNextStateGenerator.h

@@ -23,6 +23,7 @@ namespace storm {
             virtual ModelType getModelType() const override;
             virtual bool isDeterministicModel() const override;
             virtual bool isDiscreteTimeModel() const override;
+            virtual bool isPartiallyObservable() const override;
             virtual std::vector<StateType> getInitialStates(StateToIdCallback const& stateToIdCallback) override;
             
             virtual StateBehavior<ValueType, StateType> expand(StateToIdCallback const& stateToIdCallback) override;

src/storm/generator/NextStateGenerator.h

@@ -28,7 +28,8 @@ namespace storm {
             DTMC,
             CTMC,
             MDP,
-            MA
+            MA,
+            POMDP
         };
         
         template<typename ValueType, typename StateType = uint32_t>
@@ -50,6 +51,7 @@ namespace storm {
             virtual ModelType getModelType() const = 0;
             virtual bool isDeterministicModel() const = 0;
             virtual bool isDiscreteTimeModel() const = 0;
+            virtual bool isPartiallyObservable() const = 0;
             virtual std::vector<StateType> getInitialStates(StateToIdCallback const& stateToIdCallback) = 0;
             
             void load(CompressedState const& state);

src/storm/generator/PrismNextStateGenerator.cpp

@@ -117,6 +117,7 @@ namespace storm {
                 case storm::prism::Program::ModelType::CTMC: return ModelType::CTMC;
                 case storm::prism::Program::ModelType::MDP: return ModelType::MDP;
                 case storm::prism::Program::ModelType::MA: return ModelType::MA;
+                case storm::prism::Program::ModelType::POMDP: return ModelType::POMDP;
                 default:
                     STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Invalid model type.");
             }
@@ -132,6 +133,11 @@ namespace storm {
             return program.isDiscreteTimeModel();
         }
 
+        template<typename ValueType,typename StateType>
+        bool PrismNextStateGenerator<ValueType, StateType>::isPartiallyObservable() const {
+            return program.isPartiallyObservable();
+        }
+        
         template<typename ValueType, typename StateType>
         std::vector<StateType> PrismNextStateGenerator<ValueType, StateType>::getInitialStates(StateToIdCallback const& stateToIdCallback) {
             // Prepare an SMT solver to enumerate all initial states.

src/storm/generator/PrismNextStateGenerator.h

@@ -21,6 +21,7 @@ namespace storm {
             virtual ModelType getModelType() const override;
             virtual bool isDeterministicModel() const override;
             virtual bool isDiscreteTimeModel() const override;
+            virtual bool isPartiallyObservable() const override;
             virtual std::vector<StateType> getInitialStates(StateToIdCallback const& stateToIdCallback) override;
 
             virtual StateBehavior<ValueType, StateType> expand(StateToIdCallback const& stateToIdCallback) override;

src/storm/models/sparse/Mdp.cpp

@@ -60,13 +60,10 @@ namespace storm {
             }
 
             template class Mdp<double>;
-
-#ifdef STORM_HAVE_CARL
             template class Mdp<storm::RationalNumber>;
 
             template class Mdp<double, storm::models::sparse::StandardRewardModel<storm::Interval>>;
             template class Mdp<storm::RationalFunction>;
-#endif
         } // namespace sparse
     } // namespace models
 } // namespace storm

src/storm/models/sparse/Pomdp.cpp

@@ -0,0 +1,35 @@
+#include "storm/models/sparse/Pomdp.h"
+
+namespace storm {
+    namespace models {
+        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) {
+                // 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) {
+                // Intentionally left empty.
+            }
+
+            template <typename ValueType, typename RewardModelType>
+            Pomdp<ValueType, RewardModelType>::Pomdp(storm::storage::sparse::ModelComponents<ValueType, RewardModelType> const &components) : Mdp<ValueType, RewardModelType>(components) {
+
+            }
+
+            template <typename ValueType, typename RewardModelType>
+            Pomdp<ValueType, RewardModelType>::Pomdp(storm::storage::sparse::ModelComponents<ValueType, RewardModelType> &&components): Mdp<ValueType, RewardModelType>(components) {
+
+            }
+
+
+            template class Pomdp<double>;
+            template class Pomdp<storm::RationalNumber>;
+            template class Pomdp<double, storm::models::sparse::StandardRewardModel<storm::Interval>>;
+            template class Pomdp<storm::RationalFunction>;
+
+        }
+    }
+}

src/storm/models/sparse/Pomdp.h

@@ -0,0 +1,61 @@
+#pragma once
+
+#include "storm/models/sparse/Mdp.h"
+
+#include "storm/models/sparse/StandardRewardModel.h"
+
+namespace storm {
+    namespace models {
+        namespace sparse {
+
+            /*!
+             * This class represents a partially observable Markov decision process.
+             */
+            template<class ValueType, typename RewardModelType = StandardRewardModel <ValueType>>
+            class Pomdp : public Mdp<ValueType, RewardModelType> {
+            public:
+                /*!
+                 * Constructs a model from the given data.
+                 *
+                 * @param transitionMatrix The matrix representing the transitions in the model.
+                 * @param stateLabeling The labeling of the states.
+                 * @param rewardModels A mapping of reward model names to reward models.
+                 */
+                Pomdp(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>());
+
+                /*!
+                 * Constructs a model by moving the given data.
+                 *
+                 * @param transitionMatrix The matrix representing the transitions in the model.
+                 * @param stateLabeling The labeling of the states.
+                 * @param rewardModels A mapping of reward model names to reward models.
+                 */
+                Pomdp(storm::storage::SparseMatrix<ValueType> &&transitionMatrix,
+                      storm::models::sparse::StateLabeling &&stateLabeling,
+                      std::unordered_map <std::string, RewardModelType> &&rewardModels = std::unordered_map<std::string, RewardModelType>());
+
+                /*!
+                 * Constructs a model from the given data.
+                 *
+                 * @param components The components for this model.
+                 */
+                Pomdp(storm::storage::sparse::ModelComponents<ValueType, RewardModelType> const &components);
+
+                Pomdp(storm::storage::sparse::ModelComponents<ValueType, RewardModelType> &&components);
+
+                Pomdp(Pomdp <ValueType, RewardModelType> const &other) = default;
+
+                Pomdp &operator=(Pomdp <ValueType, RewardModelType> const &other) = default;
+
+                Pomdp(Pomdp <ValueType, RewardModelType> &&other) = default;
+
+                Pomdp &operator=(Pomdp <ValueType, RewardModelType> &&other) = default;
+
+            protected:
+                StateLabeling observations;
+            };
+        }
+    }
+}

src/storm/parser/PrismParser.cpp

@@ -84,6 +84,8 @@ namespace storm {
             modelTypeDefinition %= modelType_;
             modelTypeDefinition.name("model type");
 
+
+            
             undefinedBooleanConstantDefinition = ((qi::lit("const") >> qi::lit("bool")) > identifier > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createUndefinedBooleanConstant, phoenix::ref(*this), qi::_1)];
             undefinedBooleanConstantDefinition.name("undefined boolean constant declaration");
             
@@ -143,6 +145,9 @@ 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.name("observables construct");
+            
             systemCompositionConstruct = (qi::lit("system") > parallelComposition > qi::lit("endsystem"))[phoenix::bind(&PrismParser::addSystemCompositionConstruct, phoenix::ref(*this), qi::_1, qi::_r1)];
             systemCompositionConstruct.name("system composition construct");
             
@@ -217,8 +222,9 @@ namespace storm {
             moduleDefinitionList.name("module list");
             
             start = (qi::eps[phoenix::bind(&PrismParser::removeInitialConstruct, phoenix::ref(*this), qi::_a)]
-                     > *(modelTypeDefinition[phoenix::bind(&PrismParser::setModelType, phoenix::ref(*this), qi::_a, qi::_1)]
-                         | definedConstantDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::constants, qi::_a), qi::_1)]
+                     > modelTypeDefinition[phoenix::bind(&PrismParser::setModelType, phoenix::ref(*this), qi::_a, qi::_1)]
+                     > -observablesConstruct
+                     >  *(  definedConstantDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::constants, qi::_a), qi::_1)]
                          | undefinedConstantDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::constants, qi::_a), qi::_1)]
                          | formulaDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::formulas, qi::_a), qi::_1)]
                          | globalVariableDefinition(qi::_a)
@@ -528,7 +534,8 @@ namespace storm {
                     }
                 }
             }
-            return storm::prism::BooleanVariable(manager->getVariable(variableName), initialValueExpression, this->getFilename());
+            bool observable = false; // TODO
+            return storm::prism::BooleanVariable(manager->getVariable(variableName), initialValueExpression, observable, this->getFilename());
         }
         
         storm::prism::IntegerVariable PrismParser::createIntegerVariable(std::string const& variableName, storm::expressions::Expression lowerBoundExpression, storm::expressions::Expression upperBoundExpression, storm::expressions::Expression initialValueExpression) const {
@@ -544,7 +551,8 @@ namespace storm {
                     }
                 }
             }
-            return storm::prism::IntegerVariable(manager->getVariable(variableName), lowerBoundExpression, upperBoundExpression, initialValueExpression, this->getFilename());
+            bool observable = false; // TODO
+            return storm::prism::IntegerVariable(manager->getVariable(variableName), lowerBoundExpression, upperBoundExpression, initialValueExpression, observable, this->getFilename());
         }
         
         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 {
@@ -609,8 +617,8 @@ namespace storm {
                 for (auto const& variable : moduleToRename.getBooleanVariables()) {
                     auto const& renamingPair = renaming.find(variable.getName());
                     STORM_LOG_THROW(renamingPair != renaming.end(), storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Boolean variable '" << variable.getName() << " was not renamed.");
-                    
-                    booleanVariables.push_back(storm::prism::BooleanVariable(manager->getVariable(renamingPair->second), variable.hasInitialValue() ? variable.getInitialValueExpression().substitute(expressionRenaming) : variable.getInitialValueExpression(), this->getFilename(), get_line(qi::_1)));
+                    bool observable = false; // TODO
+                    booleanVariables.push_back(storm::prism::BooleanVariable(manager->getVariable(renamingPair->second), variable.hasInitialValue() ? variable.getInitialValueExpression().substitute(expressionRenaming) : variable.getInitialValueExpression(), observable, this->getFilename(), get_line(qi::_1)));
                 }
                 
                 // Rename the integer variables.
@@ -618,8 +626,8 @@ namespace storm {
                 for (auto const& variable : moduleToRename.getIntegerVariables()) {
                     auto const& renamingPair = renaming.find(variable.getName());
                     STORM_LOG_THROW(renamingPair != renaming.end(), storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Integer variable '" << variable.getName() << " was not renamed.");
-                    
-                    integerVariables.push_back(storm::prism::IntegerVariable(manager->getVariable(renamingPair->second), variable.getLowerBoundExpression().substitute(expressionRenaming), variable.getUpperBoundExpression().substitute(expressionRenaming), variable.hasInitialValue() ? variable.getInitialValueExpression().substitute(expressionRenaming) : variable.getInitialValueExpression(), this->getFilename(), get_line(qi::_1)));
+                    bool observable = false; // TODO
+                    integerVariables.push_back(storm::prism::IntegerVariable(manager->getVariable(renamingPair->second), variable.getLowerBoundExpression().substitute(expressionRenaming), variable.getUpperBoundExpression().substitute(expressionRenaming), variable.hasInitialValue() ? variable.getInitialValueExpression().substitute(expressionRenaming) : variable.getInitialValueExpression(), observable, this->getFilename(), get_line(qi::_1)));
                 }
                 
                 // Rename commands.

src/storm/parser/PrismParser.h

@@ -45,6 +45,7 @@ namespace storm {
             storm::prism::InitialConstruct initialConstruct;
             boost::optional<storm::prism::SystemCompositionConstruct> systemCompositionConstruct;
 
+            
             // Counters to provide unique indexing for commands and updates.
             uint_fast64_t currentCommandIndex;
             uint_fast64_t currentUpdateIndex;
@@ -77,7 +78,8 @@ namespace storm {
                     ("ctmc", storm::prism::Program::ModelType::CTMC)
                     ("mdp", storm::prism::Program::ModelType::MDP)
                     ("ctmdp", storm::prism::Program::ModelType::CTMDP)
-                    ("ma", storm::prism::Program::ModelType::MA);
+                    ("ma", storm::prism::Program::ModelType::MA)
+                    ("pomdp", storm::prism::Program::ModelType::POMDP);
                 }
             };
             
@@ -89,21 +91,22 @@ namespace storm {
                     ("mdp", 3)
                     ("ctmdp", 4)
                     ("ma", 5)
-                    ("const", 6)
-                    ("int", 7)
-                    ("bool", 8)
-                    ("module", 9)
-                    ("endmodule", 10)
-                    ("rewards", 11)
-                    ("endrewards", 12)
-                    ("true", 13)
-                    ("false", 14)
-                    ("min", 15)
-                    ("max", 16)
-                    ("floor", 17)
-                    ("ceil", 18)
-                    ("init", 19)
-                    ("endinit", 20);
+                    ("pomdp", 6)
+                    ("const", 7)
+                    ("int", 8)
+                    ("bool", 9)
+                    ("module", 10)
+                    ("endmodule", 11)
+                    ("rewards", 12)
+                    ("endrewards", 13)
+                    ("true", 14)
+                    ("false", 15)
+                    ("min", 16)
+                    ("max", 17)
+                    ("floor", 18)
+                    ("ceil", 19)
+                    ("init", 20)
+                    ("endinit", 21);
                 }
             };
             
@@ -158,6 +161,8 @@ namespace storm {
              */
             std::string const& getFilename() const;
 
+            std::vector<std::string> observables;
+
             // A function used for annotating the entities with their position.
             phoenix::function<PositionAnnotation> annotate;
             
@@ -208,6 +213,8 @@ namespace storm {
             // Rules for initial states expression.
             qi::rule<Iterator, qi::unused_type(GlobalProgramInformation&), Skipper> initialStatesConstruct;
 
+            qi::rule<Iterator, qi::unused_type(), Skipper> observablesConstruct;
+
             // Rules for the system composition.
             qi::rule<Iterator, qi::unused_type(GlobalProgramInformation&), Skipper> systemCompositionConstruct;
             qi::rule<Iterator, std::shared_ptr<storm::prism::Composition>(), Skipper> parallelComposition;

src/storm/storage/prism/BooleanVariable.cpp

@@ -4,12 +4,12 @@
 
 namespace storm {
     namespace prism {
-        BooleanVariable::BooleanVariable(storm::expressions::Variable const& variable, storm::expressions::Expression const& initialValueExpression, std::string const& filename, uint_fast64_t lineNumber) : Variable(variable, initialValueExpression, filename, lineNumber) {
+        BooleanVariable::BooleanVariable(storm::expressions::Variable const& variable, storm::expressions::Expression const& initialValueExpression, bool observable, std::string const& filename, uint_fast64_t lineNumber) : Variable(variable, initialValueExpression, observable, filename, lineNumber) {
             // Nothing to do here.
         }
         
         BooleanVariable BooleanVariable::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const {
-            return BooleanVariable(this->getExpressionVariable(), this->getInitialValueExpression().isInitialized() ? this->getInitialValueExpression().substitute(substitution) : this->getInitialValueExpression(), this->getFilename(), this->getLineNumber());
+            return BooleanVariable(this->getExpressionVariable(), this->getInitialValueExpression().isInitialized() ? this->getInitialValueExpression().substitute(substitution) : this->getInitialValueExpression(), this->isObservable(), this->getFilename(), this->getLineNumber());
         }
         
         void BooleanVariable::createMissingInitialValue() {

src/storm/storage/prism/BooleanVariable.h

@@ -25,7 +25,7 @@ namespace storm {
              * @param filename The filename in which the variable is defined.
              * @param lineNumber The line number in which the variable is defined.
              */
-            BooleanVariable(storm::expressions::Variable const& variable, storm::expressions::Expression const& initialValueExpression, std::string const& filename = "", uint_fast64_t lineNumber = 0);
+            BooleanVariable(storm::expressions::Variable const& variable, storm::expressions::Expression const& initialValueExpression, bool observable, std::string const& filename = "", uint_fast64_t lineNumber = 0);
             
             /*!
              * Substitutes all identifiers in the boolean variable according to the given map.

src/storm/storage/prism/IntegerVariable.cpp

@@ -2,7 +2,7 @@
 
 namespace storm {
     namespace prism {
-        IntegerVariable::IntegerVariable(storm::expressions::Variable const& variable, storm::expressions::Expression const& lowerBoundExpression, storm::expressions::Expression const& upperBoundExpression, storm::expressions::Expression const& initialValueExpression, std::string const& filename, uint_fast64_t lineNumber) : Variable(variable, initialValueExpression, filename, lineNumber), lowerBoundExpression(lowerBoundExpression), upperBoundExpression(upperBoundExpression) {
+        IntegerVariable::IntegerVariable(storm::expressions::Variable const& variable, storm::expressions::Expression const& lowerBoundExpression, storm::expressions::Expression const& upperBoundExpression, storm::expressions::Expression const& initialValueExpression, bool observable, std::string const& filename, uint_fast64_t lineNumber) : Variable(variable, initialValueExpression, observable, filename, lineNumber), lowerBoundExpression(lowerBoundExpression), upperBoundExpression(upperBoundExpression) {
             // Intentionally left empty.
         }
         
@@ -19,7 +19,7 @@ namespace storm {
         }
         
         IntegerVariable IntegerVariable::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const {
-            return IntegerVariable(this->getExpressionVariable(), this->getLowerBoundExpression().substitute(substitution), this->getUpperBoundExpression().substitute(substitution), this->getInitialValueExpression().isInitialized() ? this->getInitialValueExpression().substitute(substitution) : this->getInitialValueExpression(), this->getFilename(), this->getLineNumber());
+            return IntegerVariable(this->getExpressionVariable(), this->getLowerBoundExpression().substitute(substitution), this->getUpperBoundExpression().substitute(substitution), this->getInitialValueExpression().isInitialized() ? this->getInitialValueExpression().substitute(substitution) : this->getInitialValueExpression(), this->isObservable(), this->getFilename(), this->getLineNumber());
         }
         
         void IntegerVariable::createMissingInitialValue() {

src/storm/storage/prism/IntegerVariable.h

@@ -27,7 +27,7 @@ namespace storm {
              * @param filename The filename in which the variable is defined.
              * @param lineNumber The line number in which the variable is defined.
              */
-            IntegerVariable(storm::expressions::Variable const& variable, storm::expressions::Expression const& lowerBoundExpression, storm::expressions::Expression const& upperBoundExpression, storm::expressions::Expression const& initialValueExpression, std::string const& filename = "", uint_fast64_t lineNumber = 0);
+            IntegerVariable(storm::expressions::Variable const& variable, storm::expressions::Expression const& lowerBoundExpression, storm::expressions::Expression const& upperBoundExpression, storm::expressions::Expression const& initialValueExpression, bool observable, std::string const& filename = "", uint_fast64_t lineNumber = 0);
             
             /*!
              * Retrieves an expression defining the lower bound for this integer variable.

src/storm/storage/prism/Program.cpp

@@ -188,13 +188,17 @@ namespace storm {
         }
         
         bool Program::isDiscreteTimeModel() const {
-            return modelType == ModelType::DTMC || modelType == ModelType::MDP;
+            return modelType == ModelType::DTMC || modelType == ModelType::MDP || modelType == ModelType::POMDP;
         }
         
         bool Program::isDeterministicModel() const {
             return modelType == ModelType::DTMC || modelType == ModelType::CTMC;
         }
 
+        bool Program::isPartiallyObservable() const {
+            return modelType == ModelType::POMDP;
+        }
+
         bool Program::hasUndefinedConstants() const {
             for (auto const& constant : this->getConstants()) {
                 if (!constant.isDefined()) {

src/storm/storage/prism/Program.h

@@ -31,7 +31,7 @@ namespace storm {
             /*!
              * An enum for the different model types.
              */
-            enum class ModelType {UNDEFINED, DTMC, CTMC, MDP, CTMDP, MA};
+            enum class ModelType {UNDEFINED, DTMC, CTMC, MDP, CTMDP, MA, POMDP};
             
             enum class ValidityCheckLevel  : unsigned {VALIDINPUT = 0, READYFORPROCESSING = 1};
             
@@ -85,6 +85,11 @@ namespace storm {
              */
             bool isDeterministicModel() const;
 
+            /*!
+             * Retrieves whether the model has restricted observability
+             */
+            bool isPartiallyObservable() const;
+
             /*!
              * Retrieves whether there are undefined constants of any type in the program.
              *

src/storm/storage/prism/Variable.cpp

@@ -5,11 +5,11 @@
 
 namespace storm {
     namespace prism {
-        Variable::Variable(storm::expressions::Variable const& variable, storm::expressions::Expression const& initialValueExpression, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), variable(variable), initialValueExpression(initialValueExpression) {
+        Variable::Variable(storm::expressions::Variable const& variable, storm::expressions::Expression const& initialValueExpression, bool observable, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), variable(variable), initialValueExpression(initialValueExpression), observable(observable) {
             // Nothing to do here.
         }
         
-        Variable::Variable(storm::expressions::ExpressionManager& manager, Variable const& oldVariable, std::string const& newName, std::map<storm::expressions::Variable, storm::expressions::Expression> const& renaming, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), variable(manager.declareVariable(newName, oldVariable.variable.getType())), initialValueExpression(oldVariable.getInitialValueExpression().substitute(renaming)) {
+        Variable::Variable(storm::expressions::ExpressionManager& manager, Variable const& oldVariable, std::string const& newName, std::map<storm::expressions::Variable, storm::expressions::Expression> const& renaming, bool observable, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), variable(manager.declareVariable(newName, oldVariable.variable.getType())), initialValueExpression(oldVariable.getInitialValueExpression().substitute(renaming)), observable(observable) {
             // Intentionally left empty.
         }
         
@@ -37,5 +37,9 @@ namespace storm {
             return variable.getExpression();
         }
 
+        bool Variable::isObservable() const {
+            return this->observable;
+        }
+        
     } // namespace prism
 } // namespace storm

src/storm/storage/prism/Variable.h

@@ -61,6 +61,11 @@ namespace storm {
              */
             storm::expressions::Expression getExpression() const;
 
+            /*!
+             * Retrieves whether the variable is observable.
+             */
+            bool isObservable() const;
+            
             /*!
              * Equips the variable with an initial value based on its type if not initial value is present.
              */
@@ -75,10 +80,11 @@ namespace storm {
              *
              * @param variable The associated expression variable.
              * @param initialValueExpression The constant expression that defines the initial value of the variable.
+             * @param observable Whether the variable is listed as observable
              * @param filename The filename in which the variable is defined.
              * @param lineNumber The line number in which the variable is defined.
              */
-            Variable(storm::expressions::Variable const& variable, storm::expressions::Expression const& initialValueExpression, std::string const& filename = "", uint_fast64_t lineNumber = 0);
+            Variable(storm::expressions::Variable const& variable, storm::expressions::Expression const& initialValueExpression, bool observable = false, std::string const& filename = "", uint_fast64_t lineNumber = 0);
             
             /*!
              * Creates a copy of the given variable and performs the provided renaming.
@@ -87,10 +93,11 @@ namespace storm {
              * @param oldVariable The variable to copy.
              * @param newName New name of this variable.
              * @param renaming A mapping from variables to the expressions with which they are to be replaced.
+             * @param observable Whether the variable is listed as observable
              * @param filename The filename in which the variable is defined.
              * @param lineNumber The line number in which the variable is defined.
              */
-            Variable(storm::expressions::ExpressionManager& manager, Variable const& oldVariable, std::string const& newName, std::map<storm::expressions::Variable, storm::expressions::Expression> const& renaming, std::string const& filename = "", uint_fast64_t lineNumber = 0);
+            Variable(storm::expressions::ExpressionManager& manager, Variable const& oldVariable, std::string const& newName, std::map<storm::expressions::Variable, storm::expressions::Expression> const& renaming, bool observable = false, std::string const& filename = "", uint_fast64_t lineNumber = 0);
             
         private:
             // The expression variable associated with this variable.
@@ -98,6 +105,9 @@ namespace storm {
             
             // The constant expression defining the initial value of the variable.
             storm::expressions::Expression initialValueExpression;
+
+            // Whether this variable is a so-called observable. If true, the variable is listed as observable
+            bool observable;
         };
         
     } // namespace prism

src/storm/utility/builder.cpp

@@ -4,6 +4,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"
 
 namespace storm {
@@ -19,6 +20,8 @@ namespace storm {
                         return std::make_shared<storm::models::sparse::Ctmc<ValueType, RewardModelType>>(std::move(components));
                     case storm::models::ModelType::Mdp:
                         return std::make_shared<storm::models::sparse::Mdp<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::MarkovAutomaton:
                         return std::make_shared<storm::models::sparse::MarkovAutomaton<ValueType, RewardModelType>>(std::move(components));
                     case storm::models::ModelType::S2pg: