storm parses and builds pomdps

src/storm/builder/ExplicitModelBuilder.cpp

@@ -328,7 +328,14 @@ namespace storm {
                 auto originData = choiceInformationBuilder.buildDataOfChoiceOrigins(modelComponents.transitionMatrix.getRowCount());
                 modelComponents.choiceOrigins = generator->generateChoiceOrigins(originData);
             }
-            
+            if (generator->isPartiallyObservable()) {
+                std::vector<uint32_t> classes;
+                classes.resize(stateStorage.getNumberOfStates());
+                for (auto const& bitVectorIndexPair : stateStorage.stateToId) {
+                    classes[bitVectorIndexPair.second] = generator->observabilityClass(bitVectorIndexPair.first);
+                }
+                modelComponents.observabilityClasses = classes;
+            }
             return modelComponents;
         }
         

src/storm/generator/CompressedState.cpp

@@ -43,6 +43,46 @@ namespace storm {
             return result;
         }
 
+        storm::storage::BitVector computeObservabilityMask(VariableInformation const& variableInformation) {
+            storm::storage::BitVector result(variableInformation.getTotalBitOffset(true));
+            for (auto const& locationVariable : variableInformation.locationVariables) {
+                if (locationVariable.observable) {
+                    for (uint64_t i = locationVariable.bitOffset; i < locationVariable.bitOffset + locationVariable.bitWidth; ++i) {
+                        result.set(i, true);
+                    }
+                }
+            }
+
+            for (auto const& booleanVariable : variableInformation.booleanVariables) {
+                if (booleanVariable.observable) {
+                    result.set(booleanVariable.bitOffset, true);
+                }
+            }
+
+            for (auto const& integerVariable : variableInformation.integerVariables) {
+                if (integerVariable.observable) {
+                    for (uint64_t i = integerVariable.bitOffset; i < integerVariable.bitOffset + integerVariable.bitWidth; ++i) {
+                        result.set(i, true);
+                    }
+                }
+            }
+            return result;
+        }
+
+        uint32_t unpackStateToObservabilityClass(CompressedState const& state, std::unordered_map<storm::storage::BitVector,uint32_t>& observabilityMap, storm::storage::BitVector const& mask) {
+            STORM_LOG_ASSERT(state.size() == mask.size(), "Mask should be as long as state.");
+            storm::storage::BitVector observeClass = state & mask;
+            auto it = observabilityMap.find(observeClass);
+            if (it != observabilityMap.end()) {
+                return it->second;
+            } else {
+                uint32_t newClassIndex = observabilityMap.size();
+                observabilityMap.emplace(observeClass, newClassIndex);
+                return newClassIndex;
+            }
+        }
+
+
         template void unpackStateIntoEvaluator<double>(CompressedState const& state, VariableInformation const& variableInformation, storm::expressions::ExpressionEvaluator<double>& evaluator);
         storm::expressions::SimpleValuation unpackStateIntoValuation(CompressedState const& state, VariableInformation const& variableInformation, storm::expressions::ExpressionManager const& manager);
 

src/storm/generator/CompressedState.h

@@ -2,6 +2,7 @@
 #define STORM_GENERATOR_COMPRESSEDSTATE_H_
 
 #include "storm/storage/BitVector.h"
+#include <unordered_map>
 
 namespace storm {
     namespace expressions {
@@ -12,7 +13,6 @@ namespace storm {
     }
     
     namespace generator {
-        
         typedef storm::storage::BitVector CompressedState;
 
         struct VariableInformation;
@@ -36,6 +36,10 @@ namespace storm {
          * @return A valuation that corresponds to the compressed state.
          */
         storm::expressions::SimpleValuation unpackStateIntoValuation(CompressedState const& state, VariableInformation const& variableInformation, storm::expressions::ExpressionManager const& manager);
+
+        storm::storage::BitVector computeObservabilityMask(VariableInformation const& variableInformation);
+        uint32_t unpackStateToObservabilityClass(CompressedState const& state, std::unordered_map<storm::storage::BitVector,uint32_t>& observabilityMap, storm::storage::BitVector const& mask);
+
     }
 }
 

src/storm/generator/NextStateGenerator.cpp

@@ -154,6 +154,17 @@ namespace storm {
             return nullptr;
         }
 
+        template<typename ValueType, typename StateType>
+        uint32_t NextStateGenerator<ValueType, StateType>::observabilityClass(CompressedState const &state) const {
+            if (this->mask.size() == 0) {
+                this->mask = computeObservabilityMask(variableInformation);
+                std::cout << mask.size() << std::endl;
+            }
+            std::cout << state.size() << std::endl;
+
+            return unpackStateToObservabilityClass(state, observabilityMap, mask);
+        }
+
         template class NextStateGenerator<double>;
 
 #ifdef STORM_HAVE_CARL

src/storm/generator/NextStateGenerator.h

@@ -62,7 +62,9 @@ namespace storm {
             virtual storm::builder::RewardModelInformation getRewardModelInformation(uint64_t const& index) const = 0;
             
             storm::expressions::SimpleValuation toValuation(CompressedState const& state) const;
-            
+
+            uint32 observabilityClass(CompressedState const& state) const;
+
             virtual storm::models::sparse::StateLabeling label(storm::storage::BitVectorHashMap<StateType> const& states, std::vector<StateType> const& initialStateIndices = {}, std::vector<StateType> const& deadlockStateIndices = {}) = 0;
             
             NextStateGeneratorOptions const& getOptions() const;
@@ -97,6 +99,13 @@ namespace storm {
             
             /// A comparator used to compare constants.
             storm::utility::ConstantsComparator<ValueType> comparator;
+
+            /// The mask to compute the observability class (Constructed upon first use)
+            mutable storm::storage::BitVector mask;
+
+            /// The observability classes handed out so far.
+            // TODO consider using a BitVectorHashMap for this?
+            mutable std::unordered_map<storm::storage::BitVector, uint32_t> observabilityMap;
         };
     }
 }

src/storm/generator/VariableInformation.cpp

@@ -17,40 +17,40 @@
 namespace storm {
     namespace generator {
         
-        BooleanVariableInformation::BooleanVariableInformation(storm::expressions::Variable const& variable, uint_fast64_t bitOffset, bool global) : variable(variable), bitOffset(bitOffset), global(global) {
+        BooleanVariableInformation::BooleanVariableInformation(storm::expressions::Variable const& variable, uint_fast64_t bitOffset, bool global, bool observable) : variable(variable), bitOffset(bitOffset), global(global), observable(observable) {
             // Intentionally left empty.
         }
         
-        IntegerVariableInformation::IntegerVariableInformation(storm::expressions::Variable const& variable, int_fast64_t lowerBound, int_fast64_t upperBound, uint_fast64_t bitOffset, uint_fast64_t bitWidth, bool global) : variable(variable), lowerBound(lowerBound), upperBound(upperBound), bitOffset(bitOffset), bitWidth(bitWidth), global(global) {
+        IntegerVariableInformation::IntegerVariableInformation(storm::expressions::Variable const& variable, int_fast64_t lowerBound, int_fast64_t upperBound, uint_fast64_t bitOffset, uint_fast64_t bitWidth, bool global, bool observable) : variable(variable), lowerBound(lowerBound), upperBound(upperBound), bitOffset(bitOffset), bitWidth(bitWidth), global(global), observable(observable) {
             // Intentionally left empty.
         }
         
-        LocationVariableInformation::LocationVariableInformation(storm::expressions::Variable const& variable, uint64_t highestValue, uint_fast64_t bitOffset, uint_fast64_t bitWidth) : variable(variable), highestValue(highestValue), bitOffset(bitOffset), bitWidth(bitWidth) {
+        LocationVariableInformation::LocationVariableInformation(storm::expressions::Variable const& variable, uint64_t highestValue, uint_fast64_t bitOffset, uint_fast64_t bitWidth, bool observable) : variable(variable), highestValue(highestValue), bitOffset(bitOffset), bitWidth(bitWidth), observable(observable) {
             // Intentionally left empty.
         }
         
         VariableInformation::VariableInformation(storm::prism::Program const& program) : totalBitOffset(0) {
             for (auto const& booleanVariable : program.getGlobalBooleanVariables()) {
-                booleanVariables.emplace_back(booleanVariable.getExpressionVariable(), totalBitOffset, true);
+                booleanVariables.emplace_back(booleanVariable.getExpressionVariable(), totalBitOffset, true, booleanVariable.isObservable());
                 ++totalBitOffset;
             }
             for (auto const& integerVariable : program.getGlobalIntegerVariables()) {
                 int_fast64_t lowerBound = integerVariable.getLowerBoundExpression().evaluateAsInt();
                 int_fast64_t upperBound = integerVariable.getUpperBoundExpression().evaluateAsInt();
                 uint_fast64_t bitwidth = static_cast<uint_fast64_t>(std::ceil(std::log2(upperBound - lowerBound + 1)));
-                integerVariables.emplace_back(integerVariable.getExpressionVariable(), lowerBound, upperBound, totalBitOffset, bitwidth, true);
+                integerVariables.emplace_back(integerVariable.getExpressionVariable(), lowerBound, upperBound, totalBitOffset, bitwidth, true, integerVariable.isObservable());
                 totalBitOffset += bitwidth;
             }
             for (auto const& module : program.getModules()) {
                 for (auto const& booleanVariable : module.getBooleanVariables()) {
-                    booleanVariables.emplace_back(booleanVariable.getExpressionVariable(), totalBitOffset);
+                    booleanVariables.emplace_back(booleanVariable.getExpressionVariable(), totalBitOffset, false, booleanVariable.isObservable());
                     ++totalBitOffset;
                 }
                 for (auto const& integerVariable : module.getIntegerVariables()) {
                     int_fast64_t lowerBound = integerVariable.getLowerBoundExpression().evaluateAsInt();
                     int_fast64_t upperBound = integerVariable.getUpperBoundExpression().evaluateAsInt();
                     uint_fast64_t bitwidth = static_cast<uint_fast64_t>(std::ceil(std::log2(upperBound - lowerBound + 1)));
-                    integerVariables.emplace_back(integerVariable.getExpressionVariable(), lowerBound, upperBound, totalBitOffset, bitwidth);
+                    integerVariables.emplace_back(integerVariable.getExpressionVariable(), lowerBound, upperBound, totalBitOffset, bitwidth, false, integerVariable.isObservable());
                     totalBitOffset += bitwidth;
                 }
             }
@@ -69,7 +69,7 @@ namespace storm {
             
             for (auto const& variable : model.getGlobalVariables().getBooleanVariables()) {
                 if (!variable.isTransient()) {
-                    booleanVariables.emplace_back(variable.getExpressionVariable(), totalBitOffset, true);
+                    booleanVariables.emplace_back(variable.getExpressionVariable(), totalBitOffset, true, true);
                     ++totalBitOffset;
                 }
             }
@@ -78,7 +78,7 @@ namespace storm {
                     int_fast64_t lowerBound = variable.getLowerBound().evaluateAsInt();
                     int_fast64_t upperBound = variable.getUpperBound().evaluateAsInt();
                     uint_fast64_t bitwidth = static_cast<uint_fast64_t>(std::ceil(std::log2(upperBound - lowerBound + 1)));
-                    integerVariables.emplace_back(variable.getExpressionVariable(), lowerBound, upperBound, totalBitOffset, bitwidth, true);
+                    integerVariables.emplace_back(variable.getExpressionVariable(), lowerBound, upperBound, totalBitOffset, bitwidth, true, true);
                     totalBitOffset += bitwidth;
                 }
             }
@@ -92,12 +92,12 @@ namespace storm {
         
         void VariableInformation::createVariablesForAutomaton(storm::jani::Automaton const& automaton) {
             uint_fast64_t bitwidth = static_cast<uint_fast64_t>(std::ceil(std::log2(automaton.getNumberOfLocations())));
-            locationVariables.emplace_back(automaton.getLocationExpressionVariable(), automaton.getNumberOfLocations() - 1, totalBitOffset, bitwidth);
+            locationVariables.emplace_back(automaton.getLocationExpressionVariable(), automaton.getNumberOfLocations() - 1, totalBitOffset, bitwidth, true);
             totalBitOffset += bitwidth;
             
             for (auto const& variable : automaton.getVariables().getBooleanVariables()) {
                 if (!variable.isTransient()) {
-                    booleanVariables.emplace_back(variable.getExpressionVariable(), totalBitOffset);
+                    booleanVariables.emplace_back(variable.getExpressionVariable(), totalBitOffset, false, true);
                     ++totalBitOffset;
                 }
             }
@@ -106,7 +106,7 @@ namespace storm {
                     int_fast64_t lowerBound = variable.getLowerBound().evaluateAsInt();
                     int_fast64_t upperBound = variable.getUpperBound().evaluateAsInt();
                     uint_fast64_t bitwidth = static_cast<uint_fast64_t>(std::ceil(std::log2(upperBound - lowerBound + 1)));
-                    integerVariables.emplace_back(variable.getExpressionVariable(), lowerBound, upperBound, totalBitOffset, bitwidth);
+                    integerVariables.emplace_back(variable.getExpressionVariable(), lowerBound, upperBound, totalBitOffset, bitwidth, false, true);
                     totalBitOffset += bitwidth;
                 }
             }

src/storm/generator/VariableInformation.h

@@ -17,10 +17,9 @@ namespace storm {
     }
     
     namespace generator {
-        
         // A structure storing information about the boolean variables of the model.
         struct BooleanVariableInformation {
-            BooleanVariableInformation(storm::expressions::Variable const& variable, uint_fast64_t bitOffset, bool global = false);
+            BooleanVariableInformation(storm::expressions::Variable const& variable, uint_fast64_t bitOffset, bool global, bool observable);
             
             // The boolean variable.
             storm::expressions::Variable variable;
@@ -30,11 +29,14 @@ namespace storm {
 
             // A flag indicating whether the variable is a global one.
             bool global;
+
+            //
+            bool observable;
         };
         
         // A structure storing information about the integer variables of the model.
         struct IntegerVariableInformation {
-            IntegerVariableInformation(storm::expressions::Variable const& variable, int_fast64_t lowerBound, int_fast64_t upperBound, uint_fast64_t bitOffset, uint_fast64_t bitWidth, bool global = false);
+            IntegerVariableInformation(storm::expressions::Variable const& variable, int_fast64_t lowerBound, int_fast64_t upperBound, uint_fast64_t bitOffset, uint_fast64_t bitWidth, bool global, bool observable);
             
             // The integer variable.
             storm::expressions::Variable variable;
@@ -53,11 +55,13 @@ namespace storm {
             
             // A flag indicating whether the variable is a global one.
             bool global;
+
+            bool observable;
         };
         
         // A structure storing information about the location variables of the model.
         struct LocationVariableInformation {
-            LocationVariableInformation(storm::expressions::Variable const& variable, uint64_t highestValue, uint_fast64_t bitOffset, uint_fast64_t bitWidth);
+            LocationVariableInformation(storm::expressions::Variable const& variable, uint64_t highestValue, uint_fast64_t bitOffset, uint_fast64_t bitWidth, bool observable);
 
             // The expression variable for this location.
             storm::expressions::Variable variable;
@@ -70,6 +74,8 @@ namespace storm {
             
             // Its bit width in the compressed state.
             uint_fast64_t bitWidth;
+
+            bool observable;
         };
         
         // A structure storing information about the used variables of the program.

src/storm/models/sparse/Pomdp.cpp

@@ -15,13 +15,33 @@ 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) {
-
+            Pomdp<ValueType, RewardModelType>::Pomdp(storm::storage::sparse::ModelComponents<ValueType, RewardModelType> const &components) : Mdp<ValueType, RewardModelType>(components, storm::models::ModelType::Pomdp), observations(components.observabilityClasses.get()) {
+                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) {
+            Pomdp<ValueType, RewardModelType>::Pomdp(storm::storage::sparse::ModelComponents<ValueType, RewardModelType> &&components): Mdp<ValueType, RewardModelType>(components, storm::models::ModelType::Pomdp), observations(components.observabilityClasses.get()) {
+                computeNrObservations();
+            }
+
+            template<typename ValueType, typename RewardModelType>
+            void Pomdp<ValueType, RewardModelType>::printModelInformationToStream(std::ostream& out) const {
+                this->printModelInformationHeaderToStream(out);
+                out << "Choices: \t" << this->getNumberOfChoices() << std::endl;
+                out << "Observations: \t" << this->nrObservations << std::endl;
+                this->printModelInformationFooterToStream(out);
+            }
 
+            template<typename ValueType, typename RewardModelType>
+            void Pomdp<ValueType, RewardModelType>::computeNrObservations() {
+                uint64_t highestEntry = 0;
+                for (uint32_t entry : observations) {
+                    if (entry > highestEntry) {
+                        highestEntry = entry;
+                    }
+                }
+                nrObservations = highestEntry;
+                // In debug mode, ensure that every observability is used.
             }
 
 

src/storm/models/sparse/Pomdp.h

@@ -53,8 +53,16 @@ namespace storm {
 
                 Pomdp &operator=(Pomdp <ValueType, RewardModelType> &&other) = default;
 
+                virtual void printModelInformationToStream(std::ostream& out) const override;
+
+
             protected:
-                StateLabeling observations;
+                // TODO: consider a bitvector based presentation (depending on our needs).
+                std::vector<uint32_t> observations;
+
+                uint64_t nrObservations;
+
+                void computeNrObservations();
             };
         }
     }

src/storm/storage/sparse/ModelComponents.h

@@ -63,7 +63,7 @@ namespace storm {
                 // stores for each choice from which parts of the input model description it originates
                 boost::optional<std::shared_ptr<storm::storage::sparse::ChoiceOrigins>> choiceOrigins;
 
-                
+                boost::optional<std::vector<uint32_t>> observabilityClasses;
                 // Continuous time specific components (CTMCs, Markov Automata):
                 
                 // True iff the transition values (for Markovian choices) are interpreted as rates.