Browse Source

Minor fixes

Former-commit-id: 9344ebe5aa
tempestpy_adaptions
Mavo 8 years ago
parent
commit
1bfd974795
  1. 19
      src/builder/ExplicitDFTModelBuilderApprox.cpp
  2. 4
      src/generator/DftNextStateGenerator.cpp
  3. 2
      src/modelchecker/dft/DFTModelChecker.cpp

19
src/builder/ExplicitDFTModelBuilderApprox.cpp

@ -75,12 +75,16 @@ namespace storm {
STORM_LOG_ASSERT(stateStorage.initialStateIndices.size() == 1, "Only one initial state assumed."); STORM_LOG_ASSERT(stateStorage.initialStateIndices.size() == 1, "Only one initial state assumed.");
initialStateIndex = stateStorage.initialStateIndices[0]; initialStateIndex = stateStorage.initialStateIndices[0];
STORM_LOG_TRACE("Initial state: " << initialStateIndex); STORM_LOG_TRACE("Initial state: " << initialStateIndex);
// Initialize heuristic values for inital state
statesNotExplored.at(initialStateIndex)->setHeuristicValues(0, storm::utility::zero<ValueType>(), storm::utility::zero<ValueType>());
} else { } else {
initializeNextIteration(); initializeNextIteration();
} }
switch (heuristic) { switch (heuristic) {
case storm::builder::ApproximationHeuristic::NONE:
// Do not change anything
break;
case storm::builder::ApproximationHeuristic::DEPTH: case storm::builder::ApproximationHeuristic::DEPTH:
approximationThreshold = iteration; approximationThreshold = iteration;
break; break;
@ -246,6 +250,7 @@ namespace storm {
matrixBuilder.newRowGroup(); matrixBuilder.newRowGroup();
// Try to explore the next state // Try to explore the next state
bool fixQueue = false;
generator.load(currentState); generator.load(currentState);
if (currentState->isSkip(approximationThreshold, heuristic)) { if (currentState->isSkip(approximationThreshold, heuristic)) {
@ -270,15 +275,21 @@ namespace storm {
for (auto const& stateProbabilityPair : choice) { for (auto const& stateProbabilityPair : choice) {
// Set transition to state id + offset. This helps in only remapping all previously skipped states. // Set transition to state id + offset. This helps in only remapping all previously skipped states.
matrixBuilder.addTransition(matrixBuilder.mappingOffset + stateProbabilityPair.first, stateProbabilityPair.second); matrixBuilder.addTransition(matrixBuilder.mappingOffset + stateProbabilityPair.first, stateProbabilityPair.second);
// TODO Matthias: set heuristic values here
// Set heuristic values for reached states
auto iter = statesNotExplored.find(stateProbabilityPair.first);
if (iter != statesNotExplored.end()) {
iter->second->setHeuristicValues(currentState, stateProbabilityPair.second, choice.getTotalMass());
fixQueue = true;
}
} }
matrixBuilder.finishRow(); matrixBuilder.finishRow();
} }
} }
// Update priority queue // Update priority queue
// TODO Matthias: only when necessary
explorationQueue.fix();
if (fixQueue) {
explorationQueue.fix();
}
} // end exploration } // end exploration
} }

4
src/generator/DftNextStateGenerator.cpp

@ -20,7 +20,6 @@ namespace storm {
template<typename ValueType, typename StateType> template<typename ValueType, typename StateType>
std::vector<StateType> DftNextStateGenerator<ValueType, StateType>::getInitialStates(StateToIdCallback const& stateToIdCallback) { std::vector<StateType> DftNextStateGenerator<ValueType, StateType>::getInitialStates(StateToIdCallback const& stateToIdCallback) {
DFTStatePointer initialState = std::make_shared<storm::storage::DFTState<ValueType>>(mDft, mStateGenerationInfo, 0); DFTStatePointer initialState = std::make_shared<storm::storage::DFTState<ValueType>>(mDft, mStateGenerationInfo, 0);
initialState->setHeuristicValues(0, storm::utility::zero<ValueType>(), storm::utility::zero<ValueType>());
// Register initial state // Register initial state
StateType id = stateToIdCallback(initialState); StateType id = stateToIdCallback(initialState);
@ -158,10 +157,8 @@ namespace storm {
ValueType remainingProbability = storm::utility::one<ValueType>() - probability; ValueType remainingProbability = storm::utility::one<ValueType>() - probability;
choice.addProbability(unsuccessfulStateId, remainingProbability); choice.addProbability(unsuccessfulStateId, remainingProbability);
STORM_LOG_TRACE("Added transition to " << unsuccessfulStateId << " with remaining probability " << remainingProbability); STORM_LOG_TRACE("Added transition to " << unsuccessfulStateId << " with remaining probability " << remainingProbability);
unsuccessfulState->setHeuristicValues(state, remainingProbability, storm::utility::one<ValueType>());
} }
result.addChoice(std::move(choice)); result.addChoice(std::move(choice));
newState->setHeuristicValues(state, probability, storm::utility::one<ValueType>());
} else { } else {
// Failure is due to "normal" BE failure // Failure is due to "normal" BE failure
// Set failure rate according to activation // Set failure rate according to activation
@ -174,7 +171,6 @@ namespace storm {
STORM_LOG_ASSERT(!storm::utility::isZero(rate), "Rate is 0."); STORM_LOG_ASSERT(!storm::utility::isZero(rate), "Rate is 0.");
choice.addProbability(newStateId, rate); choice.addProbability(newStateId, rate);
STORM_LOG_TRACE("Added transition to " << newStateId << " with " << (isActive ? "active" : "passive") << " failure rate " << rate); STORM_LOG_TRACE("Added transition to " << newStateId << " with " << (isActive ? "active" : "passive") << " failure rate " << rate);
newState->setHeuristicValues(state, rate, choice.getTotalMass());
} }
++currentFailable; ++currentFailable;

2
src/modelchecker/dft/DFTModelChecker.cpp

@ -204,7 +204,7 @@ namespace storm {
if (approximationError >= 0.0) { if (approximationError >= 0.0) {
storm::builder::ExplicitDFTModelBuilderApprox<ValueType> builder(dft, symmetries, enableDC); storm::builder::ExplicitDFTModelBuilderApprox<ValueType> builder(dft, symmetries, enableDC);
typename storm::builder::ExplicitDFTModelBuilderApprox<ValueType>::LabelOptions labeloptions; // TODO initialize this with the formula typename storm::builder::ExplicitDFTModelBuilderApprox<ValueType>::LabelOptions labeloptions; // TODO initialize this with the formula
builder.buildModel(labeloptions, true);
builder.buildModel(labeloptions, 0);
model = builder.getModel(); model = builder.getModel();
} else { } else {
storm::builder::ExplicitDFTModelBuilder<ValueType> builder(dft, symmetries, enableDC); storm::builder::ExplicitDFTModelBuilder<ValueType> builder(dft, symmetries, enableDC);

Loading…
Cancel
Save