added a sh*t ton of debug output, didn't help

Former-commit-id: a1bf88c024

src/builder/ExplicitPrismModelBuilder.cpp

@@ -229,10 +229,10 @@ namespace storm {
         
         template <typename ValueType, typename RewardModelType, typename StateType>
         StateType ExplicitPrismModelBuilder<ValueType, RewardModelType, StateType>::getOrAddStateIndex(CompressedState const& state) {
-            uint32_t newIndex = stateStorage.numberOfStates;
+            StateType newIndex = static_cast<StateType>(stateStorage.getNumberOfStates());
             
             // Check, if the state was already registered.
-            std::pair<uint32_t, std::size_t> actualIndexBucketPair = stateStorage.stateToId.findOrAddAndGetBucket(state, newIndex);
+            std::pair<StateType, std::size_t> actualIndexBucketPair = stateStorage.stateToId.findOrAddAndGetBucket(state, newIndex);
             
             if (actualIndexBucketPair.first == newIndex) {
                 if (options.explorationOrder == ExplorationOrder::Dfs) {
@@ -245,7 +245,6 @@ namespace storm {
                 } else {
                     STORM_LOG_ASSERT(false, "Invalid exploration order.");
                 }
-                ++stateStorage.numberOfStates;
             }
             
             return actualIndexBucketPair.first;
@@ -467,7 +466,7 @@ namespace storm {
             
             // Finally -- if requested -- build the state information that can be retrieved from the outside.
             if (options.buildStateValuations) {
-                stateValuations = storm::storage::sparse::StateValuations(stateStorage.numberOfStates);
+                stateValuations = storm::storage::sparse::StateValuations(stateStorage.getNumberOfStates());
                 for (auto const& bitVectorIndexPair : stateStorage.stateToId) {
                     stateValuations.get().valuations[bitVectorIndexPair.second] = unpackStateIntoValuation(bitVectorIndexPair.first, variableInformation, program.getManager());
                 }

src/modelchecker/exploration/Bounds.cpp

@@ -10,18 +10,14 @@ namespace storm {
             std::pair<ValueType, ValueType> Bounds<StateType, ValueType>::getBoundsForState(StateType const& state, ExplorationInformation<StateType, ValueType> const& explorationInformation) const {
                 ActionType index = explorationInformation.getRowGroup(state);
                 if (index == explorationInformation.getUnexploredMarker()) {
+                    std::cout << "state " << state << " is unexplored! retuning zero/one" << std::endl;
                     return std::make_pair(storm::utility::zero<ValueType>(), storm::utility::one<ValueType>());
                 } else {
+                    std::cout << "accessing at index " << index << " out of " << boundsPerState.size() << std::endl;
                     return boundsPerState[index];
                 }
             }
-            
-            template<typename StateType, typename ValueType>
-            std::pair<ValueType, ValueType> const& Bounds<StateType, ValueType>::getBoundsForExploredState(StateType const& state, ExplorationInformation<StateType, ValueType> const& explorationInformation) const {
-                ActionType index = explorationInformation.getRowGroup(state);
-                return boundsPerState[index];
-            }
-            
+                        
             template<typename StateType, typename ValueType>
             ValueType Bounds<StateType, ValueType>::getLowerBoundForState(StateType const& state, ExplorationInformation<StateType, ValueType> const& explorationInformation) const {
                 ActionType index = explorationInformation.getRowGroup(state);
@@ -78,7 +74,7 @@ namespace storm {
             
             template<typename StateType, typename ValueType>
             ValueType Bounds<StateType, ValueType>::getDifferenceOfStateBounds(StateType const& state, ExplorationInformation<StateType, ValueType> const& explorationInformation) const {
-                std::pair<ValueType, ValueType> const& bounds = getBoundsForExploredState(state, explorationInformation);
+                std::pair<ValueType, ValueType> bounds = getBoundsForState(state, explorationInformation);
                 return bounds.second - bounds.first;
             }
             
@@ -120,6 +116,7 @@ namespace storm {
             template<typename StateType, typename ValueType>
             void Bounds<StateType, ValueType>::setBoundsForState(StateType const& state, ExplorationInformation<StateType, ValueType> const& explorationInformation, std::pair<ValueType, ValueType> const& values) {
                 StateType const& rowGroup = explorationInformation.getRowGroup(state);
+                std::cout << "setting " << values.first << ", " << values.second << " for state " << state << std::endl;
                 setBoundsForRowGroup(rowGroup, values);
             }
             

src/modelchecker/exploration/Bounds.h

@@ -21,8 +21,6 @@ namespace storm {
                 typedef StateType ActionType;
                 
                 std::pair<ValueType, ValueType> getBoundsForState(StateType const& state, ExplorationInformation<StateType, ValueType> const& explorationInformation) const;
-
-                std::pair<ValueType, ValueType> const& getBoundsForExploredState(StateType const& state, ExplorationInformation<StateType, ValueType> const& explorationInformation) const;
                 
                 ValueType getLowerBoundForState(StateType const& state, ExplorationInformation<StateType, ValueType> const& explorationInformation) const;
                 

src/modelchecker/exploration/ExplorationInformation.cpp

@@ -10,7 +10,7 @@ namespace storm {
         namespace exploration_detail {
             
             template<typename StateType, typename ValueType>
-            ExplorationInformation<StateType, ValueType>::ExplorationInformation(uint_fast64_t bitsPerBucket, storm::OptimizationDirection const& direction, ActionType const& unexploredMarker) : stateStorage(bitsPerBucket), unexploredMarker(unexploredMarker), optimizationDirection(direction), localPrecomputation(false), numberOfExplorationStepsUntilPrecomputation(100000), numberOfSampledPathsUntilPrecomputation(), nextStateHeuristic(storm::settings::modules::ExplorationSettings::NextStateHeuristic::DifferenceWeightedProbability) {
+            ExplorationInformation<StateType, ValueType>::ExplorationInformation(storm::OptimizationDirection const& direction, ActionType const& unexploredMarker) : unexploredMarker(unexploredMarker), optimizationDirection(direction), localPrecomputation(false), numberOfExplorationStepsUntilPrecomputation(100000), numberOfSampledPathsUntilPrecomputation(), nextStateHeuristic(storm::settings::modules::ExplorationSettings::NextStateHeuristic::DifferenceWeightedProbability) {
                 
                 storm::settings::modules::ExplorationSettings const& settings = storm::settings::explorationSettings();
                 localPrecomputation = settings.isLocalPrecomputationSet();
@@ -24,25 +24,24 @@ namespace storm {
             }
             
             template<typename StateType, typename ValueType>
-            void ExplorationInformation<StateType, ValueType>::setInitialStates(std::vector<StateType> const& initialStates) {
-                stateStorage.initialStateIndices = initialStates;
+            typename ExplorationInformation<StateType, ValueType>::const_iterator ExplorationInformation<StateType, ValueType>::findUnexploredState(StateType const& state) const {
+                return unexploredStates.find(state);
             }
             
             template<typename StateType, typename ValueType>
-            StateType ExplorationInformation<StateType, ValueType>::getFirstInitialState() const {
-                return stateStorage.initialStateIndices.front();
+            typename ExplorationInformation<StateType, ValueType>::const_iterator ExplorationInformation<StateType, ValueType>::unexploredStatesEnd() const {
+                return unexploredStates.end();
             }
             
             template<typename StateType, typename ValueType>
-            std::size_t ExplorationInformation<StateType, ValueType>::getNumberOfInitialStates() const {
-                return stateStorage.initialStateIndices.size();
+            void ExplorationInformation<StateType, ValueType>::removeUnexploredState(const_iterator it) {
+                unexploredStates.erase(it);
             }
             
             template<typename StateType, typename ValueType>
-            void ExplorationInformation<StateType, ValueType>::addUnexploredState(storm::generator::CompressedState const& compressedState) {
+            void ExplorationInformation<StateType, ValueType>::addUnexploredState(StateType const& stateId, storm::generator::CompressedState const& compressedState) {
                 stateToRowGroupMapping.push_back(unexploredMarker);
-                unexploredStates[stateStorage.numberOfStates] = compressedState;
-                ++stateStorage.numberOfStates;
+                unexploredStates[stateId] = compressedState;
             }
             
             template<typename StateType, typename ValueType>
@@ -71,6 +70,21 @@ namespace storm {
                 newRowGroup(matrix.size());
             }
             
+            template<typename StateType, typename ValueType>
+            void ExplorationInformation<StateType, ValueType>::terminateCurrentRowGroup() {
+                rowGroupIndices.push_back(matrix.size());
+            }
+            
+            template<typename StateType, typename ValueType>
+            void ExplorationInformation<StateType, ValueType>::moveActionToBackOfMatrix(ActionType const& action) {
+                matrix.emplace_back(std::move(matrix[action]));
+            }
+            
+            template<typename StateType, typename ValueType>
+            StateType ExplorationInformation<StateType, ValueType>::getActionCount() const {
+                return matrix.size();
+            }
+            
             template<typename StateType, typename ValueType>
             std::size_t ExplorationInformation<StateType, ValueType>::getNumberOfUnexploredStates() const {
                 return unexploredStates.size();
@@ -78,7 +92,7 @@ namespace storm {
             
             template<typename StateType, typename ValueType>
             std::size_t ExplorationInformation<StateType, ValueType>::getNumberOfDiscoveredStates() const {
-                return stateStorage.numberOfStates;
+                return stateToRowGroupMapping.size();
             }
             
             template<typename StateType, typename ValueType>
@@ -132,7 +146,7 @@ namespace storm {
             }
             
             template<typename StateType, typename ValueType>
-            void ExplorationInformation<StateType, ValueType>::addRowsToMatrix(std::size_t const& count) {
+            void ExplorationInformation<StateType, ValueType>::addActionsToMatrix(std::size_t const& count) {
                 matrix.resize(matrix.size() + count);
             }
             

src/modelchecker/exploration/ExplorationInformation.h

@@ -13,7 +13,6 @@
 #include "src/generator/CompressedState.h"
 
 #include "src/storage/SparseMatrix.h"
-#include "src/storage/sparse/StateStorage.h"
 
 #include "src/settings/modules/ExplorationSettings.h"
 
@@ -25,16 +24,19 @@ namespace storm {
             public:
                 typedef StateType ActionType;
                 typedef boost::container::flat_set<StateType> StateSet;
+                typedef std::unordered_map<StateType, storm::generator::CompressedState> IdToStateMap;
+                typedef typename IdToStateMap::const_iterator const_iterator;
+                typedef std::vector<std::vector<storm::storage::MatrixEntry<StateType, ValueType>>> MatrixType;
                 
-                ExplorationInformation(uint_fast64_t bitsPerBucket, storm::OptimizationDirection const& direction, ActionType const& unexploredMarker = std::numeric_limits<ActionType>::max());
+                ExplorationInformation(storm::OptimizationDirection const& direction, ActionType const& unexploredMarker = std::numeric_limits<ActionType>::max());
                 
-                void setInitialStates(std::vector<StateType> const& initialStates);
+                const_iterator findUnexploredState(StateType const& state) const;
                 
-                StateType getFirstInitialState() const;
+                const_iterator unexploredStatesEnd() const;
                 
-                std::size_t getNumberOfInitialStates() const;
+                void removeUnexploredState(const_iterator it);
                 
-                void addUnexploredState(storm::generator::CompressedState const& compressedState);
+                void addUnexploredState(StateType const& stateId, storm::generator::CompressedState const& compressedState);
                 
                 void assignStateToRowGroup(StateType const& state, ActionType const& rowGroup);
                 
@@ -46,6 +48,12 @@ namespace storm {
                 
                 void newRowGroup();
                 
+                void terminateCurrentRowGroup();
+                
+                void moveActionToBackOfMatrix(ActionType const& action);
+                
+                StateType getActionCount() const;
+                
                 std::size_t getNumberOfUnexploredStates() const;
                 
                 std::size_t getNumberOfDiscoveredStates() const;
@@ -70,7 +78,7 @@ namespace storm {
                 
                 std::vector<storm::storage::MatrixEntry<StateType, ValueType>> const& getRowOfMatrix(ActionType const& row) const;
                 
-                void addRowsToMatrix(std::size_t const& count);
+                void addActionsToMatrix(std::size_t const& count);
                 
                 bool maximize() const;
                 
@@ -95,14 +103,12 @@ namespace storm {
                 void setOptimizationDirection(storm::OptimizationDirection const& direction);
                 
             private:
-                storm::storage::sparse::StateStorage<StateType> stateStorage;
-                
-                std::vector<std::vector<storm::storage::MatrixEntry<StateType, ValueType>>> matrix;
+                MatrixType matrix;
                 std::vector<StateType> rowGroupIndices;
                 
                 std::vector<StateType> stateToRowGroupMapping;
                 StateType unexploredMarker;
-                std::unordered_map<StateType, storm::generator::CompressedState> unexploredStates;
+                IdToStateMap unexploredStates;
                 
                 storm::OptimizationDirection optimizationDirection;
                 StateSet terminalStates;

src/modelchecker/exploration/SparseMdpExplorationModelChecker.cpp

@@ -52,45 +52,26 @@ namespace storm {
             storm::logic::Formula const& targetFormula = untilFormula.getRightSubformula();
             STORM_LOG_THROW(program.isDeterministicModel() || checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException, "For nondeterministic systems, an optimization direction (min/max) must be given in the property.");
             
-            std::map<std::string, storm::expressions::Expression> labelToExpressionMapping = program.getLabelToExpressionMapping();
-            StateGeneration<StateType, ValueType> stateGeneration(program, variableInformation, conditionFormula.toExpression(program.getManager(), labelToExpressionMapping), targetFormula.toExpression(program.getManager(), labelToExpressionMapping));
-            
-            ExplorationInformation<StateType, ValueType> explorationInformation(variableInformation.getTotalBitOffset(true), checkTask.isOptimizationDirectionSet() ? checkTask.getOptimizationDirection() : storm::OptimizationDirection::Maximize);
-            
+            ExplorationInformation<StateType, ValueType> explorationInformation(checkTask.isOptimizationDirectionSet() ? checkTask.getOptimizationDirection() : storm::OptimizationDirection::Maximize);
+
             // The first row group starts at action 0.
             explorationInformation.newRowGroup(0);
             
-            // Create a callback for the next-state generator to enable it to request the index of states.
-            stateGeneration.setStateToIdCallback(createStateToIdCallback(explorationInformation));
+            std::map<std::string, storm::expressions::Expression> labelToExpressionMapping = program.getLabelToExpressionMapping();
+            StateGeneration<StateType, ValueType> stateGeneration(program, variableInformation, explorationInformation, conditionFormula.toExpression(program.getManager(), labelToExpressionMapping), targetFormula.toExpression(program.getManager(), labelToExpressionMapping));
+            
             
             // Compute and return result.
             std::tuple<StateType, ValueType, ValueType> boundsForInitialState = performExploration(stateGeneration, explorationInformation);
             return std::make_unique<ExplicitQuantitativeCheckResult<ValueType>>(std::get<0>(boundsForInitialState), std::get<1>(boundsForInitialState));
         }
-        
-        template<typename ValueType>
-        std::function<typename SparseMdpExplorationModelChecker<ValueType>::StateType (storm::generator::CompressedState const&)> SparseMdpExplorationModelChecker<ValueType>::createStateToIdCallback(ExplorationInformation<StateType, ValueType>& explorationInformation) const {
-            return [&explorationInformation,this] (storm::generator::CompressedState const& state) -> StateType {
-                StateType newIndex = explorationInformation.getNumberOfDiscoveredStates();
                 
-                // Check, if the state was already registered.
-                std::pair<uint32_t, std::size_t> actualIndexBucketPair = explorationInformation.stateStorage.stateToId.findOrAddAndGetBucket(state, newIndex);
-                
-                if (actualIndexBucketPair.first == newIndex) {
-                    explorationInformation.addUnexploredState(state);
-                }
-                
-                return actualIndexBucketPair.first;
-            };
-        }
-        
         template<typename ValueType>
         std::tuple<typename SparseMdpExplorationModelChecker<ValueType>::StateType, ValueType, ValueType> SparseMdpExplorationModelChecker<ValueType>::performExploration(StateGeneration<StateType, ValueType>& stateGeneration, ExplorationInformation<StateType, ValueType>& explorationInformation) const {
-            
             // Generate the initial state so we know where to start the simulation.
-            explorationInformation.setInitialStates(stateGeneration.getInitialStates());
-            STORM_LOG_THROW(explorationInformation.getNumberOfInitialStates() == 1, storm::exceptions::NotSupportedException, "Currently only models with one initial state are supported by the exploration engine.");
-            StateType initialStateIndex = explorationInformation.getFirstInitialState();
+            stateGeneration.computeInitialStates();
+            STORM_LOG_THROW(stateGeneration.getNumberOfInitialStates() == 1, storm::exceptions::NotSupportedException, "Currently only models with one initial state are supported by the exploration engine.");
+            StateType initialStateIndex = stateGeneration.getFirstInitialState();
             
             // Create a structure that holds the bounds for the states and actions.
             Bounds<StateType, ValueType> bounds;
@@ -141,7 +122,7 @@ namespace storm {
         template<typename ValueType>
         bool SparseMdpExplorationModelChecker<ValueType>::samplePathFromInitialState(StateGeneration<StateType, ValueType>& stateGeneration, ExplorationInformation<StateType, ValueType>& explorationInformation, StateActionStack& stack, Bounds<StateType, ValueType>& bounds, Statistics<StateType, ValueType>& stats) const {
             // Start the search from the initial state.
-            stack.push_back(std::make_pair(explorationInformation.getFirstInitialState(), 0));
+            stack.push_back(std::make_pair(stateGeneration.getFirstInitialState(), 0));
             
             // As long as we didn't find a terminal (accepting or rejecting) state in the search, sample a new successor.
             bool foundTerminalState = false;
@@ -150,8 +131,8 @@ namespace storm {
                 STORM_LOG_TRACE("State on top of stack is: " << currentStateId << ".");
                 
                 // If the state is not yet explored, we need to retrieve its behaviors.
-                auto unexploredIt = explorationInformation.unexploredStates.find(currentStateId);
-                if (unexploredIt != explorationInformation.unexploredStates.end()) {
+                auto unexploredIt = explorationInformation.findUnexploredState(currentStateId);
+                if (unexploredIt != explorationInformation.unexploredStatesEnd()) {
                     STORM_LOG_TRACE("State was not yet explored.");
                     
                     // Explore the previously unexplored state.
@@ -160,7 +141,7 @@ namespace storm {
                     if (foundTerminalState) {
                         STORM_LOG_TRACE("Aborting sampling of path, because a terminal state was reached.");
                     }
-                    explorationInformation.unexploredStates.erase(unexploredIt);
+                    explorationInformation.removeUnexploredState(unexploredIt);
                 } else {
                     // If the state was already explored, we check whether it is a terminal state or not.
                     if (explorationInformation.isTerminal(currentStateId)) {
@@ -245,30 +226,31 @@ namespace storm {
                 // need to store its behavior.
                 if (!isTerminalState) {
                     // Next, we insert the behavior into our matrix structure.
-                    StateType startRow = explorationInformation.matrix.size();
-                    explorationInformation.addRowsToMatrix(behavior.getNumberOfChoices());
+                    StateType startAction = explorationInformation.getActionCount();
+                    explorationInformation.addActionsToMatrix(behavior.getNumberOfChoices());
                     
-                    ActionType currentAction = 0;
+                    ActionType localAction = 0;
                     
                     // Retrieve the lowest state bounds (wrt. to the current optimization direction).
                     std::pair<ValueType, ValueType> stateBounds = getLowestBounds(explorationInformation.getOptimizationDirection());
                     
                     for (auto const& choice : behavior) {
                         for (auto const& entry : choice) {
-                            explorationInformation.getRowOfMatrix(startRow + currentAction).emplace_back(entry.first, entry.second);
+                            explorationInformation.getRowOfMatrix(startAction + localAction).emplace_back(entry.first, entry.second);
+                            std::cout << "adding " << (startAction + localAction) << "x" << entry.first << " -> " << entry.second << std::endl;
                         }
                         
-                        std::pair<ValueType, ValueType> actionBounds = computeBoundsOfAction(startRow + currentAction, explorationInformation, bounds);
+                        std::pair<ValueType, ValueType> actionBounds = computeBoundsOfAction(startAction + localAction, explorationInformation, bounds);
                         bounds.initializeBoundsForNextAction(actionBounds);
                         stateBounds = combineBounds(explorationInformation.getOptimizationDirection(), stateBounds, actionBounds);
 
-                        STORM_LOG_TRACE("Initializing bounds of action " << (startRow + currentAction) << " to " << bounds.getLowerBoundForAction(startRow + currentAction) << " and " << bounds.getUpperBoundForAction(startRow + currentAction) << ".");
+                        STORM_LOG_TRACE("Initializing bounds of action " << (startAction + localAction) << " to " << bounds.getLowerBoundForAction(startAction + localAction) << " and " << bounds.getUpperBoundForAction(startAction + localAction) << ".");
                         
-                        ++currentAction;
+                        ++localAction;
                     }
                     
                     // Terminate the row group.
-                    explorationInformation.rowGroupIndices.push_back(explorationInformation.matrix.size());
+                    explorationInformation.terminateCurrentRowGroup();
                     
                     bounds.setBoundsForState(currentStateId, explorationInformation, stateBounds);
                     STORM_LOG_TRACE("Initializing bounds of state " << currentStateId << " to " << bounds.getLowerBoundForState(currentStateId, explorationInformation) << " and " << bounds.getUpperBoundForState(currentStateId, explorationInformation) << ".");
@@ -292,7 +274,7 @@ namespace storm {
                 }
                 
                 // Increase the size of the matrix, but leave the row empty.
-                explorationInformation.addRowsToMatrix(1);
+                explorationInformation.addActionsToMatrix(1);
                 
                 // Terminate the row group.
                 explorationInformation.newRowGroup();
@@ -342,9 +324,9 @@ namespace storm {
         template<typename ValueType>
         typename SparseMdpExplorationModelChecker<ValueType>::StateType SparseMdpExplorationModelChecker<ValueType>::sampleSuccessorFromAction(ActionType const& chosenAction, ExplorationInformation<StateType, ValueType> const& explorationInformation, Bounds<StateType, ValueType> const& bounds) const {
             std::vector<storm::storage::MatrixEntry<StateType, ValueType>> const& row = explorationInformation.getRowOfMatrix(chosenAction);
-//            if (row.size() == 1) {
-//                return row.front().getColumn();
-//            }
+            if (row.size() == 1) {
+                return row.front().getColumn();
+            }
             
             std::vector<ValueType> probabilities(row.size());
             
@@ -352,6 +334,7 @@ namespace storm {
             if (explorationInformation.useDifferenceWeightedProbabilityHeuristic()) {
                 std::transform(row.begin(), row.end(), probabilities.begin(),
                                [&bounds, &explorationInformation] (storm::storage::MatrixEntry<StateType, ValueType> const& entry) {
+                                   std::cout << entry.getColumn() << " with diff " << bounds.getDifferenceOfStateBounds(entry.getColumn(), explorationInformation) << std::endl;
                                    return entry.getValue() * bounds.getDifferenceOfStateBounds(entry.getColumn(), explorationInformation);
                                });
             } else if (explorationInformation.useProbabilityHeuristic()) {
@@ -393,9 +376,8 @@ namespace storm {
                 relevantStates.resize(std::distance(relevantStates.begin(), newEnd));
             } else {
                 for (StateType state = 0; state < explorationInformation.getNumberOfDiscoveredStates(); ++state) {
-                    // Add the state to the relevant states if they are not unexplored. Additionally, if we are
-                    // computing minimal probabilities, we only consider it relevant if it's not a target state.
-                    if (!explorationInformation.isUnexplored(state) && (explorationInformation.maximize() || !comparator.isOne(bounds.getLowerBoundForState(state, explorationInformation)))) {
+                    // Add the state to the relevant states if they are not unexplored.
+                    if (!explorationInformation.isUnexplored(state)) {
                         relevantStates.push_back(state);
                     }
                 }
@@ -408,8 +390,10 @@ namespace storm {
             storm::storage::BitVector targetStates(sink + 1);
             for (StateType index = 0; index < relevantStates.size(); ++index) {
                 relevantStateToNewRowGroupMapping.emplace(relevantStates[index], index);
+                std::cout << "lower bound for state " << relevantStates[index] << " is " << bounds.getLowerBoundForState(relevantStates[index], explorationInformation) << std::endl;
                 if (storm::utility::isOne(bounds.getLowerBoundForState(relevantStates[index], explorationInformation))) {
                     targetStates.set(index);
+                    std::cout << relevantStates[index] << " was identified as a target state" << std::endl;
                 }
             }
             
@@ -425,9 +409,11 @@ namespace storm {
                         if (it != relevantStateToNewRowGroupMapping.end()) {
                             // If the entry is a relevant state, we copy it over (and compensate for the offset change).
                             builder.addNextValue(currentRow, it->second, entry.getValue());
+                            std::cout << state << " to " << entry.getColumn() << " with prob " << entry.getValue() << std::endl;
                         } else {
                             // If the entry is an unexpanded state, we gather the probability to later redirect it to an unexpanded sink.
                             unexpandedProbability += entry.getValue();
+                            std::cout << state << " has unexpanded prob " << unexpandedProbability << " to succ " << entry.getColumn() << std::endl;
                         }
                     }
                     if (unexpandedProbability != storm::utility::zero<ValueType>()) {
@@ -487,9 +473,13 @@ namespace storm {
                 statesWithProbability1 = storm::utility::graph::performProb1A(relevantStatesMatrix, relevantStatesMatrix.getRowGroupIndices(), transposedMatrix, allStates, targetStates);
             }
             
+            std::cout << statesWithProbability0 << std::endl;
+            std::cout << statesWithProbability1 << std::endl;
+            
             // Set the bounds of the identified states.
             for (auto state : statesWithProbability0) {
                 StateType originalState = relevantStates[state];
+                std::cout << "determined " << originalState << " as a prob0 state" << std::endl;
                 bounds.setUpperBoundForState(originalState, explorationInformation, storm::utility::zero<ValueType>());
                 explorationInformation.addTerminalState(originalState);
             }
@@ -558,7 +548,7 @@ namespace storm {
                 // the actions and the new state.
                 std::pair<ValueType, ValueType> stateBounds = getLowestBounds(explorationInformation.getOptimizationDirection());
                 for (auto const& action : leavingActions) {
-                    explorationInformation.matrix.emplace_back(std::move(explorationInformation.matrix[action]));
+                    explorationInformation.moveActionToBackOfMatrix(action);
                     std::pair<ValueType, ValueType> const& actionBounds = bounds.getBoundsForAction(action);
                     bounds.initializeBoundsForNextAction(actionBounds);
                     stateBounds = combineBounds(explorationInformation.getOptimizationDirection(), stateBounds, actionBounds);
@@ -566,7 +556,7 @@ namespace storm {
                 bounds.setBoundsForRowGroup(nextRowGroup, stateBounds);
                 
                 // Terminate the row group of the newly introduced state.
-                explorationInformation.rowGroupIndices.push_back(explorationInformation.matrix.size());
+                explorationInformation.terminateCurrentRowGroup();
             }
         }
         

src/modelchecker/exploration/SparseMdpExplorationModelChecker.h

@@ -44,8 +44,6 @@ namespace storm {
             virtual std::unique_ptr<CheckResult> computeUntilProbabilities(CheckTask<storm::logic::UntilFormula> const& checkTask) override;
             
         private:
-            std::function<StateType (storm::generator::CompressedState const&)> createStateToIdCallback(ExplorationInformation<StateType, ValueType>& explorationInformation) const;
-            
             std::tuple<StateType, ValueType, ValueType> performExploration(StateGeneration<StateType, ValueType>& stateGeneration, ExplorationInformation<StateType, ValueType>& explorationInformation) const;
 
             bool samplePathFromInitialState(StateGeneration<StateType, ValueType>& stateGeneration, ExplorationInformation<StateType, ValueType>& explorationInformation, StateActionStack& stack, Bounds<StateType, ValueType>& bounds, Statistics<StateType, ValueType>& stats) const;

src/modelchecker/exploration/StateGeneration.cpp

@@ -1,17 +1,26 @@
 #include "src/modelchecker/exploration/StateGeneration.h"
 
+#include "src/modelchecker/exploration/ExplorationInformation.h"
+
 namespace storm {
     namespace modelchecker {
         namespace exploration_detail {
             
             template <typename StateType, typename ValueType>
-            StateGeneration<StateType, ValueType>::StateGeneration(storm::prism::Program const& program, storm::generator::VariableInformation const& variableInformation, storm::expressions::Expression const& conditionStateExpression, storm::expressions::Expression const& targetStateExpression) : generator(program, variableInformation, false), conditionStateExpression(conditionStateExpression), targetStateExpression(targetStateExpression) {
-                // Intentionally left empty.
-            }
-            
-            template <typename StateType, typename ValueType>
-            void StateGeneration<StateType, ValueType>::setStateToIdCallback(std::function<StateType (storm::generator::CompressedState const&)> const& stateToIdCallback) {
-                this->stateToIdCallback = stateToIdCallback;
+            StateGeneration<StateType, ValueType>::StateGeneration(storm::prism::Program const& program, storm::generator::VariableInformation const& variableInformation, ExplorationInformation<StateType, ValueType>& explorationInformation, storm::expressions::Expression const& conditionStateExpression, storm::expressions::Expression const& targetStateExpression) : generator(program, variableInformation, false), stateStorage(variableInformation.getTotalBitOffset(true)), conditionStateExpression(conditionStateExpression), targetStateExpression(targetStateExpression) {
+                
+                stateToIdCallback = [&explorationInformation, this] (storm::generator::CompressedState const& state) -> StateType {
+                    StateType newIndex = stateStorage.getNumberOfStates();
+                    
+                    // Check, if the state was already registered.
+                    std::pair<StateType, std::size_t> actualIndexBucketPair = stateStorage.stateToId.findOrAddAndGetBucket(state, newIndex);
+                    
+                    if (actualIndexBucketPair.first == newIndex) {
+                        explorationInformation.addUnexploredState(newIndex, state);
+                    }
+                    
+                    return actualIndexBucketPair.first;
+                };
             }
             
             template <typename StateType, typename ValueType>
@@ -21,7 +30,7 @@ namespace storm {
             
             template <typename StateType, typename ValueType>
             std::vector<StateType> StateGeneration<StateType, ValueType>::getInitialStates() {
-                return generator.getInitialStates(stateToIdCallback);
+                return stateStorage.initialStateIndices;
             }
             
             template <typename StateType, typename ValueType>
@@ -38,7 +47,22 @@ namespace storm {
             bool StateGeneration<StateType, ValueType>::isTargetState() const {
                 return generator.satisfies(targetStateExpression);
             }
-         
+            
+            template<typename StateType, typename ValueType>
+            void StateGeneration<StateType, ValueType>::computeInitialStates() {
+                stateStorage.initialStateIndices = generator.getInitialStates(stateToIdCallback);
+            }
+            
+            template<typename StateType, typename ValueType>
+            StateType StateGeneration<StateType, ValueType>::getFirstInitialState() const {
+                return stateStorage.initialStateIndices.front();
+            }
+            
+            template<typename StateType, typename ValueType>
+            std::size_t StateGeneration<StateType, ValueType>::getNumberOfInitialStates() const {
+                return stateStorage.initialStateIndices.size();
+            }
+            
             template class StateGeneration<uint32_t, double>;
         }
     }

src/modelchecker/exploration/StateGeneration.h

@@ -4,6 +4,8 @@
 #include "src/generator/CompressedState.h"
 #include "src/generator/PrismNextStateGenerator.h"
 
+#include "src/storage/sparse/StateStorage.h"
+
 namespace storm {
     namespace generator {
         template<typename ValueType, typename StateType>
@@ -13,19 +15,26 @@ namespace storm {
     namespace modelchecker {
         namespace exploration_detail {
             
+            template <typename StateType, typename ValueType>
+            class ExplorationInformation;
+            
             template <typename StateType, typename ValueType>
             class StateGeneration {
             public:
-                StateGeneration(storm::prism::Program const& program, storm::generator::VariableInformation const& variableInformation, storm::expressions::Expression const& conditionStateExpression, storm::expressions::Expression const& targetStateExpression);
-                
-                void setStateToIdCallback(std::function<StateType (storm::generator::CompressedState const&)> const& stateToIdCallback);
-                
+                StateGeneration(storm::prism::Program const& program, storm::generator::VariableInformation const& variableInformation, ExplorationInformation<StateType, ValueType>& explorationInformation, storm::expressions::Expression const& conditionStateExpression, storm::expressions::Expression const& targetStateExpression);
+                                
                 void load(storm::generator::CompressedState const& state);
                 
                 std::vector<StateType> getInitialStates();
                 
                 storm::generator::StateBehavior<ValueType, StateType> expand();
                 
+                void computeInitialStates();
+                
+                StateType getFirstInitialState() const;
+                
+                std::size_t getNumberOfInitialStates() const;
+                
                 bool isConditionState() const;
                 
                 bool isTargetState() const;
@@ -33,6 +42,9 @@ namespace storm {
             private:
                 storm::generator::PrismNextStateGenerator<ValueType, StateType> generator;
                 std::function<StateType (storm::generator::CompressedState const&)> stateToIdCallback;
+                
+                storm::storage::sparse::StateStorage<StateType> stateStorage;
+
                 storm::expressions::Expression conditionStateExpression;
                 storm::expressions::Expression targetStateExpression;
             };

src/settings/modules/ExplorationSettings.cpp

@@ -19,8 +19,8 @@ namespace storm {
             ExplorationSettings::ExplorationSettings(storm::settings::SettingsManager& settingsManager) : ModuleSettings(settingsManager, moduleName) {
                 std::vector<std::string> types = { "local", "global" };
                     this->addOption(storm::settings::OptionBuilder(moduleName, precomputationTypeOptionName, true, "Sets the kind of precomputation used. Available are: { local, global }.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the type to use.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(types)).setDefaultValueString("global").build()).build());
-                this->addOption(storm::settings::OptionBuilder(moduleName, numberOfExplorationStepsUntilPrecomputationOptionName, false, "Sets the number of exploration steps to perform until a precomputation is triggered.").addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("count", "The number of exploration steps to perform.").setDefaultValueUnsignedInteger(100000).build()).build());
-                this->addOption(storm::settings::OptionBuilder(moduleName, numberOfSampledPathsUntilPrecomputationOptionName, false, "If set, a precomputation is perfomed periodically after the given number of paths has been sampled.").addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("count", "The number of paths to sample until a precomputation is triggered.").setDefaultValueUnsignedInteger(100000).build()).build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, numberOfExplorationStepsUntilPrecomputationOptionName, true, "Sets the number of exploration steps to perform until a precomputation is triggered.").addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("count", "The number of exploration steps to perform.").setDefaultValueUnsignedInteger(100000).build()).build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, numberOfSampledPathsUntilPrecomputationOptionName, true, "If set, a precomputation is perfomed periodically after the given number of paths has been sampled.").addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("count", "The number of paths to sample until a precomputation is triggered.").setDefaultValueUnsignedInteger(100000).build()).build());
                 
                 std::vector<std::string> nextStateHeuristics = { "probdiff", "prob" };
                 this->addOption(storm::settings::OptionBuilder(moduleName, nextStateHeuristicOptionName, true, "Sets the next-state heuristic to use. Available are: { probdiff, prob } where 'prob' samples according to the probabilities in the system and 'probdiff' weights the probabilities with the differences between the current bounds.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the heuristic to use.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(nextStateHeuristics)).setDefaultValueString("probdiff").build()).build());

src/storage/sparse/StateStorage.cpp

@@ -5,10 +5,15 @@ namespace storm {
         namespace sparse {
                         
             template <typename StateType>
-            StateStorage<StateType>::StateStorage(uint64_t bitsPerState) : stateToId(bitsPerState, 10000000), initialStateIndices(), bitsPerState(bitsPerState), numberOfStates() {
+            StateStorage<StateType>::StateStorage(uint64_t bitsPerState) : stateToId(bitsPerState, 10000000), initialStateIndices(), bitsPerState(bitsPerState) {
                 // Intentionally left empty.
             }
 
+            template <typename StateType>
+            uint_fast64_t StateStorage<StateType>::getNumberOfStates() const {
+                return stateToId.size();
+            }
+            
             template class StateStorage<uint32_t>;
         }
     }

src/storage/sparse/StateStorage.h

@@ -25,7 +25,7 @@ namespace storm {
                 uint64_t bitsPerState;
                 
                 // The number of states that were found in the exploration so far.
-                uint_fast64_t numberOfStates;
+                uint_fast64_t getNumberOfStates() const;
             };
             
         }