diff --git a/src/modelchecker/exploration/Bounds.cpp b/src/modelchecker/exploration/Bounds.cpp index 9892c33f0..db36d0f16 100644 --- a/src/modelchecker/exploration/Bounds.cpp +++ b/src/modelchecker/exploration/Bounds.cpp @@ -10,10 +10,8 @@ namespace storm { std::pair Bounds::getBoundsForState(StateType const& state, ExplorationInformation 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(), storm::utility::one()); } else { - std::cout << "accessing at index " << index << " out of " << boundsPerState.size() << std::endl; return boundsPerState[index]; } } @@ -116,7 +114,6 @@ namespace storm { template void Bounds::setBoundsForState(StateType const& state, ExplorationInformation const& explorationInformation, std::pair const& values) { StateType const& rowGroup = explorationInformation.getRowGroup(state); - std::cout << "setting " << values.first << ", " << values.second << " for state " << state << std::endl; setBoundsForRowGroup(rowGroup, values); } diff --git a/src/modelchecker/exploration/ExplorationInformation.cpp b/src/modelchecker/exploration/ExplorationInformation.cpp index 7f45eb6c6..756fd57d9 100644 --- a/src/modelchecker/exploration/ExplorationInformation.cpp +++ b/src/modelchecker/exploration/ExplorationInformation.cpp @@ -10,7 +10,7 @@ namespace storm { namespace exploration_detail { template - ExplorationInformation::ExplorationInformation(storm::OptimizationDirection const& direction, ActionType const& unexploredMarker) : unexploredMarker(unexploredMarker), optimizationDirection(direction), localPrecomputation(false), numberOfExplorationStepsUntilPrecomputation(100000), numberOfSampledPathsUntilPrecomputation(), nextStateHeuristic(storm::settings::modules::ExplorationSettings::NextStateHeuristic::DifferenceWeightedProbability) { + ExplorationInformation::ExplorationInformation(storm::OptimizationDirection const& direction, ActionType const& unexploredMarker) : unexploredMarker(unexploredMarker), optimizationDirection(direction), localPrecomputation(false), numberOfExplorationStepsUntilPrecomputation(100000), numberOfSampledPathsUntilPrecomputation(), nextStateHeuristic(storm::settings::modules::ExplorationSettings::NextStateHeuristic::DifferenceProbabilitySum) { storm::settings::modules::ExplorationSettings const& settings = storm::settings::explorationSettings(); localPrecomputation = settings.isLocalPrecomputationSet(); @@ -20,7 +20,6 @@ namespace storm { } nextStateHeuristic = settings.getNextStateHeuristic(); - STORM_LOG_ASSERT(useDifferenceWeightedProbabilityHeuristic() || useProbabilityHeuristic(), "Illegal next-state heuristic."); } template @@ -198,14 +197,19 @@ namespace storm { } template - bool ExplorationInformation::useDifferenceWeightedProbabilityHeuristic() const { - return nextStateHeuristic == storm::settings::modules::ExplorationSettings::NextStateHeuristic::DifferenceWeightedProbability; + bool ExplorationInformation::useDifferenceProbabilitySumHeuristic() const { + return nextStateHeuristic == storm::settings::modules::ExplorationSettings::NextStateHeuristic::DifferenceProbabilitySum; } template bool ExplorationInformation::useProbabilityHeuristic() const { return nextStateHeuristic == storm::settings::modules::ExplorationSettings::NextStateHeuristic::Probability; } + + template + bool ExplorationInformation::useUniformHeuristic() const { + return nextStateHeuristic == storm::settings::modules::ExplorationSettings::NextStateHeuristic::Uniform; + } template storm::OptimizationDirection const& ExplorationInformation::getOptimizationDirection() const { diff --git a/src/modelchecker/exploration/ExplorationInformation.h b/src/modelchecker/exploration/ExplorationInformation.h index 550b3d32c..4716bfc96 100644 --- a/src/modelchecker/exploration/ExplorationInformation.h +++ b/src/modelchecker/exploration/ExplorationInformation.h @@ -94,10 +94,12 @@ namespace storm { storm::settings::modules::ExplorationSettings::NextStateHeuristic const& getNextStateHeuristic() const; - bool useDifferenceWeightedProbabilityHeuristic() const; + bool useDifferenceProbabilitySumHeuristic() const; bool useProbabilityHeuristic() const; + bool useUniformHeuristic() const; + storm::OptimizationDirection const& getOptimizationDirection() const; void setOptimizationDirection(storm::OptimizationDirection const& direction); diff --git a/src/modelchecker/exploration/SparseMdpExplorationModelChecker.cpp b/src/modelchecker/exploration/SparseMdpExplorationModelChecker.cpp index 9fd4c85f8..542273713 100644 --- a/src/modelchecker/exploration/SparseMdpExplorationModelChecker.cpp +++ b/src/modelchecker/exploration/SparseMdpExplorationModelChecker.cpp @@ -53,7 +53,7 @@ namespace storm { STORM_LOG_THROW(program.isDeterministicModel() || checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException, "For nondeterministic systems, an optimization direction (min/max) must be given in the property."); ExplorationInformation explorationInformation(checkTask.isOptimizationDirectionSet() ? checkTask.getOptimizationDirection() : storm::OptimizationDirection::Maximize); - + // The first row group starts at action 0. explorationInformation.newRowGroup(0); @@ -65,7 +65,7 @@ namespace storm { std::tuple boundsForInitialState = performExploration(stateGeneration, explorationInformation); return std::make_unique>(std::get<0>(boundsForInitialState), std::get<1>(boundsForInitialState)); } - + template std::tuple::StateType, ValueType, ValueType> SparseMdpExplorationModelChecker::performExploration(StateGeneration& stateGeneration, ExplorationInformation& explorationInformation) const { // Generate the initial state so we know where to start the simulation. @@ -75,7 +75,7 @@ namespace storm { // Create a structure that holds the bounds for the states and actions. Bounds bounds; - + // Create a stack that is used to track the path we sampled. StateActionStack stack; @@ -237,13 +237,13 @@ namespace storm { for (auto const& choice : behavior) { for (auto const& entry : choice) { explorationInformation.getRowOfMatrix(startAction + localAction).emplace_back(entry.first, entry.second); - std::cout << "adding " << (startAction + localAction) << "x" << entry.first << " -> " << entry.second << std::endl; + STORM_LOG_TRACE("Found transition " << currentStateId << "-[" << (startAction + localAction) << ", " << entry.second << "]-> " << entry.first << "."); } std::pair actionBounds = computeBoundsOfAction(startAction + localAction, explorationInformation, bounds); bounds.initializeBoundsForNextAction(actionBounds); stateBounds = combineBounds(explorationInformation.getOptimizationDirection(), stateBounds, actionBounds); - + STORM_LOG_TRACE("Initializing bounds of action " << (startAction + localAction) << " to " << bounds.getLowerBoundForAction(startAction + localAction) << " and " << bounds.getUpperBoundForAction(startAction + localAction) << "."); ++localAction; @@ -260,7 +260,7 @@ namespace storm { // terminal state. isTerminalState = true; } - + if (isTerminalState) { STORM_LOG_TRACE("State does not need to be explored, because it is " << (isTargetState ? "a target state" : "a rejecting terminal state") << "."); explorationInformation.addTerminalState(currentStateId); @@ -328,26 +328,29 @@ namespace storm { return row.front().getColumn(); } - std::vector probabilities(row.size()); // Depending on the selected next-state heuristic, we give the states other likelihoods of getting chosen. - if (explorationInformation.useDifferenceWeightedProbabilityHeuristic()) { + if (explorationInformation.useDifferenceProbabilitySumHeuristic() || explorationInformation.useProbabilityHeuristic()) { + std::vector probabilities(row.size()); + if (explorationInformation.useDifferenceProbabilitySumHeuristic()) { std::transform(row.begin(), row.end(), probabilities.begin(), [&bounds, &explorationInformation] (storm::storage::MatrixEntry 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()) { - std::transform(row.begin(), row.end(), probabilities.begin(), - [&bounds, &explorationInformation] (storm::storage::MatrixEntry const& entry) { - return entry.getValue(); + return entry.getValue() + bounds.getDifferenceOfStateBounds(entry.getColumn(), explorationInformation); }); + } else if (explorationInformation.useProbabilityHeuristic()) { + std::transform(row.begin(), row.end(), probabilities.begin(), + [&bounds, &explorationInformation] (storm::storage::MatrixEntry const& entry) { + return entry.getValue(); + }); + } + + // Now sample according to the probabilities. + std::discrete_distribution distribution(probabilities.begin(), probabilities.end()); + return row[distribution(randomGenerator)].getColumn(); + } else if (explorationInformation.useUniformHeuristic()) { + std::uniform_int_distribution distribution(0, row.size() - 1); + return row[distribution(randomGenerator)].getColumn(); } - - // Now sample according to the probabilities. - std::discrete_distribution distribution(probabilities.begin(), probabilities.end()); - StateType offset = distribution(randomGenerator); - return row[offset].getColumn(); } template @@ -359,7 +362,7 @@ namespace storm { // 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."); - + // 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); @@ -390,10 +393,8 @@ 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; } } @@ -409,11 +410,9 @@ 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()) { @@ -441,11 +440,11 @@ namespace storm { 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; @@ -473,13 +472,9 @@ 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()); explorationInformation.addTerminalState(originalState); } @@ -588,7 +583,7 @@ namespace storm { } return result; } - + template std::pair SparseMdpExplorationModelChecker::computeBoundsOfState(StateType const& currentStateId, ExplorationInformation const& explorationInformation, Bounds const& bounds) const { StateType group = explorationInformation.getRowGroup(currentStateId); @@ -620,7 +615,7 @@ namespace storm { // Check if we need to update the values for the states. if (explorationInformation.maximize()) { bounds.setLowerBoundOfStateIfGreaterThanOld(state, explorationInformation, newBoundsForAction.first); - + StateType rowGroup = explorationInformation.getRowGroup(state); if (newBoundsForAction.second < bounds.getUpperBoundForRowGroup(rowGroup)) { if (explorationInformation.getRowGroupSize(rowGroup) > 1) { @@ -631,7 +626,7 @@ namespace storm { } } else { bounds.setUpperBoundOfStateIfLessThanOld(state, explorationInformation, newBoundsForAction.second); - + StateType rowGroup = explorationInformation.getRowGroup(state); if (bounds.getLowerBoundForRowGroup(rowGroup) < newBoundsForAction.first) { if (explorationInformation.getRowGroupSize(rowGroup) > 1) { diff --git a/src/settings/modules/ExplorationSettings.cpp b/src/settings/modules/ExplorationSettings.cpp index 4a3a2796d..306d63aa8 100644 --- a/src/settings/modules/ExplorationSettings.cpp +++ b/src/settings/modules/ExplorationSettings.cpp @@ -22,8 +22,8 @@ namespace storm { 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 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()); + std::vector nextStateHeuristics = { "probdiffs", "prob", "unif" }; + this->addOption(storm::settings::OptionBuilder(moduleName, nextStateHeuristicOptionName, true, "Sets the next-state heuristic to use. Available are: { probdiffs, prob, unif } where 'prob' samples according to the probabilities in the system, 'probdiffs' takes into account probabilities and the differences between the current bounds and 'unif' samples uniformly.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the heuristic to use.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(nextStateHeuristics)).setDefaultValueString("probdiffs").build()).build()); } bool ExplorationSettings::isLocalPrecomputationSet() const { @@ -64,10 +64,12 @@ namespace storm { ExplorationSettings::NextStateHeuristic ExplorationSettings::getNextStateHeuristic() const { std::string nextStateHeuristicAsString = this->getOption(nextStateHeuristicOptionName).getArgumentByName("name").getValueAsString(); - if (nextStateHeuristicAsString == "probdiff") { - return ExplorationSettings::NextStateHeuristic::DifferenceWeightedProbability; + if (nextStateHeuristicAsString == "probdiffs") { + return ExplorationSettings::NextStateHeuristic::DifferenceProbabilitySum; } else if (nextStateHeuristicAsString == "prob") { return ExplorationSettings::NextStateHeuristic::Probability; + } else if (nextStateHeuristicAsString == "unif") { + return ExplorationSettings::NextStateHeuristic::Uniform; } STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown next-state heuristic '" << nextStateHeuristicAsString << "'."); } diff --git a/src/settings/modules/ExplorationSettings.h b/src/settings/modules/ExplorationSettings.h index 10dcaf080..18126acfe 100644 --- a/src/settings/modules/ExplorationSettings.h +++ b/src/settings/modules/ExplorationSettings.h @@ -16,7 +16,7 @@ namespace storm { enum class PrecomputationType { Local, Global }; // The available heuristics to choose the next state. - enum class NextStateHeuristic { DifferenceWeightedProbability, Probability }; + enum class NextStateHeuristic { DifferenceProbabilitySum, Probability, Uniform }; /*! * Creates a new set of exploration settings that is managed by the given manager.