outline of learning algorithm

Former-commit-id: d770d1b7dc

src/builder/ExplicitPrismModelBuilder.cpp

@@ -312,7 +312,8 @@ namespace storm {
                 
                 STORM_LOG_TRACE("Exploring state with id " << currentIndex << ".");
                 
-                storm::generator::StateBehavior<ValueType, StateType> behavior = generator.expand(currentState, stateToIdCallback);
+                generator.load(currentState);
+                storm::generator::StateBehavior<ValueType, StateType> behavior = generator.expand(stateToIdCallback);
                 
                 // If there is no behavior, we might have to introduce a self-loop.
                 if (behavior.empty()) {

src/generator/NextStateGenerator.h

@@ -4,6 +4,8 @@
 #include <vector>
 #include <cstdint>
 
+#include "src/storage/expressions/Expression.h"
+
 #include "src/generator/CompressedState.h"
 #include "src/generator/StateBehavior.h"
 
@@ -16,7 +18,10 @@ namespace storm {
 
             virtual bool isDeterministicModel() const = 0;
             virtual std::vector<StateType> getInitialStates(StateToIdCallback const& stateToIdCallback) = 0;
-            virtual StateBehavior<ValueType, StateType> expand(CompressedState const& state, StateToIdCallback const& stateToIdCallback) = 0;
+            
+            virtual void load(CompressedState const& state) = 0;
+            virtual StateBehavior<ValueType, StateType> expand(StateToIdCallback const& stateToIdCallback) = 0;
+            virtual bool satisfies(storm::expressions::Expression const& expression) = 0;
         };
     }
 }

src/generator/PrismNextStateGenerator.cpp

@@ -10,7 +10,7 @@ namespace storm {
     namespace generator {
         
         template<typename ValueType, typename StateType>
-        PrismNextStateGenerator<ValueType, StateType>::PrismNextStateGenerator(storm::prism::Program const& program, VariableInformation const& variableInformation, bool buildChoiceLabeling) : program(program), selectedRewardModels(), buildChoiceLabeling(buildChoiceLabeling), variableInformation(variableInformation), evaluator(program.getManager()), comparator() {
+        PrismNextStateGenerator<ValueType, StateType>::PrismNextStateGenerator(storm::prism::Program const& program, VariableInformation const& variableInformation, bool buildChoiceLabeling) : program(program), selectedRewardModels(), buildChoiceLabeling(buildChoiceLabeling), variableInformation(variableInformation), evaluator(program.getManager()), state(nullptr), comparator() {
             // Intentionally left empty.
         }
         
@@ -49,10 +49,21 @@ namespace storm {
         }
         
         template<typename ValueType, typename StateType>
-        StateBehavior<ValueType, StateType> PrismNextStateGenerator<ValueType, StateType>::expand(CompressedState const& state, StateToIdCallback const& stateToIdCallback) {
+        void PrismNextStateGenerator<ValueType, StateType>::load(CompressedState const& state) {
             // Since almost all subsequent operations are based on the evaluator, we load the state into it now.
             unpackStateIntoEvaluator(state, variableInformation, evaluator);
             
+            // Also, we need to store a pointer to the state itself, because we need to be able to access it when expanding it.
+            this->state = &state;
+        }
+        
+        template<typename ValueType, typename StateType>
+        bool PrismNextStateGenerator<ValueType, StateType>::satisfies(storm::expressions::Expression const& expression) {
+            return evaluator.asBool(expression);
+        }
+        
+        template<typename ValueType, typename StateType>
+        StateBehavior<ValueType, StateType> PrismNextStateGenerator<ValueType, StateType>::expand(StateToIdCallback const& stateToIdCallback) {
             // Prepare the result, in case we return early.
             StateBehavior<ValueType, StateType> result;
             
@@ -76,8 +87,8 @@ namespace storm {
             }
             
             // Get all choices for the state.
-            std::vector<Choice<ValueType>> allChoices = getUnlabeledChoices(state, stateToIdCallback);
-            std::vector<Choice<ValueType>> allLabeledChoices = getLabeledChoices(state, stateToIdCallback);
+            std::vector<Choice<ValueType>> allChoices = getUnlabeledChoices(*this->state, stateToIdCallback);
+            std::vector<Choice<ValueType>> allLabeledChoices = getLabeledChoices(*this->state, stateToIdCallback);
             for (auto& choice : allLabeledChoices) {
                 allChoices.push_back(std::move(choice));
             }

src/generator/PrismNextStateGenerator.h

@@ -31,7 +31,10 @@ namespace storm {
             
             virtual bool isDeterministicModel() const override;
             virtual std::vector<StateType> getInitialStates(StateToIdCallback const& stateToIdCallback) override;
-            virtual StateBehavior<ValueType, StateType> expand(CompressedState const& state, StateToIdCallback const& stateToIdCallback) override;
+
+            virtual void load(CompressedState const& state) override;
+            virtual StateBehavior<ValueType, StateType> expand(StateToIdCallback const& stateToIdCallback) override;
+            virtual bool satisfies(storm::expressions::Expression const& expression) override;
 
         private:
             /*!
@@ -98,6 +101,8 @@ namespace storm {
             // An evaluator used to evaluate expressions.
             storm::expressions::ExpressionEvaluator<ValueType> evaluator;
             
+            CompressedState const* state;
+            
             // A comparator used to compare constants.
             storm::utility::ConstantsComparator<ValueType> comparator;
         };

src/modelchecker/reachability/SparseMdpLearningModelChecker.cpp

@@ -11,6 +11,9 @@
 
 #include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h"
 
+#include "src/utility/macros.h"
+#include "src/exceptions/NotSupportedException.h"
+
 namespace storm {
     namespace modelchecker {
         template<typename ValueType>
@@ -21,18 +24,47 @@ namespace storm {
         template<typename ValueType>
         bool SparseMdpLearningModelChecker<ValueType>::canHandle(CheckTask<storm::logic::Formula> const& checkTask) const {
             storm::logic::Formula const& formula = checkTask.getFormula();
-            storm::logic::FragmentSpecification fragment = storm::logic::propositional().setProbabilityOperatorsAllowed(true).setReachabilityProbabilityFormulasAllowed(true);
+            storm::logic::FragmentSpecification fragment = storm::logic::propositional().setProbabilityOperatorsAllowed(true).setReachabilityProbabilityFormulasAllowed(true).setNestedOperatorsAllowed(false);
             return formula.isInFragment(fragment) && checkTask.isOnlyInitialStatesRelevantSet();
         }
         
+        template<typename ValueType>
+        void SparseMdpLearningModelChecker<ValueType>::updateProbabilities(StateType const& sourceStateId, uint32_t action, StateType const& targetStateId, std::vector<std::vector<storm::storage::MatrixEntry<StateType, ValueType>>> const& transitionMatrix, std::vector<StateType> const& rowGroupIndices, std::vector<StateType> const& stateToRowGroupMapping, std::vector<ValueType>& lowerBounds, std::vector<ValueType>& upperBounds) const {
+            // Find out which row of the matrix we have to consider for the given action.
+            StateType sourceRowGroup = stateToRowGroupMapping[sourceStateId];
+            StateType sourceRow = sourceRowGroup + action;
+            
+            // Compute the new lower/upper values of the action.
+            ValueType newLowerValue = storm::utility::zero<ValueType>();
+            ValueType newUpperValue = storm::utility::zero<ValueType>();
+            for (auto const& element : transitionMatrix[sourceRow]) {
+                newLowerValue += element.getValue() * upperBounds[stateToRowGroupMapping[element.getColumn()]];
+                newUpperValue += element.getValue() * lowerBounds[stateToRowGroupMapping[element.getColumn()]];
+            }
+            
+            // And set them as the current value.
+            lowerBounds[stateToRowGroupMapping[sourceStateId]] = newLowerValue;
+            upperBounds[stateToRowGroupMapping[sourceStateId]] = newUpperValue;
+        }
+        
         template<typename ValueType>
         std::unique_ptr<CheckResult> SparseMdpLearningModelChecker<ValueType>::computeReachabilityProbabilities(CheckTask<storm::logic::EventuallyFormula> const& checkTask) {
-            // Create a callback for the next-state generator to enable it to request the index of states.
-            std::function<StateType (storm::generator::CompressedState const&)> stateToIdCallback = std::bind(&SparseMdpLearningModelChecker<ValueType>::getOrAddStateIndex, this, std::placeholders::_1);
+            storm::logic::EventuallyFormula const& eventuallyFormula = checkTask.getFormula();
+            storm::logic::Formula const& subformula = eventuallyFormula.getSubformula();
+            STORM_LOG_THROW(subformula.isAtomicExpressionFormula() || subformula.isAtomicLabelFormula(), storm::exceptions::NotSupportedException, "Learning engine can only deal with formulas of the form 'F \"label\"' or 'F expression'.");
+            storm::expressions::Expression targetStateExpression;
+            if (subformula.isAtomicExpressionFormula()) {
+                targetStateExpression = subformula.asAtomicExpressionFormula().getExpression();
+            } else {
+                targetStateExpression = program.getLabelExpression(subformula.asAtomicLabelFormula().getLabel());
+            }
             
             // A container for the encountered states.
             storm::storage::sparse::StateStorage<StateType> stateStorage(variableInformation.getTotalBitOffset(true));
             
+            // A container that stores the states that were already expanded.
+            storm::storage::BitVector expandedStates;
+            
             // A generator used to explore the model.
             storm::generator::PrismNextStateGenerator<ValueType, StateType> generator(program, variableInformation, false);
             
@@ -49,16 +81,78 @@ namespace storm {
             std::vector<ValueType> lowerBounds;
             std::vector<ValueType> upperBounds;
 
-            // Now perform the actual exploration loop.
+            // Create a callback for the next-state generator to enable it to request the index of states.
+            std::function<StateType (storm::generator::CompressedState const&)> stateToIdCallback = [&stateStorage] (storm::generator::CompressedState const& state) -> StateType {
+                StateType newIndex = stateStorage.numberOfStates;
+                
+                // Check, if the state was already registered.
+                std::pair<uint32_t, std::size_t> actualIndexBucketPair = stateStorage.stateToId.findOrAddAndGetBucket(state, newIndex);
+                
+                if (actualIndexBucketPair.first == newIndex) {
+                    ++stateStorage.numberOfStates;
+                }
+                
+                return actualIndexBucketPair.first;
+            };
+
+            stateStorage.initialStateIndices = generator.getInitialStates(stateToIdCallback);
+            STORM_LOG_THROW(stateStorage.initialStateIndices.size() == 1, storm::exceptions::NotSupportedException, "Currently only models with one initial state are supported by the learning engine.");
+            
+            // Now perform the actual sampling.
+            std::unordered_map<StateType, storm::generator::CompressedState> unexploredStates;
+            std::vector<std::pair<StateType, uint32_t>> stateActionStack;
+            stateActionStack.push_back(std::make_pair(stateStorage.initialStateIndices.front(), 0));
+            bool foundTargetState = false;
+            
+            while (!foundTargetState) {
+                StateType const& currentStateId = stateActionStack.back().first;
+                
+                // If the state is not yet expanded, we need to retrieve its behaviors.
+                if (!expandedStates.get(currentStateId)) {
+                    // First, we need to get the compressed state back from the id.
+                    auto it = unexploredStates.find(currentStateId);
+                    STORM_LOG_ASSERT(it != unexploredStates.end(), "Unable to find unexplored state.");
+                    storm::storage::BitVector currentState = it->second;
+                    
+                    // Before generating the behavior of the state, we need to determine whether it's a target state that
+                    // does not need to be expanded.
+                    generator.load(currentState);
+                    if (generator.satisfies(targetStateExpression)) {
+                        // If it's in fact a goal state, we need to go backwards in the stack and update the probabilities.
+                        foundTargetState = true;
+                        stateActionStack.pop_back();
+                        
+                        while (!stateActionStack.empty()) {
+                            updateProbabilities(stateActionStack.back().first, stateActionStack.back().second, currentStateId, matrix, rowGroupIndices, stateToRowGroupMapping, lowerBounds, upperBounds);
+                        }
+                        break;
+                    } else {
+                        // If it needs to be expanded, we use the generator to retrieve the behavior of the new state.
+                        storm::generator::StateBehavior<ValueType, StateType> behavior = generator.expand(stateToIdCallback);
+                        
+                        stateToRowGroupMapping.push_back(rowGroupIndices.size());
+                        rowGroupIndices.push_back(matrix.size());
+                        
+                        // Next, we insert the behavior into our matrix structure.
+                        for (auto const& choice : behavior) {
+                            matrix.resize(matrix.size() + 1);
+                            for (auto const& entry : choice) {
+                                matrix.back().push_back(storm::storage::MatrixEntry<StateType, ValueType>(entry.first, entry.second));
+                            }
+                        }
+                        
+                        // Now that we have explored the state, we can dispose of it.
+                        unexploredStates.erase(it);
+                    }
+                }
+                
+                // At this point, we can be sure that the state was expanded and that we can sample according to the probabilities.
+                // TODO: set action of topmost stack element
+            }
 
             return nullptr;
         }
         
-        template<typename ValueType>
-        typename SparseMdpLearningModelChecker<ValueType>::StateType SparseMdpLearningModelChecker<ValueType>::getOrAddStateIndex(storm::generator::CompressedState const& state) {
-            
-        }
-        
         template class SparseMdpLearningModelChecker<double>;
     }
 }

src/modelchecker/reachability/SparseMdpLearningModelChecker.h

@@ -25,7 +25,7 @@ namespace storm {
             virtual std::unique_ptr<CheckResult> computeReachabilityProbabilities(CheckTask<storm::logic::EventuallyFormula> const& checkTask) override;
             
         private:
-            StateType getOrAddStateIndex(storm::generator::CompressedState const& state);
+            void updateProbabilities(StateType const& sourceStateId, uint32_t action, StateType const& targetStateId, std::vector<std::vector<storm::storage::MatrixEntry<StateType, ValueType>>> const& transitionMatrix, std::vector<StateType> const& rowGroupIndices, std::vector<StateType> const& stateToRowGroupMapping, std::vector<ValueType>& lowerBounds, std::vector<ValueType>& upperBounds) const;
             
             // The program that defines the model to check.
             storm::prism::Program program;

src/storage/SparseMatrix.cpp

@@ -1320,6 +1320,9 @@ namespace storm {
         template std::vector<double> SparseMatrix<double>::getPointwiseProductRowSumVector(storm::storage::SparseMatrix<double> const& otherMatrix) const;
         template bool SparseMatrix<double>::isSubmatrixOf(SparseMatrix<double> const& matrix) const;
 
+        template class MatrixEntry<uint32_t, double>;
+        template std::ostream& operator<<(std::ostream& out, MatrixEntry<uint32_t, double> const& entry);
+        
         // float
         template class MatrixEntry<typename SparseMatrix<float>::index_type, float>;
         template std::ostream& operator<<(std::ostream& out, MatrixEntry<typename SparseMatrix<float>::index_type, float> const& entry);