Browse Source

fixed compiling storm-dft

tempestpy_adaptions
TimQu 8 years ago
parent
commit
f2ab549b36
  1. 19
      src/storm-dft/builder/ExplicitDFTModelBuilder.cpp
  2. 18
      src/storm-dft/builder/ExplicitDFTModelBuilderApprox.cpp

19
src/storm-dft/builder/ExplicitDFTModelBuilder.cpp

@ -138,22 +138,13 @@ namespace storm {
} }
std::shared_ptr<storm::models::sparse::Model<ValueType>> model; std::shared_ptr<storm::models::sparse::Model<ValueType>> model;
storm::storage::sparse::ModelComponents<ValueType> components(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling));
components.exitRates = std::move(modelComponents.exitRates);
if (deterministic) { if (deterministic) {
// Turn the probabilities into rates by multiplying each row with the exit rate of the state.
// TODO Matthias: avoid transforming back and forth
storm::storage::SparseMatrix<ValueType> rateMatrix(modelComponents.transitionMatrix);
for (uint_fast64_t row = 0; row < rateMatrix.getRowCount(); ++row) {
STORM_LOG_ASSERT(row < modelComponents.markovianStates.size(), "Row exceeds no. of markovian states.");
if (modelComponents.markovianStates.get(row)) {
for (auto& entry : rateMatrix.getRow(row)) {
entry.setValue(entry.getValue() * modelComponents.exitRates[row]);
}
}
}
model = std::make_shared<storm::models::sparse::Ctmc<ValueType>>(std::move(rateMatrix), std::move(modelComponents.exitRates), std::move(modelComponents.stateLabeling));
model = std::make_shared<storm::models::sparse::Ctmc<ValueType>>(std::move(components));
} else { } else {
std::shared_ptr<storm::models::sparse::MarkovAutomaton<ValueType>> ma = std::make_shared<storm::models::sparse::MarkovAutomaton<ValueType>>(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), std::move(modelComponents.markovianStates), std::move(modelComponents.exitRates), true);
components.markovianStates = std::move(modelComponents.markovianStates);
std::shared_ptr<storm::models::sparse::MarkovAutomaton<ValueType>> ma = std::make_shared<storm::models::sparse::MarkovAutomaton<ValueType>>(std::move(components));
if (ma->hasOnlyTrivialNondeterminism()) { if (ma->hasOnlyTrivialNondeterminism()) {
// Markov automaton can be converted into CTMC // Markov automaton can be converted into CTMC
model = ma->convertToCTMC(); model = ma->convertToCTMC();

18
src/storm-dft/builder/ExplicitDFTModelBuilderApprox.cpp

@ -525,7 +525,11 @@ namespace storm {
} }
STORM_LOG_TRACE("Exit rates: " << modelComponents.exitRates); 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);
storm::storage::sparse::ModelComponents<ValueType> maComponents(std::move(matrix), std::move(labeling));
maComponents.rateTransitions = true;
maComponents.markovianStates = modelComponents.markovianStates;
maComponents.exitRates = modelComponents.exitRates;
std::shared_ptr<storm::models::sparse::MarkovAutomaton<ValueType>> ma = std::make_shared<storm::models::sparse::MarkovAutomaton<ValueType>>(std::move(maComponents));
if (ma->hasOnlyTrivialNondeterminism()) { if (ma->hasOnlyTrivialNondeterminism()) {
// Markov automaton can be converted into CTMC // Markov automaton can be converted into CTMC
// TODO Matthias: change components which were not moved accordingly // TODO Matthias: change components which were not moved accordingly
@ -573,9 +577,17 @@ namespace storm {
std::shared_ptr<storm::models::sparse::MarkovAutomaton<ValueType>> ma; std::shared_ptr<storm::models::sparse::MarkovAutomaton<ValueType>> ma;
if (copy) { if (copy) {
ma = std::make_shared<storm::models::sparse::MarkovAutomaton<ValueType>>(modelComponents.transitionMatrix, modelComponents.stateLabeling, modelComponents.markovianStates, modelComponents.exitRates);
storm::storage::sparse::ModelComponents<ValueType> maComponents(modelComponents.transitionMatrix, modelComponents.stateLabeling);
maComponents.rateTransitions = true;
maComponents.markovianStates = modelComponents.markovianStates;
maComponents.exitRates = modelComponents.exitRates;
std::shared_ptr<storm::models::sparse::MarkovAutomaton<ValueType>> ma = std::make_shared<storm::models::sparse::MarkovAutomaton<ValueType>>(std::move(maComponents));
} else { } else {
ma = std::make_shared<storm::models::sparse::MarkovAutomaton<ValueType>>(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), std::move(modelComponents.markovianStates), std::move(modelComponents.exitRates));
storm::storage::sparse::ModelComponents<ValueType> maComponents(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling));
maComponents.rateTransitions = true;
maComponents.markovianStates = std::move(modelComponents.markovianStates);
maComponents.exitRates = std::move(modelComponents.exitRates);
std::shared_ptr<storm::models::sparse::MarkovAutomaton<ValueType>> ma = std::make_shared<storm::models::sparse::MarkovAutomaton<ValueType>>(std::move(maComponents));
} }
if (ma->hasOnlyTrivialNondeterminism()) { if (ma->hasOnlyTrivialNondeterminism()) {
// Markov automaton can be converted into CTMC // Markov automaton can be converted into CTMC

Loading…
Cancel
Save