diff --git a/src/modelchecker/AbstractModelChecker.h b/src/modelchecker/AbstractModelChecker.h
index 5517dbacd..73f6dfc7e 100644
--- a/src/modelchecker/AbstractModelChecker.h
+++ b/src/modelchecker/AbstractModelChecker.h
@@ -8,9 +8,11 @@
#ifndef STORM_MODELCHECKER_ABSTRACTMODELCHECKER_H_
#define STORM_MODELCHECKER_ABSTRACTMODELCHECKER_H_
-namespace storm { namespace modelChecker {
+namespace storm {
+namespace modelChecker {
template <class Type> class AbstractModelChecker;
-}}
+}
+}
#include "src/exceptions/InvalidPropertyException.h"
#include "src/formula/Formulas.h"
@@ -49,17 +51,17 @@ class AbstractModelChecker :
public virtual storm::formula::IReachabilityRewardModelChecker<Type>,
public virtual storm::formula::ICumulativeRewardModelChecker<Type>,
public virtual storm::formula::IInstantaneousRewardModelChecker<Type> {
-
+
public:
explicit AbstractModelChecker(storm::models::AbstractModel<Type>& model)
: model(model) {
// Nothing to do here...
}
-
+
explicit AbstractModelChecker(AbstractModelChecker<Type>* modelChecker)
: model(modelChecker->model) {
}
-
+
template <template <class T> class Target>
const Target<Type>* as() const {
try {
@@ -243,11 +245,11 @@ public:
delete quantitativeResult;
return result;
}
-
+
void setModel(storm::models::AbstractModel<Type>& model) {
this->model = model;
}
-
+
template <class Model>
Model& getModel() const {
return *dynamic_cast<Model*>(&this->model);
diff --git a/src/modelchecker/EigenDtmcPrctlModelChecker.h b/src/modelchecker/EigenDtmcPrctlModelChecker.h
index 167b02f72..50ad01f3b 100644
--- a/src/modelchecker/EigenDtmcPrctlModelChecker.h
+++ b/src/modelchecker/EigenDtmcPrctlModelChecker.h
@@ -123,7 +123,7 @@ private:
LOG4CPLUS_ERROR(logger, "Solving of Submatrix failed: InvalidInput");
} else if(solver.info() == Eigen::ComputationInfo::NoConvergence) {
// NoConvergence
- throw storm::exceptions::NoConvergenceException() << "Failed to converge within " << solver.iterations() << " out of a maximum of " << solver.maxIterations() << " iterations.";
+ throw storm::exceptions::NoConvergenceException() << "Failed to converge within " << solver.iterations() << " out of a maximum of " << solver.maxIterations() << " iterations.";
} else if(solver.info() == Eigen::ComputationInfo::NumericalIssue) {
// NumericalIssue
LOG4CPLUS_ERROR(logger, "Solving of Submatrix failed: NumericalIssue");
diff --git a/src/modelchecker/GmmxxDtmcPrctlModelChecker.h b/src/modelchecker/GmmxxDtmcPrctlModelChecker.h
index 8c88d0a30..9bc3a470e 100644
--- a/src/modelchecker/GmmxxDtmcPrctlModelChecker.h
+++ b/src/modelchecker/GmmxxDtmcPrctlModelChecker.h
@@ -238,7 +238,7 @@ private:
LOG4CPLUS_INFO(logger, "Starting iterative Jacobi Solver.");
-
+
// x_(k + 1) = D^-1 * (b - R * x_k)
// In x we keep a copy of the result for swapping in the loop (e.g. less copy-back)
std::vector<Type>* xNext = new std::vector<Type>(x.size());
@@ -256,7 +256,7 @@ private:
gmm::add(b, gmm::scaled(*xNext, -1.0), *xNext);
// D^-1 * (b - R * x_k) -> xNext
gmm::mult(*gmmxxDiagonalInverted, *xNext, *xNext);
-
+
// swap xNext with xCurrent so that the next iteration can use xCurrent again without having to copy the vector
std::vector<Type> *const swap = xNext;
xNext = xCurrent;
diff --git a/src/parser/AutoParser.h b/src/parser/AutoParser.h
index f7331da7e..e09d6f340 100644
--- a/src/parser/AutoParser.h
+++ b/src/parser/AutoParser.h
@@ -79,8 +79,11 @@ class AutoParser : Parser {
* @brief Returns the type of model that was parsed.
*/
storm::models::ModelType getType() {
- if (this->model) return this->model->getType();
- else return storm::models::Unknown;
+ if (this->model) {
+ return this->model->getType();
+ } else {
+ return storm::models::Unknown;
+ }
}
/*!
@@ -90,7 +93,7 @@ class AutoParser : Parser {
std::shared_ptr<Model> getModel() {
return this->model->template as<Model>();
}
-
+
private:
/*!
diff --git a/src/parser/DeterministicModelParser.cpp b/src/parser/DeterministicModelParser.cpp
index 35818ffbf..5e39170ec 100644
--- a/src/parser/DeterministicModelParser.cpp
+++ b/src/parser/DeterministicModelParser.cpp
@@ -31,12 +31,12 @@ DeterministicModelParser::DeterministicModelParser(std::string const & transitio
std::string const & stateRewardFile, std::string const & transitionRewardFile) {
storm::parser::DeterministicSparseTransitionParser tp(transitionSystemFile);
this->transitionSystem = tp.getMatrix();
-
+
uint_fast64_t stateCount = this->transitionSystem->getRowCount();
storm::parser::AtomicPropositionLabelingParser lp(stateCount, labelingFile);
this->labeling = lp.getLabeling();
-
+
this->stateRewards = nullptr;
this->transitionRewards = nullptr;
diff --git a/src/parser/DeterministicModelParser.h b/src/parser/DeterministicModelParser.h
index 04d637dce..de067f925 100644
--- a/src/parser/DeterministicModelParser.h
+++ b/src/parser/DeterministicModelParser.h
@@ -52,7 +52,7 @@ class DeterministicModelParser: public storm::parser::Parser {
std::shared_ptr<storm::models::AtomicPropositionsLabeling> labeling;
std::shared_ptr<std::vector<double>> stateRewards;
std::shared_ptr<storm::storage::SparseMatrix<double>> transitionRewards;
-
+
std::shared_ptr<storm::models::Dtmc<double>> dtmc;
std::shared_ptr<storm::models::Ctmc<double>> ctmc;
};
diff --git a/src/parser/DeterministicSparseTransitionParser.cpp b/src/parser/DeterministicSparseTransitionParser.cpp
index cea04c4d7..c999bbeab 100644
--- a/src/parser/DeterministicSparseTransitionParser.cpp
+++ b/src/parser/DeterministicSparseTransitionParser.cpp
@@ -55,68 +55,68 @@ uint_fast64_t DeterministicSparseTransitionParser::firstPass(char* buf, uint_fas
buf = strchr(buf, '\n') + 1; // skip format hint
}
- /*
- * Check all transitions for non-zero diagonal entries and deadlock states.
- */
- int_fast64_t lastRow = -1;
- uint_fast64_t row, col;
+ /*
+ * Check all transitions for non-zero diagonal entries and deadlock states.
+ */
+ int_fast64_t lastRow = -1;
+ int_fast64_t row, col;
uint_fast64_t readTransitionCount = 0;
- bool rowHadDiagonalEntry = false;
- double val;
- maxnode = 0;
- while (buf[0] != '\0') {
- /*
- * Read row and column.
- */
- row = checked_strtol(buf, &buf);
- col = checked_strtol(buf, &buf);
-
- if (!isRewardMatrix) {
- if (lastRow != (int_fast64_t)row) {
- if ((lastRow != -1) && (!rowHadDiagonalEntry)) {
- ++nonZeroEntryCount;
- rowHadDiagonalEntry = true;
- }
- for (uint_fast64_t skippedRow = (uint_fast64_t)(lastRow + 1); skippedRow < row; ++skippedRow) {
- ++nonZeroEntryCount;
- }
- lastRow = row;
- rowHadDiagonalEntry = false;
- }
+ bool rowHadDiagonalEntry = false;
+ double val;
+ maxnode = 0;
+ while (buf[0] != '\0') {
+ /*
+ * Read row and column.
+ */
+ row = checked_strtol(buf, &buf);
+ col = checked_strtol(buf, &buf);
- if (col == row) {
- rowHadDiagonalEntry = true;
- } else if (col > row && !rowHadDiagonalEntry) {
+ if (!isRewardMatrix) {
+ if (lastRow != (int_fast64_t)row) {
+ if ((lastRow != -1) && (!rowHadDiagonalEntry)) {
+ ++nonZeroEntryCount;
rowHadDiagonalEntry = true;
+ }
+ for (uint_fast64_t skippedRow = (uint_fast64_t)(lastRow + 1); skippedRow < row; ++skippedRow) {
++nonZeroEntryCount;
}
- }
-
- /*
- * Check if one is larger than the current maximum id.
- */
- if (row > maxnode) maxnode = row;
- if (col > maxnode) maxnode = col;
-
- /*
- * Read probability of this transition.
- * Check, if the value is a probability, i.e. if it is between 0 and 1.
- */
- val = checked_strtod(buf, &buf);
- if ((val < 0.0) || (val > 1.0)) {
- LOG4CPLUS_ERROR(logger, "Expected a positive probability but got \"" << val << "\".");
- return 0;
- }
- ++nonZeroEntryCount;
- ++readTransitionCount;
- buf = trimWhitespaces(buf);
- }
-
- if (!rowHadDiagonalEntry && !isRewardMatrix) {
- ++nonZeroEntryCount;
- }
-
- return nonZeroEntryCount;
+ lastRow = row;
+ rowHadDiagonalEntry = false;
+ }
+
+ if (col == row) {
+ rowHadDiagonalEntry = true;
+ } else if (col > row && !rowHadDiagonalEntry) {
+ rowHadDiagonalEntry = true;
+ ++nonZeroEntryCount;
+ }
+ }
+
+ /*
+ * Check if one is larger than the current maximum id.
+ */
+ if (row > maxnode) maxnode = row;
+ if (col > maxnode) maxnode = col;
+
+ /*
+ * Read probability of this transition.
+ * Check, if the value is a probability, i.e. if it is between 0 and 1.
+ */
+ val = checked_strtod(buf, &buf);
+ if ((val < 0.0) || (val > 1.0)) {
+ LOG4CPLUS_ERROR(logger, "Expected a positive probability but got \"" << val << "\".");
+ return 0;
+ }
+ ++nonZeroEntryCount;
+ ++readTransitionCount;
+ buf = trimWhitespaces(buf);
+ }
+
+ if (!rowHadDiagonalEntry && !isRewardMatrix) {
+ ++nonZeroEntryCount;
+ }
+
+ return nonZeroEntryCount;
}
diff --git a/src/parser/DeterministicSparseTransitionParser.h b/src/parser/DeterministicSparseTransitionParser.h
index 870b1415e..d4029ad29 100644
--- a/src/parser/DeterministicSparseTransitionParser.h
+++ b/src/parser/DeterministicSparseTransitionParser.h
@@ -18,18 +18,18 @@ namespace parser {
class DeterministicSparseTransitionParser : public Parser {
public:
DeterministicSparseTransitionParser(std::string const &filename, bool insertDiagonalEntriesIfMissing = true, RewardMatrixInformationStruct* rewardMatrixInformation = nullptr);
-
+
std::shared_ptr<storm::storage::SparseMatrix<double>> getMatrix() {
return this->matrix;
}
-
+
private:
std::shared_ptr<storm::storage::SparseMatrix<double>> matrix;
-
+
uint_fast64_t firstPass(char* buf, uint_fast64_t &maxnode, RewardMatrixInformationStruct* rewardMatrixInformation);
-
+
};
-
+
} // namespace parser
} // namespace storm
diff --git a/src/parser/NondeterministicModelParser.cpp b/src/parser/NondeterministicModelParser.cpp
index a0ce35674..3408da9bf 100644
--- a/src/parser/NondeterministicModelParser.cpp
+++ b/src/parser/NondeterministicModelParser.cpp
@@ -47,7 +47,7 @@ NondeterministicModelParser::NondeterministicModelParser(std::string const & tra
this->probabilityMatrix = tp.getMatrix();
this->stateLabeling = lp.getLabeling();
this->rowMapping = tp.getRowMapping();
-
+
this->mdp = nullptr;
this->ctmdp = nullptr;
}
diff --git a/src/parser/NondeterministicSparseTransitionParser.h b/src/parser/NondeterministicSparseTransitionParser.h
index 5731017ec..a696b568f 100644
--- a/src/parser/NondeterministicSparseTransitionParser.h
+++ b/src/parser/NondeterministicSparseTransitionParser.h
@@ -20,23 +20,23 @@ namespace parser {
class NondeterministicSparseTransitionParser : public Parser {
public:
NondeterministicSparseTransitionParser(std::string const &filename, RewardMatrixInformationStruct* rewardMatrixInformation = nullptr);
-
+
inline std::shared_ptr<storm::storage::SparseMatrix<double>> getMatrix() const {
return this->matrix;
}
-
+
inline std::shared_ptr<std::vector<uint_fast64_t>> getRowMapping() const {
return this->rowMapping;
}
-
+
private:
std::shared_ptr<storm::storage::SparseMatrix<double>> matrix;
std::shared_ptr<std::vector<uint_fast64_t>> rowMapping;
-
+
uint_fast64_t firstPass(char* buf, uint_fast64_t& choices, int_fast64_t& maxnode, RewardMatrixInformationStruct* rewardMatrixInformation);
-
+
};
-
+
} // namespace parser
} // namespace storm
diff --git a/src/parser/Parser.h b/src/parser/Parser.h
index 6cb4abe65..2d857e5a4 100644
--- a/src/parser/Parser.h
+++ b/src/parser/Parser.h
@@ -31,7 +31,7 @@ namespace storm {
* methods for efficient file access (see MappedFile).
*/
namespace parser {
-
+
struct RewardMatrixInformationStruct {
RewardMatrixInformationStruct() : rowCount(0), columnCount(0), nondeterministicChoiceIndices(nullptr) {
// Intentionally left empty.
@@ -61,7 +61,7 @@ namespace parser {
#if !defined LINUX && !defined MACOSX && !defined WINDOWS
#error Platform not supported
#endif
-
+
class MappedFile {
private:
#if defined LINUX || defined MACOSX
@@ -73,7 +73,7 @@ namespace parser {
HANDLE file;
HANDLE mapping;
#endif
-
+
#if defined LINUX
/*!
* @brief stat information about the file.
@@ -90,7 +90,7 @@ namespace parser {
*/
struct __stat64 st;
#endif
-
+
public:
/*!
* @brief pointer to actual file content.
@@ -112,7 +112,7 @@ namespace parser {
*/
~MappedFile();
};
-
+
class Parser {
protected:
/*!
diff --git a/src/storage/SparseMatrix.h b/src/storage/SparseMatrix.h
index 5259a8052..cf175c417 100644
--- a/src/storage/SparseMatrix.h
+++ b/src/storage/SparseMatrix.h
@@ -25,12 +25,12 @@
extern log4cplus::Logger logger;
// Forward declaration for adapter classes.
-namespace storm {
- namespace adapters{
- class GmmxxAdapter;
- class EigenAdapter;
- class StormAdapter;
- }
+namespace storm {
+ namespace adapters {
+ class GmmxxAdapter;
+ class EigenAdapter;
+ class StormAdapter
+ }
}
namespace storm {
diff --git a/src/storm.cpp b/src/storm.cpp
index 4ae79224f..0534ac440 100644
--- a/src/storm.cpp
+++ b/src/storm.cpp
@@ -103,7 +103,7 @@ bool parseOptions(const int argc, const char* argv[]) {
std::cout << std::endl << storm::settings::help;
return false;
}
-
+
if (s->isSet("help")) {
std::cout << storm::settings::help;
return false;
@@ -112,7 +112,7 @@ bool parseOptions(const int argc, const char* argv[]) {
storm::parser::PrctlParser parser(s->getString("test-prctl").c_str());
return false;
}
-
+
if (s->isSet("verbose")) {
logger.getAppender("mainConsoleAppender")->setThreshold(log4cplus::INFO_LOG_LEVEL);
LOG4CPLUS_INFO(logger, "Enable verbose mode, log output gets printed to console.");