diff --git a/src/modelchecker/exploration/BoundValues.cpp b/src/modelchecker/exploration/BoundValues.cpp deleted file mode 100644 index e69de29bb..000000000 diff --git a/src/modelchecker/exploration/BoundValues.h b/src/modelchecker/exploration/BoundValues.h deleted file mode 100644 index 3640fa9c6..000000000 --- a/src/modelchecker/exploration/BoundValues.h +++ /dev/null @@ -1,137 +0,0 @@ -#ifndef STORM_MODELCHECKER_EXPLORATION_SPARSEMDPEXPLORATIONMODELCHECKER_H_ -#define STORM_MODELCHECKER_REACHABILITY_SPARSEMDPEXPLORATIONMODELCHECKER_H_ - -namespace storm { - namespace modelchecker { - namespace exploration_detail { - - // A struct containg the lower and upper bounds per state and action. - struct BoundValues { - std::vector lowerBoundsPerState; - std::vector upperBoundsPerState; - std::vector lowerBoundsPerAction; - std::vector upperBoundsPerAction; - - std::pair getBoundsForState(StateType const& state, ExplorationInformation const& explorationInformation) const { - ActionType index = explorationInformation.getRowGroup(state); - if (index == explorationInformation.getUnexploredMarker()) { - return std::make_pair(storm::utility::zero(), storm::utility::one()); - } else { - return std::make_pair(lowerBoundsPerState[index], upperBoundsPerState[index]); - } - } - - ValueType getLowerBoundForState(StateType const& state, ExplorationInformation const& explorationInformation) const { - ActionType index = explorationInformation.getRowGroup(state); - if (index == explorationInformation.getUnexploredMarker()) { - return storm::utility::zero(); - } else { - return getLowerBoundForRowGroup(index); - } - } - - ValueType const& getLowerBoundForRowGroup(StateType const& rowGroup) const { - return lowerBoundsPerState[rowGroup]; - } - - ValueType getUpperBoundForState(StateType const& state, ExplorationInformation const& explorationInformation) const { - ActionType index = explorationInformation.getRowGroup(state); - if (index == explorationInformation.getUnexploredMarker()) { - return storm::utility::one(); - } else { - return getUpperBoundForRowGroup(index); - } - } - - ValueType const& getUpperBoundForRowGroup(StateType const& rowGroup) const { - return upperBoundsPerState[rowGroup]; - } - - std::pair getBoundsForAction(ActionType const& action) const { - return std::make_pair(lowerBoundsPerAction[action], upperBoundsPerAction[action]); - } - - ValueType const& getLowerBoundForAction(ActionType const& action) const { - return lowerBoundsPerAction[action]; - } - - ValueType const& getUpperBoundForAction(ActionType const& action) const { - return upperBoundsPerAction[action]; - } - - ValueType const& getBoundForAction(storm::OptimizationDirection const& direction, ActionType const& action) const { - if (direction == storm::OptimizationDirection::Maximize) { - return getUpperBoundForAction(action); - } else { - return getLowerBoundForAction(action); - } - } - - ValueType getDifferenceOfStateBounds(StateType const& state, ExplorationInformation const& explorationInformation) const { - std::pair bounds = getBoundsForState(state, explorationInformation); - return bounds.second - bounds.first; - } - - void initializeBoundsForNextState(std::pair const& vals = std::pair(storm::utility::zero(), storm::utility::one())) { - lowerBoundsPerState.push_back(vals.first); - upperBoundsPerState.push_back(vals.second); - } - - void initializeBoundsForNextAction(std::pair const& vals = std::pair(storm::utility::zero(), storm::utility::one())) { - lowerBoundsPerAction.push_back(vals.first); - upperBoundsPerAction.push_back(vals.second); - } - - void setLowerBoundForState(StateType const& state, ExplorationInformation const& explorationInformation, ValueType const& value) { - setLowerBoundForRowGroup(explorationInformation.getRowGroup(state), value); - } - - void setLowerBoundForRowGroup(StateType const& group, ValueType const& value) { - lowerBoundsPerState[group] = value; - } - - void setUpperBoundForState(StateType const& state, ExplorationInformation const& explorationInformation, ValueType const& value) { - setUpperBoundForRowGroup(explorationInformation.getRowGroup(state), value); - } - - void setUpperBoundForRowGroup(StateType const& group, ValueType const& value) { - upperBoundsPerState[group] = value; - } - - void setBoundsForAction(ActionType const& action, std::pair const& values) { - lowerBoundsPerAction[action] = values.first; - upperBoundsPerAction[action] = values.second; - } - - 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; - } - - bool setLowerBoundOfStateIfGreaterThanOld(StateType const& state, ExplorationInformation const& explorationInformation, ValueType const& newLowerValue) { - StateType const& rowGroup = explorationInformation.getRowGroup(state); - if (lowerBoundsPerState[rowGroup] < newLowerValue) { - lowerBoundsPerState[rowGroup] = newLowerValue; - return true; - } - return false; - } - - bool setUpperBoundOfStateIfLessThanOld(StateType const& state, ExplorationInformation const& explorationInformation, ValueType const& newUpperValue) { - StateType const& rowGroup = explorationInformation.getRowGroup(state); - if (newUpperValue < upperBoundsPerState[rowGroup]) { - upperBoundsPerState[rowGroup] = newUpperValue; - return true; - } - return false; - } - }; - - } - } -} \ No newline at end of file diff --git a/src/modelchecker/exploration/Bounds.cpp b/src/modelchecker/exploration/Bounds.cpp new file mode 100644 index 000000000..32ad0cb92 --- /dev/null +++ b/src/modelchecker/exploration/Bounds.cpp @@ -0,0 +1,155 @@ +#include "src/modelchecker/exploration/Bounds.h" + +#include "src/modelchecker/exploration/ExplorationInformation.h" + +namespace storm { + namespace modelchecker { + namespace exploration_detail { + + template + std::pair Bounds::getBoundsForState(StateType const& state, ExplorationInformation const& explorationInformation) const { + ActionType index = explorationInformation.getRowGroup(state); + if (index == explorationInformation.getUnexploredMarker()) { + return std::make_pair(storm::utility::zero(), storm::utility::one()); + } else { + return boundsPerState[index]; + } + } + + template + std::pair const& Bounds::getBoundsForExploredState(StateType const& state, ExplorationInformation const& explorationInformation) const { + ActionType index = explorationInformation.getRowGroup(state); + return boundsPerState[index]; + } + + template + ValueType Bounds::getLowerBoundForState(StateType const& state, ExplorationInformation const& explorationInformation) const { + ActionType index = explorationInformation.getRowGroup(state); + if (index == explorationInformation.getUnexploredMarker()) { + return storm::utility::zero(); + } else { + return getLowerBoundForRowGroup(index); + } + } + + template + ValueType const& Bounds::getLowerBoundForRowGroup(StateType const& rowGroup) const { + return boundsPerState[rowGroup].first; + } + + template + ValueType Bounds::getUpperBoundForState(StateType const& state, ExplorationInformation const& explorationInformation) const { + ActionType index = explorationInformation.getRowGroup(state); + if (index == explorationInformation.getUnexploredMarker()) { + return storm::utility::one(); + } else { + return getUpperBoundForRowGroup(index); + } + } + + template + ValueType const& Bounds::getUpperBoundForRowGroup(StateType const& rowGroup) const { + return boundsPerState[rowGroup].second; + } + + template + std::pair const& Bounds::getBoundsForAction(ActionType const& action) const { + return boundsPerAction[action]; + } + + template + ValueType const& Bounds::getLowerBoundForAction(ActionType const& action) const { + return boundsPerAction[action].first; + } + + template + ValueType const& Bounds::getUpperBoundForAction(ActionType const& action) const { + return boundsPerAction[action].second; + } + + template + ValueType const& Bounds::getBoundForAction(storm::OptimizationDirection const& direction, ActionType const& action) const { + if (direction == storm::OptimizationDirection::Maximize) { + return getUpperBoundForAction(action); + } else { + return getLowerBoundForAction(action); + } + } + + template + ValueType Bounds::getDifferenceOfStateBounds(StateType const& state, ExplorationInformation const& explorationInformation) const { + std::pair const& bounds = getBoundsForExploredState(state, explorationInformation); + return bounds.second - bounds.first; + } + + template + void Bounds::initializeBoundsForNextState(std::pair const& vals) { + boundsPerState.push_back(vals); + } + + template + void Bounds::initializeBoundsForNextAction(std::pair const& vals) { + boundsPerAction.push_back(vals); + } + + template + void Bounds::setLowerBoundForState(StateType const& state, ExplorationInformation const& explorationInformation, ValueType const& value) { + setLowerBoundForRowGroup(explorationInformation.getRowGroup(state), value); + } + + template + void Bounds::setLowerBoundForRowGroup(StateType const& group, ValueType const& value) { + boundsPerState[group].first = value; + } + + template + void Bounds::setUpperBoundForState(StateType const& state, ExplorationInformation const& explorationInformation, ValueType const& value) { + setUpperBoundForRowGroup(explorationInformation.getRowGroup(state), value); + } + + template + void Bounds::setUpperBoundForRowGroup(StateType const& group, ValueType const& value) { + boundsPerState[group].second = value; + } + + template + void Bounds::setBoundsForAction(ActionType const& action, std::pair const& values) { + boundsPerAction[action] = values; + } + + template + void Bounds::setBoundsForState(StateType const& state, ExplorationInformation const& explorationInformation, std::pair const& values) { + StateType const& rowGroup = explorationInformation.getRowGroup(state); + setBoundsForRowGroup(rowGroup, values); + } + + template + void Bounds::setBoundsForRowGroup(StateType const& rowGroup, std::pair const& values) { + boundsPerState[rowGroup] = values; + } + + template + bool Bounds::setLowerBoundOfStateIfGreaterThanOld(StateType const& state, ExplorationInformation const& explorationInformation, ValueType const& newLowerValue) { + StateType const& rowGroup = explorationInformation.getRowGroup(state); + if (boundsPerState[rowGroup].first < newLowerValue) { + boundsPerState[rowGroup].first = newLowerValue; + return true; + } + return false; + } + + template + bool Bounds::setUpperBoundOfStateIfLessThanOld(StateType const& state, ExplorationInformation const& explorationInformation, ValueType const& newUpperValue) { + StateType const& rowGroup = explorationInformation.getRowGroup(state); + if (newUpperValue < boundsPerState[rowGroup].second) { + boundsPerState[rowGroup].second = newUpperValue; + return true; + } + return false; + } + + template class Bounds; + + } + } +} diff --git a/src/modelchecker/exploration/Bounds.h b/src/modelchecker/exploration/Bounds.h new file mode 100644 index 000000000..27e0979a5 --- /dev/null +++ b/src/modelchecker/exploration/Bounds.h @@ -0,0 +1,76 @@ +#ifndef STORM_MODELCHECKER_EXPLORATION_EXPLORATION_DETAIL_BOUNDS_H_ +#define STORM_MODELCHECKER_EXPLORATION_EXPLORATION_DETAIL_BOUNDS_H_ + +#include +#include + +#include "src/solver/OptimizationDirection.h" + +#include "src/utility/constants.h" + +namespace storm { + namespace modelchecker { + namespace exploration_detail { + + template + class ExplorationInformation; + + template + class Bounds { + public: + typedef StateType ActionType; + + std::pair getBoundsForState(StateType const& state, ExplorationInformation const& explorationInformation) const; + + std::pair const& getBoundsForExploredState(StateType const& state, ExplorationInformation const& explorationInformation) const; + + ValueType getLowerBoundForState(StateType const& state, ExplorationInformation const& explorationInformation) const; + + ValueType const& getLowerBoundForRowGroup(StateType const& rowGroup) const; + + ValueType getUpperBoundForState(StateType const& state, ExplorationInformation const& explorationInformation) const; + + ValueType const& getUpperBoundForRowGroup(StateType const& rowGroup) const; + + std::pair const& getBoundsForAction(ActionType const& action) const; + + ValueType const& getLowerBoundForAction(ActionType const& action) const; + + ValueType const& getUpperBoundForAction(ActionType const& action) const; + + ValueType const& getBoundForAction(storm::OptimizationDirection const& direction, ActionType const& action) const; + + ValueType getDifferenceOfStateBounds(StateType const& state, ExplorationInformation const& explorationInformation) const; + + void initializeBoundsForNextState(std::pair const& vals = std::pair(storm::utility::zero(), storm::utility::one())); + + void initializeBoundsForNextAction(std::pair const& vals = std::pair(storm::utility::zero(), storm::utility::one())); + + void setLowerBoundForState(StateType const& state, ExplorationInformation const& explorationInformation, ValueType const& value); + + void setLowerBoundForRowGroup(StateType const& group, ValueType const& value); + + void setUpperBoundForState(StateType const& state, ExplorationInformation const& explorationInformation, ValueType const& value); + + void setUpperBoundForRowGroup(StateType const& group, ValueType const& value); + + void setBoundsForAction(ActionType const& action, std::pair const& values); + + void setBoundsForState(StateType const& state, ExplorationInformation const& explorationInformation, std::pair const& values); + + void setBoundsForRowGroup(StateType const& rowGroup, std::pair const& values); + + bool setLowerBoundOfStateIfGreaterThanOld(StateType const& state, ExplorationInformation const& explorationInformation, ValueType const& newLowerValue); + + bool setUpperBoundOfStateIfLessThanOld(StateType const& state, ExplorationInformation const& explorationInformation, ValueType const& newUpperValue); + + private: + std::vector> boundsPerState; + std::vector> boundsPerAction; + }; + + } + } +} + +#endif /* STORM_MODELCHECKER_EXPLORATION_EXPLORATION_DETAIL_BOUNDS_H_ */ \ No newline at end of file diff --git a/src/modelchecker/exploration/ExplorationInformation.cpp b/src/modelchecker/exploration/ExplorationInformation.cpp index e69de29bb..12715f307 100644 --- a/src/modelchecker/exploration/ExplorationInformation.cpp +++ b/src/modelchecker/exploration/ExplorationInformation.cpp @@ -0,0 +1,209 @@ +#include "src/modelchecker/exploration/ExplorationInformation.h" + +#include "src/settings/SettingsManager.h" +#include "src/settings/modules/ExplorationSettings.h" + +#include "src/utility/macros.h" + +namespace storm { + namespace modelchecker { + namespace exploration_detail { + + template + ExplorationInformation::ExplorationInformation(uint_fast64_t bitsPerBucket, storm::OptimizationDirection const& direction, ActionType const& unexploredMarker) : stateStorage(bitsPerBucket), unexploredMarker(unexploredMarker), optimizationDirection(direction), localPrecomputation(false), numberOfExplorationStepsUntilPrecomputation(100000), numberOfSampledPathsUntilPrecomputation(), nextStateHeuristic(storm::settings::modules::ExplorationSettings::NextStateHeuristic::DifferenceWeightedProbability) { + + storm::settings::modules::ExplorationSettings const& settings = storm::settings::explorationSettings(); + localPrecomputation = settings.isLocalPrecomputationSet(); + numberOfExplorationStepsUntilPrecomputation = settings.getNumberOfExplorationStepsUntilPrecomputation(); + if (settings.isNumberOfSampledPathsUntilPrecomputationSet()) { + numberOfSampledPathsUntilPrecomputation = settings.getNumberOfSampledPathsUntilPrecomputation(); + } + + nextStateHeuristic = settings.getNextStateHeuristic(); + STORM_LOG_ASSERT(useDifferenceWeightedProbabilityHeuristic() || useProbabilityHeuristic(), "Illegal next-state heuristic."); + } + + template + void ExplorationInformation::setInitialStates(std::vector const& initialStates) { + stateStorage.initialStateIndices = initialStates; + } + + template + StateType ExplorationInformation::getFirstInitialState() const { + return stateStorage.initialStateIndices.front(); + } + + template + std::size_t ExplorationInformation::getNumberOfInitialStates() const { + return stateStorage.initialStateIndices.size(); + } + + template + void ExplorationInformation::addUnexploredState(storm::generator::CompressedState const& compressedState) { + stateToRowGroupMapping.push_back(unexploredMarker); + unexploredStates[stateStorage.numberOfStates] = compressedState; + ++stateStorage.numberOfStates; + } + + template + void ExplorationInformation::assignStateToRowGroup(StateType const& state, ActionType const& rowGroup) { + stateToRowGroupMapping[state] = rowGroup; + } + + template + StateType ExplorationInformation::assignStateToNextRowGroup(StateType const& state) { + stateToRowGroupMapping[state] = rowGroupIndices.size() - 1; + return stateToRowGroupMapping[state]; + } + + template + StateType ExplorationInformation::getNextRowGroup() const { + return rowGroupIndices.size() - 1; + } + + template + void ExplorationInformation::newRowGroup(ActionType const& action) { + rowGroupIndices.push_back(action); + } + + template + void ExplorationInformation::newRowGroup() { + newRowGroup(matrix.size()); + } + + template + std::size_t ExplorationInformation::getNumberOfUnexploredStates() const { + return unexploredStates.size(); + } + + template + std::size_t ExplorationInformation::getNumberOfDiscoveredStates() const { + return stateStorage.numberOfStates; + } + + template + StateType const& ExplorationInformation::getRowGroup(StateType const& state) const { + return stateToRowGroupMapping[state]; + } + + template + StateType const& ExplorationInformation::getUnexploredMarker() const { + return unexploredMarker; + } + + template + bool ExplorationInformation::isUnexplored(StateType const& state) const { + return stateToRowGroupMapping[state] == unexploredMarker; + } + + template + bool ExplorationInformation::isTerminal(StateType const& state) const { + return terminalStates.find(state) != terminalStates.end(); + } + + template + typename ExplorationInformation::ActionType const& ExplorationInformation::getStartRowOfGroup(StateType const& group) const { + return rowGroupIndices[group]; + } + + template + std::size_t ExplorationInformation::getRowGroupSize(StateType const& group) const { + return rowGroupIndices[group + 1] - rowGroupIndices[group]; + } + + template + bool ExplorationInformation::onlyOneActionAvailable(StateType const& group) const { + return getRowGroupSize(group) == 1; + } + + template + void ExplorationInformation::addTerminalState(StateType const& state) { + terminalStates.insert(state); + } + + template + std::vector>& ExplorationInformation::getRowOfMatrix(ActionType const& row) { + return matrix[row]; + } + + template + std::vector> const& ExplorationInformation::getRowOfMatrix(ActionType const& row) const { + return matrix[row]; + } + + template + void ExplorationInformation::addRowsToMatrix(std::size_t const& count) { + matrix.resize(matrix.size() + count); + } + + template + bool ExplorationInformation::maximize() const { + return optimizationDirection == storm::OptimizationDirection::Maximize; + } + + template + bool ExplorationInformation::minimize() const { + return !maximize(); + } + + template + bool ExplorationInformation::performPrecomputationExcessiveExplorationSteps(std::size_t& numberExplorationStepsSinceLastPrecomputation) const { + bool result = numberExplorationStepsSinceLastPrecomputation > numberOfExplorationStepsUntilPrecomputation; + if (result) { + numberExplorationStepsSinceLastPrecomputation = 0; + } + return result; + } + + template + bool ExplorationInformation::performPrecomputationExcessiveSampledPaths(std::size_t& numberOfSampledPathsSinceLastPrecomputation) const { + if (!numberOfSampledPathsUntilPrecomputation) { + return false; + } else { + bool result = numberOfSampledPathsSinceLastPrecomputation > numberOfSampledPathsUntilPrecomputation.get(); + if (result) { + numberOfSampledPathsSinceLastPrecomputation = 0; + } + return result; + } + } + + template + bool ExplorationInformation::useLocalPrecomputation() const { + return localPrecomputation; + } + + template + bool ExplorationInformation::useGlobalPrecomputation() const { + return !useLocalPrecomputation(); + } + + template + storm::settings::modules::ExplorationSettings::NextStateHeuristic const& ExplorationInformation::getNextStateHeuristic() const { + return nextStateHeuristic; + } + + template + bool ExplorationInformation::useDifferenceWeightedProbabilityHeuristic() const { + return nextStateHeuristic == storm::settings::modules::ExplorationSettings::NextStateHeuristic::DifferenceWeightedProbability; + } + + template + bool ExplorationInformation::useProbabilityHeuristic() const { + return nextStateHeuristic == storm::settings::modules::ExplorationSettings::NextStateHeuristic::Probability; + } + + template + storm::OptimizationDirection const& ExplorationInformation::getOptimizationDirection() const { + return optimizationDirection; + } + + template + void ExplorationInformation::setOptimizationDirection(storm::OptimizationDirection const& direction) { + optimizationDirection = direction; + } + + template class ExplorationInformation; + } + } +} \ No newline at end of file diff --git a/src/modelchecker/exploration/ExplorationInformation.h b/src/modelchecker/exploration/ExplorationInformation.h index e69de29bb..b073352cd 100644 --- a/src/modelchecker/exploration/ExplorationInformation.h +++ b/src/modelchecker/exploration/ExplorationInformation.h @@ -0,0 +1,120 @@ +#ifndef STORM_MODELCHECKER_EXPLORATION_EXPLORATION_DETAIL_EXPLORATIONINFORMATION_H_ +#define STORM_MODELCHECKER_EXPLORATION_EXPLORATION_DETAIL_EXPLORATIONINFORMATION_H_ + +#include +#include +#include + +#include +#include + +#include "src/solver/OptimizationDirection.h" + +#include "src/generator/CompressedState.h" + +#include "src/storage/SparseMatrix.h" +#include "src/storage/sparse/StateStorage.h" + +#include "src/settings/modules/ExplorationSettings.h" + +namespace storm { + namespace modelchecker { + namespace exploration_detail { + template + class ExplorationInformation { + public: + typedef StateType ActionType; + typedef boost::container::flat_set StateSet; + + ExplorationInformation(uint_fast64_t bitsPerBucket, storm::OptimizationDirection const& direction, ActionType const& unexploredMarker = std::numeric_limits::max()); + + void setInitialStates(std::vector const& initialStates); + + StateType getFirstInitialState() const; + + std::size_t getNumberOfInitialStates() const; + + void addUnexploredState(storm::generator::CompressedState const& compressedState); + + void assignStateToRowGroup(StateType const& state, ActionType const& rowGroup); + + StateType assignStateToNextRowGroup(StateType const& state); + + StateType getNextRowGroup() const; + + void newRowGroup(ActionType const& action); + + void newRowGroup(); + + std::size_t getNumberOfUnexploredStates() const; + + std::size_t getNumberOfDiscoveredStates() const; + + StateType const& getRowGroup(StateType const& state) const; + + StateType const& getUnexploredMarker() const; + + bool isUnexplored(StateType const& state) const; + + bool isTerminal(StateType const& state) const; + + ActionType const& getStartRowOfGroup(StateType const& group) const; + + std::size_t getRowGroupSize(StateType const& group) const; + + bool onlyOneActionAvailable(StateType const& group) const; + + void addTerminalState(StateType const& state); + + std::vector>& getRowOfMatrix(ActionType const& row); + + std::vector> const& getRowOfMatrix(ActionType const& row) const; + + void addRowsToMatrix(std::size_t const& count); + + bool maximize() const; + + bool minimize() const; + + bool performPrecomputationExcessiveExplorationSteps(std::size_t& numberExplorationStepsSinceLastPrecomputation) const; + + bool performPrecomputationExcessiveSampledPaths(std::size_t& numberOfSampledPathsSinceLastPrecomputation) const; + + bool useLocalPrecomputation() const; + + bool useGlobalPrecomputation() const; + + storm::settings::modules::ExplorationSettings::NextStateHeuristic const& getNextStateHeuristic() const; + + bool useDifferenceWeightedProbabilityHeuristic() const; + + bool useProbabilityHeuristic() const; + + storm::OptimizationDirection const& getOptimizationDirection() const; + + void setOptimizationDirection(storm::OptimizationDirection const& direction); + + private: + storm::storage::sparse::StateStorage stateStorage; + + std::vector>> matrix; + std::vector rowGroupIndices; + + std::vector stateToRowGroupMapping; + StateType unexploredMarker; + std::unordered_map unexploredStates; + + storm::OptimizationDirection optimizationDirection; + StateSet terminalStates; + + bool localPrecomputation; + std::size_t numberOfExplorationStepsUntilPrecomputation; + boost::optional numberOfSampledPathsUntilPrecomputation; + + storm::settings::modules::ExplorationSettings::NextStateHeuristic nextStateHeuristic; + }; + } + } +} + +#endif /* STORM_MODELCHECKER_EXPLORATION_EXPLORATION_DETAIL_EXPLORATIONINFORMATION_H_ */ \ No newline at end of file diff --git a/src/modelchecker/exploration/SparseMdpExplorationModelChecker.cpp b/src/modelchecker/exploration/SparseMdpExplorationModelChecker.cpp index 037d97800..4ad5b5613 100644 --- a/src/modelchecker/exploration/SparseMdpExplorationModelChecker.cpp +++ b/src/modelchecker/exploration/SparseMdpExplorationModelChecker.cpp @@ -1,20 +1,30 @@ #include "src/modelchecker/exploration/SparseMdpExplorationModelChecker.h" +#include "src/modelchecker/exploration/ExplorationInformation.h" +#include "src/modelchecker/exploration/StateGeneration.h" +#include "src/modelchecker/exploration/Bounds.h" +#include "src/modelchecker/exploration/Statistics.h" + +#include "src/generator/CompressedState.h" + #include "src/storage/SparseMatrix.h" #include "src/storage/MaximalEndComponentDecomposition.h" -#include "src/storage/expressions/SimpleValuation.h" -#include "src/logic/FragmentSpecification.h" +#include "src/storage/prism/Program.h" -#include "src/utility/prism.h" +#include "src/logic/FragmentSpecification.h" #include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h" #include "src/models/sparse/StandardRewardModel.h" +#include "src/settings/SettingsManager.h" #include "src/settings/modules/GeneralSettings.h" +#include "src/utility/macros.h" +#include "src/utility/constants.h" #include "src/utility/graph.h" +#include "src/utility/prism.h" #include "src/exceptions/InvalidOperationException.h" #include "src/exceptions/InvalidPropertyException.h" @@ -43,16 +53,15 @@ 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."); std::map labelToExpressionMapping = program.getLabelToExpressionMapping(); - StateGeneration stateGeneration(program, variableInformation, conditionFormula.toExpression(program.getManager(), labelToExpressionMapping), targetFormula.toExpression(program.getManager(), labelToExpressionMapping)); + StateGeneration stateGeneration(program, variableInformation, conditionFormula.toExpression(program.getManager(), labelToExpressionMapping), targetFormula.toExpression(program.getManager(), labelToExpressionMapping)); - ExplorationInformation explorationInformation(variableInformation.getTotalBitOffset(true), storm::settings::explorationSettings().getNumberOfExplorationStepsUntilPrecomputation()); - explorationInformation.optimizationDirection = checkTask.isOptimizationDirectionSet() ? checkTask.getOptimizationDirection() : storm::OptimizationDirection::Maximize; + ExplorationInformation explorationInformation(variableInformation.getTotalBitOffset(true), checkTask.isOptimizationDirectionSet() ? checkTask.getOptimizationDirection() : storm::OptimizationDirection::Maximize); // The first row group starts at action 0. explorationInformation.newRowGroup(0); // Create a callback for the next-state generator to enable it to request the index of states. - stateGeneration.stateToIdCallback = createStateToIdCallback(explorationInformation); + stateGeneration.setStateToIdCallback(createStateToIdCallback(explorationInformation)); // Compute and return result. std::tuple boundsForInitialState = performExploration(stateGeneration, explorationInformation); @@ -60,9 +69,9 @@ namespace storm { } template - std::function::StateType (storm::generator::CompressedState const&)> SparseMdpExplorationModelChecker::createStateToIdCallback(ExplorationInformation& explorationInformation) const { + std::function::StateType (storm::generator::CompressedState const&)> SparseMdpExplorationModelChecker::createStateToIdCallback(ExplorationInformation& explorationInformation) const { return [&explorationInformation,this] (storm::generator::CompressedState const& state) -> StateType { - StateType newIndex = explorationInformation.stateStorage.numberOfStates; + StateType newIndex = explorationInformation.getNumberOfDiscoveredStates(); // Check, if the state was already registered. std::pair actualIndexBucketPair = explorationInformation.stateStorage.stateToId.findOrAddAndGetBucket(state, newIndex); @@ -76,7 +85,7 @@ namespace storm { } template - std::tuple::StateType, ValueType, ValueType> SparseMdpExplorationModelChecker::performExploration(StateGeneration& stateGeneration, ExplorationInformation& explorationInformation) const { + std::tuple::StateType, ValueType, ValueType> SparseMdpExplorationModelChecker::performExploration(StateGeneration& stateGeneration, ExplorationInformation& explorationInformation) const { // Generate the initial state so we know where to start the simulation. explorationInformation.setInitialStates(stateGeneration.getInitialStates()); @@ -84,13 +93,13 @@ namespace storm { StateType initialStateIndex = explorationInformation.getFirstInitialState(); // Create a structure that holds the bounds for the states and actions. - BoundValues bounds; + Bounds bounds; // Create a stack that is used to track the path we sampled. StateActionStack stack; // Now perform the actual sampling. - Statistics stats; + Statistics stats; bool convergenceCriterionMet = false; while (!convergenceCriterionMet) { bool result = samplePathFromInitialState(stateGeneration, explorationInformation, stack, bounds, stats); @@ -130,7 +139,7 @@ namespace storm { } template - bool SparseMdpExplorationModelChecker::samplePathFromInitialState(StateGeneration& stateGeneration, ExplorationInformation& explorationInformation, StateActionStack& stack, BoundValues& bounds, Statistics& stats) const { + bool SparseMdpExplorationModelChecker::samplePathFromInitialState(StateGeneration& stateGeneration, ExplorationInformation& explorationInformation, StateActionStack& stack, Bounds& bounds, Statistics& stats) const { // Start the search from the initial state. stack.push_back(std::make_pair(explorationInformation.getFirstInitialState(), 0)); @@ -192,7 +201,7 @@ namespace storm { } template - bool SparseMdpExplorationModelChecker::exploreState(StateGeneration& stateGeneration, StateType const& currentStateId, storm::generator::CompressedState const& currentState, ExplorationInformation& explorationInformation, BoundValues& bounds, Statistics& stats) const { + bool SparseMdpExplorationModelChecker::exploreState(StateGeneration& stateGeneration, StateType const& currentStateId, storm::generator::CompressedState const& currentState, ExplorationInformation& explorationInformation, Bounds& bounds, Statistics& stats) const { bool isTerminalState = false; bool isTargetState = false; @@ -242,7 +251,7 @@ namespace storm { ActionType currentAction = 0; // Retrieve the lowest state bounds (wrt. to the current optimization direction). - std::pair stateBounds = getLowestBounds(explorationInformation.optimizationDirection); + std::pair stateBounds = getLowestBounds(explorationInformation.getOptimizationDirection()); for (auto const& choice : behavior) { for (auto const& entry : choice) { @@ -251,7 +260,7 @@ namespace storm { std::pair actionBounds = computeBoundsOfAction(startRow + currentAction, explorationInformation, bounds); bounds.initializeBoundsForNextAction(actionBounds); - stateBounds = combineBounds(explorationInformation.optimizationDirection, stateBounds, actionBounds); + stateBounds = combineBounds(explorationInformation.getOptimizationDirection(), stateBounds, actionBounds); STORM_LOG_TRACE("Initializing bounds of action " << (startRow + currentAction) << " to " << bounds.getLowerBoundForAction(startRow + currentAction) << " and " << bounds.getUpperBoundForAction(startRow + currentAction) << "."); @@ -293,7 +302,7 @@ namespace storm { } template - typename SparseMdpExplorationModelChecker::ActionType SparseMdpExplorationModelChecker::sampleActionOfState(StateType const& currentStateId, ExplorationInformation const& explorationInformation, BoundValues& bounds) const { + typename SparseMdpExplorationModelChecker::ActionType SparseMdpExplorationModelChecker::sampleActionOfState(StateType const& currentStateId, ExplorationInformation const& explorationInformation, Bounds& bounds) const { // Determine the values of all available actions. std::vector> actionValues; StateType rowGroup = explorationInformation.getRowGroup(currentStateId); @@ -307,7 +316,7 @@ namespace storm { STORM_LOG_TRACE("Sampling from actions leaving the state."); for (uint32_t row = explorationInformation.getStartRowOfGroup(rowGroup); row < explorationInformation.getStartRowOfGroup(rowGroup + 1); ++row) { - actionValues.push_back(std::make_pair(row, bounds.getBoundForAction(explorationInformation.optimizationDirection, row))); + actionValues.push_back(std::make_pair(row, bounds.getBoundForAction(explorationInformation.getOptimizationDirection(), row))); } STORM_LOG_ASSERT(!actionValues.empty(), "Values for actions must not be empty."); @@ -331,7 +340,7 @@ namespace storm { } template - typename SparseMdpExplorationModelChecker::StateType SparseMdpExplorationModelChecker::sampleSuccessorFromAction(ActionType const& chosenAction, ExplorationInformation const& explorationInformation, BoundValues const& bounds) const { + typename SparseMdpExplorationModelChecker::StateType SparseMdpExplorationModelChecker::sampleSuccessorFromAction(ActionType const& chosenAction, ExplorationInformation const& explorationInformation, Bounds const& bounds) const { std::vector> const& row = explorationInformation.getRowOfMatrix(chosenAction); // if (row.size() == 1) { // return row.front().getColumn(); @@ -359,7 +368,7 @@ namespace storm { } template - bool SparseMdpExplorationModelChecker::performPrecomputation(StateActionStack const& stack, ExplorationInformation& explorationInformation, BoundValues& bounds, Statistics& stats) const { + bool SparseMdpExplorationModelChecker::performPrecomputation(StateActionStack const& stack, ExplorationInformation& explorationInformation, Bounds& bounds, Statistics& stats) const { ++stats.numberOfPrecomputations; // Outline: @@ -383,9 +392,9 @@ namespace storm { auto newEnd = std::unique(relevantStates.begin(), relevantStates.end()); relevantStates.resize(std::distance(relevantStates.begin(), newEnd)); } else { - for (StateType state = 0; state < explorationInformation.stateStorage.numberOfStates; ++state) { - // Add the state to the relevant states if it's unexplored. Additionally, if we are computing minimal - // probabilities, we only consider it relevant if it's not a target state. + for (StateType state = 0; state < explorationInformation.getNumberOfDiscoveredStates(); ++state) { + // Add the state to the relevant states if they are not unexplored. Additionally, if we are + // computing minimal probabilities, we only consider it relevant if it's not a target state. if (!explorationInformation.isUnexplored(state) && (explorationInformation.maximize() || !comparator.isOne(bounds.getLowerBoundForState(state, explorationInformation)))) { relevantStates.push_back(state); } @@ -493,7 +502,7 @@ namespace storm { } template - void SparseMdpExplorationModelChecker::collapseMec(storm::storage::MaximalEndComponent const& mec, std::vector const& relevantStates, storm::storage::SparseMatrix const& relevantStatesMatrix, ExplorationInformation& explorationInformation, BoundValues& bounds) const { + void SparseMdpExplorationModelChecker::collapseMec(storm::storage::MaximalEndComponent const& mec, std::vector const& relevantStates, storm::storage::SparseMatrix const& relevantStatesMatrix, ExplorationInformation& explorationInformation, Bounds& bounds) const { bool containsTargetState = false; // Now we record all actions leaving the EC. @@ -547,12 +556,12 @@ namespace storm { // Add to the new row group all leaving actions of contained states and set the appropriate bounds for // the actions and the new state. - std::pair stateBounds = getLowestBounds(explorationInformation.optimizationDirection); + std::pair stateBounds = getLowestBounds(explorationInformation.getOptimizationDirection()); for (auto const& action : leavingActions) { explorationInformation.matrix.emplace_back(std::move(explorationInformation.matrix[action])); std::pair const& actionBounds = bounds.getBoundsForAction(action); bounds.initializeBoundsForNextAction(actionBounds); - stateBounds = combineBounds(explorationInformation.optimizationDirection, stateBounds, actionBounds); + stateBounds = combineBounds(explorationInformation.getOptimizationDirection(), stateBounds, actionBounds); } bounds.setBoundsForRowGroup(nextRowGroup, stateBounds); @@ -562,7 +571,7 @@ namespace storm { } template - ValueType SparseMdpExplorationModelChecker::computeLowerBoundOfAction(ActionType const& action, ExplorationInformation const& explorationInformation, BoundValues const& bounds) const { + ValueType SparseMdpExplorationModelChecker::computeLowerBoundOfAction(ActionType const& action, ExplorationInformation const& explorationInformation, Bounds const& bounds) const { ValueType result = storm::utility::zero(); for (auto const& element : explorationInformation.getRowOfMatrix(action)) { result += element.getValue() * bounds.getLowerBoundForState(element.getColumn(), explorationInformation); @@ -571,7 +580,7 @@ namespace storm { } template - ValueType SparseMdpExplorationModelChecker::computeUpperBoundOfAction(ActionType const& action, ExplorationInformation const& explorationInformation, BoundValues const& bounds) const { + ValueType SparseMdpExplorationModelChecker::computeUpperBoundOfAction(ActionType const& action, ExplorationInformation const& explorationInformation, Bounds const& bounds) const { ValueType result = storm::utility::zero(); for (auto const& element : explorationInformation.getRowOfMatrix(action)) { result += element.getValue() * bounds.getUpperBoundForState(element.getColumn(), explorationInformation); @@ -580,7 +589,7 @@ namespace storm { } template - std::pair SparseMdpExplorationModelChecker::computeBoundsOfAction(ActionType const& action, ExplorationInformation const& explorationInformation, BoundValues const& bounds) const { + std::pair SparseMdpExplorationModelChecker::computeBoundsOfAction(ActionType const& action, ExplorationInformation const& explorationInformation, Bounds const& bounds) const { // TODO: take into account self-loops? std::pair result = std::make_pair(storm::utility::zero(), storm::utility::zero()); for (auto const& element : explorationInformation.getRowOfMatrix(action)) { @@ -591,18 +600,18 @@ namespace storm { } template - std::pair SparseMdpExplorationModelChecker::computeBoundsOfState(StateType const& currentStateId, ExplorationInformation const& explorationInformation, BoundValues const& bounds) const { + std::pair SparseMdpExplorationModelChecker::computeBoundsOfState(StateType const& currentStateId, ExplorationInformation const& explorationInformation, Bounds const& bounds) const { StateType group = explorationInformation.getRowGroup(currentStateId); - std::pair result = getLowestBounds(explorationInformation.optimizationDirection); + std::pair result = getLowestBounds(explorationInformation.getOptimizationDirection()); for (ActionType action = explorationInformation.getStartRowOfGroup(group); action < explorationInformation.getStartRowOfGroup(group + 1); ++action) { std::pair actionValues = computeBoundsOfAction(action, explorationInformation, bounds); - result = combineBounds(explorationInformation.optimizationDirection, result, actionValues); + result = combineBounds(explorationInformation.getOptimizationDirection(), result, actionValues); } return result; } template - void SparseMdpExplorationModelChecker::updateProbabilityBoundsAlongSampledPath(StateActionStack& stack, ExplorationInformation const& explorationInformation, BoundValues& bounds) const { + void SparseMdpExplorationModelChecker::updateProbabilityBoundsAlongSampledPath(StateActionStack& stack, ExplorationInformation const& explorationInformation, Bounds& bounds) const { stack.pop_back(); while (!stack.empty()) { updateProbabilityOfAction(stack.back().first, stack.back().second, explorationInformation, bounds); @@ -611,7 +620,7 @@ namespace storm { } template - void SparseMdpExplorationModelChecker::updateProbabilityOfAction(StateType const& state, ActionType const& action, ExplorationInformation const& explorationInformation, BoundValues& bounds) const { + void SparseMdpExplorationModelChecker::updateProbabilityOfAction(StateType const& state, ActionType const& action, ExplorationInformation const& explorationInformation, Bounds& bounds) const { // Compute the new lower/upper values of the action. std::pair newBoundsForAction = computeBoundsOfAction(action, explorationInformation, bounds); @@ -646,8 +655,8 @@ namespace storm { } template - ValueType SparseMdpExplorationModelChecker::computeBoundOverAllOtherActions(storm::OptimizationDirection const& direction, StateType const& state, ActionType const& action, ExplorationInformation const& explorationInformation, BoundValues const& bounds) const { - ValueType bound = getLowestBound(explorationInformation.optimizationDirection); + ValueType SparseMdpExplorationModelChecker::computeBoundOverAllOtherActions(storm::OptimizationDirection const& direction, StateType const& state, ActionType const& action, ExplorationInformation const& explorationInformation, Bounds const& bounds) const { + ValueType bound = getLowestBound(explorationInformation.getOptimizationDirection()); ActionType group = explorationInformation.getRowGroup(state); for (auto currentAction = explorationInformation.getStartRowOfGroup(group); currentAction < explorationInformation.getStartRowOfGroup(group + 1); ++currentAction) { diff --git a/src/modelchecker/exploration/SparseMdpExplorationModelChecker.h b/src/modelchecker/exploration/SparseMdpExplorationModelChecker.h index f73f7b39f..74e78cf0e 100644 --- a/src/modelchecker/exploration/SparseMdpExplorationModelChecker.h +++ b/src/modelchecker/exploration/SparseMdpExplorationModelChecker.h @@ -6,44 +6,35 @@ #include "src/modelchecker/AbstractModelChecker.h" #include "src/storage/prism/Program.h" -#include "src/storage/sparse/StateStorage.h" -#include "src/generator/PrismNextStateGenerator.h" #include "src/generator/CompressedState.h" #include "src/generator/VariableInformation.h" -#include "src/settings/SettingsManager.h" -#include "src/settings/modules/ExplorationSettings.h" - -#include "src/utility/macros.h" #include "src/utility/ConstantsComparator.h" -#include "src/utility/constants.h" namespace storm { namespace storage { - namespace sparse { - template - class StateStorage; - } - class MaximalEndComponent; } - - namespace generator { - template - class PrismNextStateGenerator; + namespace prism { + class Program; } namespace modelchecker { + namespace exploration_detail { + template class StateGeneration; + template class ExplorationInformation; + template class Bounds; + template class Statistics; + } + + using namespace exploration_detail; template class SparseMdpExplorationModelChecker : public AbstractModelChecker { public: typedef uint32_t StateType; - typedef uint32_t ActionType; - typedef boost::container::flat_set StateSet; - typedef boost::container::flat_set ActionSet; - typedef std::shared_ptr ActionSetPointer; + typedef StateType ActionType; typedef std::vector> StateActionStack; SparseMdpExplorationModelChecker(storm::prism::Program const& program, boost::optional> const& constantDefinitions); @@ -53,278 +44,31 @@ namespace storm { virtual std::unique_ptr computeUntilProbabilities(CheckTask const& checkTask) override; private: - // A structure containing the data assembled during exploration. - struct ExplorationInformation { - ExplorationInformation(uint_fast64_t bitsPerBucket, ActionType const& unexploredMarker = std::numeric_limits::max()) : stateStorage(bitsPerBucket), unexploredMarker(unexploredMarker), localPrecomputation(false), numberOfExplorationStepsUntilPrecomputation(100000), numberOfSampledPathsUntilPrecomputation(), nextStateHeuristic(storm::settings::modules::ExplorationSettings::NextStateHeuristic::DifferenceWeightedProbability) { - - storm::settings::modules::ExplorationSettings const& settings = storm::settings::explorationSettings(); - localPrecomputation = settings.isLocalPrecomputationSet(); - if (settings.isNumberOfSampledPathsUntilPrecomputationSet()) { - numberOfSampledPathsUntilPrecomputation = settings.getNumberOfSampledPathsUntilPrecomputation(); - } - - nextStateHeuristic = settings.getNextStateHeuristic(); - STORM_LOG_ASSERT(useDifferenceWeightedProbabilityHeuristic() || useProbabilityHeuristic(), "Illegal next-state heuristic."); - } - - storm::storage::sparse::StateStorage stateStorage; - - std::vector>> matrix; - std::vector rowGroupIndices; - - std::vector stateToRowGroupMapping; - StateType unexploredMarker; - std::unordered_map unexploredStates; - - storm::OptimizationDirection optimizationDirection; - StateSet terminalStates; - - bool localPrecomputation; - uint_fast64_t numberOfExplorationStepsUntilPrecomputation; - boost::optional numberOfSampledPathsUntilPrecomputation; - - storm::settings::modules::ExplorationSettings::NextStateHeuristic nextStateHeuristic; - - void setInitialStates(std::vector const& initialStates) { - stateStorage.initialStateIndices = initialStates; - } - - StateType getFirstInitialState() const { - return stateStorage.initialStateIndices.front(); - } - - std::size_t getNumberOfInitialStates() const { - return stateStorage.initialStateIndices.size(); - } - - void addUnexploredState(storm::generator::CompressedState const& compressedState) { - stateToRowGroupMapping.push_back(unexploredMarker); - unexploredStates[stateStorage.numberOfStates] = compressedState; - ++stateStorage.numberOfStates; - } - - void assignStateToRowGroup(StateType const& state, ActionType const& rowGroup) { - stateToRowGroupMapping[state] = rowGroup; - } - - StateType assignStateToNextRowGroup(StateType const& state) { - stateToRowGroupMapping[state] = rowGroupIndices.size() - 1; - return stateToRowGroupMapping[state]; - } - - StateType getNextRowGroup() const { - return rowGroupIndices.size() - 1; - } - - void newRowGroup(ActionType const& action) { - rowGroupIndices.push_back(action); - } - - void newRowGroup() { - newRowGroup(matrix.size()); - } - - std::size_t getNumberOfUnexploredStates() const { - return unexploredStates.size(); - } - - std::size_t getNumberOfDiscoveredStates() const { - return stateStorage.numberOfStates; - } - - StateType const& getRowGroup(StateType const& state) const { - return stateToRowGroupMapping[state]; - } - - StateType const& getUnexploredMarker() const { - return unexploredMarker; - } - - bool isUnexplored(StateType const& state) const { - return stateToRowGroupMapping[state] == unexploredMarker; - } - - bool isTerminal(StateType const& state) const { - return terminalStates.find(state) != terminalStates.end(); - } - - ActionType const& getStartRowOfGroup(StateType const& group) const { - return rowGroupIndices[group]; - } - - std::size_t getRowGroupSize(StateType const& group) const { - return rowGroupIndices[group + 1] - rowGroupIndices[group]; - } - - bool onlyOneActionAvailable(StateType const& group) const { - return getRowGroupSize(group) == 1; - } - - void addTerminalState(StateType const& state) { - terminalStates.insert(state); - } - - std::vector>& getRowOfMatrix(ActionType const& row) { - return matrix[row]; - } - - std::vector> const& getRowOfMatrix(ActionType const& row) const { - return matrix[row]; - } - - void addRowsToMatrix(std::size_t const& count) { - matrix.resize(matrix.size() + count); - } - - bool maximize() const { - return optimizationDirection == storm::OptimizationDirection::Maximize; - } - - bool minimize() const { - return !maximize(); - } - - bool performPrecomputationExcessiveExplorationSteps(std::size_t& numberExplorationStepsSinceLastPrecomputation) const { - bool result = numberExplorationStepsSinceLastPrecomputation > numberOfExplorationStepsUntilPrecomputation; - if (result) { - numberExplorationStepsSinceLastPrecomputation = 0; - } - return result; - } - - bool performPrecomputationExcessiveSampledPaths(std::size_t& numberOfSampledPathsSinceLastPrecomputation) const { - if (!numberOfSampledPathsUntilPrecomputation) { - return false; - } else { - bool result = numberOfSampledPathsSinceLastPrecomputation > numberOfSampledPathsUntilPrecomputation.get(); - if (result) { - numberOfSampledPathsSinceLastPrecomputation = 0; - } - return result; - } - } - - bool useLocalPrecomputation() const { - return localPrecomputation; - } - - bool useGlobalPrecomputation() const { - return !useLocalPrecomputation(); - } - - storm::settings::modules::ExplorationSettings::NextStateHeuristic const& getNextStateHeuristic() const { - return nextStateHeuristic; - } - - bool useDifferenceWeightedProbabilityHeuristic() const { - return nextStateHeuristic == storm::settings::modules::ExplorationSettings::NextStateHeuristic::DifferenceWeightedProbability; - } - - bool useProbabilityHeuristic() const { - return nextStateHeuristic == storm::settings::modules::ExplorationSettings::NextStateHeuristic::Probability; - } - }; - - // A struct that keeps track of certain statistics during the computation. - struct Statistics { - Statistics() : pathsSampled(0), pathsSampledSinceLastPrecomputation(0), explorationSteps(0), explorationStepsSinceLastPrecomputation(0), maxPathLength(0), numberOfTargetStates(0), numberOfExploredStates(0), numberOfPrecomputations(0), ecDetections(0), failedEcDetections(0), totalNumberOfEcDetected(0) { - // Intentionally left empty. - } - - void explorationStep() { - ++explorationSteps; - ++explorationStepsSinceLastPrecomputation; - } - - void sampledPath() { - ++pathsSampled; - ++pathsSampledSinceLastPrecomputation; - } - - void updateMaxPathLength(std::size_t const& currentPathLength) { - maxPathLength = std::max(maxPathLength, currentPathLength); - } - - std::size_t pathsSampled; - std::size_t pathsSampledSinceLastPrecomputation; - std::size_t explorationSteps; - std::size_t explorationStepsSinceLastPrecomputation; - std::size_t maxPathLength; - std::size_t numberOfTargetStates; - std::size_t numberOfExploredStates; - std::size_t numberOfPrecomputations; - std::size_t ecDetections; - std::size_t failedEcDetections; - std::size_t totalNumberOfEcDetected; - - void printToStream(std::ostream& out, ExplorationInformation const& explorationInformation) const { - out << std::endl << "Exploration statistics:" << std::endl; - out << "Discovered states: " << explorationInformation.getNumberOfDiscoveredStates() << " (" << numberOfExploredStates << " explored, " << explorationInformation.getNumberOfUnexploredStates() << " unexplored, " << numberOfTargetStates << " target)" << std::endl; - out << "Exploration steps: " << explorationSteps << std::endl; - out << "Sampled paths: " << pathsSampled << std::endl; - out << "Maximal path length: " << maxPathLength << std::endl; - out << "Precomputations: " << numberOfPrecomputations << std::endl; - out << "EC detections: " << ecDetections << " (" << failedEcDetections << " failed, " << totalNumberOfEcDetected << " EC(s) detected)" << std::endl; - } - }; - - // A struct containing the data required for state exploration. - struct StateGeneration { - StateGeneration(storm::prism::Program const& program, storm::generator::VariableInformation const& variableInformation, storm::expressions::Expression const& conditionStateExpression, storm::expressions::Expression const& targetStateExpression) : generator(program, variableInformation, false), conditionStateExpression(conditionStateExpression), targetStateExpression(targetStateExpression) { - // Intentionally left empty. - } - - void load(storm::generator::CompressedState const& state) { - generator.load(state); - } - - std::vector getInitialStates() { - return generator.getInitialStates(stateToIdCallback); - } - - storm::generator::StateBehavior expand() { - return generator.expand(stateToIdCallback); - } - - bool isConditionState() const { - return generator.satisfies(conditionStateExpression); - } - - bool isTargetState() const { - return generator.satisfies(targetStateExpression); - } - - storm::generator::PrismNextStateGenerator generator; - std::function stateToIdCallback; - storm::expressions::Expression conditionStateExpression; - storm::expressions::Expression targetStateExpression; - }; - - std::function createStateToIdCallback(ExplorationInformation& explorationInformation) const; + std::function createStateToIdCallback(ExplorationInformation& explorationInformation) const; - std::tuple performExploration(StateGeneration& stateGeneration, ExplorationInformation& explorationInformation) const; + std::tuple performExploration(StateGeneration& stateGeneration, ExplorationInformation& explorationInformation) const; - bool samplePathFromInitialState(StateGeneration& stateGeneration, ExplorationInformation& explorationInformation, StateActionStack& stack, BoundValues& bounds, Statistics& stats) const; + bool samplePathFromInitialState(StateGeneration& stateGeneration, ExplorationInformation& explorationInformation, StateActionStack& stack, Bounds& bounds, Statistics& stats) const; - bool exploreState(StateGeneration& stateGeneration, StateType const& currentStateId, storm::generator::CompressedState const& currentState, ExplorationInformation& explorationInformation, BoundValues& bounds, Statistics& stats) const; + bool exploreState(StateGeneration& stateGeneration, StateType const& currentStateId, storm::generator::CompressedState const& currentState, ExplorationInformation& explorationInformation, Bounds& bounds, Statistics& stats) const; - ActionType sampleActionOfState(StateType const& currentStateId, ExplorationInformation const& explorationInformation, BoundValues& bounds) const; + ActionType sampleActionOfState(StateType const& currentStateId, ExplorationInformation const& explorationInformation, Bounds& bounds) const; - StateType sampleSuccessorFromAction(ActionType const& chosenAction, ExplorationInformation const& explorationInformation, BoundValues const& bounds) const; + StateType sampleSuccessorFromAction(ActionType const& chosenAction, ExplorationInformation const& explorationInformation, Bounds const& bounds) const; - bool performPrecomputation(StateActionStack const& stack, ExplorationInformation& explorationInformation, BoundValues& bounds, Statistics& stats) const; + bool performPrecomputation(StateActionStack const& stack, ExplorationInformation& explorationInformation, Bounds& bounds, Statistics& stats) const; - void collapseMec(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, Bounds& bounds) const; - void updateProbabilityBoundsAlongSampledPath(StateActionStack& stack, ExplorationInformation const& explorationInformation, BoundValues& bounds) const; + void updateProbabilityBoundsAlongSampledPath(StateActionStack& stack, ExplorationInformation const& explorationInformation, Bounds& bounds) const; - void updateProbabilityOfAction(StateType const& state, ActionType const& action, ExplorationInformation const& explorationInformation, BoundValues& bounds) const; + void updateProbabilityOfAction(StateType const& state, ActionType const& action, ExplorationInformation const& explorationInformation, Bounds& bounds) const; - std::pair computeBoundsOfAction(ActionType const& action, ExplorationInformation const& explorationInformation, BoundValues const& bounds) const; - ValueType computeBoundOverAllOtherActions(storm::OptimizationDirection const& direction, StateType const& state, ActionType const& action, ExplorationInformation const& explorationInformation, BoundValues const& bounds) const; - std::pair computeBoundsOfState(StateType const& currentStateId, ExplorationInformation const& explorationInformation, BoundValues const& bounds) const; - ValueType computeLowerBoundOfAction(ActionType const& action, ExplorationInformation const& explorationInformation, BoundValues const& bounds) const; - ValueType computeUpperBoundOfAction(ActionType const& action, ExplorationInformation const& explorationInformation, BoundValues const& bounds) const; + std::pair computeBoundsOfAction(ActionType const& action, ExplorationInformation const& explorationInformation, Bounds const& bounds) const; + ValueType computeBoundOverAllOtherActions(storm::OptimizationDirection const& direction, StateType const& state, ActionType const& action, ExplorationInformation const& explorationInformation, Bounds const& bounds) const; + std::pair computeBoundsOfState(StateType const& currentStateId, ExplorationInformation const& explorationInformation, Bounds const& bounds) const; + ValueType computeLowerBoundOfAction(ActionType const& action, ExplorationInformation const& explorationInformation, Bounds const& bounds) const; + ValueType computeUpperBoundOfAction(ActionType const& action, ExplorationInformation const& explorationInformation, Bounds const& bounds) const; std::pair getLowestBounds(storm::OptimizationDirection const& direction) const; ValueType getLowestBound(storm::OptimizationDirection const& direction) const; diff --git a/src/modelchecker/exploration/StateGeneration.cpp b/src/modelchecker/exploration/StateGeneration.cpp index e69de29bb..ae2343706 100644 --- a/src/modelchecker/exploration/StateGeneration.cpp +++ b/src/modelchecker/exploration/StateGeneration.cpp @@ -0,0 +1,45 @@ +#include "src/modelchecker/exploration/StateGeneration.h" + +namespace storm { + namespace modelchecker { + namespace exploration_detail { + + template + StateGeneration::StateGeneration(storm::prism::Program const& program, storm::generator::VariableInformation const& variableInformation, storm::expressions::Expression const& conditionStateExpression, storm::expressions::Expression const& targetStateExpression) : generator(program, variableInformation, false), conditionStateExpression(conditionStateExpression), targetStateExpression(targetStateExpression) { + // Intentionally left empty. + } + + template + void StateGeneration::setStateToIdCallback(std::function const& stateToIdCallback) { + this->stateToIdCallback = stateToIdCallback; + } + + template + void StateGeneration::load(storm::generator::CompressedState const& state) { + generator.load(state); + } + + template + std::vector StateGeneration::getInitialStates() { + return generator.getInitialStates(stateToIdCallback); + } + + template + storm::generator::StateBehavior StateGeneration::expand() { + return generator.expand(stateToIdCallback); + } + + template + bool StateGeneration::isConditionState() const { + return generator.satisfies(conditionStateExpression); + } + + template + bool StateGeneration::isTargetState() const { + return generator.satisfies(targetStateExpression); + } + + template class StateGeneration; + } + } +} \ No newline at end of file diff --git a/src/modelchecker/exploration/StateGeneration.h b/src/modelchecker/exploration/StateGeneration.h index e69de29bb..a10ff2883 100644 --- a/src/modelchecker/exploration/StateGeneration.h +++ b/src/modelchecker/exploration/StateGeneration.h @@ -0,0 +1,44 @@ +#ifndef STORM_MODELCHECKER_EXPLORATION_EXPLORATION_DETAIL_STATEGENERATION_H_ +#define STORM_MODELCHECKER_EXPLORATION_EXPLORATION_DETAIL_STATEGENERATION_H_ + +#include "src/generator/CompressedState.h" +#include "src/generator/PrismNextStateGenerator.h" + +namespace storm { + namespace generator { + template + class PrismNextStateGenerator; + } + + namespace modelchecker { + namespace exploration_detail { + + template + class StateGeneration { + public: + StateGeneration(storm::prism::Program const& program, storm::generator::VariableInformation const& variableInformation, storm::expressions::Expression const& conditionStateExpression, storm::expressions::Expression const& targetStateExpression); + + void setStateToIdCallback(std::function const& stateToIdCallback); + + void load(storm::generator::CompressedState const& state); + + std::vector getInitialStates(); + + storm::generator::StateBehavior expand(); + + bool isConditionState() const; + + bool isTargetState() const; + + private: + storm::generator::PrismNextStateGenerator generator; + std::function stateToIdCallback; + storm::expressions::Expression conditionStateExpression; + storm::expressions::Expression targetStateExpression; + }; + + } + } +} + +#endif /* STORM_MODELCHECKER_EXPLORATION_EXPLORATION_DETAIL_STATEGENERATION_H_ */ \ No newline at end of file diff --git a/src/modelchecker/exploration/Statistics.cpp b/src/modelchecker/exploration/Statistics.cpp new file mode 100644 index 000000000..d74a62815 --- /dev/null +++ b/src/modelchecker/exploration/Statistics.cpp @@ -0,0 +1,46 @@ +#include "src/modelchecker/exploration/Statistics.h" + +#include "src/modelchecker/exploration/ExplorationInformation.h" + +namespace storm { + namespace modelchecker { + namespace exploration_detail { + + template + Statistics::Statistics() : pathsSampled(0), pathsSampledSinceLastPrecomputation(0), explorationSteps(0), explorationStepsSinceLastPrecomputation(0), maxPathLength(0), numberOfTargetStates(0), numberOfExploredStates(0), numberOfPrecomputations(0), ecDetections(0), failedEcDetections(0), totalNumberOfEcDetected(0) { + // Intentionally left empty. + } + + template + void Statistics::explorationStep() { + ++explorationSteps; + ++explorationStepsSinceLastPrecomputation; + } + + template + void Statistics::sampledPath() { + ++pathsSampled; + ++pathsSampledSinceLastPrecomputation; + } + + template + void Statistics::updateMaxPathLength(std::size_t const& currentPathLength) { + maxPathLength = std::max(maxPathLength, currentPathLength); + } + + template + void Statistics::printToStream(std::ostream& out, ExplorationInformation const& explorationInformation) const { + out << std::endl << "Exploration statistics:" << std::endl; + out << "Discovered states: " << explorationInformation.getNumberOfDiscoveredStates() << " (" << numberOfExploredStates << " explored, " << explorationInformation.getNumberOfUnexploredStates() << " unexplored, " << numberOfTargetStates << " target)" << std::endl; + out << "Exploration steps: " << explorationSteps << std::endl; + out << "Sampled paths: " << pathsSampled << std::endl; + out << "Maximal path length: " << maxPathLength << std::endl; + out << "Precomputations: " << numberOfPrecomputations << std::endl; + out << "EC detections: " << ecDetections << " (" << failedEcDetections << " failed, " << totalNumberOfEcDetected << " EC(s) detected)" << std::endl; + } + + template class Statistics; + + } + } +} diff --git a/src/modelchecker/exploration/Statistics.h b/src/modelchecker/exploration/Statistics.h new file mode 100644 index 000000000..2d6b9d89f --- /dev/null +++ b/src/modelchecker/exploration/Statistics.h @@ -0,0 +1,44 @@ +#ifndef STORM_MODELCHECKER_EXPLORATION_EXPLORATION_DETAIL_STATISTICS_H_ +#define STORM_MODELCHECKER_EXPLORATION_EXPLORATION_DETAIL_STATISTICS_H_ + +#include +#include + +namespace storm { + namespace modelchecker { + namespace exploration_detail { + + template + class ExplorationInformation; + + // A struct that keeps track of certain statistics during the exploration. + template + struct Statistics { + Statistics(); + + void explorationStep(); + + void sampledPath(); + + void updateMaxPathLength(std::size_t const& currentPathLength); + + void printToStream(std::ostream& out, ExplorationInformation const& explorationInformation) const; + + std::size_t pathsSampled; + std::size_t pathsSampledSinceLastPrecomputation; + std::size_t explorationSteps; + std::size_t explorationStepsSinceLastPrecomputation; + std::size_t maxPathLength; + std::size_t numberOfTargetStates; + std::size_t numberOfExploredStates; + std::size_t numberOfPrecomputations; + std::size_t ecDetections; + std::size_t failedEcDetections; + std::size_t totalNumberOfEcDetected; + }; + + } + } +} + +#endif /* STORM_MODELCHECKER_EXPLORATION_EXPLORATION_DETAIL_STATISTICS_H_ */ \ No newline at end of file