Fixed typo in CTMC class. Moved GraphAnalyzer to utility.

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<double>(this->getModel(), *leftStates, *rightStates, &notExistsPhiUntilPsiStates, &alwaysPhiUntilPsiStates);
+		storm::utility::GraphAnalyzer::getPhiUntilPsiStates<double>(this->getModel(), *leftStates, *rightStates, &notExistsPhiUntilPsiStates, &alwaysPhiUntilPsiStates);
 		notExistsPhiUntilPsiStates.complement();
 
 		delete leftStates;

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, &notExistsPhiUntilPsiStates, &alwaysPhiUntilPsiStates);
+		storm::utility::GraphAnalyzer::getPhiUntilPsiStates(this->getModel(), *leftStates, *rightStates, &notExistsPhiUntilPsiStates, &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.

src/models/Ctmc.h

@@ -139,7 +139,7 @@ public:
 	 */
 	storm::models::GraphTransitions<T>& getBackwardTransitions() {
 		if (this->backwardTransitions == nullptr) {
-			this->backwardTransitions = new storm::models::GraphTransitions<T>(this->probabilityMatrix, false);
+			this->backwardTransitions = new storm::models::GraphTransitions<T>(this->rateMatrix, false);
 		}
 		return *this->backwardTransitions;
 	}

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"
 

src/solver/GraphAnalyzer.h → 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_ */