From 863aebaa2a1e8dbd2fde4c62b4d0a5975483132d Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Fri, 7 Feb 2020 15:56:40 +0100 Subject: [PATCH] add flag for canonicity --- src/storm-pomdp/analysis/QualitativeAnalysis.cpp | 1 + .../transformer/ApplyFiniteSchedulerToPomdp.cpp | 1 + src/storm-pomdp/transformer/MakePOMDPCanonic.cpp | 2 +- src/storm/models/sparse/Pomdp.cpp | 10 ++++++++-- src/storm/models/sparse/Pomdp.h | 8 ++++++-- 5 files changed, 17 insertions(+), 5 deletions(-) diff --git a/src/storm-pomdp/analysis/QualitativeAnalysis.cpp b/src/storm-pomdp/analysis/QualitativeAnalysis.cpp index 09e2cf496..8eb39e5fb 100644 --- a/src/storm-pomdp/analysis/QualitativeAnalysis.cpp +++ b/src/storm-pomdp/analysis/QualitativeAnalysis.cpp @@ -30,6 +30,7 @@ namespace storm { template storm::storage::BitVector QualitativeAnalysis::analyseProb0or1(storm::logic::ProbabilityOperatorFormula const& formula, bool prob0) const { // check whether the property is minimizing or maximizing + STORM_LOG_THROW(pomdp.isCanonic(), storm::exceptions::IllegalArgumentException, "POMDP needs to be canonic"); STORM_LOG_THROW(formula.hasOptimalityType() || formula.hasBound(), storm::exceptions::InvalidPropertyException, "The formula " << formula << " does not specify whether to minimize or maximize."); bool minimizes = (formula.hasOptimalityType() && storm::solver::minimize(formula.getOptimalityType())) || (formula.hasBound() && storm::logic::isLowerBound(formula.getBound().comparisonType)); diff --git a/src/storm-pomdp/transformer/ApplyFiniteSchedulerToPomdp.cpp b/src/storm-pomdp/transformer/ApplyFiniteSchedulerToPomdp.cpp index 8f432bb2e..1757598ce 100644 --- a/src/storm-pomdp/transformer/ApplyFiniteSchedulerToPomdp.cpp +++ b/src/storm-pomdp/transformer/ApplyFiniteSchedulerToPomdp.cpp @@ -70,6 +70,7 @@ namespace storm { template std::shared_ptr> ApplyFiniteSchedulerToPomdp::transform(PomdpFscApplicationMode applicationMode ) const { + STORM_LOG_THROW(pomdp.isCanonic(), storm::exceptions::IllegalArgumentException, "POMDP needs to be canonic"); storm::storage::sparse::ModelComponents modelComponents; uint64_t nrStates = pomdp.getNumberOfStates(); diff --git a/src/storm-pomdp/transformer/MakePOMDPCanonic.cpp b/src/storm-pomdp/transformer/MakePOMDPCanonic.cpp index ec172ae44..da03d47ca 100644 --- a/src/storm-pomdp/transformer/MakePOMDPCanonic.cpp +++ b/src/storm-pomdp/transformer/MakePOMDPCanonic.cpp @@ -137,7 +137,7 @@ namespace storm { false, boost::none); modelcomponents.observabilityClasses = pomdp.getObservations(); //modelcomponents.choiceLabeling = pomdp.getChoiceLabeling(); - return std::make_shared>(modelcomponents); + return std::make_shared>(modelcomponents, true); } diff --git a/src/storm/models/sparse/Pomdp.cpp b/src/storm/models/sparse/Pomdp.cpp index b3930822c..02293dba8 100644 --- a/src/storm/models/sparse/Pomdp.cpp +++ b/src/storm/models/sparse/Pomdp.cpp @@ -15,12 +15,12 @@ namespace storm { } template - Pomdp::Pomdp(storm::storage::sparse::ModelComponents const &components) : Mdp(components, storm::models::ModelType::Pomdp), observations(components.observabilityClasses.get()) { + Pomdp::Pomdp(storm::storage::sparse::ModelComponents const &components, bool canonicFlag) : Mdp(components, storm::models::ModelType::Pomdp), observations(components.observabilityClasses.get()), canonicFlag(canonicFlag) { computeNrObservations(); } template - Pomdp::Pomdp(storm::storage::sparse::ModelComponents &&components): Mdp(components, storm::models::ModelType::Pomdp), observations(components.observabilityClasses.get()) { + Pomdp::Pomdp(storm::storage::sparse::ModelComponents &&components, bool canonicFlag): Mdp(components, storm::models::ModelType::Pomdp), observations(components.observabilityClasses.get()), canonicFlag(canonicFlag) { computeNrObservations(); } @@ -59,6 +59,12 @@ namespace storm { return observations; } + template + bool Pomdp::isCanonic() const { + return canonicFlag; + }; + + diff --git a/src/storm/models/sparse/Pomdp.h b/src/storm/models/sparse/Pomdp.h index de77ef6f0..b50f41fa2 100644 --- a/src/storm/models/sparse/Pomdp.h +++ b/src/storm/models/sparse/Pomdp.h @@ -41,9 +41,9 @@ namespace storm { * * @param components The components for this model. */ - Pomdp(storm::storage::sparse::ModelComponents const &components); + Pomdp(storm::storage::sparse::ModelComponents const &components, bool canonicFlag = false); - Pomdp(storm::storage::sparse::ModelComponents &&components); + Pomdp(storm::storage::sparse::ModelComponents &&components, bool canonicFlag = false ); Pomdp(Pomdp const &other) = default; @@ -61,6 +61,8 @@ namespace storm { std::vector const& getObservations() const; + bool isCanonic() const; + protected: @@ -69,6 +71,8 @@ namespace storm { uint64_t nrObservations; + bool canonicFlag = false; + void computeNrObservations(); }; }