state generator now takes into account observable expressions when building POMDPs

src/storm/generator/CompressedState.cpp

@@ -69,9 +69,13 @@ namespace storm {
             return result;
         }
 
-        uint32_t unpackStateToObservabilityClass(CompressedState const& state, std::unordered_map<storm::storage::BitVector,uint32_t>& observabilityMap, storm::storage::BitVector const& mask) {
+        uint32_t unpackStateToObservabilityClass(CompressedState const& state, storm::storage::BitVector const& observationVector, 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;
+            if (observationVector.size() != 0) {
+                observeClass.concat(observationVector);
+            }
+
             auto it = observabilityMap.find(observeClass);
             if (it != observabilityMap.end()) {
                 return it->second;

src/storm/generator/CompressedState.h

@@ -50,7 +50,7 @@ namespace storm {
          * @param mask
          * @return
          */
-        uint32_t unpackStateToObservabilityClass(CompressedState const& state, std::unordered_map<storm::storage::BitVector,uint32_t>& observabilityMap, storm::storage::BitVector const& mask);
+        uint32_t unpackStateToObservabilityClass(CompressedState const& state,  storm::storage::BitVector const& observationVector, std::unordered_map<storm::storage::BitVector,uint32_t>& observabilityMap, storm::storage::BitVector const& mask);
         /*!
          *
          * @param varInfo

src/storm/generator/JaniNextStateGenerator.cpp

@@ -1119,7 +1119,14 @@ namespace storm {
             
             return std::make_shared<storm::storage::sparse::JaniChoiceOrigins>(std::make_shared<storm::jani::Model>(model), std::move(identifiers), std::move(identifierToEdgeIndexSetMapping));
         }
-        
+
+        template<typename ValueType, typename StateType>
+        storm::storage::BitVector JaniNextStateGenerator<ValueType, StateType>::evaluateObservationLabels(CompressedState const& state) const {
+            STORM_LOG_WARN("There are no observation labels in JANI currenty");
+            return storm::storage::BitVector(0);
+        };
+
+
         template<typename ValueType, typename StateType>
         void JaniNextStateGenerator<ValueType, StateType>::checkValid() const {
             // If the program still contains undefined constants and we are not in a parametric setting, assemble an appropriate error message.

src/storm/generator/JaniNextStateGenerator.h

@@ -91,7 +91,16 @@ namespace storm {
              * @return The resulting state.
              */
             void applyTransientUpdate(TransientVariableValuation<ValueType>& transientValuation, storm::jani::detail::ConstAssignments const& transientAssignments, storm::expressions::ExpressionEvaluator<ValueType> const& expressionEvaluator);
-            
+
+            /**
+             * Required method to overload, but currently throws an error as POMDPs are not yet specified in JANI.
+             * Furthermore, it might be that these observation labels will not be used and that one uses transient variables instead.
+             *
+             * @param state
+             * @return
+             */
+            virtual storm::storage::BitVector evaluateObservationLabels(CompressedState const& state) const override;
+
             /*!
              * Retrieves all choices possible from the given state.
              *

src/storm/generator/NextStateGenerator.cpp

@@ -183,8 +183,7 @@ namespace storm {
             if (this->mask.size() == 0) {
                 this->mask = computeObservabilityMask(variableInformation);
             }
-
-            return unpackStateToObservabilityClass(state, observabilityMap, mask);
+            return unpackStateToObservabilityClass(state, evaluateObservationLabels(state), observabilityMap, mask);
         }
 
         template<typename ValueType, typename StateType>

src/storm/generator/NextStateGenerator.h

@@ -68,6 +68,8 @@ namespace storm {
             virtual storm::models::sparse::StateLabeling label(storm::storage::sparse::StateStorage<StateType> const& stateStorage, std::vector<StateType> const& initialStateIndices = {}, std::vector<StateType> const& deadlockStateIndices = {}) = 0;
 
             NextStateGeneratorOptions const& getOptions() const;
+
+
             
             virtual std::shared_ptr<storm::storage::sparse::ChoiceOrigins> generateChoiceOrigins(std::vector<boost::any>& dataForChoiceOrigins) const;
 
@@ -83,7 +85,9 @@ namespace storm {
              * Creates the state labeling for the given states using the provided labels and expressions.
              */
             storm::models::sparse::StateLabeling label(storm::storage::sparse::StateStorage<StateType> const& stateStorage, std::vector<StateType> const& initialStateIndices, std::vector<StateType> const& deadlockStateIndices, std::vector<std::pair<std::string, storm::expressions::Expression>> labelsAndExpressions);
-            
+
+            virtual storm::storage::BitVector evaluateObservationLabels(CompressedState const& state) const =0;
+
             void postprocess(StateBehavior<ValueType, StateType>& result);
             
             /// The options to be used for next-state generation.

src/storm/generator/PrismNextStateGenerator.cpp

@@ -682,7 +682,20 @@ namespace storm {
             
             return NextStateGenerator<ValueType, StateType>::label(stateStorage, initialStateIndices, deadlockStateIndices, labels);
         }
-        
+
+        template<typename ValueType, typename StateType>
+        storm::storage::BitVector PrismNextStateGenerator<ValueType, StateType>::evaluateObservationLabels(CompressedState const& state) const {
+            // TODO consider to avoid reloading by computing these bitvectors in an earlier build stage
+            unpackStateIntoEvaluator(state, this->variableInformation, *this->evaluator);
+
+            storm::storage::BitVector result(program.getNumberOfObservationLabels() * 64);
+            for (uint64_t i = 0; i < program.getNumberOfObservationLabels(); ++i) {
+                result.setFromInt(64*i,64,this->evaluator->asInt(program.getObservationLabels()[i].getStatePredicateExpression()));
+            }
+            return result;
+        };
+
+
         template<typename ValueType, typename StateType>
         std::size_t PrismNextStateGenerator<ValueType, StateType>::getNumberOfRewardModels() const {
             return rewardModels.size();

src/storm/generator/PrismNextStateGenerator.h

@@ -92,7 +92,13 @@ namespace storm {
              * @return The labeled choices of the state.
              */
             std::vector<Choice<ValueType>> getLabeledChoices(CompressedState const& state, StateToIdCallback stateToIdCallback, CommandFilter const& commandFilter = CommandFilter::All);
-            
+
+
+            /*!
+             * Evaluate observation labels
+             */
+            storm::storage::BitVector evaluateObservationLabels(CompressedState const& state) const override;
+
             /*!
              * A recursive helper function to generate a synchronziing distribution.
              */

src/storm/storage/sparse/ModelComponents.h

@@ -63,21 +63,19 @@ 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;
 
+                // POMDP specific components
+                // The POMDP observations
                 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.
                 bool rateTransitions;
-                
                 // The exit rate for each state. Must be given for CTMCs and MAs, if rateTransitions is false. Otherwise, it is optional.
                 boost::optional<std::vector<ValueType>> exitRates;
-
                 // A vector that stores which states are markovian (only for Markov Automata).
                 boost::optional<storm::storage::BitVector> markovianStates;
 
-                
                 // Stochastic two player game specific components:
-                
                 // The matrix of player 1 choices (needed for stochastic two player games
                 boost::optional<storm::storage::SparseMatrix<storm::storage::sparse::state_type>> player1Matrix;
             };