diff --git a/src/modelchecker/EigenDtmcPrctlModelChecker.h b/src/modelchecker/EigenDtmcPrctlModelChecker.h index a7b749129..61867620d 100644 --- a/src/modelchecker/EigenDtmcPrctlModelChecker.h +++ b/src/modelchecker/EigenDtmcPrctlModelChecker.h @@ -12,7 +12,7 @@ #include "src/models/Dtmc.h" #include "src/modelchecker/DtmcPrctlModelChecker.h" -#include "src/solver/GraphAnalyzer.h" +#include "src/utility/GraphAnalyzer.h" #include "src/utility/ConstTemplates.h" #include "src/exceptions/NoConvergenceException.h" @@ -128,7 +128,7 @@ public: // all states that have probability 0 and 1 of satisfying the until-formula. storm::storage::BitVector notExistsPhiUntilPsiStates(this->getModel().getNumberOfStates()); storm::storage::BitVector alwaysPhiUntilPsiStates(this->getModel().getNumberOfStates()); - storm::solver::GraphAnalyzer::getPhiUntilPsiStates(this->getModel(), *leftStates, *rightStates, ¬ExistsPhiUntilPsiStates, &alwaysPhiUntilPsiStates); + storm::utility::GraphAnalyzer::getPhiUntilPsiStates(this->getModel(), *leftStates, *rightStates, ¬ExistsPhiUntilPsiStates, &alwaysPhiUntilPsiStates); notExistsPhiUntilPsiStates.complement(); delete leftStates; diff --git a/src/modelchecker/GmmxxDtmcPrctlModelChecker.h b/src/modelchecker/GmmxxDtmcPrctlModelChecker.h index 009ecd678..a1b11af0a 100644 --- a/src/modelchecker/GmmxxDtmcPrctlModelChecker.h +++ b/src/modelchecker/GmmxxDtmcPrctlModelChecker.h @@ -12,7 +12,7 @@ #include "src/models/Dtmc.h" #include "src/modelchecker/DtmcPrctlModelChecker.h" -#include "src/solver/GraphAnalyzer.h" +#include "src/utility/GraphAnalyzer.h" #include "src/utility/Vector.h" #include "src/utility/ConstTemplates.h" #include "src/utility/Settings.h" @@ -113,7 +113,7 @@ public: // all states that have probability 0 and 1 of satisfying the until-formula. storm::storage::BitVector notExistsPhiUntilPsiStates(this->getModel().getNumberOfStates()); storm::storage::BitVector alwaysPhiUntilPsiStates(this->getModel().getNumberOfStates()); - storm::solver::GraphAnalyzer::getPhiUntilPsiStates(this->getModel(), *leftStates, *rightStates, ¬ExistsPhiUntilPsiStates, &alwaysPhiUntilPsiStates); + storm::utility::GraphAnalyzer::getPhiUntilPsiStates(this->getModel(), *leftStates, *rightStates, ¬ExistsPhiUntilPsiStates, &alwaysPhiUntilPsiStates); notExistsPhiUntilPsiStates.complement(); // Delete sub-results that are obsolete now. @@ -253,7 +253,7 @@ public: // Determine which states have a reward of infinity by definition. storm::storage::BitVector infinityStates(this->getModel().getNumberOfStates()); storm::storage::BitVector trueStates(this->getModel().getNumberOfStates(), true); - storm::solver::GraphAnalyzer::getAlwaysPhiUntilPsiStates(this->getModel(), trueStates, *targetStates, &infinityStates); + storm::utility::GraphAnalyzer::getAlwaysPhiUntilPsiStates(this->getModel(), trueStates, *targetStates, &infinityStates); infinityStates.complement(); // Create resulting vector. diff --git a/src/models/Ctmc.h b/src/models/Ctmc.h index 263a62fe9..ef6cd4658 100644 --- a/src/models/Ctmc.h +++ b/src/models/Ctmc.h @@ -139,7 +139,7 @@ public: */ storm::models::GraphTransitions& getBackwardTransitions() { if (this->backwardTransitions == nullptr) { - this->backwardTransitions = new storm::models::GraphTransitions(this->probabilityMatrix, false); + this->backwardTransitions = new storm::models::GraphTransitions(this->rateMatrix, false); } return *this->backwardTransitions; } diff --git a/src/storm.cpp b/src/storm.cpp index 2015e85e4..f0b528f99 100644 --- a/src/storm.cpp +++ b/src/storm.cpp @@ -26,7 +26,6 @@ #include "src/modelchecker/GmmxxDtmcPrctlModelChecker.h" #include "src/parser/AutoParser.h" #include "src/parser/PrctlParser.h" -#include "src/solver/GraphAnalyzer.h" #include "src/utility/Settings.h" #include "src/formula/Formulas.h" diff --git a/src/solver/GraphAnalyzer.h b/src/utility/GraphAnalyzer.h similarity index 97% rename from src/solver/GraphAnalyzer.h rename to src/utility/GraphAnalyzer.h index 70b6b10f5..0e3479338 100644 --- a/src/solver/GraphAnalyzer.h +++ b/src/utility/GraphAnalyzer.h @@ -5,8 +5,8 @@ * Author: Christian Dehnert */ -#ifndef STORM_SOLVER_GRAPHANALYZER_H_ -#define STORM_SOLVER_GRAPHANALYZER_H_ +#ifndef STORM_UTILITY_GRAPHANALYZER_H_ +#define STORM_UTILITY_GRAPHANALYZER_H_ #include "src/models/Dtmc.h" #include "src/exceptions/InvalidArgumentException.h" @@ -18,7 +18,7 @@ extern log4cplus::Logger logger; namespace storm { -namespace solver { +namespace utility { class GraphAnalyzer { public: @@ -148,8 +148,8 @@ public: }; -} // namespace solver +} // namespace utility } // namespace storm -#endif /* STORM_SOLVER_GRAPHANALYZER_H_ */ +#endif /* STORM_UTILITY_GRAPHANALYZER_H_ */