From 63fd02937f9e0ee25e01abe59e9d01a18abe4644 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Thu, 17 Aug 2017 13:44:57 +0200 Subject: [PATCH] pomdps --- src/storm/api/builder.h | 3 +++ src/storm/models/sparse/Mdp.cpp | 18 ++++++++++-------- src/storm/models/sparse/Mdp.h | 8 ++++---- src/storm/models/sparse/Model.cpp | 2 +- src/storm/models/sparse/Pomdp.cpp | 8 ++++---- src/storm/parser/PrismParser.cpp | 20 +++++++++++++++++--- src/storm/parser/PrismParser.h | 6 ++++-- 7 files changed, 43 insertions(+), 22 deletions(-) diff --git a/src/storm/api/builder.h b/src/storm/api/builder.h index ca21f99fc..fb7556776 100644 --- a/src/storm/api/builder.h +++ b/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>(std::move(components)); case storm::models::ModelType::MarkovAutomaton: return std::make_shared>(std::move(components)); + case storm::models::ModelType::Pomdp: + return std::make_shared>(std::move(components)); case storm::models::ModelType::S2pg: return std::make_shared>(std::move(components)); } diff --git a/src/storm/models/sparse/Mdp.cpp b/src/storm/models/sparse/Mdp.cpp index fdb49f89d..ef802d5ac 100644 --- a/src/storm/models/sparse/Mdp.cpp +++ b/src/storm/models/sparse/Mdp.cpp @@ -13,27 +13,29 @@ namespace storm { template Mdp::Mdp(storm::storage::SparseMatrix const& transitionMatrix, storm::models::sparse::StateLabeling const& stateLabeling, - std::unordered_map const& rewardModels) - : Mdp(storm::storage::sparse::ModelComponents(transitionMatrix, stateLabeling, rewardModels)) { + std::unordered_map const& rewardModels, ModelType type) + : Mdp(storm::storage::sparse::ModelComponents(transitionMatrix, stateLabeling, rewardModels), type) { // Intentionally left empty } template Mdp::Mdp(storm::storage::SparseMatrix&& transitionMatrix, storm::models::sparse::StateLabeling&& stateLabeling, - std::unordered_map&& rewardModels) - : Mdp(storm::storage::sparse::ModelComponents(std::move(transitionMatrix), std::move(stateLabeling), std::move(rewardModels))) { + std::unordered_map&& rewardModels, ModelType type) + : Mdp(storm::storage::sparse::ModelComponents(std::move(transitionMatrix), std::move(stateLabeling), std::move(rewardModels)), type) { // Intentionally left empty } template - Mdp::Mdp(storm::storage::sparse::ModelComponents const& components) - : NondeterministicModel(storm::models::ModelType::Mdp, components) { + Mdp::Mdp(storm::storage::sparse::ModelComponents const& components, ModelType type) + : NondeterministicModel(type, components) { + assert(type == storm::models::ModelType::Mdp || type == storm::models::ModelType::Pomdp); // Intentionally left empty } template - Mdp::Mdp(storm::storage::sparse::ModelComponents&& components) - : NondeterministicModel(storm::models::ModelType::Mdp, std::move(components)) { + Mdp::Mdp(storm::storage::sparse::ModelComponents&& components, ModelType type) + : NondeterministicModel(type, std::move(components)) { + assert(type == storm::models::ModelType::Mdp || type == storm::models::ModelType::Pomdp); // Intentionally left empty } diff --git a/src/storm/models/sparse/Mdp.h b/src/storm/models/sparse/Mdp.h index e65770275..60d1a6b63 100644 --- a/src/storm/models/sparse/Mdp.h +++ b/src/storm/models/sparse/Mdp.h @@ -24,7 +24,7 @@ namespace storm { */ Mdp(storm::storage::SparseMatrix const& transitionMatrix, storm::models::sparse::StateLabeling const& stateLabeling, - std::unordered_map const& rewardModels = std::unordered_map()); + std::unordered_map const& rewardModels = std::unordered_map(), ModelType type = ModelType::Mdp); /*! * Constructs a model by moving the given data. @@ -35,15 +35,15 @@ namespace storm { */ Mdp(storm::storage::SparseMatrix&& transitionMatrix, storm::models::sparse::StateLabeling&& stateLabeling, - std::unordered_map&& rewardModels = std::unordered_map()); + std::unordered_map&& rewardModels = std::unordered_map(), ModelType type = ModelType::Mdp); /*! * Constructs a model from the given data. * * @param components The components for this model. */ - Mdp(storm::storage::sparse::ModelComponents const& components); - Mdp(storm::storage::sparse::ModelComponents&& components); + Mdp(storm::storage::sparse::ModelComponents const& components, ModelType type = ModelType::Mdp); + Mdp(storm::storage::sparse::ModelComponents&& components, ModelType type = ModelType::Mdp); Mdp(Mdp const& other) = default; Mdp& operator=(Mdp const& other) = default; diff --git a/src/storm/models/sparse/Model.cpp b/src/storm/models/sparse/Model.cpp index a1ca205a7..55bd9abab 100644 --- a/src/storm/models/sparse/Model.cpp +++ b/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)."); diff --git a/src/storm/models/sparse/Pomdp.cpp b/src/storm/models/sparse/Pomdp.cpp index 9adaf72ca..182374fac 100644 --- a/src/storm/models/sparse/Pomdp.cpp +++ b/src/storm/models/sparse/Pomdp.cpp @@ -5,22 +5,22 @@ namespace storm { 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) { + Pomdp::Pomdp(storm::storage::SparseMatrix const &transitionMatrix, storm::models::sparse::StateLabeling const &stateLabeling, std::unordered_map const &rewardModels) : Mdp(transitionMatrix, stateLabeling, rewardModels, storm::models::ModelType::Pomdp) { // Intentionally left blank. } template - Pomdp::Pomdp(storm::storage::SparseMatrix &&transitionMatrix, storm::models::sparse::StateLabeling &&stateLabeling, std::unordered_map &&rewardModels) : Mdp(transitionMatrix, stateLabeling, rewardModels) { + Pomdp::Pomdp(storm::storage::SparseMatrix &&transitionMatrix, storm::models::sparse::StateLabeling &&stateLabeling, std::unordered_map &&rewardModels) : Mdp(transitionMatrix, stateLabeling, rewardModels, storm::models::ModelType::Pomdp) { // Intentionally left empty. } template - Pomdp::Pomdp(storm::storage::sparse::ModelComponents const &components) : Mdp(components) { + Pomdp::Pomdp(storm::storage::sparse::ModelComponents const &components) : Mdp(components, storm::models::ModelType::Pomdp) { } template - Pomdp::Pomdp(storm::storage::sparse::ModelComponents &&components): Mdp(components) { + Pomdp::Pomdp(storm::storage::sparse::ModelComponents &&components): Mdp(components, storm::models::ModelType::Pomdp) { } diff --git a/src/storm/parser/PrismParser.cpp b/src/storm/parser/PrismParser.cpp index a32f0eb81..ab850fb4d 100644 --- a/src/storm/parser/PrismParser.cpp +++ b/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 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 const& booleanVariables, std::vector const& integerVariables, std::vector const& commands, GlobalProgramInformation& globalProgramInformation) const { globalProgramInformation.moduleToIndexMap[moduleName] = globalProgramInformation.modules.size(); diff --git a/src/storm/parser/PrismParser.h b/src/storm/parser/PrismParser.h index d220361f8..7c26b9f8c 100644 --- a/src/storm/parser/PrismParser.h +++ b/src/storm/parser/PrismParser.h @@ -161,7 +161,7 @@ namespace storm { */ std::string const& getFilename() const; - std::vector observables; + mutable std::set observables; // A function used for annotating the entities with their position. phoenix::function annotate; @@ -282,7 +282,9 @@ namespace storm { storm::prism::Module createModule(std::string const& moduleName, std::vector const& booleanVariables, std::vector const& integerVariables, std::vector const& commands, GlobalProgramInformation& globalProgramInformation) const; storm::prism::Module createRenamedModule(std::string const& newModuleName, std::string const& oldModuleName, std::map const& renaming, GlobalProgramInformation& globalProgramInformation) const; storm::prism::Program createProgram(GlobalProgramInformation const& globalProgramInformation) const; - + void createObservablesList(std::vector const& observables); + + void removeInitialConstruct(GlobalProgramInformation& globalProgramInformation) const; // An error handler function.