add flag for canonicity

src/storm-pomdp/analysis/QualitativeAnalysis.cpp

@@ -30,6 +30,7 @@ namespace storm {
         template<typename ValueType>
         storm::storage::BitVector QualitativeAnalysis<ValueType>::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));
             

src/storm-pomdp/transformer/ApplyFiniteSchedulerToPomdp.cpp

@@ -70,6 +70,7 @@ namespace storm {
 
         template<typename ValueType>
         std::shared_ptr<storm::models::sparse::Model<storm::RationalFunction>> ApplyFiniteSchedulerToPomdp<ValueType>::transform(PomdpFscApplicationMode applicationMode ) const {
+            STORM_LOG_THROW(pomdp.isCanonic(), storm::exceptions::IllegalArgumentException, "POMDP needs to be canonic");
             storm::storage::sparse::ModelComponents<storm::RationalFunction> modelComponents;
 
             uint64_t nrStates = pomdp.getNumberOfStates();

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<storm::models::sparse::Pomdp<ValueType>>(modelcomponents);
+            return std::make_shared<storm::models::sparse::Pomdp<ValueType>>(modelcomponents, true);
         }
 
 

src/storm/models/sparse/Pomdp.cpp

@@ -15,12 +15,12 @@ namespace storm {
             }
 
             template <typename ValueType, typename RewardModelType>
-            Pomdp<ValueType, RewardModelType>::Pomdp(storm::storage::sparse::ModelComponents<ValueType, RewardModelType> const &components) : Mdp<ValueType, RewardModelType>(components, storm::models::ModelType::Pomdp), observations(components.observabilityClasses.get()) {
+            Pomdp<ValueType, RewardModelType>::Pomdp(storm::storage::sparse::ModelComponents<ValueType, RewardModelType> const &components, bool canonicFlag) : Mdp<ValueType, RewardModelType>(components, storm::models::ModelType::Pomdp), observations(components.observabilityClasses.get()), canonicFlag(canonicFlag)  {
                 computeNrObservations();
             }
 
             template <typename ValueType, typename RewardModelType>
-            Pomdp<ValueType, RewardModelType>::Pomdp(storm::storage::sparse::ModelComponents<ValueType, RewardModelType> &&components): Mdp<ValueType, RewardModelType>(components, storm::models::ModelType::Pomdp), observations(components.observabilityClasses.get()) {
+            Pomdp<ValueType, RewardModelType>::Pomdp(storm::storage::sparse::ModelComponents<ValueType, RewardModelType> &&components, bool canonicFlag): Mdp<ValueType, RewardModelType>(components, storm::models::ModelType::Pomdp), observations(components.observabilityClasses.get()), canonicFlag(canonicFlag) {
                 computeNrObservations();
             }
 
@@ -59,6 +59,12 @@ namespace storm {
                 return observations;
             }
 
+            template<typename ValueType, typename RewardModelType>
+            bool Pomdp<ValueType, RewardModelType>::isCanonic() const {
+                return canonicFlag;
+            };
+
+
 
 
 

src/storm/models/sparse/Pomdp.h

@@ -41,9 +41,9 @@ namespace storm {
                  *
                  * @param components The components for this model.
                  */
-                Pomdp(storm::storage::sparse::ModelComponents<ValueType, RewardModelType> const &components);
+                Pomdp(storm::storage::sparse::ModelComponents<ValueType, RewardModelType> const &components, bool canonicFlag = false);
 
-                Pomdp(storm::storage::sparse::ModelComponents<ValueType, RewardModelType> &&components);
+                Pomdp(storm::storage::sparse::ModelComponents<ValueType, RewardModelType> &&components, bool canonicFlag = false );
 
                 Pomdp(Pomdp <ValueType, RewardModelType> const &other) = default;
 
@@ -61,6 +61,8 @@ namespace storm {
 
                 std::vector<uint32_t> const& getObservations() const;
 
+                bool isCanonic() const;
+
 
 
             protected:
@@ -69,6 +71,8 @@ namespace storm {
 
                 uint64_t nrObservations;
 
+                bool canonicFlag = false;
+
                 void computeNrObservations();
             };
         }