sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

further refactoring of exploration (better name than 'learning') based engine 

Former-commit-id: 72622d821d
tempestpy_adaptions
dehnert 9 years ago
parent
1424d536ca
commit
f9193325d4
12 changed files with 810 additions and 455 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 0
      src/modelchecker/exploration/BoundValues.cpp
  2. 137
      src/modelchecker/exploration/BoundValues.h
  3. 155
      src/modelchecker/exploration/Bounds.cpp
  4. 76
      src/modelchecker/exploration/Bounds.h
  5. 209
      src/modelchecker/exploration/ExplorationInformation.cpp
  6. 120
      src/modelchecker/exploration/ExplorationInformation.h
  7. 81
      src/modelchecker/exploration/SparseMdpExplorationModelChecker.cpp
  8. 308
      src/modelchecker/exploration/SparseMdpExplorationModelChecker.h
  9. 45
      src/modelchecker/exploration/StateGeneration.cpp
  10. 44
      src/modelchecker/exploration/StateGeneration.h
  11. 46
      src/modelchecker/exploration/Statistics.cpp
  12. 44
      src/modelchecker/exploration/Statistics.h

0
src/modelchecker/exploration/BoundValues.cpp
View File

137
src/modelchecker/exploration/BoundValues.h
View File

@ -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<ValueType> lowerBoundsPerState;
std::vector<ValueType> upperBoundsPerState;
std::vector<ValueType> lowerBoundsPerAction;
std::vector<ValueType> upperBoundsPerAction;
std::pair<ValueType, ValueType> getBoundsForState(StateType const& state, ExplorationInformation const& explorationInformation) const {
ActionType index = explorationInformation.getRowGroup(state);
if (index == explorationInformation.getUnexploredMarker()) {
return std::make_pair(storm::utility::zero<ValueType>(), storm::utility::one<ValueType>());
} 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<ValueType>();
} 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<ValueType>();
} else {
return getUpperBoundForRowGroup(index);
}
}
ValueType const& getUpperBoundForRowGroup(StateType const& rowGroup) const {
return upperBoundsPerState[rowGroup];
}
std::pair<ValueType, ValueType> 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<ValueType, ValueType> bounds = getBoundsForState(state, explorationInformation);
return bounds.second - bounds.first;
}
void initializeBoundsForNextState(std::pair<ValueType, ValueType> const& vals = std::pair<ValueType, ValueType>(storm::utility::zero<ValueType>(), storm::utility::one<ValueType>())) {
lowerBoundsPerState.push_back(vals.first);
upperBoundsPerState.push_back(vals.second);
}
void initializeBoundsForNextAction(std::pair<ValueType, ValueType> const& vals = std::pair<ValueType, ValueType>(storm::utility::zero<ValueType>(), storm::utility::one<ValueType>())) {
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<ValueType, ValueType> const& values) {
lowerBoundsPerAction[action] = values.first;
upperBoundsPerAction[action] = values.second;
}
void setBoundsForState(StateType const& state, ExplorationInformation const& explorationInformation, std::pair<ValueType, ValueType> const& values) {
StateType const& rowGroup = explorationInformation.getRowGroup(state);
setBoundsForRowGroup(rowGroup, values);
}
void setBoundsForRowGroup(StateType const& rowGroup, std::pair<ValueType, ValueType> const& values) {
lowerBoundsPerState[rowGroup] = values.first;
upperBoundsPerState[rowGroup] = values.second;
}
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;
}
};
}
}
}

155
src/modelchecker/exploration/Bounds.cpp
View File

@ -0,0 +1,155 @@
#include "src/modelchecker/exploration/Bounds.h"
#include "src/modelchecker/exploration/ExplorationInformation.h"
namespace storm {
namespace modelchecker {
namespace exploration_detail {
template<typename StateType, typename ValueType>
std::pair<ValueType, ValueType> Bounds<StateType, ValueType>::getBoundsForState(StateType const& state, ExplorationInformation<StateType, ValueType> const& explorationInformation) const {
ActionType index = explorationInformation.getRowGroup(state);
if (index == explorationInformation.getUnexploredMarker()) {
return std::make_pair(storm::utility::zero<ValueType>(), storm::utility::one<ValueType>());
} else {
return boundsPerState[index];
}
}
template<typename StateType, typename ValueType>
std::pair<ValueType, ValueType> const& Bounds<StateType, ValueType>::getBoundsForExploredState(StateType const& state, ExplorationInformation<StateType, ValueType> const& explorationInformation) const {
ActionType index = explorationInformation.getRowGroup(state);
return boundsPerState[index];
}
template<typename StateType, typename ValueType>
ValueType Bounds<StateType, ValueType>::getLowerBoundForState(StateType const& state, ExplorationInformation<StateType, ValueType> const& explorationInformation) const {
ActionType index = explorationInformation.getRowGroup(state);
if (index == explorationInformation.getUnexploredMarker()) {
return storm::utility::zero<ValueType>();
} else {
return getLowerBoundForRowGroup(index);
}
}
template<typename StateType, typename ValueType>
ValueType const& Bounds<StateType, ValueType>::getLowerBoundForRowGroup(StateType const& rowGroup) const {
return boundsPerState[rowGroup].first;
}
template<typename StateType, typename ValueType>
ValueType Bounds<StateType, ValueType>::getUpperBoundForState(StateType const& state, ExplorationInformation<StateType, ValueType> const& explorationInformation) const {
ActionType index = explorationInformation.getRowGroup(state);
if (index == explorationInformation.getUnexploredMarker()) {
return storm::utility::one<ValueType>();
} else {
return getUpperBoundForRowGroup(index);
}
}
template<typename StateType, typename ValueType>
ValueType const& Bounds<StateType, ValueType>::getUpperBoundForRowGroup(StateType const& rowGroup) const {
return boundsPerState[rowGroup].second;
}
template<typename StateType, typename ValueType>
std::pair<ValueType, ValueType> const& Bounds<StateType, ValueType>::getBoundsForAction(ActionType const& action) const {
return boundsPerAction[action];
}
template<typename StateType, typename ValueType>
ValueType const& Bounds<StateType, ValueType>::getLowerBoundForAction(ActionType const& action) const {
return boundsPerAction[action].first;
}
template<typename StateType, typename ValueType>
ValueType const& Bounds<StateType, ValueType>::getUpperBoundForAction(ActionType const& action) const {
return boundsPerAction[action].second;
}
template<typename StateType, typename ValueType>
ValueType const& Bounds<StateType, ValueType>::getBoundForAction(storm::OptimizationDirection const& direction, ActionType const& action) const {
if (direction == storm::OptimizationDirection::Maximize) {
return getUpperBoundForAction(action);
} else {
return getLowerBoundForAction(action);
}
}
template<typename StateType, typename ValueType>
ValueType Bounds<StateType, ValueType>::getDifferenceOfStateBounds(StateType const& state, ExplorationInformation<StateType, ValueType> const& explorationInformation) const {
std::pair<ValueType, ValueType> const& bounds = getBoundsForExploredState(state, explorationInformation);
return bounds.second - bounds.first;
}
template<typename StateType, typename ValueType>
void Bounds<StateType, ValueType>::initializeBoundsForNextState(std::pair<ValueType, ValueType> const& vals) {
boundsPerState.push_back(vals);
}
template<typename StateType, typename ValueType>
void Bounds<StateType, ValueType>::initializeBoundsForNextAction(std::pair<ValueType, ValueType> const& vals) {
boundsPerAction.push_back(vals);
}
template<typename StateType, typename ValueType>
void Bounds<StateType, ValueType>::setLowerBoundForState(StateType const& state, ExplorationInformation<StateType, ValueType> const& explorationInformation, ValueType const& value) {
setLowerBoundForRowGroup(explorationInformation.getRowGroup(state), value);
}
template<typename StateType, typename ValueType>
void Bounds<StateType, ValueType>::setLowerBoundForRowGroup(StateType const& group, ValueType const& value) {
boundsPerState[group].first = value;
}
template<typename StateType, typename ValueType>
void Bounds<StateType, ValueType>::setUpperBoundForState(StateType const& state, ExplorationInformation<StateType, ValueType> const& explorationInformation, ValueType const& value) {
setUpperBoundForRowGroup(explorationInformation.getRowGroup(state), value);
}
template<typename StateType, typename ValueType>
void Bounds<StateType, ValueType>::setUpperBoundForRowGroup(StateType const& group, ValueType const& value) {
boundsPerState[group].second = value;
}
template<typename StateType, typename ValueType>
void Bounds<StateType, ValueType>::setBoundsForAction(ActionType const& action, std::pair<ValueType, ValueType> const& values) {
boundsPerAction[action] = values;
}
template<typename StateType, typename ValueType>
void Bounds<StateType, ValueType>::setBoundsForState(StateType const& state, ExplorationInformation<StateType, ValueType> const& explorationInformation, std::pair<ValueType, ValueType> const& values) {
StateType const& rowGroup = explorationInformation.getRowGroup(state);
setBoundsForRowGroup(rowGroup, values);
}
template<typename StateType, typename ValueType>
void Bounds<StateType, ValueType>::setBoundsForRowGroup(StateType const& rowGroup, std::pair<ValueType, ValueType> const& values) {
boundsPerState[rowGroup] = values;
}
template<typename StateType, typename ValueType>
bool Bounds<StateType, ValueType>::setLowerBoundOfStateIfGreaterThanOld(StateType const& state, ExplorationInformation<StateType, ValueType> 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<typename StateType, typename ValueType>
bool Bounds<StateType, ValueType>::setUpperBoundOfStateIfLessThanOld(StateType const& state, ExplorationInformation<StateType, ValueType> 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<uint32_t, double>;
}
}
}

76
src/modelchecker/exploration/Bounds.h
View File

@ -0,0 +1,76 @@
#ifndef STORM_MODELCHECKER_EXPLORATION_EXPLORATION_DETAIL_BOUNDS_H_
#define STORM_MODELCHECKER_EXPLORATION_EXPLORATION_DETAIL_BOUNDS_H_
#include <vector>
#include <utility>
#include "src/solver/OptimizationDirection.h"
#include "src/utility/constants.h"
namespace storm {
namespace modelchecker {
namespace exploration_detail {
template<typename StateType, typename ValueType>
class ExplorationInformation;
template<typename StateType, typename ValueType>
class Bounds {
public:
typedef StateType ActionType;
std::pair<ValueType, ValueType> getBoundsForState(StateType const& state, ExplorationInformation<StateType, ValueType> const& explorationInformation) const;
std::pair<ValueType, ValueType> const& getBoundsForExploredState(StateType const& state, ExplorationInformation<StateType, ValueType> const& explorationInformation) const;
ValueType getLowerBoundForState(StateType const& state, ExplorationInformation<StateType, ValueType> const& explorationInformation) const;
ValueType const& getLowerBoundForRowGroup(StateType const& rowGroup) const;
ValueType getUpperBoundForState(StateType const& state, ExplorationInformation<StateType, ValueType> const& explorationInformation) const;
ValueType const& getUpperBoundForRowGroup(StateType const& rowGroup) const;
std::pair<ValueType, ValueType> 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<StateType, ValueType> const& explorationInformation) const;
void initializeBoundsForNextState(std::pair<ValueType, ValueType> const& vals = std::pair<ValueType, ValueType>(storm::utility::zero<ValueType>(), storm::utility::one<ValueType>()));
void initializeBoundsForNextAction(std::pair<ValueType, ValueType> const& vals = std::pair<ValueType, ValueType>(storm::utility::zero<ValueType>(), storm::utility::one<ValueType>()));
void setLowerBoundForState(StateType const& state, ExplorationInformation<StateType, ValueType> const& explorationInformation, ValueType const& value);
void setLowerBoundForRowGroup(StateType const& group, ValueType const& value);
void setUpperBoundForState(StateType const& state, ExplorationInformation<StateType, ValueType> const& explorationInformation, ValueType const& value);
void setUpperBoundForRowGroup(StateType const& group, ValueType const& value);
void setBoundsForAction(ActionType const& action, std::pair<ValueType, ValueType> const& values);
void setBoundsForState(StateType const& state, ExplorationInformation<StateType, ValueType> const& explorationInformation, std::pair<ValueType, ValueType> const& values);
void setBoundsForRowGroup(StateType const& rowGroup, std::pair<ValueType, ValueType> const& values);
bool setLowerBoundOfStateIfGreaterThanOld(StateType const& state, ExplorationInformation<StateType, ValueType> const& explorationInformation, ValueType const& newLowerValue);
bool setUpperBoundOfStateIfLessThanOld(StateType const& state, ExplorationInformation<StateType, ValueType> const& explorationInformation, ValueType const& newUpperValue);
private:
std::vector<std::pair<ValueType, ValueType>> boundsPerState;
std::vector<std::pair<ValueType, ValueType>> boundsPerAction;
};
}
}
}
#endif /* STORM_MODELCHECKER_EXPLORATION_EXPLORATION_DETAIL_BOUNDS_H_ */

209
src/modelchecker/exploration/ExplorationInformation.cpp
View File

@ -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<typename StateType, typename ValueType>
ExplorationInformation<StateType, ValueType>::ExplorationInformation(uint_fast64_t bitsPerBucket, storm::OptimizationDirection const& direction, ActionType const& unexploredMarker) : stateStorage(bitsPerBucket), unexploredMarker(unexploredMarker), optimizationDirection(direction), localPrecomputation(false), numberOfExplorationStepsUntilPrecomputation(100000), numberOfSampledPathsUntilPrecomputation(), nextStateHeuristic(storm::settings::modules::ExplorationSettings::NextStateHeuristic::DifferenceWeightedProbability) {
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<typename StateType, typename ValueType>
void ExplorationInformation<StateType, ValueType>::setInitialStates(std::vector<StateType> const& initialStates) {
stateStorage.initialStateIndices = initialStates;
}
template<typename StateType, typename ValueType>
StateType ExplorationInformation<StateType, ValueType>::getFirstInitialState() const {
return stateStorage.initialStateIndices.front();
}
template<typename StateType, typename ValueType>
std::size_t ExplorationInformation<StateType, ValueType>::getNumberOfInitialStates() const {
return stateStorage.initialStateIndices.size();
}
template<typename StateType, typename ValueType>
void ExplorationInformation<StateType, ValueType>::addUnexploredState(storm::generator::CompressedState const& compressedState) {
stateToRowGroupMapping.push_back(unexploredMarker);
unexploredStates[stateStorage.numberOfStates] = compressedState;
++stateStorage.numberOfStates;
}
template<typename StateType, typename ValueType>
void ExplorationInformation<StateType, ValueType>::assignStateToRowGroup(StateType const& state, ActionType const& rowGroup) {
stateToRowGroupMapping[state] = rowGroup;
}
template<typename StateType, typename ValueType>
StateType ExplorationInformation<StateType, ValueType>::assignStateToNextRowGroup(StateType const& state) {
stateToRowGroupMapping[state] = rowGroupIndices.size() - 1;
return stateToRowGroupMapping[state];
}
template<typename StateType, typename ValueType>
StateType ExplorationInformation<StateType, ValueType>::getNextRowGroup() const {
return rowGroupIndices.size() - 1;
}
template<typename StateType, typename ValueType>
void ExplorationInformation<StateType, ValueType>::newRowGroup(ActionType const& action) {
rowGroupIndices.push_back(action);
}
template<typename StateType, typename ValueType>
void ExplorationInformation<StateType, ValueType>::newRowGroup() {
newRowGroup(matrix.size());
}
template<typename StateType, typename ValueType>
std::size_t ExplorationInformation<StateType, ValueType>::getNumberOfUnexploredStates() const {
return unexploredStates.size();
}
template<typename StateType, typename ValueType>
std::size_t ExplorationInformation<StateType, ValueType>::getNumberOfDiscoveredStates() const {
return stateStorage.numberOfStates;
}
template<typename StateType, typename ValueType>
StateType const& ExplorationInformation<StateType, ValueType>::getRowGroup(StateType const& state) const {
return stateToRowGroupMapping[state];
}
template<typename StateType, typename ValueType>
StateType const& ExplorationInformation<StateType, ValueType>::getUnexploredMarker() const {
return unexploredMarker;
}
template<typename StateType, typename ValueType>
bool ExplorationInformation<StateType, ValueType>::isUnexplored(StateType const& state) const {
return stateToRowGroupMapping[state] == unexploredMarker;
}
template<typename StateType, typename ValueType>
bool ExplorationInformation<StateType, ValueType>::isTerminal(StateType const& state) const {
return terminalStates.find(state) != terminalStates.end();
}
template<typename StateType, typename ValueType>
typename ExplorationInformation<StateType, ValueType>::ActionType const& ExplorationInformation<StateType, ValueType>::getStartRowOfGroup(StateType const& group) const {
return rowGroupIndices[group];
}
template<typename StateType, typename ValueType>
std::size_t ExplorationInformation<StateType, ValueType>::getRowGroupSize(StateType const& group) const {
return rowGroupIndices[group + 1] - rowGroupIndices[group];
}
template<typename StateType, typename ValueType>
bool ExplorationInformation<StateType, ValueType>::onlyOneActionAvailable(StateType const& group) const {
return getRowGroupSize(group) == 1;
}
template<typename StateType, typename ValueType>
void ExplorationInformation<StateType, ValueType>::addTerminalState(StateType const& state) {
terminalStates.insert(state);
}
template<typename StateType, typename ValueType>
std::vector<storm::storage::MatrixEntry<StateType, ValueType>>& ExplorationInformation<StateType, ValueType>::getRowOfMatrix(ActionType const& row) {
return matrix[row];
}
template<typename StateType, typename ValueType>
std::vector<storm::storage::MatrixEntry<StateType, ValueType>> const& ExplorationInformation<StateType, ValueType>::getRowOfMatrix(ActionType const& row) const {
return matrix[row];
}
template<typename StateType, typename ValueType>
void ExplorationInformation<StateType, ValueType>::addRowsToMatrix(std::size_t const& count) {
matrix.resize(matrix.size() + count);
}
template<typename StateType, typename ValueType>
bool ExplorationInformation<StateType, ValueType>::maximize() const {
return optimizationDirection == storm::OptimizationDirection::Maximize;
}
template<typename StateType, typename ValueType>
bool ExplorationInformation<StateType, ValueType>::minimize() const {
return !maximize();
}
template<typename StateType, typename ValueType>
bool ExplorationInformation<StateType, ValueType>::performPrecomputationExcessiveExplorationSteps(std::size_t& numberExplorationStepsSinceLastPrecomputation) const {
bool result = numberExplorationStepsSinceLastPrecomputation > numberOfExplorationStepsUntilPrecomputation;
if (result) {
numberExplorationStepsSinceLastPrecomputation = 0;
}
return result;
}
template<typename StateType, typename ValueType>
bool ExplorationInformation<StateType, ValueType>::performPrecomputationExcessiveSampledPaths(std::size_t& numberOfSampledPathsSinceLastPrecomputation) const {
if (!numberOfSampledPathsUntilPrecomputation) {
return false;
} else {
bool result = numberOfSampledPathsSinceLastPrecomputation > numberOfSampledPathsUntilPrecomputation.get();
if (result) {
numberOfSampledPathsSinceLastPrecomputation = 0;
}
return result;
}
}
template<typename StateType, typename ValueType>
bool ExplorationInformation<StateType, ValueType>::useLocalPrecomputation() const {
return localPrecomputation;
}
template<typename StateType, typename ValueType>
bool ExplorationInformation<StateType, ValueType>::useGlobalPrecomputation() const {
return !useLocalPrecomputation();
}
template<typename StateType, typename ValueType>
storm::settings::modules::ExplorationSettings::NextStateHeuristic const& ExplorationInformation<StateType, ValueType>::getNextStateHeuristic() const {
return nextStateHeuristic;
}
template<typename StateType, typename ValueType>
bool ExplorationInformation<StateType, ValueType>::useDifferenceWeightedProbabilityHeuristic() const {
return nextStateHeuristic == storm::settings::modules::ExplorationSettings::NextStateHeuristic::DifferenceWeightedProbability;
}
template<typename StateType, typename ValueType>
bool ExplorationInformation<StateType, ValueType>::useProbabilityHeuristic() const {
return nextStateHeuristic == storm::settings::modules::ExplorationSettings::NextStateHeuristic::Probability;
}
template<typename StateType, typename ValueType>
storm::OptimizationDirection const& ExplorationInformation<StateType, ValueType>::getOptimizationDirection() const {
return optimizationDirection;
}
template<typename StateType, typename ValueType>
void ExplorationInformation<StateType, ValueType>::setOptimizationDirection(storm::OptimizationDirection const& direction) {
optimizationDirection = direction;
}
template class ExplorationInformation<uint32_t, double>;
}
}
}

120
src/modelchecker/exploration/ExplorationInformation.h
View File

@ -0,0 +1,120 @@
#ifndef STORM_MODELCHECKER_EXPLORATION_EXPLORATION_DETAIL_EXPLORATIONINFORMATION_H_
#define STORM_MODELCHECKER_EXPLORATION_EXPLORATION_DETAIL_EXPLORATIONINFORMATION_H_
#include <vector>
#include <limits>
#include <unordered_map>
#include <boost/optional.hpp>
#include <boost/container/flat_set.hpp>
#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<typename StateType, typename ValueType>
class ExplorationInformation {
public:
typedef StateType ActionType;
typedef boost::container::flat_set<StateType> StateSet;
ExplorationInformation(uint_fast64_t bitsPerBucket, storm::OptimizationDirection const& direction, ActionType const& unexploredMarker = std::numeric_limits<ActionType>::max());
void setInitialStates(std::vector<StateType> 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<storm::storage::MatrixEntry<StateType, ValueType>>& getRowOfMatrix(ActionType const& row);
std::vector<storm::storage::MatrixEntry<StateType, ValueType>> 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<StateType> stateStorage;
std::vector<std::vector<storm::storage::MatrixEntry<StateType, ValueType>>> matrix;
std::vector<StateType> rowGroupIndices;
std::vector<StateType> stateToRowGroupMapping;
StateType unexploredMarker;
std::unordered_map<StateType, storm::generator::CompressedState> unexploredStates;
storm::OptimizationDirection optimizationDirection;
StateSet terminalStates;
bool localPrecomputation;
std::size_t numberOfExplorationStepsUntilPrecomputation;
boost::optional<std::size_t> numberOfSampledPathsUntilPrecomputation;
storm::settings::modules::ExplorationSettings::NextStateHeuristic nextStateHeuristic;
};
}
}
}
#endif /* STORM_MODELCHECKER_EXPLORATION_EXPLORATION_DETAIL_EXPLORATIONINFORMATION_H_ */

81
src/modelchecker/exploration/SparseMdpExplorationModelChecker.cpp
View File

@ -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<std::string, storm::expressions::Expression> labelToExpressionMapping = program.getLabelToExpressionMapping();
StateGeneration stateGeneration(program, variableInformation, conditionFormula.toExpression(program.getManager(), labelToExpressionMapping), targetFormula.toExpression(program.getManager(), labelToExpressionMapping));
StateGeneration<StateType, ValueType> 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<StateType, ValueType> 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<StateType, ValueType, ValueType> boundsForInitialState = performExploration(stateGeneration, explorationInformation);
@ -60,9 +69,9 @@ namespace storm {
}
template<typename ValueType>
std::function<typename SparseMdpExplorationModelChecker<ValueType>::StateType (storm::generator::CompressedState const&)> SparseMdpExplorationModelChecker<ValueType>::createStateToIdCallback(ExplorationInformation& explorationInformation) const {
std::function<typename SparseMdpExplorationModelChecker<ValueType>::StateType (storm::generator::CompressedState const&)> SparseMdpExplorationModelChecker<ValueType>::createStateToIdCallback(ExplorationInformation<StateType, ValueType>& explorationInformation) const {
return [&explorationInformation,this] (storm::generator::CompressedState const& state) -> StateType {
StateType newIndex = explorationInformation.stateStorage.numberOfStates;
StateType newIndex = explorationInformation.getNumberOfDiscoveredStates();
// Check, if the state was already registered.
std::pair<uint32_t, std::size_t> actualIndexBucketPair = explorationInformation.stateStorage.stateToId.findOrAddAndGetBucket(state, newIndex);
@ -76,7 +85,7 @@ namespace storm {
}
template<typename ValueType>
std::tuple<typename SparseMdpExplorationModelChecker<ValueType>::StateType, ValueType, ValueType> SparseMdpExplorationModelChecker<ValueType>::performExploration(StateGeneration& stateGeneration, ExplorationInformation& explorationInformation) const {
std::tuple<typename SparseMdpExplorationModelChecker<ValueType>::StateType, ValueType, ValueType> SparseMdpExplorationModelChecker<ValueType>::performExploration(StateGeneration<StateType, ValueType>& stateGeneration, ExplorationInformation<StateType, ValueType>& explorationInformation) const {
// Generate the initial state so we know where to start the simulation.
explorationInformation.setInitialStates(stateGeneration.getInitialStates());
@ -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<StateType, ValueType> bounds;
// Create a stack that is used to track the path we sampled.
StateActionStack stack;
// Now perform the actual sampling.
Statistics stats;
Statistics<StateType, ValueType> stats;
bool convergenceCriterionMet = false;
while (!convergenceCriterionMet) {
bool result = samplePathFromInitialState(stateGeneration, explorationInformation, stack, bounds, stats);
@ -130,7 +139,7 @@ namespace storm {
}
template<typename ValueType>
bool SparseMdpExplorationModelChecker<ValueType>::samplePathFromInitialState(StateGeneration& stateGeneration, ExplorationInformation& explorationInformation, StateActionStack& stack, BoundValues& bounds, Statistics& stats) const {
bool SparseMdpExplorationModelChecker<ValueType>::samplePathFromInitialState(StateGeneration<StateType, ValueType>& stateGeneration, ExplorationInformation<StateType, ValueType>& explorationInformation, StateActionStack& stack, Bounds<StateType, ValueType>& bounds, Statistics<StateType, ValueType>& stats) const {
// Start the search from the initial state.
stack.push_back(std::make_pair(explorationInformation.getFirstInitialState(), 0));
@ -192,7 +201,7 @@ namespace storm {
}
template<typename ValueType>
bool SparseMdpExplorationModelChecker<ValueType>::exploreState(StateGeneration& stateGeneration, StateType const& currentStateId, storm::generator::CompressedState const& currentState, ExplorationInformation& explorationInformation, BoundValues& bounds, Statistics& stats) const {
bool SparseMdpExplorationModelChecker<ValueType>::exploreState(StateGeneration<StateType, ValueType>& stateGeneration, StateType const& currentStateId, storm::generator::CompressedState const& currentState, ExplorationInformation<StateType, ValueType>& explorationInformation, Bounds<StateType, ValueType>& bounds, Statistics<StateType, ValueType>& 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<ValueType, ValueType> stateBounds = getLowestBounds(explorationInformation.optimizationDirection);
std::pair<ValueType, ValueType> stateBounds = getLowestBounds(explorationInformation.getOptimizationDirection());
for (auto const& choice : behavior) {
for (auto const& entry : choice) {
@ -251,7 +260,7 @@ namespace storm {
std::pair<ValueType, ValueType> 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 ValueType>
typename SparseMdpExplorationModelChecker<ValueType>::ActionType SparseMdpExplorationModelChecker<ValueType>::sampleActionOfState(StateType const& currentStateId, ExplorationInformation const& explorationInformation, BoundValues& bounds) const {
typename SparseMdpExplorationModelChecker<ValueType>::ActionType SparseMdpExplorationModelChecker<ValueType>::sampleActionOfState(StateType const& currentStateId, ExplorationInformation<StateType, ValueType> const& explorationInformation, Bounds<StateType, ValueType>& bounds) const {
// Determine the values of all available actions.
std::vector<std::pair<ActionType, ValueType>> 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 ValueType>
typename SparseMdpExplorationModelChecker<ValueType>::StateType SparseMdpExplorationModelChecker<ValueType>::sampleSuccessorFromAction(ActionType const& chosenAction, ExplorationInformation const& explorationInformation, BoundValues const& bounds) const {
typename SparseMdpExplorationModelChecker<ValueType>::StateType SparseMdpExplorationModelChecker<ValueType>::sampleSuccessorFromAction(ActionType const& chosenAction, ExplorationInformation<StateType, ValueType> const& explorationInformation, Bounds<StateType, ValueType> const& bounds) const {
std::vector<storm::storage::MatrixEntry<StateType, ValueType>> const& row = explorationInformation.getRowOfMatrix(chosenAction);
// if (row.size() == 1) {
// return row.front().getColumn();
@ -359,7 +368,7 @@ namespace storm {
}
template<typename ValueType>
bool SparseMdpExplorationModelChecker<ValueType>::performPrecomputation(StateActionStack const& stack, ExplorationInformation& explorationInformation, BoundValues& bounds, Statistics& stats) const {
bool SparseMdpExplorationModelChecker<ValueType>::performPrecomputation(StateActionStack const& stack, ExplorationInformation<StateType, ValueType>& explorationInformation, Bounds<StateType, ValueType>& bounds, Statistics<StateType, ValueType>& 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<typename ValueType>
void SparseMdpExplorationModelChecker<ValueType>::collapseMec(storm::storage::MaximalEndComponent const& mec, std::vector<StateType> const& relevantStates, storm::storage::SparseMatrix<ValueType> const& relevantStatesMatrix, ExplorationInformation& explorationInformation, BoundValues& bounds) const {
void SparseMdpExplorationModelChecker<ValueType>::collapseMec(storm::storage::MaximalEndComponent const& mec, std::vector<StateType> const& relevantStates, storm::storage::SparseMatrix<ValueType> const& relevantStatesMatrix, ExplorationInformation<StateType, ValueType>& explorationInformation, Bounds<StateType, ValueType>& 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<ValueType, ValueType> stateBounds = getLowestBounds(explorationInformation.optimizationDirection);
std::pair<ValueType, ValueType> stateBounds = getLowestBounds(explorationInformation.getOptimizationDirection());
for (auto const& action : leavingActions) {
explorationInformation.matrix.emplace_back(std::move(explorationInformation.matrix[action]));
std::pair<ValueType, ValueType> 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<typename ValueType>
ValueType SparseMdpExplorationModelChecker<ValueType>::computeLowerBoundOfAction(ActionType const& action, ExplorationInformation const& explorationInformation, BoundValues const& bounds) const {
ValueType SparseMdpExplorationModelChecker<ValueType>::computeLowerBoundOfAction(ActionType const& action, ExplorationInformation<StateType, ValueType> const& explorationInformation, Bounds<StateType, ValueType> const& bounds) const {
ValueType result = storm::utility::zero<ValueType>();
for (auto const& element : explorationInformation.getRowOfMatrix(action)) {
result += element.getValue() * bounds.getLowerBoundForState(element.getColumn(), explorationInformation);
@ -571,7 +580,7 @@ namespace storm {
}
template<typename ValueType>
ValueType SparseMdpExplorationModelChecker<ValueType>::computeUpperBoundOfAction(ActionType const& action, ExplorationInformation const& explorationInformation, BoundValues const& bounds) const {
ValueType SparseMdpExplorationModelChecker<ValueType>::computeUpperBoundOfAction(ActionType const& action, ExplorationInformation<StateType, ValueType> const& explorationInformation, Bounds<StateType, ValueType> const& bounds) const {
ValueType result = storm::utility::zero<ValueType>();
for (auto const& element : explorationInformation.getRowOfMatrix(action)) {
result += element.getValue() * bounds.getUpperBoundForState(element.getColumn(), explorationInformation);
@ -580,7 +589,7 @@ namespace storm {
}
template<typename ValueType>
std::pair<ValueType, ValueType> SparseMdpExplorationModelChecker<ValueType>::computeBoundsOfAction(ActionType const& action, ExplorationInformation const& explorationInformation, BoundValues const& bounds) const {
std::pair<ValueType, ValueType> SparseMdpExplorationModelChecker<ValueType>::computeBoundsOfAction(ActionType const& action, ExplorationInformation<StateType, ValueType> const& explorationInformation, Bounds<StateType, ValueType> const& bounds) const {
// TODO: take into account self-loops?
std::pair<ValueType, ValueType> result = std::make_pair(storm::utility::zero<ValueType>(), storm::utility::zero<ValueType>());
for (auto const& element : explorationInformation.getRowOfMatrix(action)) {
@ -591,18 +600,18 @@ namespace storm {
}
template<typename ValueType>
std::pair<ValueType, ValueType> SparseMdpExplorationModelChecker<ValueType>::computeBoundsOfState(StateType const& currentStateId, ExplorationInformation const& explorationInformation, BoundValues const& bounds) const {
std::pair<ValueType, ValueType> SparseMdpExplorationModelChecker<ValueType>::computeBoundsOfState(StateType const& currentStateId, ExplorationInformation<StateType, ValueType> const& explorationInformation, Bounds<StateType, ValueType> const& bounds) const {
StateType group = explorationInformation.getRowGroup(currentStateId);
std::pair<ValueType, ValueType> result = getLowestBounds(explorationInformation.optimizationDirection);
std::pair<ValueType, ValueType> result = getLowestBounds(explorationInformation.getOptimizationDirection());
for (ActionType action = explorationInformation.getStartRowOfGroup(group); action < explorationInformation.getStartRowOfGroup(group + 1); ++action) {
std::pair<ValueType, ValueType> actionValues = computeBoundsOfAction(action, explorationInformation, bounds);
result = combineBounds(explorationInformation.optimizationDirection, result, actionValues);
result = combineBounds(explorationInformation.getOptimizationDirection(), result, actionValues);
}
return result;
}
template<typename ValueType>
void SparseMdpExplorationModelChecker<ValueType>::updateProbabilityBoundsAlongSampledPath(StateActionStack& stack, ExplorationInformation const& explorationInformation, BoundValues& bounds) const {
void SparseMdpExplorationModelChecker<ValueType>::updateProbabilityBoundsAlongSampledPath(StateActionStack& stack, ExplorationInformation<StateType, ValueType> const& explorationInformation, Bounds<StateType, ValueType>& bounds) const {
stack.pop_back();
while (!stack.empty()) {
updateProbabilityOfAction(stack.back().first, stack.back().second, explorationInformation, bounds);
@ -611,7 +620,7 @@ namespace storm {
}
template<typename ValueType>
void SparseMdpExplorationModelChecker<ValueType>::updateProbabilityOfAction(StateType const& state, ActionType const& action, ExplorationInformation const& explorationInformation, BoundValues& bounds) const {
void SparseMdpExplorationModelChecker<ValueType>::updateProbabilityOfAction(StateType const& state, ActionType const& action, ExplorationInformation<StateType, ValueType> const& explorationInformation, Bounds<StateType, ValueType>& bounds) const {
// Compute the new lower/upper values of the action.
std::pair<ValueType, ValueType> newBoundsForAction = computeBoundsOfAction(action, explorationInformation, bounds);
@ -646,8 +655,8 @@ namespace storm {
}
template<typename ValueType>
ValueType SparseMdpExplorationModelChecker<ValueType>::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<ValueType>::computeBoundOverAllOtherActions(storm::OptimizationDirection const& direction, StateType const& state, ActionType const& action, ExplorationInformation<StateType, ValueType> const& explorationInformation, Bounds<StateType, ValueType> 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) {

308
src/modelchecker/exploration/SparseMdpExplorationModelChecker.h
View File

@ -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<typename StateType>
class StateStorage;
}
class MaximalEndComponent;
}
namespace generator {
template<typename ValueType, typename StateType>
class PrismNextStateGenerator;
namespace prism {
class Program;
}
namespace modelchecker {
namespace exploration_detail {
template <typename StateType, typename ValueType> class StateGeneration;
template <typename StateType, typename ValueType> class ExplorationInformation;
template <typename StateType, typename ValueType> class Bounds;
template <typename StateType, typename ValueType> class Statistics;
}
using namespace exploration_detail;
template<typename ValueType>
class SparseMdpExplorationModelChecker : public AbstractModelChecker {
public:
typedef uint32_t StateType;
typedef uint32_t ActionType;
typedef boost::container::flat_set<StateType> StateSet;
typedef boost::container::flat_set<ActionType> ActionSet;
typedef std::shared_ptr<ActionSet> ActionSetPointer;
typedef StateType ActionType;
typedef std::vector<std::pair<StateType, ActionType>> StateActionStack;
SparseMdpExplorationModelChecker(storm::prism::Program const& program, boost::optional<std::map<storm::expressions::Variable, storm::expressions::Expression>> const& constantDefinitions);
@ -53,278 +44,31 @@ namespace storm {
virtual std::unique_ptr<CheckResult> computeUntilProbabilities(CheckTask<storm::logic::UntilFormula> 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<ActionType>::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<StateType> stateStorage;
std::vector<std::vector<storm::storage::MatrixEntry<StateType, ValueType>>> matrix;
std::vector<StateType> rowGroupIndices;
std::vector<StateType> stateToRowGroupMapping;
StateType unexploredMarker;
std::unordered_map<StateType, storm::generator::CompressedState> unexploredStates;
storm::OptimizationDirection optimizationDirection;
StateSet terminalStates;
bool localPrecomputation;
uint_fast64_t numberOfExplorationStepsUntilPrecomputation;
boost::optional<uint_fast64_t> numberOfSampledPathsUntilPrecomputation;
storm::settings::modules::ExplorationSettings::NextStateHeuristic nextStateHeuristic;
void setInitialStates(std::vector<StateType> 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<storm::storage::MatrixEntry<StateType, ValueType>>& getRowOfMatrix(ActionType const& row) {
return matrix[row];
}
std::vector<storm::storage::MatrixEntry<StateType, ValueType>> 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<StateType> getInitialStates() {
return generator.getInitialStates(stateToIdCallback);
}
storm::generator::StateBehavior<ValueType, StateType> expand() {
return generator.expand(stateToIdCallback);
}
bool isConditionState() const {
return generator.satisfies(conditionStateExpression);
}
bool isTargetState() const {
return generator.satisfies(targetStateExpression);
}
storm::generator::PrismNextStateGenerator<ValueType, StateType> generator;
std::function<StateType (storm::generator::CompressedState const&)> stateToIdCallback;
storm::expressions::Expression conditionStateExpression;
storm::expressions::Expression targetStateExpression;
};
std::function<StateType (storm::generator::CompressedState const&)> createStateToIdCallback(ExplorationInformation& explorationInformation) const;
std::function<StateType (storm::generator::CompressedState const&)> createStateToIdCallback(ExplorationInformation<StateType, ValueType>& explorationInformation) const;
std::tuple<StateType, ValueType, ValueType> performExploration(StateGeneration& stateGeneration, ExplorationInformation& explorationInformation) const;
std::tuple<StateType, ValueType, ValueType> performExploration(StateGeneration<StateType, ValueType>& stateGeneration, ExplorationInformation<StateType, ValueType>& explorationInformation) const;
bool samplePathFromInitialState(StateGeneration& stateGeneration, ExplorationInformation& explorationInformation, StateActionStack& stack, BoundValues& bounds, Statistics& stats) const;
bool samplePathFromInitialState(StateGeneration<StateType, ValueType>& stateGeneration, ExplorationInformation<StateType, ValueType>& explorationInformation, StateActionStack& stack, Bounds<StateType, ValueType>& bounds, Statistics<StateType, ValueType>& stats) const;
bool exploreState(StateGeneration& stateGeneration, StateType const& currentStateId, storm::generator::CompressedState const& currentState, ExplorationInformation& explorationInformation, BoundValues& bounds, Statistics& stats) const;
bool exploreState(StateGeneration<StateType, ValueType>& stateGeneration, StateType const& currentStateId, storm::generator::CompressedState const& currentState, ExplorationInformation<StateType, ValueType>& explorationInformation, Bounds<StateType, ValueType>& bounds, Statistics<StateType, ValueType>& stats) const;
ActionType sampleActionOfState(StateType const& currentStateId, ExplorationInformation const& explorationInformation, BoundValues& bounds) const;
ActionType sampleActionOfState(StateType const& currentStateId, ExplorationInformation<StateType, ValueType> const& explorationInformation, Bounds<StateType, ValueType>& bounds) const;
StateType sampleSuccessorFromAction(ActionType const& chosenAction, ExplorationInformation const& explorationInformation, BoundValues const& bounds) const;
StateType sampleSuccessorFromAction(ActionType const& chosenAction, ExplorationInformation<StateType, ValueType> const& explorationInformation, Bounds<StateType, ValueType> const& bounds) const;
bool performPrecomputation(StateActionStack const& stack, ExplorationInformation& explorationInformation, BoundValues& bounds, Statistics& stats) const;
bool performPrecomputation(StateActionStack const& stack, ExplorationInformation<StateType, ValueType>& explorationInformation, Bounds<StateType, ValueType>& bounds, Statistics<StateType, ValueType>& stats) const;
void collapseMec(storm::storage::MaximalEndComponent const& mec, std::vector<StateType> const& relevantStates, storm::storage::SparseMatrix<ValueType> const& relevantStatesMatrix, ExplorationInformation& explorationInformation, BoundValues& bounds) const;
void collapseMec(storm::storage::MaximalEndComponent const& mec, std::vector<StateType> const& relevantStates, storm::storage::SparseMatrix<ValueType> const& relevantStatesMatrix, ExplorationInformation<StateType, ValueType>& explorationInformation, Bounds<StateType, ValueType>& bounds) const;
void updateProbabilityBoundsAlongSampledPath(StateActionStack& stack, ExplorationInformation const& explorationInformation, BoundValues& bounds) const;
void updateProbabilityBoundsAlongSampledPath(StateActionStack& stack, ExplorationInformation<StateType, ValueType> const& explorationInformation, Bounds<StateType, ValueType>& 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<StateType, ValueType> const& explorationInformation, Bounds<StateType, ValueType>& bounds) const;
std::pair<ValueType, ValueType> 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<ValueType, ValueType> 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<ValueType, ValueType> computeBoundsOfAction(ActionType const& action, ExplorationInformation<StateType, ValueType> const& explorationInformation, Bounds<StateType, ValueType> const& bounds) const;
ValueType computeBoundOverAllOtherActions(storm::OptimizationDirection const& direction, StateType const& state, ActionType const& action, ExplorationInformation<StateType, ValueType> const& explorationInformation, Bounds<StateType, ValueType> const& bounds) const;
std::pair<ValueType, ValueType> computeBoundsOfState(StateType const& currentStateId, ExplorationInformation<StateType, ValueType> const& explorationInformation, Bounds<StateType, ValueType> const& bounds) const;
ValueType computeLowerBoundOfAction(ActionType const& action, ExplorationInformation<StateType, ValueType> const& explorationInformation, Bounds<StateType, ValueType> const& bounds) const;
ValueType computeUpperBoundOfAction(ActionType const& action, ExplorationInformation<StateType, ValueType> const& explorationInformation, Bounds<StateType, ValueType> const& bounds) const;
std::pair<ValueType, ValueType> getLowestBounds(storm::OptimizationDirection const& direction) const;
ValueType getLowestBound(storm::OptimizationDirection const& direction) const;

45
src/modelchecker/exploration/StateGeneration.cpp
View File

@ -0,0 +1,45 @@
#include "src/modelchecker/exploration/StateGeneration.h"
namespace storm {
namespace modelchecker {
namespace exploration_detail {
template <typename StateType, typename ValueType>
StateGeneration<StateType, ValueType>::StateGeneration(storm::prism::Program const& program, storm::generator::VariableInformation const& variableInformation, storm::expressions::Expression const& conditionStateExpression, storm::expressions::Expression const& targetStateExpression) : generator(program, variableInformation, false), conditionStateExpression(conditionStateExpression), targetStateExpression(targetStateExpression) {
// Intentionally left empty.
}
template <typename StateType, typename ValueType>
void StateGeneration<StateType, ValueType>::setStateToIdCallback(std::function<StateType (storm::generator::CompressedState const&)> const& stateToIdCallback) {
this->stateToIdCallback = stateToIdCallback;
}
template <typename StateType, typename ValueType>
void StateGeneration<StateType, ValueType>::load(storm::generator::CompressedState const& state) {
generator.load(state);
}
template <typename StateType, typename ValueType>
std::vector<StateType> StateGeneration<StateType, ValueType>::getInitialStates() {
return generator.getInitialStates(stateToIdCallback);
}
template <typename StateType, typename ValueType>
storm::generator::StateBehavior<ValueType, StateType> StateGeneration<StateType, ValueType>::expand() {
return generator.expand(stateToIdCallback);
}
template <typename StateType, typename ValueType>
bool StateGeneration<StateType, ValueType>::isConditionState() const {
return generator.satisfies(conditionStateExpression);
}
template <typename StateType, typename ValueType>
bool StateGeneration<StateType, ValueType>::isTargetState() const {
return generator.satisfies(targetStateExpression);
}
template class StateGeneration<uint32_t, double>;
}
}
}

44
src/modelchecker/exploration/StateGeneration.h
View File

@ -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<typename ValueType, typename StateType>
class PrismNextStateGenerator;
}
namespace modelchecker {
namespace exploration_detail {
template <typename StateType, typename ValueType>
class StateGeneration {
public:
StateGeneration(storm::prism::Program const& program, storm::generator::VariableInformation const& variableInformation, storm::expressions::Expression const& conditionStateExpression, storm::expressions::Expression const& targetStateExpression);
void setStateToIdCallback(std::function<StateType (storm::generator::CompressedState const&)> const& stateToIdCallback);
void load(storm::generator::CompressedState const& state);
std::vector<StateType> getInitialStates();
storm::generator::StateBehavior<ValueType, StateType> expand();
bool isConditionState() const;
bool isTargetState() const;
private:
storm::generator::PrismNextStateGenerator<ValueType, StateType> generator;
std::function<StateType (storm::generator::CompressedState const&)> stateToIdCallback;
storm::expressions::Expression conditionStateExpression;
storm::expressions::Expression targetStateExpression;
};
}
}
}
#endif /* STORM_MODELCHECKER_EXPLORATION_EXPLORATION_DETAIL_STATEGENERATION_H_ */

46
src/modelchecker/exploration/Statistics.cpp
View File

@ -0,0 +1,46 @@
#include "src/modelchecker/exploration/Statistics.h"
#include "src/modelchecker/exploration/ExplorationInformation.h"
namespace storm {
namespace modelchecker {
namespace exploration_detail {
template<typename StateType, typename ValueType>
Statistics<StateType, ValueType>::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<typename StateType, typename ValueType>
void Statistics<StateType, ValueType>::explorationStep() {
++explorationSteps;
++explorationStepsSinceLastPrecomputation;
}
template<typename StateType, typename ValueType>
void Statistics<StateType, ValueType>::sampledPath() {
++pathsSampled;
++pathsSampledSinceLastPrecomputation;
}
template<typename StateType, typename ValueType>
void Statistics<StateType, ValueType>::updateMaxPathLength(std::size_t const& currentPathLength) {
maxPathLength = std::max(maxPathLength, currentPathLength);
}
template<typename StateType, typename ValueType>
void Statistics<StateType, ValueType>::printToStream(std::ostream& out, ExplorationInformation<StateType, ValueType> 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<uint32_t, double>;
}
}
}

44
src/modelchecker/exploration/Statistics.h
View File

@ -0,0 +1,44 @@
#ifndef STORM_MODELCHECKER_EXPLORATION_EXPLORATION_DETAIL_STATISTICS_H_
#define STORM_MODELCHECKER_EXPLORATION_EXPLORATION_DETAIL_STATISTICS_H_
#include <cstddef>
#include <iostream>
namespace storm {
namespace modelchecker {
namespace exploration_detail {
template<typename StateType, typename ValueType>
class ExplorationInformation;
// A struct that keeps track of certain statistics during the exploration.
template<typename StateType, typename ValueType>
struct Statistics {
Statistics();
void explorationStep();
void sampledPath();
void updateMaxPathLength(std::size_t const& currentPathLength);
void printToStream(std::ostream& out, ExplorationInformation<StateType, ValueType> 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_ */
Write Preview
Loading…
Cancel
Save