Browse Source

Cosmetics: Trailing whitespaces, space indentation, ...

main
gereon 12 years ago
parent
commit
6c19ddb877
  1. 16
      src/modelchecker/AbstractModelChecker.h
  2. 2
      src/modelchecker/EigenDtmcPrctlModelChecker.h
  3. 4
      src/modelchecker/GmmxxDtmcPrctlModelChecker.h
  4. 9
      src/parser/AutoParser.h
  5. 4
      src/parser/DeterministicModelParser.cpp
  6. 2
      src/parser/DeterministicModelParser.h
  7. 114
      src/parser/DeterministicSparseTransitionParser.cpp
  8. 10
      src/parser/DeterministicSparseTransitionParser.h
  9. 2
      src/parser/NondeterministicModelParser.cpp
  10. 12
      src/parser/NondeterministicSparseTransitionParser.h
  11. 10
      src/parser/Parser.h
  12. 12
      src/storage/SparseMatrix.h
  13. 4
      src/storm.cpp

16
src/modelchecker/AbstractModelChecker.h

@ -8,9 +8,11 @@
#ifndef STORM_MODELCHECKER_ABSTRACTMODELCHECKER_H_ #ifndef STORM_MODELCHECKER_ABSTRACTMODELCHECKER_H_
#define STORM_MODELCHECKER_ABSTRACTMODELCHECKER_H_ #define STORM_MODELCHECKER_ABSTRACTMODELCHECKER_H_
namespace storm { namespace modelChecker { namespace storm {
namespace modelChecker {
template <class Type> class AbstractModelChecker; template <class Type> class AbstractModelChecker;
}} }
}
#include "src/exceptions/InvalidPropertyException.h" #include "src/exceptions/InvalidPropertyException.h"
#include "src/formula/Formulas.h" #include "src/formula/Formulas.h"
@ -49,17 +51,17 @@ class AbstractModelChecker :
public virtual storm::formula::IReachabilityRewardModelChecker<Type>, public virtual storm::formula::IReachabilityRewardModelChecker<Type>,
public virtual storm::formula::ICumulativeRewardModelChecker<Type>, public virtual storm::formula::ICumulativeRewardModelChecker<Type>,
public virtual storm::formula::IInstantaneousRewardModelChecker<Type> { public virtual storm::formula::IInstantaneousRewardModelChecker<Type> {
public: public:
explicit AbstractModelChecker(storm::models::AbstractModel<Type>& model) explicit AbstractModelChecker(storm::models::AbstractModel<Type>& model)
: model(model) { : model(model) {
// Nothing to do here... // Nothing to do here...
} }
explicit AbstractModelChecker(AbstractModelChecker<Type>* modelChecker) explicit AbstractModelChecker(AbstractModelChecker<Type>* modelChecker)
: model(modelChecker->model) { : model(modelChecker->model) {
} }
template <template <class T> class Target> template <template <class T> class Target>
const Target<Type>* as() const { const Target<Type>* as() const {
try { try {
@ -243,11 +245,11 @@ public:
delete quantitativeResult; delete quantitativeResult;
return result; return result;
} }
void setModel(storm::models::AbstractModel<Type>& model) { void setModel(storm::models::AbstractModel<Type>& model) {
this->model = model; this->model = model;
} }
template <class Model> template <class Model>
Model& getModel() const { Model& getModel() const {
return *dynamic_cast<Model*>(&this->model); return *dynamic_cast<Model*>(&this->model);

2
src/modelchecker/EigenDtmcPrctlModelChecker.h

@ -123,7 +123,7 @@ private:
LOG4CPLUS_ERROR(logger, "Solving of Submatrix failed: InvalidInput"); LOG4CPLUS_ERROR(logger, "Solving of Submatrix failed: InvalidInput");
} else if(solver.info() == Eigen::ComputationInfo::NoConvergence) { } else if(solver.info() == Eigen::ComputationInfo::NoConvergence) {
// 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) { } else if(solver.info() == Eigen::ComputationInfo::NumericalIssue) {
// NumericalIssue // NumericalIssue
LOG4CPLUS_ERROR(logger, "Solving of Submatrix failed: NumericalIssue"); LOG4CPLUS_ERROR(logger, "Solving of Submatrix failed: NumericalIssue");

4
src/modelchecker/GmmxxDtmcPrctlModelChecker.h

@ -238,7 +238,7 @@ private:
LOG4CPLUS_INFO(logger, "Starting iterative Jacobi Solver."); LOG4CPLUS_INFO(logger, "Starting iterative Jacobi Solver.");
// x_(k + 1) = D^-1 * (b - R * x_k) // 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) // 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()); std::vector<Type>* xNext = new std::vector<Type>(x.size());
@ -256,7 +256,7 @@ private:
gmm::add(b, gmm::scaled(*xNext, -1.0), *xNext); gmm::add(b, gmm::scaled(*xNext, -1.0), *xNext);
// D^-1 * (b - R * x_k) -> xNext // D^-1 * (b - R * x_k) -> xNext
gmm::mult(*gmmxxDiagonalInverted, *xNext, *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 // 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; std::vector<Type> *const swap = xNext;
xNext = xCurrent; xNext = xCurrent;

9
src/parser/AutoParser.h

@ -79,8 +79,11 @@ class AutoParser : Parser {
* @brief Returns the type of model that was parsed. * @brief Returns the type of model that was parsed.
*/ */
storm::models::ModelType getType() { storm::models::ModelType getType() {
if (this->model) return this->model->getType(); if (this->model) {
else return storm::models::Unknown; return this->model->getType();
} else {
return storm::models::Unknown;
}
} }
/*! /*!
@ -90,7 +93,7 @@ class AutoParser : Parser {
std::shared_ptr<Model> getModel() { std::shared_ptr<Model> getModel() {
return this->model->template as<Model>(); return this->model->template as<Model>();
} }
private: private:
/*! /*!

4
src/parser/DeterministicModelParser.cpp

@ -31,12 +31,12 @@ DeterministicModelParser::DeterministicModelParser(std::string const & transitio
std::string const & stateRewardFile, std::string const & transitionRewardFile) { std::string const & stateRewardFile, std::string const & transitionRewardFile) {
storm::parser::DeterministicSparseTransitionParser tp(transitionSystemFile); storm::parser::DeterministicSparseTransitionParser tp(transitionSystemFile);
this->transitionSystem = tp.getMatrix(); this->transitionSystem = tp.getMatrix();
uint_fast64_t stateCount = this->transitionSystem->getRowCount(); uint_fast64_t stateCount = this->transitionSystem->getRowCount();
storm::parser::AtomicPropositionLabelingParser lp(stateCount, labelingFile); storm::parser::AtomicPropositionLabelingParser lp(stateCount, labelingFile);
this->labeling = lp.getLabeling(); this->labeling = lp.getLabeling();
this->stateRewards = nullptr; this->stateRewards = nullptr;
this->transitionRewards = nullptr; this->transitionRewards = nullptr;

2
src/parser/DeterministicModelParser.h

@ -52,7 +52,7 @@ class DeterministicModelParser: public storm::parser::Parser {
std::shared_ptr<storm::models::AtomicPropositionsLabeling> labeling; std::shared_ptr<storm::models::AtomicPropositionsLabeling> labeling;
std::shared_ptr<std::vector<double>> stateRewards; std::shared_ptr<std::vector<double>> stateRewards;
std::shared_ptr<storm::storage::SparseMatrix<double>> transitionRewards; std::shared_ptr<storm::storage::SparseMatrix<double>> transitionRewards;
std::shared_ptr<storm::models::Dtmc<double>> dtmc; std::shared_ptr<storm::models::Dtmc<double>> dtmc;
std::shared_ptr<storm::models::Ctmc<double>> ctmc; std::shared_ptr<storm::models::Ctmc<double>> ctmc;
}; };

114
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 buf = strchr(buf, '\n') + 1; // skip format hint
} }
/* /*
* Check all transitions for non-zero diagonal entries and deadlock states. * Check all transitions for non-zero diagonal entries and deadlock states.
*/ */
int_fast64_t lastRow = -1; int_fast64_t lastRow = -1;
uint_fast64_t row, col; int_fast64_t row, col;
uint_fast64_t readTransitionCount = 0; uint_fast64_t readTransitionCount = 0;
bool rowHadDiagonalEntry = false; bool rowHadDiagonalEntry = false;
double val; double val;
maxnode = 0; maxnode = 0;
while (buf[0] != '\0') { while (buf[0] != '\0') {
/* /*
* Read row and column. * Read row and column.
*/ */
row = checked_strtol(buf, &buf); row = checked_strtol(buf, &buf);
col = 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;
}
if (col == row) { if (!isRewardMatrix) {
rowHadDiagonalEntry = true; if (lastRow != (int_fast64_t)row) {
} else if (col > row && !rowHadDiagonalEntry) { if ((lastRow != -1) && (!rowHadDiagonalEntry)) {
++nonZeroEntryCount;
rowHadDiagonalEntry = true; rowHadDiagonalEntry = true;
}
for (uint_fast64_t skippedRow = (uint_fast64_t)(lastRow + 1); skippedRow < row; ++skippedRow) {
++nonZeroEntryCount; ++nonZeroEntryCount;
} }
} lastRow = row;
rowHadDiagonalEntry = false;
/* }
* Check if one is larger than the current maximum id. if (col == row) {
*/ rowHadDiagonalEntry = true;
if (row > maxnode) maxnode = row; } else if (col > row && !rowHadDiagonalEntry) {
if (col > maxnode) maxnode = col; rowHadDiagonalEntry = true;
++nonZeroEntryCount;
/* }
* Read probability of this transition. }
* Check, if the value is a probability, i.e. if it is between 0 and 1. /*
*/ * Check if one is larger than the current maximum id.
val = checked_strtod(buf, &buf); */
if ((val < 0.0) || (val > 1.0)) { if (row > maxnode) maxnode = row;
LOG4CPLUS_ERROR(logger, "Expected a positive probability but got \"" << val << "\"."); if (col > maxnode) maxnode = col;
return 0; /*
} * Read probability of this transition.
++nonZeroEntryCount; * Check, if the value is a probability, i.e. if it is between 0 and 1.
++readTransitionCount; */
buf = trimWhitespaces(buf); val = checked_strtod(buf, &buf);
} if ((val < 0.0) || (val > 1.0)) {
LOG4CPLUS_ERROR(logger, "Expected a positive probability but got \"" << val << "\".");
if (!rowHadDiagonalEntry && !isRewardMatrix) { return 0;
++nonZeroEntryCount; }
} ++nonZeroEntryCount;
++readTransitionCount;
return nonZeroEntryCount; buf = trimWhitespaces(buf);
}
if (!rowHadDiagonalEntry && !isRewardMatrix) {
++nonZeroEntryCount;
}
return nonZeroEntryCount;
} }

10
src/parser/DeterministicSparseTransitionParser.h

@ -18,18 +18,18 @@ namespace parser {
class DeterministicSparseTransitionParser : public Parser { class DeterministicSparseTransitionParser : public Parser {
public: public:
DeterministicSparseTransitionParser(std::string const &filename, bool insertDiagonalEntriesIfMissing = true, RewardMatrixInformationStruct* rewardMatrixInformation = nullptr); DeterministicSparseTransitionParser(std::string const &filename, bool insertDiagonalEntriesIfMissing = true, RewardMatrixInformationStruct* rewardMatrixInformation = nullptr);
std::shared_ptr<storm::storage::SparseMatrix<double>> getMatrix() { std::shared_ptr<storm::storage::SparseMatrix<double>> getMatrix() {
return this->matrix; return this->matrix;
} }
private: private:
std::shared_ptr<storm::storage::SparseMatrix<double>> matrix; std::shared_ptr<storm::storage::SparseMatrix<double>> matrix;
uint_fast64_t firstPass(char* buf, uint_fast64_t &maxnode, RewardMatrixInformationStruct* rewardMatrixInformation); uint_fast64_t firstPass(char* buf, uint_fast64_t &maxnode, RewardMatrixInformationStruct* rewardMatrixInformation);
}; };
} // namespace parser } // namespace parser
} // namespace storm } // namespace storm

2
src/parser/NondeterministicModelParser.cpp

@ -47,7 +47,7 @@ NondeterministicModelParser::NondeterministicModelParser(std::string const & tra
this->probabilityMatrix = tp.getMatrix(); this->probabilityMatrix = tp.getMatrix();
this->stateLabeling = lp.getLabeling(); this->stateLabeling = lp.getLabeling();
this->rowMapping = tp.getRowMapping(); this->rowMapping = tp.getRowMapping();
this->mdp = nullptr; this->mdp = nullptr;
this->ctmdp = nullptr; this->ctmdp = nullptr;
} }

12
src/parser/NondeterministicSparseTransitionParser.h

@ -20,23 +20,23 @@ namespace parser {
class NondeterministicSparseTransitionParser : public Parser { class NondeterministicSparseTransitionParser : public Parser {
public: public:
NondeterministicSparseTransitionParser(std::string const &filename, RewardMatrixInformationStruct* rewardMatrixInformation = nullptr); NondeterministicSparseTransitionParser(std::string const &filename, RewardMatrixInformationStruct* rewardMatrixInformation = nullptr);
inline std::shared_ptr<storm::storage::SparseMatrix<double>> getMatrix() const { inline std::shared_ptr<storm::storage::SparseMatrix<double>> getMatrix() const {
return this->matrix; return this->matrix;
} }
inline std::shared_ptr<std::vector<uint_fast64_t>> getRowMapping() const { inline std::shared_ptr<std::vector<uint_fast64_t>> getRowMapping() const {
return this->rowMapping; return this->rowMapping;
} }
private: private:
std::shared_ptr<storm::storage::SparseMatrix<double>> matrix; std::shared_ptr<storm::storage::SparseMatrix<double>> matrix;
std::shared_ptr<std::vector<uint_fast64_t>> rowMapping; 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); uint_fast64_t firstPass(char* buf, uint_fast64_t& choices, int_fast64_t& maxnode, RewardMatrixInformationStruct* rewardMatrixInformation);
}; };
} // namespace parser } // namespace parser
} // namespace storm } // namespace storm

10
src/parser/Parser.h

@ -31,7 +31,7 @@ namespace storm {
* methods for efficient file access (see MappedFile). * methods for efficient file access (see MappedFile).
*/ */
namespace parser { namespace parser {
struct RewardMatrixInformationStruct { struct RewardMatrixInformationStruct {
RewardMatrixInformationStruct() : rowCount(0), columnCount(0), nondeterministicChoiceIndices(nullptr) { RewardMatrixInformationStruct() : rowCount(0), columnCount(0), nondeterministicChoiceIndices(nullptr) {
// Intentionally left empty. // Intentionally left empty.
@ -61,7 +61,7 @@ namespace parser {
#if !defined LINUX && !defined MACOSX && !defined WINDOWS #if !defined LINUX && !defined MACOSX && !defined WINDOWS
#error Platform not supported #error Platform not supported
#endif #endif
class MappedFile { class MappedFile {
private: private:
#if defined LINUX || defined MACOSX #if defined LINUX || defined MACOSX
@ -73,7 +73,7 @@ namespace parser {
HANDLE file; HANDLE file;
HANDLE mapping; HANDLE mapping;
#endif #endif
#if defined LINUX #if defined LINUX
/*! /*!
* @brief stat information about the file. * @brief stat information about the file.
@ -90,7 +90,7 @@ namespace parser {
*/ */
struct __stat64 st; struct __stat64 st;
#endif #endif
public: public:
/*! /*!
* @brief pointer to actual file content. * @brief pointer to actual file content.
@ -112,7 +112,7 @@ namespace parser {
*/ */
~MappedFile(); ~MappedFile();
}; };
class Parser { class Parser {
protected: protected:
/*! /*!

12
src/storage/SparseMatrix.h

@ -25,12 +25,12 @@
extern log4cplus::Logger logger; extern log4cplus::Logger logger;
// Forward declaration for adapter classes. // Forward declaration for adapter classes.
namespace storm { namespace storm {
namespace adapters{ namespace adapters {
class GmmxxAdapter; class GmmxxAdapter;
class EigenAdapter; class EigenAdapter;
class StormAdapter; class StormAdapter
} }
} }
namespace storm { namespace storm {

4
src/storm.cpp

@ -103,7 +103,7 @@ bool parseOptions(const int argc, const char* argv[]) {
std::cout << std::endl << storm::settings::help; std::cout << std::endl << storm::settings::help;
return false; return false;
} }
if (s->isSet("help")) { if (s->isSet("help")) {
std::cout << storm::settings::help; std::cout << storm::settings::help;
return false; return false;
@ -112,7 +112,7 @@ bool parseOptions(const int argc, const char* argv[]) {
storm::parser::PrctlParser parser(s->getString("test-prctl").c_str()); storm::parser::PrctlParser parser(s->getString("test-prctl").c_str());
return false; return false;
} }
if (s->isSet("verbose")) { if (s->isSet("verbose")) {
logger.getAppender("mainConsoleAppender")->setThreshold(log4cplus::INFO_LOG_LEVEL); logger.getAppender("mainConsoleAppender")->setThreshold(log4cplus::INFO_LOG_LEVEL);
LOG4CPLUS_INFO(logger, "Enable verbose mode, log output gets printed to console."); LOG4CPLUS_INFO(logger, "Enable verbose mode, log output gets printed to console.");

|||||||
100:0
Loading…
Cancel
Save