learning seems to work find on first larger example

Former-commit-id: 706981a362

src/builder/ExplicitPrismModelBuilder.cpp

@@ -227,18 +227,6 @@ namespace storm {
             return result;
         }
         
-        template <typename ValueType, typename RewardModelType, typename StateType>
-        storm::expressions::SimpleValuation ExplicitPrismModelBuilder<ValueType, RewardModelType, StateType>::unpackStateIntoValuation(storm::storage::BitVector const& currentState) {
-            storm::expressions::SimpleValuation result(program.getManager().getSharedPointer());
-            for (auto const& booleanVariable : variableInformation.booleanVariables) {
-                result.setBooleanValue(booleanVariable.variable, currentState.get(booleanVariable.bitOffset));
-            }
-            for (auto const& integerVariable : variableInformation.integerVariables) {
-                result.setIntegerValue(integerVariable.variable, currentState.getAsInt(integerVariable.bitOffset, integerVariable.bitWidth) + integerVariable.lowerBound);
-            }
-            return result;
-        }
-        
         template <typename ValueType, typename RewardModelType, typename StateType>
         StateType ExplicitPrismModelBuilder<ValueType, RewardModelType, StateType>::getOrAddStateIndex(CompressedState const& state) {
             uint32_t newIndex = stateStorage.numberOfStates;
@@ -343,7 +331,7 @@ namespace storm {
                         ++currentRow;
                         ++currentRowGroup;
                     } else {
-                        std::cout << unpackStateIntoValuation(currentState).toString(true) << std::endl;
+                        std::cout << storm::generator::unpackStateIntoValuation(currentState, variableInformation, program.getManager()).toString(true) << std::endl;
                         STORM_LOG_THROW(false, storm::exceptions::WrongFormatException,
                                         "Error while creating sparse matrix from probabilistic program: found deadlock state. For fixing these, please provide the appropriate option.");
                     }
@@ -481,7 +469,7 @@ namespace storm {
             if (options.buildStateValuations) {
                 stateValuations = storm::storage::sparse::StateValuations(stateStorage.numberOfStates);
                 for (auto const& bitVectorIndexPair : stateStorage.stateToId) {
-                    stateValuations.get().valuations[bitVectorIndexPair.second] = unpackStateIntoValuation(bitVectorIndexPair.first);
+                    stateValuations.get().valuations[bitVectorIndexPair.second] = unpackStateIntoValuation(bitVectorIndexPair.first, variableInformation, program.getManager());
                 }
             }
             

src/builder/ExplicitPrismModelBuilder.h

@@ -190,8 +190,6 @@ namespace storm {
             storm::prism::Program const& getTranslatedProgram() const;
             
         private:
-            storm::expressions::SimpleValuation unpackStateIntoValuation(storm::storage::BitVector const& currentState);
-            
             /*!
              * Retrieves the state id of the given state. If the state has not been encountered yet, it will be added to
              * the lists of all states with a new id. If the state was already known, the object that is pointed to by

src/generator/CompressedState.cpp

@@ -1,6 +1,8 @@
 #include "src/generator/CompressedState.h"
 
 #include "src/generator/VariableInformation.h"
+#include "src/storage/expressions/ExpressionManager.h"
+#include "src/storage/expressions/SimpleValuation.h"
 #include "src/storage/expressions/ExpressionEvaluator.h"
 
 namespace storm {
@@ -14,10 +16,21 @@ namespace storm {
             for (auto const& integerVariable : variableInformation.integerVariables) {
                 evaluator.setIntegerValue(integerVariable.variable, state.getAsInt(integerVariable.bitOffset, integerVariable.bitWidth) + integerVariable.lowerBound);
             }
-
+        }
+        
+        storm::expressions::SimpleValuation unpackStateIntoValuation(CompressedState const& state, VariableInformation const& variableInformation, storm::expressions::ExpressionManager const& manager) {
+            storm::expressions::SimpleValuation result(manager.getSharedPointer());
+            for (auto const& booleanVariable : variableInformation.booleanVariables) {
+                result.setBooleanValue(booleanVariable.variable, state.get(booleanVariable.bitOffset));
+            }
+            for (auto const& integerVariable : variableInformation.integerVariables) {
+                result.setIntegerValue(integerVariable.variable, state.getAsInt(integerVariable.bitOffset, integerVariable.bitWidth) + integerVariable.lowerBound);
+            }
+            return result;
         }
 
         template void unpackStateIntoEvaluator<double>(CompressedState const& state, VariableInformation const& variableInformation, storm::expressions::ExpressionEvaluator<double>& evaluator);
         template void unpackStateIntoEvaluator<storm::RationalFunction>(CompressedState const& state, VariableInformation const& variableInformation, storm::expressions::ExpressionEvaluator<storm::RationalFunction>& evaluator);
+        storm::expressions::SimpleValuation unpackStateIntoValuation(CompressedState const& state, VariableInformation const& variableInformation, storm::expressions::ExpressionManager const& manager);
     }
 }

src/generator/CompressedState.h

@@ -6,6 +6,9 @@
 namespace storm {
     namespace expressions {
         template<typename ValueType> class ExpressionEvaluator;
+        
+        class ExpressionManager;
+        class SimpleValuation;
     }
     
     namespace generator {
@@ -18,11 +21,21 @@ namespace storm {
          * Unpacks the compressed state into the evaluator.
          *
          * @param state The state to unpack.
-         * @param variableInformation The information about how the variables are packed with the state.
+         * @param variableInformation The information about how the variables are packed within the state.
          * @param evaluator The evaluator into which to load the state.
          */
         template<typename ValueType>
         void unpackStateIntoEvaluator(CompressedState const& state, VariableInformation const& variableInformation, storm::expressions::ExpressionEvaluator<ValueType>& evaluator);
+
+        /*!
+         * Converts the compressed state into an explicit representation in the form of a valuation.
+         *
+         * @param state The state to unpack.
+         * @param variableInformation The information about how the variables are packed within the state.
+         * @param manager The manager responsible for the variables.
+         * @return A valuation that corresponds to the compressed state.
+         */
+        storm::expressions::SimpleValuation unpackStateIntoValuation(CompressedState const& state, VariableInformation const& variableInformation, storm::expressions::ExpressionManager const& manager);
     }
 }
 

src/modelchecker/reachability/SparseMdpLearningModelChecker.cpp

@@ -2,6 +2,7 @@
 
 #include "src/storage/SparseMatrix.h"
 #include "src/storage/MaximalEndComponentDecomposition.h"
+#include "src/storage/expressions/SimpleValuation.h"
 
 #include "src/logic/FragmentSpecification.h"
 
@@ -15,6 +16,8 @@
 #include "src/settings/modules/GeneralSettings.h"
 #include "src/settings/modules/LearningSettings.h"
 
+#include "src/utility/graph.h"
+
 #include "src/utility/macros.h"
 #include "src/exceptions/InvalidOperationException.h"
 #include "src/exceptions/InvalidPropertyException.h"
@@ -42,7 +45,7 @@ namespace storm {
             
             StateGeneration stateGeneration(program, variableInformation, getTargetStateExpression(subformula));
             
-            ExplorationInformation explorationInformation(variableInformation.getTotalBitOffset(true), storm::settings::learningSettings().isLocalECDetectionSet());
+            ExplorationInformation explorationInformation(variableInformation.getTotalBitOffset(true), storm::settings::learningSettings().isLocalPrecomputationSet(), storm::settings::learningSettings().getNumberOfExplorationStepsUntilPrecomputation());
             explorationInformation.optimizationDirection = checkTask.isOptimizationDirectionSet() ? checkTask.getOptimizationDirection() : storm::OptimizationDirection::Maximize;
             
             // The first row group starts at action 0.
@@ -70,7 +73,7 @@ namespace storm {
         
         template<typename ValueType>
         std::function<typename SparseMdpLearningModelChecker<ValueType>::StateType (storm::generator::CompressedState const&)> SparseMdpLearningModelChecker<ValueType>::createStateToIdCallback(ExplorationInformation& explorationInformation) const {
-            return [&explorationInformation] (storm::generator::CompressedState const& state) -> StateType {
+            return [&explorationInformation,this] (storm::generator::CompressedState const& state) -> StateType {
                 StateType newIndex = explorationInformation.stateStorage.numberOfStates;
                 
                 // Check, if the state was already registered.
@@ -118,16 +121,16 @@ namespace storm {
                 STORM_LOG_DEBUG("Discovered states: " << explorationInformation.getNumberOfDiscoveredStates() << " (" << stats.numberOfExploredStates << " explored, " << explorationInformation.getNumberOfUnexploredStates() << " unexplored).");
                 STORM_LOG_DEBUG("Value of initial state is in [" << bounds.getLowerBoundForState(initialStateIndex, explorationInformation) << ", " << bounds.getUpperBoundForState(initialStateIndex, explorationInformation) << "].");
                 ValueType difference = bounds.getDifferenceOfStateBounds(initialStateIndex, explorationInformation);
-                STORM_LOG_DEBUG("Difference after iteration " << stats.iterations << " is " << difference << ".");
+                STORM_LOG_DEBUG("Difference after iteration " << stats.pathsSampled << " is " << difference << ".");
                 convergenceCriterionMet = comparator.isZero(difference);
                 
-                ++stats.iterations;
+                ++stats.pathsSampled;
             }
             
             if (storm::settings::generalSettings().isShowStatisticsSet()) {
                 std::cout << std::endl << "Learning summary -------------------------" << std::endl;
                 std::cout << "Discovered states: " << explorationInformation.getNumberOfDiscoveredStates() << " (" << stats.numberOfExploredStates << " explored, " << explorationInformation.getNumberOfUnexploredStates() << " unexplored, " << stats.numberOfTargetStates << " target)" << std::endl;
-                std::cout << "Sampled paths: " << stats.iterations << std::endl;
+                std::cout << "Sampled paths: " << stats.pathsSampled << std::endl;
                 std::cout << "Maximal path length: " << stats.maxPathLength << std::endl;
                 std::cout << "EC detections: " << stats.ecDetections << " (" << stats.failedEcDetections << " failed, " << stats.totalNumberOfEcDetected << " EC(s) detected)" << std::endl;
             }
@@ -154,6 +157,9 @@ namespace storm {
                     // Explore the previously unexplored state.
                     storm::generator::CompressedState const& compressedState = unexploredIt->second;
                     foundTerminalState = exploreState(stateGeneration, currentStateId, compressedState, explorationInformation, bounds, stats);
+                    if (foundTerminalState) {
+                        STORM_LOG_TRACE("Aborting sampling of path, because a terminal state was reached.");
+                    }
                     explorationInformation.unexploredStates.erase(unexploredIt);
                 } else {
                     // If the state was already explored, we check whether it is a terminal state or not.
@@ -163,6 +169,9 @@ namespace storm {
                     }
                 }
                 
+                // Increase the number of exploration steps to eventually trigger the precomputation.
+                ++stats.explorationSteps;
+                
                 // If the state was not a terminal state, we continue the path search and sample the next state.
                 if (!foundTerminalState) {
                     // At this point, we can be sure that the state was expanded and that we can sample according to the
@@ -171,25 +180,20 @@ namespace storm {
                     stack.back().second = chosenAction;
                     STORM_LOG_TRACE("Sampled action " << chosenAction << " in state " << currentStateId << ".");
                     
-                    StateType successor = sampleSuccessorFromAction(chosenAction, explorationInformation);
+                    StateType successor = sampleSuccessorFromAction(chosenAction, explorationInformation, bounds);
                     STORM_LOG_TRACE("Sampled successor " << successor << " according to action " << chosenAction << " of state " << currentStateId << ".");
                     
                     // Put the successor state and a dummy action on top of the stack.
                     stack.emplace_back(successor, 0);
                     stats.maxPathLength = std::max(stats.maxPathLength, stack.size());
                     
-                    // If the current path length exceeds the threshold and the model is a nondeterministic one, we
-                    // perform an EC detection.
-                    if (stack.size() > explorationInformation.getPathLengthUntilEndComponentDetection()) {
-                        bool success = detectEndComponents(stack, explorationInformation, bounds, stats);
+                    // If the number of exploration steps exceeds a certain threshold, do a precomputation.
+                    if (explorationInformation.performPrecomputation(stats.explorationSteps)) {
+                        performPrecomputation(stack, explorationInformation, bounds, stats);
                         
-                        // Only if the detection found an EC, we abort the search.
-                        if (success) {
-                            // Abort the current search.
-                            STORM_LOG_TRACE("Aborting the search after succesful EC detection.");
-                            stack.clear();
-                            break;
-                        }
+                        STORM_LOG_TRACE("Aborting the search after precomputation.");
+                        stack.clear();
+                        break;
                     }
                 }
             }
@@ -333,10 +337,10 @@ namespace storm {
         }
         
         template<typename ValueType>
-        typename SparseMdpLearningModelChecker<ValueType>::StateType SparseMdpLearningModelChecker<ValueType>::sampleSuccessorFromAction(ActionType const& chosenAction, ExplorationInformation const& explorationInformation) const {
+        typename SparseMdpLearningModelChecker<ValueType>::StateType SparseMdpLearningModelChecker<ValueType>::sampleSuccessorFromAction(ActionType const& chosenAction, ExplorationInformation const& explorationInformation, BoundValues const& bounds) const {
             // TODO: precompute this?
             std::vector<ValueType> probabilities(explorationInformation.getRowOfMatrix(chosenAction).size());
-            std::transform(explorationInformation.getRowOfMatrix(chosenAction).begin(), explorationInformation.getRowOfMatrix(chosenAction).end(), probabilities.begin(), [] (storm::storage::MatrixEntry<StateType, ValueType> const& entry) { return entry.getValue(); } );
+            std::transform(explorationInformation.getRowOfMatrix(chosenAction).begin(), explorationInformation.getRowOfMatrix(chosenAction).end(), probabilities.begin(), [&bounds, &explorationInformation] (storm::storage::MatrixEntry<StateType, ValueType> const& entry) { return entry.getValue() * bounds.getDifferenceOfStateBounds(entry.getColumn(), explorationInformation) ; } );
             
             // Now sample according to the probabilities.
             std::discrete_distribution<StateType> distribution(probabilities.begin(), probabilities.end());
@@ -345,21 +349,27 @@ namespace storm {
         }
         
         template<typename ValueType>
-        bool SparseMdpLearningModelChecker<ValueType>::detectEndComponents(StateActionStack const& stack, ExplorationInformation& explorationInformation, BoundValues& bounds, Statistics& stats) const {
-            STORM_LOG_TRACE("Starting " << (explorationInformation.useLocalECDetection() ? "local" : "global") << "EC detection.");
-            ++stats.ecDetections;
-            
+        bool SparseMdpLearningModelChecker<ValueType>::performPrecomputation(StateActionStack const& stack, ExplorationInformation& explorationInformation, BoundValues& bounds, Statistics& stats) const {
             // Outline:
             // 1. construct a sparse transition matrix of the relevant part of the state space.
-            // 2. use this matrix to compute an MEC decomposition.
-            // 3. if non-empty, analyze the decomposition for accepting/rejecting MECs.
+            // 2. use this matrix to compute states with probability 0/1 and an MEC decomposition (in the max case).
+            // 3. use MEC decomposition to collapse MECs.
+            STORM_LOG_TRACE("Starting " << (explorationInformation.useLocalPrecomputation() ? "local" : "global") << " precomputation.");
+
+            for (int row = 0; row < explorationInformation.matrix.size(); ++row) {
+                std::cout << "row " << row << ":";
+                for (auto const& el : explorationInformation.matrix[row]) {
+                    std::cout << el.getColumn() << ", " << el.getValue() << " [" << bounds.getLowerBoundForState(el.getColumn(), explorationInformation) << ", " << bounds.getUpperBoundForState(el.getColumn(), explorationInformation) << "]" << "  ";
+                }
+                std::cout << std::endl;
+            }
             
-            // Start with 1.
+            // Construct the matrix that represents the fragment of the system contained in the currently sampled path.
             storm::storage::SparseMatrixBuilder<ValueType> builder(0, 0, 0, false, true, 0);
             
             // Determine the set of states that was expanded.
             std::vector<StateType> relevantStates;
-            if (explorationInformation.useLocalECDetection()) {
+            if (explorationInformation.useLocalPrecomputation()) {
                 for (auto const& stateActionPair : stack) {
                     if (explorationInformation.maximize() || !comparator.isOne(bounds.getLowerBoundForState(stateActionPair.first, explorationInformation))) {
                         relevantStates.push_back(stateActionPair.first);
@@ -380,9 +390,15 @@ namespace storm {
             StateType sink = relevantStates.size();
             
             // Create a mapping for faster look-up during the translation of flexible matrix to the real sparse matrix.
+            // While doing so, record all target states.
             std::unordered_map<StateType, StateType> relevantStateToNewRowGroupMapping;
+            storm::storage::BitVector targetStates(sink + 1);
             for (StateType index = 0; index < relevantStates.size(); ++index) {
                 relevantStateToNewRowGroupMapping.emplace(relevantStates[index], index);
+                if (storm::utility::isOne(bounds.getLowerBoundForState(relevantStates[index], explorationInformation))) {
+                    std::cout << "target states: " << targetStates << std::endl;
+                    targetStates.set(index);
+                }
             }
             
             // Do the actual translation.
@@ -411,48 +427,76 @@ namespace storm {
             // Then, make the unexpanded state absorbing.
             builder.newRowGroup(currentRow);
             builder.addNextValue(currentRow, sink, storm::utility::one<ValueType>());
-            STORM_LOG_TRACE("Successfully built matrix for MEC decomposition.");
-            
-            // Go on to step 2.
             storm::storage::SparseMatrix<ValueType> relevantStatesMatrix = builder.build();
-            storm::storage::MaximalEndComponentDecomposition<ValueType> mecDecomposition(relevantStatesMatrix, relevantStatesMatrix.transpose(true));
-            STORM_LOG_TRACE("Successfully computed MEC decomposition. Found " << (mecDecomposition.size() > 1 ? (mecDecomposition.size() - 1) : 0) << " MEC(s).");
-            
-            // If the decomposition contains only the MEC consisting of the sink state, we count it as 'failed'.
-            if (mecDecomposition.size() <= 1) {
-                ++stats.failedEcDetections;
-//                explorationInformation.increasePathLengthUntilEndComponentDetection();
-                return false;
-            } else {
-                stats.totalNumberOfEcDetected += mecDecomposition.size() - 1;
-                
-                // 3. Analyze the MEC decomposition.
-                for (auto const& mec : mecDecomposition) {
-                    // Ignore the (expected) MEC of the sink state.
-                    if (mec.containsState(sink)) {
-                        continue;
-                    }
+            storm::storage::SparseMatrix<ValueType> transposedMatrix = relevantStatesMatrix.transpose(true);
+            STORM_LOG_TRACE("Successfully built matrix for precomputation.");
+            
+            storm::storage::BitVector allStates(sink + 1, true);
+            storm::storage::BitVector statesWithProbability0;
+            storm::storage::BitVector statesWithProbability1;
+            if (explorationInformation.maximize()) {
+                // If we are computing maximal probabilities, we first perform a detection of states that have
+                // probability 01 and then additionally perform an MEC decomposition. The reason for this somewhat
+                // duplicate work is the following. Optimally, we would only do the MEC decomposition, because we need
+                // it anyway. However, when only detecting (accepting) MECs, we do not infer which of the other states
+                // (not contained in MECs) also have probability 0/1.
+                statesWithProbability0 = storm::utility::graph::performProb0A(relevantStatesMatrix, relevantStatesMatrix.getRowGroupIndices(), transposedMatrix, allStates, targetStates);
+                targetStates.set(sink, true);
+                statesWithProbability1 = storm::utility::graph::performProb1E(relevantStatesMatrix, relevantStatesMatrix.getRowGroupIndices(), transposedMatrix, allStates, targetStates);
+
+                storm::storage::MaximalEndComponentDecomposition<ValueType> mecDecomposition(relevantStatesMatrix, relevantStatesMatrix.transpose(true));
+                ++stats.ecDetections;
+                STORM_LOG_TRACE("Successfully computed MEC decomposition. Found " << (mecDecomposition.size() > 1 ? (mecDecomposition.size() - 1) : 0) << " MEC(s).");
+
+                // If the decomposition contains only the MEC consisting of the sink state, we count it as 'failed'.
+                if (mecDecomposition.size() > 1) {
+                    ++stats.failedEcDetections;
+                } else {
+                    stats.totalNumberOfEcDetected += mecDecomposition.size() - 1;
                     
-                    if (explorationInformation.maximize()) {
-                        analyzeMecForMaximalProbabilities(mec, relevantStates, relevantStatesMatrix, explorationInformation, bounds);
-                    } else {
-                        analyzeMecForMinimalProbabilities(mec, relevantStates, relevantStatesMatrix, explorationInformation, bounds);
+                    // 3. Analyze the MEC decomposition.
+                    for (auto const& mec : mecDecomposition) {
+                        // Ignore the (expected) MEC of the sink state.
+                        if (mec.containsState(sink)) {
+                            continue;
+                        }
+                        
+                        collapseMec(mec, relevantStates, relevantStatesMatrix, explorationInformation, bounds);
                     }
                 }
+            } else {
+                // If we are computing minimal probabilities, we do not need to perform an EC-detection. We rather
+                // compute all states (of the considered fragment) that have probability 0/1. For states with
+                // probability 0, we have to mark the sink as being a target. For states with probability 1, however,
+                // we must treat the sink as being rejecting.
+                targetStates.set(sink, true);
+                statesWithProbability0 = storm::utility::graph::performProb0E(relevantStatesMatrix, relevantStatesMatrix.getRowGroupIndices(), transposedMatrix, allStates, targetStates);
+                targetStates.set(sink, false);
+                statesWithProbability1 = storm::utility::graph::performProb1A(relevantStatesMatrix, relevantStatesMatrix.getRowGroupIndices(), transposedMatrix, allStates, targetStates);
+            }
+            
+            std::cout << "prob0: " << statesWithProbability0 << std::endl;
+            std::cout << "prob1: " << statesWithProbability1 << std::endl;
+            
+            // Set the bounds of the identified states.
+            for (auto state : statesWithProbability0) {
+                StateType originalState = relevantStates[state];
+                bounds.setUpperBoundForState(originalState, explorationInformation, storm::utility::zero<ValueType>());
+                explorationInformation.addTerminalState(originalState);
+            }
+            for (auto state : statesWithProbability1) {
+                StateType originalState = relevantStates[state];
+                bounds.setLowerBoundForState(originalState, explorationInformation, storm::utility::one<ValueType>());
+                explorationInformation.addTerminalState(originalState);
             }
             return true;
         }
         
         template<typename ValueType>
-        void SparseMdpLearningModelChecker<ValueType>::analyzeMecForMaximalProbabilities(storm::storage::MaximalEndComponent const& mec, std::vector<StateType> const& relevantStates, storm::storage::SparseMatrix<ValueType> const& relevantStatesMatrix, ExplorationInformation& explorationInformation, BoundValues& bounds) const {
-            // For maximal probabilities, we check (a) which MECs contain a target state, because the associated states
-            // have a probability of 1 (and we can therefore set their lower bounds to 1) and (b) which of the remaining
-            // MECs have no outgoing action, because the associated states have a probability of 0 (and we can therefore
-            // set their upper bounds to 0).
-            
+        void SparseMdpLearningModelChecker<ValueType>::collapseMec(storm::storage::MaximalEndComponent const& mec, std::vector<StateType> const& relevantStates, storm::storage::SparseMatrix<ValueType> const& relevantStatesMatrix, ExplorationInformation& explorationInformation, BoundValues& bounds) const {
             bool containsTargetState = false;
             
-            // Now we record all choices leaving the EC.
+            // Now we record all actions leaving the EC.
             std::vector<ActionType> leavingActions;
             for (auto const& stateAndChoices : mec) {
                 // Compute the state of the original model that corresponds to the current state.
@@ -485,34 +529,14 @@ namespace storm {
                 }
             }
             
-            // If one of the states of the EC is a target state, all states in the EC have probability 1.
-            if (containsTargetState) {
-                STORM_LOG_TRACE("MEC contains a target state.");
-                for (auto const& stateAndChoices : mec) {
-                    // Compute the state of the original model that corresponds to the current state.
-                    StateType const& originalState = relevantStates[stateAndChoices.first];
-                    
-                    STORM_LOG_TRACE("Setting lower bound of state in row group " << explorationInformation.getRowGroup(originalState) << " to 1.");
-                    bounds.setLowerBoundForState(originalState, explorationInformation, storm::utility::one<ValueType>());
-                    explorationInformation.addTerminalState(originalState);
-                }
-            } else if (leavingActions.empty()) {
-                STORM_LOG_TRACE("MEC's leaving choices are empty.");
-                // If there is no choice leaving the EC, but it contains no target state, all states have probability 0.
-                for (auto const& stateAndChoices : mec) {
-                    // Compute the state of the original model that corresponds to the current state.
-                    StateType const& originalState = relevantStates[stateAndChoices.first];
-                    
-                    STORM_LOG_TRACE("Setting upper bound of state in row group " << explorationInformation.getRowGroup(originalState) << " to 0.");
-                    bounds.setUpperBoundForState(originalState, explorationInformation, storm::utility::zero<ValueType>());
-                    explorationInformation.addTerminalState(originalState);
-                }
-            } else {
+            // Now, we need to collapse the EC only if it does not contain a target state and the leaving actions are
+            // non-empty, because only then have the states a (potentially) non-zero, non-one probability.
+            if (!containsTargetState && !leavingActions.empty()) {
                 // In this case, no target state is contained in the MEC, but there are actions leaving the MEC. To
                 // prevent the simulation getting stuck in this MEC again, we replace all states in the MEC by a new
                 // state whose outgoing actions are the ones leaving the MEC. We do this, by assigning all states in the
                 // MEC to a new row group, which will then hold all the outgoing choices.
-
+                
                 // Remap all contained states to the new row group.
                 StateType nextRowGroup = explorationInformation.getNextRowGroup();
                 for (auto const& stateAndChoices : mec) {
@@ -530,26 +554,13 @@ namespace storm {
                     bounds.initializeBoundsForNextAction(actionBounds);
                     stateBounds = combineBounds(explorationInformation.optimizationDirection, stateBounds, actionBounds);
                 }
+                bounds.setBoundsForRowGroup(nextRowGroup, stateBounds);
                 
                 // Terminate the row group of the newly introduced state.
                 explorationInformation.rowGroupIndices.push_back(explorationInformation.matrix.size());
             }
         }
         
-        template<typename ValueType>
-        void SparseMdpLearningModelChecker<ValueType>::analyzeMecForMinimalProbabilities(storm::storage::MaximalEndComponent const& mec, std::vector<StateType> const& relevantStates, storm::storage::SparseMatrix<ValueType> const& relevantStatesMatrix, ExplorationInformation& explorationInformation, BoundValues& bounds) const {
-            // For minimal probabilities, all found MECs are guaranteed to not contain a target state. Hence, in all
-            // associated states, the probability is 0 and we can set the upper bounds of the states to 0).
-            
-            for (auto const& stateAndChoices : mec) {
-                // Compute the state of the original model that corresponds to the current state.
-                StateType originalState = relevantStates[stateAndChoices.first];
-                
-                bounds.setUpperBoundForState(originalState, explorationInformation, storm::utility::zero<ValueType>());
-                explorationInformation.addTerminalState(originalState);
-            }
-        }
-        
         template<typename ValueType>
         ValueType SparseMdpLearningModelChecker<ValueType>::computeLowerBoundOfAction(ActionType const& action, ExplorationInformation const& explorationInformation, BoundValues const& bounds) const {
             ValueType result = storm::utility::zero<ValueType>();

src/modelchecker/reachability/SparseMdpLearningModelChecker.h

@@ -51,11 +51,12 @@ namespace storm {
         private:
             // A struct that keeps track of certain statistics during the computation.
             struct Statistics {
-                Statistics() : iterations(0), maxPathLength(0), numberOfTargetStates(0), numberOfExploredStates(0), ecDetections(0), failedEcDetections(0), totalNumberOfEcDetected(0) {
+                Statistics() : pathsSampled(0), explorationSteps(0), maxPathLength(0), numberOfTargetStates(0), numberOfExploredStates(0), ecDetections(0), failedEcDetections(0), totalNumberOfEcDetected(0) {
                     // Intentionally left empty.
                 }
                 
-                std::size_t iterations;
+                std::size_t pathsSampled;
+                std::size_t explorationSteps;
                 std::size_t maxPathLength;
                 std::size_t numberOfTargetStates;
                 std::size_t numberOfExploredStates;
@@ -89,7 +90,7 @@ namespace storm {
             
             // A structure containing the data assembled during exploration.
             struct ExplorationInformation {
-                ExplorationInformation(uint_fast64_t bitsPerBucket, bool localECDetection, ActionType const& unexploredMarker = std::numeric_limits<ActionType>::max()) : stateStorage(bitsPerBucket), unexploredMarker(unexploredMarker), localECDetection(localECDetection), pathLengthUntilEndComponentDetection(10000) {
+                ExplorationInformation(uint_fast64_t bitsPerBucket, bool localPrecomputation, uint_fast64_t numberOfExplorationStepsUntilPrecomputation, ActionType const& unexploredMarker = std::numeric_limits<ActionType>::max()) : stateStorage(bitsPerBucket), unexploredMarker(unexploredMarker), localPrecomputation(localPrecomputation), numberOfExplorationStepsUntilPrecomputation(numberOfExplorationStepsUntilPrecomputation) {
                     // Intentionally left empty.
                 }
                 
@@ -105,8 +106,8 @@ namespace storm {
                 storm::OptimizationDirection optimizationDirection;
                 StateSet terminalStates;
                 
-                bool localECDetection;
-                uint_fast64_t pathLengthUntilEndComponentDetection;
+                bool localPrecomputation;
+                uint_fast64_t numberOfExplorationStepsUntilPrecomputation;
                 
                 void setInitialStates(std::vector<StateType> const& initialStates) {
                     stateStorage.initialStateIndices = initialStates;
@@ -207,20 +208,21 @@ namespace storm {
                     return !maximize();
                 }
                 
-                uint_fast64_t getPathLengthUntilEndComponentDetection() const {
-                    return pathLengthUntilEndComponentDetection;
-                }
-                
-                void increasePathLengthUntilEndComponentDetection() {
-                    pathLengthUntilEndComponentDetection += 100;
+                bool performPrecomputation(std::size_t& performedExplorationSteps) const {
+                    bool result = performedExplorationSteps > numberOfExplorationStepsUntilPrecomputation;
+                    if (result) {
+                        std::cout << "triggering precomp" << std::endl;
+                        performedExplorationSteps = 0;
+                    }
+                    return result;
                 }
                 
-                bool useLocalECDetection() const {
-                    return localECDetection;
+                bool useLocalPrecomputation() const {
+                    return localPrecomputation;
                 }
 
-                bool useGlobalECDetection() const {
-                    return !useLocalECDetection();
+                bool useGlobalPrecomputation() const {
+                    return !useLocalPrecomputation();
                 }
             };
             
@@ -286,7 +288,7 @@ namespace storm {
                     }
                 }
                 
-                ValueType getDifferenceOfStateBounds(StateType const& state, ExplorationInformation const& explorationInformation) {
+                ValueType getDifferenceOfStateBounds(StateType const& state, ExplorationInformation const& explorationInformation) const {
                     std::pair<ValueType, ValueType> bounds = getBoundsForState(state, explorationInformation);
                     return bounds.second - bounds.first;
                 }
@@ -324,6 +326,10 @@ namespace storm {
 
                 void setBoundsForState(StateType const& state, ExplorationInformation const& explorationInformation, std::pair<ValueType, ValueType> const& values) {
                     StateType const& rowGroup = explorationInformation.getRowGroup(state);
+                    setBoundsForRowGroup(rowGroup, values);
+                }
+                
+                void setBoundsForRowGroup(StateType const& rowGroup, std::pair<ValueType, ValueType> const& values) {
                     lowerBoundsPerState[rowGroup] = values.first;
                     upperBoundsPerState[rowGroup] = values.second;
                 }
@@ -359,13 +365,11 @@ namespace storm {
             
             ActionType sampleActionOfState(StateType const& currentStateId, ExplorationInformation const& explorationInformation, BoundValues& bounds) const;
 
-            StateType sampleSuccessorFromAction(ActionType const& chosenAction, ExplorationInformation const& explorationInformation) const;
+            StateType sampleSuccessorFromAction(ActionType const& chosenAction, ExplorationInformation const& explorationInformation, BoundValues const& bounds) const;
             
-            bool detectEndComponents(StateActionStack const& stack, ExplorationInformation& explorationInformation, BoundValues& bounds, Statistics& stats) const;
+            bool performPrecomputation(StateActionStack const& stack, ExplorationInformation& explorationInformation, BoundValues& bounds, Statistics& stats) const;
             
-            void analyzeMecForMaximalProbabilities(storm::storage::MaximalEndComponent const& mec, std::vector<StateType> const& relevantStates, storm::storage::SparseMatrix<ValueType> const& relevantStatesMatrix, ExplorationInformation& explorationInformation, BoundValues& bounds) const;
-
-            void analyzeMecForMinimalProbabilities(storm::storage::MaximalEndComponent const& mec, std::vector<StateType> const& relevantStates, storm::storage::SparseMatrix<ValueType> const& relevantStatesMatrix, ExplorationInformation& explorationInformation, BoundValues& bounds) const;
+            void collapseMec(storm::storage::MaximalEndComponent const& mec, std::vector<StateType> const& relevantStates, storm::storage::SparseMatrix<ValueType> const& relevantStatesMatrix, ExplorationInformation& explorationInformation, BoundValues& bounds) const;
             
             void updateProbabilityBoundsAlongSampledPath(StateActionStack& stack, ExplorationInformation const& explorationInformation, BoundValues& bounds) const;
 

src/settings/modules/LearningSettings.cpp

@@ -11,40 +11,46 @@ namespace storm {
         namespace modules {
             
             const std::string LearningSettings::moduleName = "learning";
-            const std::string LearningSettings::ecDetectionTypeOptionName = "ecdetection";
+            const std::string LearningSettings::precomputationTypeOptionName = "precomp";
+            const std::string LearningSettings::numberOfExplorationStepsUntilPrecomputationOptionName = "stepsprecomp";
             
             LearningSettings::LearningSettings(storm::settings::SettingsManager& settingsManager) : ModuleSettings(settingsManager, moduleName) {
                 std::vector<std::string> types = { "local", "global" };
-                this->addOption(storm::settings::OptionBuilder(moduleName, ecDetectionTypeOptionName, true, "Sets the kind of EC-detection 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("local").build()).build());
+                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("local").build()).build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, numberOfExplorationStepsUntilPrecomputationOptionName, false, "Sets the number of exploration steps until a precomputation is triggered.").addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("count", "The number of exploration steps to perform.").setDefaultValueUnsignedInteger(100000).build()).build());
             }
             
-            bool LearningSettings::isLocalECDetectionSet() const {
-                if (this->getOption(ecDetectionTypeOptionName).getArgumentByName("name").getValueAsString() == "local") {
+            bool LearningSettings::isLocalPrecomputationSet() const {
+                if (this->getOption(precomputationTypeOptionName).getArgumentByName("name").getValueAsString() == "local") {
                     return true;
                 }
                 return false;
             }
             
-            bool LearningSettings::isGlobalECDetectionSet() const {
-                if (this->getOption(ecDetectionTypeOptionName).getArgumentByName("name").getValueAsString() == "global") {
+            bool LearningSettings::isGlobalPrecomputationSet() const {
+                if (this->getOption(precomputationTypeOptionName).getArgumentByName("name").getValueAsString() == "global") {
                     return true;
                 }
                 return false;
             }
             
-            LearningSettings::ECDetectionType LearningSettings::getECDetectionType() const {
-                std::string typeAsString = this->getOption(ecDetectionTypeOptionName).getArgumentByName("name").getValueAsString();
+            LearningSettings::PrecomputationType LearningSettings::getPrecomputationType() const {
+                std::string typeAsString = this->getOption(precomputationTypeOptionName).getArgumentByName("name").getValueAsString();
                 if (typeAsString == "local") {
-                    return LearningSettings::ECDetectionType::Local;
+                    return LearningSettings::PrecomputationType::Local;
                 } else if (typeAsString == "global") {
-                    return LearningSettings::ECDetectionType::Global;
+                    return LearningSettings::PrecomputationType::Global;
                 }
                 STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown EC-detection type '" << typeAsString << "'.");
             }
             
+            uint_fast64_t LearningSettings::getNumberOfExplorationStepsUntilPrecomputation() const {
+                return this->getOption(numberOfExplorationStepsUntilPrecomputationOptionName).getArgumentByName("count").getValueAsUnsignedInteger();
+            }
+            
             bool LearningSettings::check() const {
-                bool optionsSet = this->getOption(ecDetectionTypeOptionName).getHasOptionBeenSet();
-                STORM_LOG_WARN_COND(storm::settings::generalSettings().getEngine() == storm::settings::modules::GeneralSettings::Engine::Learning || !optionsSet, "Bisimulation minimization is not selected, so setting options for bisimulation has no effect.");
+                bool optionsSet = this->getOption(precomputationTypeOptionName).getHasOptionBeenSet() || this->getOption(numberOfExplorationStepsUntilPrecomputationOptionName).getHasOptionBeenSet();
+                STORM_LOG_WARN_COND(storm::settings::generalSettings().getEngine() == storm::settings::modules::GeneralSettings::Engine::Learning || !optionsSet, "Learning engine is not selected, so setting options for it has no effect.");
                 return true;
             }
         } // namespace modules

src/settings/modules/LearningSettings.h

@@ -12,8 +12,8 @@ namespace storm {
              */
             class LearningSettings : public ModuleSettings {
             public:
-                // An enumeration of all available EC-detection types.
-                enum class ECDetectionType { Local, Global };
+                // An enumeration of all available precomputation types.
+                enum class PrecomputationType { Local, Global };
                 
                 /*!
                  * Creates a new set of learning settings that is managed by the given manager.
@@ -23,25 +23,32 @@ namespace storm {
                 LearningSettings(storm::settings::SettingsManager& settingsManager);
                 
                 /*!
-                 * Retrieves whether local EC-detection is to be used.
+                 * Retrieves whether local precomputation is to be used.
                  *
-                 * @return True iff local EC-detection is to be used.
+                 * @return True iff local precomputation is to be used.
                  */
-                bool isLocalECDetectionSet() const;
+                bool isLocalPrecomputationSet() const;
                 
                 /*!
-                 * Retrieves whether global EC-detection is to be used.
+                 * Retrieves whether global precomputation is to be used.
                  *
-                 * @return True iff global EC-detection is to be used.
+                 * @return True iff global precomputation is to be used.
                  */
-                bool isGlobalECDetectionSet() const;
+                bool isGlobalPrecomputationSet() const;
                 
                 /*!
-                 * Retrieves the selected EC-detection type.
+                 * Retrieves the selected precomputation type.
                  *
-                 * @return The selected EC-detection type.
+                 * @return The selected precomputation type.
                  */
-                ECDetectionType getECDetectionType() const;
+                PrecomputationType getPrecomputationType() const;
+                
+                /*!
+                 * Retrieves the number of exploration steps to perform until a precomputation is triggered.
+                 *
+                 * @return The number of exploration steps to perform until a precomputation is triggered.
+                 */
+                uint_fast64_t getNumberOfExplorationStepsUntilPrecomputation() const;
                 
                 virtual bool check() const override;
                 
@@ -50,7 +57,8 @@ namespace storm {
                 
             private:
                 // Define the string names of the options as constants.
-                static const std::string ecDetectionTypeOptionName;
+                static const std::string precomputationTypeOptionName;
+                static const std::string numberOfExplorationStepsUntilPrecomputationOptionName;
             };
         } // namespace modules
     } // namespace settings