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

Typos

tempestpy_adaptions
Matthias Volk 7 years ago
parent
21c970f8f7
commit
7f7778533a
4 changed files with 25 additions and 26 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. 6
      src/storm-dft/modelchecker/dft/DFTModelChecker.cpp
  2. 29
      src/storm-dft/storage/dft/DFT.cpp
  3. 14
      src/storm/models/sparse/MarkovAutomaton.cpp
  4. 2
      src/storm/utility/DirectEncodingExporter.cpp

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

@ -54,14 +54,14 @@ namespace storm {
case storm::storage::DFTElementType::AND:
STORM_LOG_TRACE("top modularisation called AND");
dfts = dft.topModularisation();
STORM_LOG_TRACE("Modularsation into " << dfts.size() << " submodules.");
STORM_LOG_TRACE("Modularisation into " << dfts.size() << " submodules.");
nrK = dfts.size();
nrM = dfts.size();
break;
case storm::storage::DFTElementType::OR:
STORM_LOG_TRACE("top modularisation called OR");
dfts = dft.topModularisation();
STORM_LOG_TRACE("Modularsation into " << dfts.size() << " submodules.");
STORM_LOG_TRACE("Modularisation into " << dfts.size() << " submodules.");
nrK = 0;
nrM = dfts.size();
invResults = true;
@ -69,7 +69,7 @@ namespace storm {
case storm::storage::DFTElementType::VOT:
STORM_LOG_TRACE("top modularisation called VOT");
dfts = dft.topModularisation();
STORM_LOG_TRACE("Modularsation into " << dfts.size() << " submodules.");
STORM_LOG_TRACE("Modularisation into " << dfts.size() << " submodules.");
nrK = std::static_pointer_cast<storm::storage::DFTVot<ValueType> const>(dft.getTopLevelGate())->threshold();
nrM = dfts.size();
if(nrK <= nrM/2) {

29
src/storm-dft/storage/dft/DFT.cpp
View File

@ -293,22 +293,22 @@ namespace storm {
}
return max;
}
template<typename ValueType>
DFT<ValueType> DFT<ValueType>::optimize() const {
std::vector<size_t> modIdea = findModularisationRewrite();
STORM_LOG_DEBUG("Modularisation idea: " << storm::utility::vector::toString(modIdea));
if (modIdea.empty()) {
// No rewrite needed
return *this;
}
std::vector<std::vector<size_t>> rewriteIds;
rewriteIds.push_back(modIdea);
storm::builder::DFTBuilder<ValueType> builder;
// Accumulate elements which must be rewritten
std::set<size_t> rewriteSet;
for (std::vector<size_t> rewrites : rewriteIds) {
@ -320,7 +320,7 @@ namespace storm {
builder.copyElement(elem);
}
}
// Add rewritten elements
for (std::vector<size_t> rewrites : rewriteIds) {
STORM_LOG_ASSERT(rewrites.size() > 1, "No rewritten elements.");
@ -359,7 +359,7 @@ namespace storm {
STORM_LOG_ASSERT(false, "Dft type can not be rewritten.");
break;
}
// Add parent with the new child newParent and all its remaining children
childrenNames.clear();
childrenNames.push_back(newParentName);
@ -371,7 +371,7 @@ namespace storm {
}
builder.copyGate(originalParent, childrenNames);
}
builder.setTopLevel(mElements[mTopLevelIndex]->name());
// TODO use reference?
DFT<ValueType> newDft = builder.build();
@ -750,11 +750,10 @@ namespace storm {
// suitable parent gate! - Lets check the independent submodules of the children
auto const& children = std::static_pointer_cast<DFTGate<ValueType>>(e)->children();
for(auto const& child : children) {
auto ISD = std::static_pointer_cast<DFTGate<ValueType>>(child)->independentSubDft(true);
// In the ISD, check for other children:
std::vector<size_t> rewrite = {e->id(), child->id()};
for(size_t isdElemId : ISD) {
if(isdElemId == child->id()) continue;
@ -765,13 +764,13 @@ namespace storm {
if(rewrite.size() > 2 && rewrite.size() < children.size() - 1) {
return rewrite;
}
}
}
}
}
}
return {};
}
template<typename ValueType>
std::tuple<std::vector<size_t>, std::vector<size_t>, std::vector<size_t>> DFT<ValueType>::getSortedParentAndDependencyIds(size_t index) const {

14
src/storm/models/sparse/MarkovAutomaton.cpp
View File

@ -181,7 +181,7 @@ namespace storm {
// Get number of choices in current state
uint_fast64_t numberChoices = this->getTransitionMatrix().getRowGroupIndices()[state + 1] - this->getTransitionMatrix().getRowGroupIndices()[state];
if (isMarkovianState(state)) {
STORM_LOG_ASSERT(numberChoices == 1, "Wrong number of choices for markovian state.");
STORM_LOG_ASSERT(numberChoices == 1, "Wrong number of choices for Markovian state.");
}
if (numberChoices > 1) {
STORM_LOG_ASSERT(isProbabilisticState(state), "State is not probabilistic.");
@ -211,7 +211,7 @@ namespace storm {
storm::storage::FlexibleSparseMatrix<ValueType> flexibleMatrix(this->getTransitionMatrix());
storm::storage::FlexibleSparseMatrix<ValueType> flexibleBackwardTransitions(this->getTransitionMatrix().transpose());
storm::solver::stateelimination::StateEliminator<ValueType> stateEliminator(flexibleMatrix, flexibleBackwardTransitions);
for (uint_fast64_t state = 0; state < this->getNumberOfStates(); ++state) {
STORM_LOG_ASSERT(!this->isHybridState(state), "State is hybrid.");
if (this->isProbabilisticState(state)) {
@ -220,7 +220,7 @@ namespace storm {
STORM_LOG_TRACE("Flexible matrix after eliminating state " << state << ":" << std::endl << flexibleMatrix);
}
}
// Create the rate matrix for the CTMC
storm::storage::SparseMatrixBuilder<ValueType> transitionMatrixBuilder(0, 0, 0, false, false);
// Remember state to keep
@ -230,7 +230,7 @@ namespace storm {
// State is eliminated and can be discarded
keepStates.set(state, false);
} else {
STORM_LOG_ASSERT(this->isMarkovianState(state), "State is not markovian.");
STORM_LOG_ASSERT(this->isMarkovianState(state), "State is not Markovian.");
// Copy transitions
for (uint_fast64_t row = flexibleMatrix.getRowGroupIndices()[state]; row < flexibleMatrix.getRowGroupIndices()[state + 1]; ++row) {
for (auto const& entry : flexibleMatrix.getRow(row)) {
@ -240,20 +240,20 @@ namespace storm {
}
}
}
storm::storage::SparseMatrix<ValueType> rateMatrix = transitionMatrixBuilder.build();
rateMatrix = rateMatrix.getSubmatrix(false, keepStates, keepStates, false);
STORM_LOG_TRACE("New CTMC matrix:" << std::endl << rateMatrix);
// Construct CTMC
storm::models::sparse::StateLabeling stateLabeling = this->getStateLabeling().getSubLabeling(keepStates);
//TODO update reward models and choice labels according to kept states
STORM_LOG_WARN_COND(this->getRewardModels().empty(), "Conversion of MA to CTMC does not preserve rewards.");
std::unordered_map<std::string, RewardModelType> rewardModels = this->getRewardModels();
STORM_LOG_WARN_COND(!this->hasChoiceLabeling(), "Conversion of MA to CTMC does not preserve choice labels.");
STORM_LOG_WARN_COND(!this->hasStateValuations(), "Conversion of MA to CTMC does not preserve choice labels.");
STORM_LOG_WARN_COND(!this->hasChoiceOrigins(), "Conversion of MA to CTMC does not preserve choice labels.");
return std::make_shared<storm::models::sparse::Ctmc<ValueType, RewardModelType>>(std::move(rateMatrix), std::move(stateLabeling), std::move(rewardModels));
}

2
src/storm/utility/DirectEncodingExporter.cpp
View File

@ -73,7 +73,7 @@ namespace storm {
}
if(rewardModelEntry.second.hasStateRewards()) {
os << rewardModelEntry.second.getStateRewardVector().at(group);
os << storm::utility::to_string(rewardModelEntry.second.getStateRewardVector().at(group));
} else {
os << "0";
}

Write Preview
Loading…
Cancel
Save