diff --git a/src/builder/ExplicitPrismModelBuilder.cpp b/src/builder/ExplicitPrismModelBuilder.cpp index 4820e1652..ed65da9da 100644 --- a/src/builder/ExplicitPrismModelBuilder.cpp +++ b/src/builder/ExplicitPrismModelBuilder.cpp @@ -227,18 +227,6 @@ namespace storm { return result; } - template - storm::expressions::SimpleValuation ExplicitPrismModelBuilder::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 StateType ExplicitPrismModelBuilder::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()); } } diff --git a/src/builder/ExplicitPrismModelBuilder.h b/src/builder/ExplicitPrismModelBuilder.h index 8cc724de2..d790f0bb1 100644 --- a/src/builder/ExplicitPrismModelBuilder.h +++ b/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 diff --git a/src/generator/CompressedState.cpp b/src/generator/CompressedState.cpp index c63504ebb..03ba3d4c7 100644 --- a/src/generator/CompressedState.cpp +++ b/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(CompressedState const& state, VariableInformation const& variableInformation, storm::expressions::ExpressionEvaluator& evaluator); template void unpackStateIntoEvaluator(CompressedState const& state, VariableInformation const& variableInformation, storm::expressions::ExpressionEvaluator& evaluator); + storm::expressions::SimpleValuation unpackStateIntoValuation(CompressedState const& state, VariableInformation const& variableInformation, storm::expressions::ExpressionManager const& manager); } } \ No newline at end of file diff --git a/src/generator/CompressedState.h b/src/generator/CompressedState.h index 52f0b4a62..a1b6212bb 100644 --- a/src/generator/CompressedState.h +++ b/src/generator/CompressedState.h @@ -6,6 +6,9 @@ namespace storm { namespace expressions { template 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 void unpackStateIntoEvaluator(CompressedState const& state, VariableInformation const& variableInformation, storm::expressions::ExpressionEvaluator& 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); } } diff --git a/src/modelchecker/reachability/SparseMdpLearningModelChecker.cpp b/src/modelchecker/reachability/SparseMdpLearningModelChecker.cpp index 60196c639..2e3b6c601 100644 --- a/src/modelchecker/reachability/SparseMdpLearningModelChecker.cpp +++ b/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 std::function::StateType (storm::generator::CompressedState const&)> SparseMdpLearningModelChecker::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 SparseMdpLearningModelChecker::StateType SparseMdpLearningModelChecker::sampleSuccessorFromAction(ActionType const& chosenAction, ExplorationInformation const& explorationInformation) const { + typename SparseMdpLearningModelChecker::StateType SparseMdpLearningModelChecker::sampleSuccessorFromAction(ActionType const& chosenAction, ExplorationInformation const& explorationInformation, BoundValues const& bounds) const { // TODO: precompute this? std::vector probabilities(explorationInformation.getRowOfMatrix(chosenAction).size()); - std::transform(explorationInformation.getRowOfMatrix(chosenAction).begin(), explorationInformation.getRowOfMatrix(chosenAction).end(), probabilities.begin(), [] (storm::storage::MatrixEntry const& entry) { return entry.getValue(); } ); + std::transform(explorationInformation.getRowOfMatrix(chosenAction).begin(), explorationInformation.getRowOfMatrix(chosenAction).end(), probabilities.begin(), [&bounds, &explorationInformation] (storm::storage::MatrixEntry const& entry) { return entry.getValue() * bounds.getDifferenceOfStateBounds(entry.getColumn(), explorationInformation) ; } ); // Now sample according to the probabilities. std::discrete_distribution distribution(probabilities.begin(), probabilities.end()); @@ -345,21 +349,27 @@ namespace storm { } template - bool SparseMdpLearningModelChecker::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::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 builder(0, 0, 0, false, true, 0); // Determine the set of states that was expanded. std::vector 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 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()); - STORM_LOG_TRACE("Successfully built matrix for MEC decomposition."); - - // Go on to step 2. storm::storage::SparseMatrix relevantStatesMatrix = builder.build(); - storm::storage::MaximalEndComponentDecomposition 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 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 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()); + explorationInformation.addTerminalState(originalState); + } + for (auto state : statesWithProbability1) { + StateType originalState = relevantStates[state]; + bounds.setLowerBoundForState(originalState, explorationInformation, storm::utility::one()); + explorationInformation.addTerminalState(originalState); } return true; } template - void SparseMdpLearningModelChecker::analyzeMecForMaximalProbabilities(storm::storage::MaximalEndComponent const& mec, std::vector const& relevantStates, storm::storage::SparseMatrix 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::collapseMec(storm::storage::MaximalEndComponent const& mec, std::vector const& relevantStates, storm::storage::SparseMatrix 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 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()); - 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()); - 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 - void SparseMdpLearningModelChecker::analyzeMecForMinimalProbabilities(storm::storage::MaximalEndComponent const& mec, std::vector const& relevantStates, storm::storage::SparseMatrix 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()); - explorationInformation.addTerminalState(originalState); - } - } - template ValueType SparseMdpLearningModelChecker::computeLowerBoundOfAction(ActionType const& action, ExplorationInformation const& explorationInformation, BoundValues const& bounds) const { ValueType result = storm::utility::zero(); diff --git a/src/modelchecker/reachability/SparseMdpLearningModelChecker.h b/src/modelchecker/reachability/SparseMdpLearningModelChecker.h index 9dba78bba..d9a4baf7f 100644 --- a/src/modelchecker/reachability/SparseMdpLearningModelChecker.h +++ b/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::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::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 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 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 const& values) { StateType const& rowGroup = explorationInformation.getRowGroup(state); + setBoundsForRowGroup(rowGroup, values); + } + + void setBoundsForRowGroup(StateType const& rowGroup, std::pair 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 const& relevantStates, storm::storage::SparseMatrix const& relevantStatesMatrix, ExplorationInformation& explorationInformation, BoundValues& bounds) const; - - void analyzeMecForMinimalProbabilities(storm::storage::MaximalEndComponent const& mec, std::vector const& relevantStates, storm::storage::SparseMatrix const& relevantStatesMatrix, ExplorationInformation& explorationInformation, BoundValues& bounds) const; + void collapseMec(storm::storage::MaximalEndComponent const& mec, std::vector const& relevantStates, storm::storage::SparseMatrix const& relevantStatesMatrix, ExplorationInformation& explorationInformation, BoundValues& bounds) const; void updateProbabilityBoundsAlongSampledPath(StateActionStack& stack, ExplorationInformation const& explorationInformation, BoundValues& bounds) const; diff --git a/src/settings/modules/LearningSettings.cpp b/src/settings/modules/LearningSettings.cpp index f393751f0..fdddd1672 100644 --- a/src/settings/modules/LearningSettings.cpp +++ b/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 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 diff --git a/src/settings/modules/LearningSettings.h b/src/settings/modules/LearningSettings.h index d95b9fe98..8db1fe44a 100644 --- a/src/settings/modules/LearningSettings.h +++ b/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