explicit-state-lookup, for finding states in a model based on the variable assignment

src/storm/api/builder.h

@@ -77,6 +77,26 @@ namespace storm {
             STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "CUDD does not support rational functions.");
         }
 
+        /**
+         * Initializes an explict model builder; an object/algorithm that is used to build sparse models
+         * @tparam ValueType Type of the probabilities in the sparse model
+         * @param model SymbolicModelDescription of the model
+         * @param options Builder options
+         * @return A builder
+         */
+        template<typename ValueType>
+        storm::builder::ExplicitModelBuilder<ValueType> makeExplicitModelBuilder(storm::storage::SymbolicModelDescription const& model, storm::builder::BuilderOptions const& options) {
+            std::shared_ptr<storm::generator::NextStateGenerator<ValueType, uint32_t>> generator;
+            if (model.isPrismProgram()) {
+                generator = std::make_shared<storm::generator::PrismNextStateGenerator<ValueType, uint32_t>>(model.asPrismProgram(), options);
+            } else if (model.isJaniModel()) {
+                generator = std::make_shared<storm::generator::JaniNextStateGenerator<ValueType, uint32_t>>(model.asJaniModel(), options);
+            } else {
+                STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Cannot build sparse model from this symbolic model description.");
+            }
+            return storm::builder::ExplicitModelBuilder<ValueType>(generator);
+        }
+
         template<typename ValueType>
         std::shared_ptr<storm::models::sparse::Model<ValueType>> buildSparseModel(storm::storage::SymbolicModelDescription const& model, storm::builder::BuilderOptions const& options, bool jit = false, bool doctor = false) {
             if (jit) {
@@ -92,19 +112,14 @@ namespace storm {
 
                 return builder.build();
             } else {
-                std::shared_ptr<storm::generator::NextStateGenerator<ValueType, uint32_t>> generator;
-                if (model.isPrismProgram()) {
-                    generator = std::make_shared<storm::generator::PrismNextStateGenerator<ValueType, uint32_t>>(model.asPrismProgram(), options);
-                } else if (model.isJaniModel()) {
-                    generator = std::make_shared<storm::generator::JaniNextStateGenerator<ValueType, uint32_t>>(model.asJaniModel(), options);
-                } else {
-                    STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Cannot build sparse model from this symbolic model description.");
-                }
-                storm::builder::ExplicitModelBuilder<ValueType> builder(generator);
+                storm::builder::ExplicitModelBuilder<ValueType> builder = makeExplicitModelBuilder<ValueType>(model, options);
                 return builder.build();
             }
         }
 
+
+
+
         template<typename ValueType>
         std::shared_ptr<storm::models::sparse::Model<ValueType>> buildSparseModel(storm::storage::SymbolicModelDescription const& model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, bool jit = false, bool doctor = false) {
             storm::builder::BuilderOptions options(formulas, model);

src/storm/builder/ExplicitModelBuilder.cpp

@@ -8,6 +8,7 @@
 
 #include "storm/exceptions/AbortException.h"
 #include "storm/exceptions/WrongFormatException.h"
+#include "storm/exceptions/IllegalArgumentException.h"
 
 #include "storm/generator/PrismNextStateGenerator.h"
 #include "storm/generator/JaniNextStateGenerator.h"
@@ -36,7 +37,14 @@
 
 namespace storm {
     namespace builder {
-                        
+
+        template<typename StateType>
+        StateType ExplicitStateLookup<StateType>::lookup(std::map<storm::expressions::Variable, storm::expressions::Expression> const& stateDescription) const {
+            auto cs = storm::generator::createCompressedState(this->varInfo, stateDescription, true);
+            STORM_LOG_THROW(stateToId.contains(cs), storm::exceptions::IllegalArgumentException, "State unknown.");
+            return this->stateToId.getValue(cs);
+        }
+
         template <typename ValueType, typename RewardModelType, typename StateType>
         ExplicitModelBuilder<ValueType, RewardModelType, StateType>::Options::Options() : explorationOrder(storm::settings::getModule<storm::settings::modules::BuildSettings>().getExplorationOrder()) {
             // Intentionally left empty.
@@ -103,7 +111,12 @@ namespace storm {
             
             return actualIndex;
         }
-        
+
+        template <typename ValueType, typename RewardModelType, typename StateType>
+        ExplicitStateLookup<StateType> ExplicitModelBuilder<ValueType, RewardModelType, StateType>::exportExplicitStateLookup() const {
+            return ExplicitStateLookup<StateType>(this->generator->getVariableInformation(), this->stateStorage.stateToId);
+        }
+
         template <typename ValueType, typename RewardModelType, typename StateType>
         void ExplicitModelBuilder<ValueType, RewardModelType, StateType>::buildMatrices(storm::storage::SparseMatrixBuilder<ValueType>& transitionMatrixBuilder, std::vector<RewardModelBuilder<typename RewardModelType::ValueType>>& rewardModelBuilders, ChoiceInformationBuilder& choiceInformationBuilder, boost::optional<storm::storage::BitVector>& markovianStates, boost::optional<storm::storage::sparse::StateValuationsBuilder>& stateValuationsBuilder) {
             
@@ -419,6 +432,7 @@ namespace storm {
         
         // Explicitly instantiate the class.
         template class ExplicitModelBuilder<double, storm::models::sparse::StandardRewardModel<double>, uint32_t>;
+        template class ExplicitStateLookup<uint32_t>;
 
 #ifdef STORM_HAVE_CARL
         template class ExplicitModelBuilder<RationalNumber, storm::models::sparse::StandardRewardModel<RationalNumber>, uint32_t>;

src/storm/builder/ExplicitModelBuilder.h

@@ -44,6 +44,21 @@ namespace storm {
         // Forward-declare classes.
         template <typename ValueType> class RewardModelBuilder;
         class ChoiceInformationBuilder;
+
+        template<typename StateType>
+        class ExplicitStateLookup {
+        public:
+            ExplicitStateLookup(VariableInformation const& varInfo,
+                                storm::storage::BitVectorHashMap<StateType> const& stateToId ) : varInfo(varInfo), stateToId(stateToId) {
+                // intentionally left empty.
+            }
+
+            StateType lookup(std::map<storm::expressions::Variable, storm::expressions::Expression> const& stateDescription) const;
+
+        private:
+            VariableInformation varInfo;
+            storm::storage::BitVectorHashMap<StateType>  stateToId;
+        };
         
         template<typename ValueType, typename RewardModelType = storm::models::sparse::StandardRewardModel<ValueType>, typename StateType = uint32_t>
         class ExplicitModelBuilder {
@@ -88,7 +103,13 @@ namespace storm {
              *         information (if requested).
              */
             std::shared_ptr<storm::models::sparse::Model<ValueType, RewardModelType>> build();
-            
+
+            /*!
+             * Export a wrapper that contains (a copy of) the internal information that maps states to ids.
+             * This wrapper can be helpful to find states in later stages.
+             * @return
+             */
+            ExplicitStateLookup<StateType> exportExplicitStateLookup() const;
         private:
             /*!
              * Retrieves the state id of the given state. If the state has not been encountered yet, it will be added to

src/storm/generator/CompressedState.cpp

@@ -2,6 +2,9 @@
 
 #include <boost/algorithm/string/join.hpp>
 
+#include "storm/exceptions/InvalidArgumentException.h"
+#include "storm/exceptions/NotImplementedException.h"
+
 #include "storm/generator/VariableInformation.h"
 #include "storm/storage/expressions/ExpressionManager.h"
 #include "storm/storage/expressions/SimpleValuation.h"
@@ -134,6 +137,33 @@ namespace storm {
             return result;
         }
 
+        CompressedState createCompressedState(VariableInformation const& varInfo, std::map<storm::expressions::Variable, storm::expressions::Expression> const& stateDescription, bool checkOutOfBounds) {
+            CompressedState result(varInfo.getTotalBitOffset(true));
+            auto boolItEnd = varInfo.booleanVariables.end();
+
+            for (auto boolIt = varInfo.booleanVariables.begin(); boolIt != boolItEnd; ++boolIt) {
+                STORM_LOG_THROW(stateDescription.count(boolIt->variable) > 0,storm::exceptions::InvalidArgumentException, "Assignment for Boolean variable " << boolIt->getName() << " missing." );
+                result.set(boolIt->bitOffset, stateDescription.at(boolIt->variable).evaluateAsBool());
+            }
+
+            // Iterate over all integer assignments and carry them out.
+            auto integerItEnd = varInfo.integerVariables.end();
+            for (auto integerIt = varInfo.integerVariables.begin(); integerIt != integerItEnd; ++integerIt) {
+                STORM_LOG_THROW(stateDescription.count(integerIt->variable) > 0,storm::exceptions::InvalidArgumentException, "Assignment for Integer variable " << integerIt->getName() << " missing." );
+
+                int64_t assignedValue = stateDescription.at(integerIt->variable).evaluateAsInt();
+                if (checkOutOfBounds) {
+                    STORM_LOG_THROW(assignedValue >= integerIt->lowerBound, storm::exceptions::InvalidArgumentException, "The assignment leads to an out-of-bounds value (" << assignedValue << ") for the variable '" << integerIt->getName() << "'.");
+                    STORM_LOG_THROW(assignedValue <= integerIt->upperBound, storm::exceptions::InvalidArgumentException, "The assignment leads to an out-of-bounds value (" << assignedValue << ") for the variable '" << integerIt->getName() << "'.");
+                }
+                result.setFromInt(integerIt->bitOffset, integerIt->bitWidth, assignedValue - integerIt->lowerBound);
+                STORM_LOG_ASSERT(static_cast<int_fast64_t>(result.getAsInt(integerIt->bitOffset, integerIt->bitWidth)) + integerIt->lowerBound == assignedValue, "Writing to the bit vector bucket failed (read " << result.getAsInt(integerIt->bitOffset, integerIt->bitWidth) << " but wrote " << assignedValue << ").");
+            }
+
+            STORM_LOG_THROW(varInfo.locationVariables.size() == 0, storm::exceptions::NotImplementedException, "Support for JANI is not implemented");
+            return result;
+        }
+
 #ifdef STORM_HAVE_CARL
         template void unpackStateIntoEvaluator<storm::RationalNumber>(CompressedState const& state, VariableInformation const& variableInformation, storm::expressions::ExpressionEvaluator<storm::RationalNumber>& evaluator);
         template void unpackStateIntoEvaluator<storm::RationalFunction>(CompressedState const& state, VariableInformation const& variableInformation, storm::expressions::ExpressionEvaluator<storm::RationalFunction>& evaluator);

src/storm/generator/CompressedState.h

@@ -2,6 +2,7 @@
 #define STORM_GENERATOR_COMPRESSEDSTATE_H_
 
 #include "storm/storage/BitVector.h"
+#include <map>
 #include <unordered_map>
 
 namespace storm {
@@ -10,12 +11,15 @@ namespace storm {
         
         class ExpressionManager;
         class SimpleValuation;
+        class Variable;
+        class Expression;
     }
     
     namespace generator {
         typedef storm::storage::BitVector CompressedState;
 
         struct VariableInformation;
+
         
         /*!
          * Unpacks the compressed state into the evaluator.
@@ -75,6 +79,7 @@ namespace storm {
          */
         CompressedState createOutOfBoundsState(VariableInformation const& varInfo, bool roundTo64Bit = true);
 
+        CompressedState createCompressedState(VariableInformation const& varInfo, std::map<storm::expressions::Variable, storm::expressions::Expression> const& stateDescription, bool checkOutOfBounds);
     }
 }
 

src/storm/generator/NextStateGenerator.cpp

@@ -78,6 +78,11 @@ namespace storm {
             }
             return evaluator->asBool(expression);
         }
+
+        template<typename ValueType, typename StateType>
+        VariableInformation const& NextStateGenerator<ValueType, StateType>::getVariableInformation() const {
+            return variableInformation;
+        }
         
         template<typename ValueType, typename StateType>
         void NextStateGenerator<ValueType, StateType>::addStateValuation(storm::storage::sparse::state_type const& currentStateIndex, storm::storage::sparse::StateValuationsBuilder& valuationsBuilder) const {

src/storm/generator/NextStateGenerator.h

@@ -76,8 +76,8 @@ namespace storm {
 
             NextStateGeneratorOptions const& getOptions() const;
 
+            VariableInformation const& getVariableInformation() const;
 
-            
             virtual std::shared_ptr<storm::storage::sparse::ChoiceOrigins> generateChoiceOrigins(std::vector<boost::any>& dataForChoiceOrigins) const;
 
             /*!

src/storm/generator/VariableInformation.h

@@ -24,7 +24,9 @@ namespace storm {
         // 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, bool observable);
-            
+
+            std::string const& getName() const { return variable.getName(); }
+
             // The boolean variable.
             storm::expressions::Variable variable;
             
@@ -43,6 +45,8 @@ namespace storm {
 
             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, bool observable = true, bool forceOutOfBoundsCheck = false);
 
+            std::string const& getName() const { return variable.getName(); }
+
             // The integer variable.
             storm::expressions::Variable variable;
             

src/storm/storage/sparse/StateStorage.h

@@ -1,5 +1,4 @@
-#ifndef STORM_STORAGE_SPARSE_STATESTORAGE_H_
-#define STORM_STORAGE_SPARSE_STATESTORAGE_H_
+#pragma once
 
 #include <cstdint>
 
@@ -28,11 +27,10 @@ namespace storm {
                 uint64_t bitsPerState;
                 
                 // Get the number of states that were found in the exploration so far.
-                uint_fast64_t getNumberOfStates() const;
+                uint64_t getNumberOfStates() const;
             };
             
         }
     }
 }
 
-#endif /* STORM_STORAGE_SPARSE_STATESTORAGE_H_ */