From bbb4d16965c657cfabec16677057969a39f50a5f Mon Sep 17 00:00:00 2001 From: sjunges Date: Thu, 17 Aug 2017 00:03:53 +0200 Subject: [PATCH] towards support for pomdps in storm --- src/storm/builder/ExplicitModelBuilder.cpp | 2 + .../generator/JaniNextStateGenerator.cpp | 5 ++ src/storm/generator/JaniNextStateGenerator.h | 1 + src/storm/generator/NextStateGenerator.h | 4 +- .../generator/PrismNextStateGenerator.cpp | 6 ++ src/storm/generator/PrismNextStateGenerator.h | 1 + src/storm/models/sparse/Mdp.cpp | 3 - src/storm/models/sparse/Pomdp.cpp | 35 +++++++++++ src/storm/models/sparse/Pomdp.h | 61 +++++++++++++++++++ src/storm/parser/PrismParser.cpp | 24 +++++--- src/storm/parser/PrismParser.h | 43 +++++++------ src/storm/storage/prism/BooleanVariable.cpp | 4 +- src/storm/storage/prism/BooleanVariable.h | 2 +- src/storm/storage/prism/IntegerVariable.cpp | 4 +- src/storm/storage/prism/IntegerVariable.h | 2 +- src/storm/storage/prism/Program.cpp | 8 ++- src/storm/storage/prism/Program.h | 7 ++- src/storm/storage/prism/Variable.cpp | 8 ++- src/storm/storage/prism/Variable.h | 14 ++++- src/storm/utility/builder.cpp | 3 + 20 files changed, 194 insertions(+), 43 deletions(-) create mode 100644 src/storm/models/sparse/Pomdp.cpp create mode 100644 src/storm/models/sparse/Pomdp.h diff --git a/src/storm/builder/ExplicitModelBuilder.cpp b/src/storm/builder/ExplicitModelBuilder.cpp index 9de544e7b..34c56ca04 100644 --- a/src/storm/builder/ExplicitModelBuilder.cpp +++ b/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: diff --git a/src/storm/generator/JaniNextStateGenerator.cpp b/src/storm/generator/JaniNextStateGenerator.cpp index f7d86e914..9df0d1f5e 100644 --- a/src/storm/generator/JaniNextStateGenerator.cpp +++ b/src/storm/generator/JaniNextStateGenerator.cpp @@ -133,6 +133,11 @@ namespace storm { bool JaniNextStateGenerator::isDiscreteTimeModel() const { return model.isDiscreteTimeModel(); } + + template + bool JaniNextStateGenerator::isPartiallyObservable() const { + return false; + }; template uint64_t JaniNextStateGenerator::getLocation(CompressedState const& state, LocationVariableInformation const& locationVariable) const { diff --git a/src/storm/generator/JaniNextStateGenerator.h b/src/storm/generator/JaniNextStateGenerator.h index 3fcfc2777..0e7e52689 100644 --- a/src/storm/generator/JaniNextStateGenerator.h +++ b/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 getInitialStates(StateToIdCallback const& stateToIdCallback) override; virtual StateBehavior expand(StateToIdCallback const& stateToIdCallback) override; diff --git a/src/storm/generator/NextStateGenerator.h b/src/storm/generator/NextStateGenerator.h index 25335dbfc..678584730 100644 --- a/src/storm/generator/NextStateGenerator.h +++ b/src/storm/generator/NextStateGenerator.h @@ -28,7 +28,8 @@ namespace storm { DTMC, CTMC, MDP, - MA + MA, + POMDP }; template @@ -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 getInitialStates(StateToIdCallback const& stateToIdCallback) = 0; void load(CompressedState const& state); diff --git a/src/storm/generator/PrismNextStateGenerator.cpp b/src/storm/generator/PrismNextStateGenerator.cpp index 6b80e8c52..6ea2612c4 100644 --- a/src/storm/generator/PrismNextStateGenerator.cpp +++ b/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."); } @@ -131,6 +132,11 @@ namespace storm { bool PrismNextStateGenerator::isDiscreteTimeModel() const { return program.isDiscreteTimeModel(); } + + template + bool PrismNextStateGenerator::isPartiallyObservable() const { + return program.isPartiallyObservable(); + } template std::vector PrismNextStateGenerator::getInitialStates(StateToIdCallback const& stateToIdCallback) { diff --git a/src/storm/generator/PrismNextStateGenerator.h b/src/storm/generator/PrismNextStateGenerator.h index 0097e7055..e5e46d1c5 100644 --- a/src/storm/generator/PrismNextStateGenerator.h +++ b/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 getInitialStates(StateToIdCallback const& stateToIdCallback) override; virtual StateBehavior expand(StateToIdCallback const& stateToIdCallback) override; diff --git a/src/storm/models/sparse/Mdp.cpp b/src/storm/models/sparse/Mdp.cpp index 38226702d..fdb49f89d 100644 --- a/src/storm/models/sparse/Mdp.cpp +++ b/src/storm/models/sparse/Mdp.cpp @@ -60,13 +60,10 @@ namespace storm { } template class Mdp; - -#ifdef STORM_HAVE_CARL template class Mdp; template class Mdp>; template class Mdp; -#endif } // namespace sparse } // namespace models } // namespace storm diff --git a/src/storm/models/sparse/Pomdp.cpp b/src/storm/models/sparse/Pomdp.cpp new file mode 100644 index 000000000..9adaf72ca --- /dev/null +++ b/src/storm/models/sparse/Pomdp.cpp @@ -0,0 +1,35 @@ +#include "storm/models/sparse/Pomdp.h" + +namespace storm { + namespace models { + namespace sparse { + + template + Pomdp::Pomdp(storm::storage::SparseMatrix const &transitionMatrix, storm::models::sparse::StateLabeling const &stateLabeling, std::unordered_map const &rewardModels) : Mdp(transitionMatrix, stateLabeling, rewardModels) { + // Intentionally left blank. + } + + template + Pomdp::Pomdp(storm::storage::SparseMatrix &&transitionMatrix, storm::models::sparse::StateLabeling &&stateLabeling, std::unordered_map &&rewardModels) : Mdp(transitionMatrix, stateLabeling, rewardModels) { + // Intentionally left empty. + } + + template + Pomdp::Pomdp(storm::storage::sparse::ModelComponents const &components) : Mdp(components) { + + } + + template + Pomdp::Pomdp(storm::storage::sparse::ModelComponents &&components): Mdp(components) { + + } + + + template class Pomdp; + template class Pomdp; + template class Pomdp>; + template class Pomdp; + + } + } +} \ No newline at end of file diff --git a/src/storm/models/sparse/Pomdp.h b/src/storm/models/sparse/Pomdp.h new file mode 100644 index 000000000..c981562e0 --- /dev/null +++ b/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 Pomdp : public Mdp { + 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 const &transitionMatrix, + storm::models::sparse::StateLabeling const &stateLabeling, + std::unordered_map const &rewardModels = std::unordered_map()); + + /*! + * 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 &&transitionMatrix, + storm::models::sparse::StateLabeling &&stateLabeling, + std::unordered_map &&rewardModels = std::unordered_map()); + + /*! + * Constructs a model from the given data. + * + * @param components The components for this model. + */ + Pomdp(storm::storage::sparse::ModelComponents const &components); + + Pomdp(storm::storage::sparse::ModelComponents &&components); + + Pomdp(Pomdp const &other) = default; + + Pomdp &operator=(Pomdp const &other) = default; + + Pomdp(Pomdp &&other) = default; + + Pomdp &operator=(Pomdp &&other) = default; + + protected: + StateLabeling observations; + }; + } + } +} diff --git a/src/storm/parser/PrismParser.cpp b/src/storm/parser/PrismParser.cpp index 0230fbaca..a32f0eb81 100644 --- a/src/storm/parser/PrismParser.cpp +++ b/src/storm/parser/PrismParser.cpp @@ -83,6 +83,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"); @@ -142,6 +144,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 const& booleanVariables, std::vector const& integerVariables, std::vector 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. diff --git a/src/storm/parser/PrismParser.h b/src/storm/parser/PrismParser.h index f285c5cc9..d220361f8 100644 --- a/src/storm/parser/PrismParser.h +++ b/src/storm/parser/PrismParser.h @@ -44,6 +44,7 @@ namespace storm { bool hasInitialConstruct; storm::prism::InitialConstruct initialConstruct; boost::optional systemCompositionConstruct; + // Counters to provide unique indexing for commands and updates. uint_fast64_t currentCommandIndex; @@ -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); } }; @@ -157,7 +160,9 @@ namespace storm { * @return The name of the file currently being parsed. */ std::string const& getFilename() const; - + + std::vector observables; + // A function used for annotating the entities with their position. phoenix::function annotate; @@ -207,7 +212,9 @@ namespace storm { // Rules for initial states expression. qi::rule initialStatesConstruct; - + + qi::rule observablesConstruct; + // Rules for the system composition. qi::rule systemCompositionConstruct; qi::rule(), Skipper> parallelComposition; diff --git a/src/storm/storage/prism/BooleanVariable.cpp b/src/storm/storage/prism/BooleanVariable.cpp index 4207f91fb..c3b3d3431 100644 --- a/src/storm/storage/prism/BooleanVariable.cpp +++ b/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 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() { diff --git a/src/storm/storage/prism/BooleanVariable.h b/src/storm/storage/prism/BooleanVariable.h index 80b9ca51e..acdc9865f 100644 --- a/src/storm/storage/prism/BooleanVariable.h +++ b/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. diff --git a/src/storm/storage/prism/IntegerVariable.cpp b/src/storm/storage/prism/IntegerVariable.cpp index 5a67dd1bd..d53ea618b 100644 --- a/src/storm/storage/prism/IntegerVariable.cpp +++ b/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 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() { diff --git a/src/storm/storage/prism/IntegerVariable.h b/src/storm/storage/prism/IntegerVariable.h index 3ddfd03e7..67618f6eb 100644 --- a/src/storm/storage/prism/IntegerVariable.h +++ b/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. diff --git a/src/storm/storage/prism/Program.cpp b/src/storm/storage/prism/Program.cpp index a87ea5888..fce0c6682 100644 --- a/src/storm/storage/prism/Program.cpp +++ b/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()) { diff --git a/src/storm/storage/prism/Program.h b/src/storm/storage/prism/Program.h index a92fdcbb6..b921b00ed 100644 --- a/src/storm/storage/prism/Program.h +++ b/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. * diff --git a/src/storm/storage/prism/Variable.cpp b/src/storm/storage/prism/Variable.cpp index 656b9566f..9eba111b0 100644 --- a/src/storm/storage/prism/Variable.cpp +++ b/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 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 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. } @@ -36,6 +36,10 @@ namespace storm { storm::expressions::Expression Variable::getExpression() const { return variable.getExpression(); } + + bool Variable::isObservable() const { + return this->observable; + } } // namespace prism } // namespace storm diff --git a/src/storm/storage/prism/Variable.h b/src/storm/storage/prism/Variable.h index 42ba9aec0..ae9cfcc37 100644 --- a/src/storm/storage/prism/Variable.h +++ b/src/storm/storage/prism/Variable.h @@ -60,6 +60,11 @@ namespace storm { * @return The expression associated with this variable. */ 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 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 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 diff --git a/src/storm/utility/builder.cpp b/src/storm/utility/builder.cpp index 9ace27060..a6b85e9b1 100644 --- a/src/storm/utility/builder.cpp +++ b/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>(std::move(components)); case storm::models::ModelType::Mdp: return std::make_shared>(std::move(components)); + case storm::models::ModelType::Pomdp: + return std::make_shared>(std::move(components)); case storm::models::ModelType::MarkovAutomaton: return std::make_shared>(std::move(components)); case storm::models::ModelType::S2pg: