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

Hacked approximation for probabilities

tempestpy_adaptions
Matthias Volk 8 years ago
parent
ac8cea1e53
commit
8cbfccba22
5 changed files with 87 additions and 19 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. 4
      src/storm-dft/builder/DftExplorationHeuristic.h
  2. 76
      src/storm-dft/builder/ExplicitDFTModelBuilderApprox.cpp
  3. 17
      src/storm-dft/builder/ExplicitDFTModelBuilderApprox.h
  4. 7
      src/storm-dft/modelchecker/dft/DFTModelChecker.cpp
  5. 2
      src/storm-dft/storage/BucketPriorityQueue.h

4
src/storm-dft/builder/DftExplorationHeuristic.h
View File

@ -107,8 +107,8 @@ namespace storm {
}
bool updateHeuristicValues(DFTExplorationHeuristic<ValueType> const& predecessor, ValueType, ValueType) override {
if (predecessor.getDepth() < this->depth) {
this->depth = predecessor.getDepth();
if (predecessor.getDepth() + 1 < this->depth) {
this->depth = predecessor.getDepth() + 1;
return true;
}
return false;

76
src/storm-dft/builder/ExplicitDFTModelBuilderApprox.cpp
View File

@ -65,7 +65,7 @@ namespace storm {
{
// Intentionally left empty.
// TODO Matthias: remove again
usedHeuristic = storm::builder::ApproximationHeuristic::NONE;
usedHeuristic = storm::builder::ApproximationHeuristic::DEPTH;
// Compute independent subtrees
if (dft.topLevelType() == storm::storage::DFTElementType::OR) {
@ -349,8 +349,8 @@ namespace storm {
// Try to explore the next state
generator.load(currentState);
if (approximationThreshold > 0.0 && nrExpandedStates > approximationThreshold && !currentExplorationHeuristic->isExpand()) {
//if (currentExplorationHeuristic->isSkip(approximationThreshold)) {
//if (approximationThreshold > 0.0 && nrExpandedStates > approximationThreshold && !currentExplorationHeuristic->isExpand()) {
if (approximationThreshold > 0.0 && currentExplorationHeuristic->isSkip(approximationThreshold)) {
// Skip the current state
++nrSkippedStates;
STORM_LOG_TRACE("Skip expansion of state: " << dft.getStateString(currentState));
@ -397,6 +397,7 @@ namespace storm {
STORM_LOG_ASSERT(!currentState->isPseudoState(), "State is pseudo state.");
// Initialize bounds
// TODO Mathias: avoid hack
ValueType lowerBound = getLowerBound(state);
ValueType upperBound = getUpperBound(state);
heuristic->setBounds(lowerBound, upperBound);
@ -478,10 +479,70 @@ namespace storm {
}
template<typename ValueType, typename StateType>
std::shared_ptr<storm::models::sparse::Model<ValueType>> ExplicitDFTModelBuilderApprox<ValueType, StateType>::getModelApproximation(bool lowerBound) {
// TODO Matthias: handle case with no skipped states
changeMatrixBound(modelComponents.transitionMatrix, lowerBound);
return createModel(true);
std::shared_ptr<storm::models::sparse::Model<ValueType>> ExplicitDFTModelBuilderApprox<ValueType, StateType>::getModelApproximation(bool lowerBound, bool expectedTime) {
if (expectedTime) {
// TODO Matthias: handle case with no skipped states
changeMatrixBound(modelComponents.transitionMatrix, lowerBound);
return createModel(true);
} else {
// Change model for probabilities
// TODO Matthias: make nicer
storm::storage::SparseMatrix<ValueType> matrix = modelComponents.transitionMatrix;
storm::models::sparse::StateLabeling labeling = modelComponents.stateLabeling;
if (lowerBound) {
// Set self loop for lower bound
for (auto it = skippedStates.begin(); it != skippedStates.end(); ++it) {
auto matrixEntry = matrix.getRow(it->first, 0).begin();
STORM_LOG_ASSERT(matrixEntry->getColumn() == failedStateId, "Transition has wrong target state.");
STORM_LOG_ASSERT(!it->second.first->isPseudoState(), "State is still pseudo state.");
matrixEntry->setValue(storm::utility::one<ValueType>());
matrixEntry->setColumn(it->first);
}
} else {
// Make skipped states failed states for upper bound
storm::storage::BitVector failedStates = modelComponents.stateLabeling.getStates("failed");
for (auto it = skippedStates.begin(); it != skippedStates.end(); ++it) {
failedStates.set(it->first);
}
labeling.setStates("failed", failedStates);
}
std::shared_ptr<storm::models::sparse::Model<ValueType>> model;
if (modelComponents.deterministicModel) {
model = std::make_shared<storm::models::sparse::Ctmc<ValueType>>(std::move(matrix), std::move(labeling));
} else {
// Build MA
// Compute exit rates
// TODO Matthias: avoid computing multiple times
modelComponents.exitRates = std::vector<ValueType>(modelComponents.markovianStates.size());
std::vector<typename storm::storage::SparseMatrix<ValueType>::index_type> indices = matrix.getRowGroupIndices();
for (StateType stateIndex = 0; stateIndex < modelComponents.markovianStates.size(); ++stateIndex) {
if (modelComponents.markovianStates[stateIndex]) {
modelComponents.exitRates[stateIndex] = matrix.getRowSum(indices[stateIndex]);
} else {
modelComponents.exitRates[stateIndex] = storm::utility::zero<ValueType>();
}
}
STORM_LOG_TRACE("Exit rates: " << modelComponents.exitRates);
std::shared_ptr<storm::models::sparse::MarkovAutomaton<ValueType>> ma = std::make_shared<storm::models::sparse::MarkovAutomaton<ValueType>>(std::move(matrix), std::move(labeling), modelComponents.markovianStates, modelComponents.exitRates);
if (ma->hasOnlyTrivialNondeterminism()) {
// Markov automaton can be converted into CTMC
// TODO Matthias: change components which were not moved accordingly
model = ma->convertToCTMC();
} else {
model = ma;
}
}
if (model->getNumberOfStates() <= 15) {
STORM_LOG_TRACE("Transition matrix: " << std::endl << model->getTransitionMatrix());
} else {
STORM_LOG_TRACE("Transition matrix: too big to print");
}
return model;
}
}
template<typename ValueType, typename StateType>
@ -573,6 +634,7 @@ namespace storm {
if (state->hasFailed(dft.getTopLevelIndex())) {
return storm::utility::zero<ValueType>();
}
// Get the upper bound by considering the failure of all BEs
ValueType upperBound = storm::utility::one<ValueType>();
ValueType rateSum = storm::utility::zero<ValueType>();

17
src/storm-dft/builder/ExplicitDFTModelBuilderApprox.h
View File

@ -29,7 +29,7 @@ namespace storm {
using DFTStatePointer = std::shared_ptr<storm::storage::DFTState<ValueType>>;
// TODO Matthias: make choosable
using ExplorationHeuristic = DFTExplorationHeuristicNone<ValueType>;
using ExplorationHeuristic = DFTExplorationHeuristicDepth<ValueType>;
using ExplorationHeuristicPointer = std::shared_ptr<ExplorationHeuristic>;
@ -197,11 +197,12 @@ namespace storm {
/*!
* Get the built approximation model for either the lower or upper bound.
*
* @param lowerBound If true, the lower bound model is returned, else the upper bound model
* @param lowerBound If true, the lower bound model is returned, else the upper bound model
* @param expectedTime If true, the bounds for expected time are computed, else the bounds for probabilities.
*
* @return The model built from the DFT.
*/
std::shared_ptr<storm::models::sparse::Model<ValueType>> getModelApproximation(bool lowerBound = true);
std::shared_ptr<storm::models::sparse::Model<ValueType>> getModelApproximation(bool lowerBound, bool expectedTime);
private:
@ -243,14 +244,16 @@ namespace storm {
/**
* Change matrix to reflect the lower or upper approximation bound.
*
* @param matrix Matrix to change. The change are reflected here.
* @param lowerBound Flag indicating if the lower bound should be used. Otherwise the upper bound is used.
* @param matrix Matrix to change. The change are reflected here.
* @param lowerBound Flag indicating if the lower bound should be used. Otherwise the upper bound is used.
*/
void changeMatrixBound(storm::storage::SparseMatrix<ValueType> & matrix, bool lowerBound) const;
/*!
* Get lower bound approximation for state.
*
* @param state The state.
*
* @return Lower bound approximation.
*/
ValueType getLowerBound(DFTStatePointer const& state) const;
@ -258,6 +261,8 @@ namespace storm {
/*!
* Get upper bound approximation for state.
*
* @param state The state.
*
* @return Upper bound approximation.
*/
ValueType getUpperBound(DFTStatePointer const& state) const;
@ -310,7 +315,7 @@ namespace storm {
bool enableDC = true;
//TODO Matthias: make changeable
const bool mergeFailedStates = false;
const bool mergeFailedStates = true;
// Heuristic used for approximation
storm::builder::ApproximationHeuristic usedHeuristic;

7
src/storm-dft/modelchecker/dft/DFTModelChecker.cpp
View File

@ -303,7 +303,7 @@ namespace storm {
// Build model for lower bound
STORM_LOG_INFO("Getting model for lower bound...");
model = builder.getModelApproximation(probabilityFormula ? false : true);
model = builder.getModelApproximation(true, !probabilityFormula);
// We only output the info from the lower bound as the info for the upper bound is the same
model->printModelInformationToStream(std::cout);
buildingTimer.stop();
@ -317,15 +317,16 @@ namespace storm {
// Build model for upper bound
STORM_LOG_INFO("Getting model for upper bound...");
buildingTimer.start();
model = builder.getModelApproximation(probabilityFormula ? true : false);
model = builder.getModelApproximation(false, !probabilityFormula);
buildingTimer.stop();
// Check upper bound
newResult = checkModel(model, {properties});
newResult = checkModel(model, {property});
STORM_LOG_ASSERT(newResult.size() == 1, "Wrong size for result vector.");
STORM_LOG_ASSERT(iteration == 0 || !comparator.isLess(approxResult.second, newResult[0]), "New over-approximation " << newResult[0] << " is greater than old result " << approxResult.second);
approxResult.second = newResult[0];
++iteration;
STORM_LOG_ASSERT(comparator.isLess(approxResult.first, approxResult.second) || comparator.isEqual(approxResult.first, approxResult.second), "Under-approximation " << approxResult.first << " is greater than over-approximation " << approxResult.second);
STORM_LOG_INFO("Result after iteration " << iteration << ": (" << std::setprecision(10) << approxResult.first << ", " << approxResult.second << ")");
totalTimer.stop();
printTimings();

2
src/storm-dft/storage/BucketPriorityQueue.h
View File

@ -13,7 +13,7 @@ namespace storm {
template<typename ValueType>
class BucketPriorityQueue {
using HeuristicPointer = std::shared_ptr<storm::builder::DFTExplorationHeuristicNone<ValueType>>;
using HeuristicPointer = std::shared_ptr<storm::builder::DFTExplorationHeuristicDepth<ValueType>>;
public:
explicit BucketPriorityQueue(size_t nrBuckets, double lowerValue, double ratio);

Write Preview
Loading…
Cancel
Save