diff --git a/src/formula/And.h b/src/formula/And.h
index 742633f3b..7a42193b8 100644
--- a/src/formula/And.h
+++ b/src/formula/And.h
@@ -142,7 +142,7 @@ public:
* @returns A bit vector indicating all states that satisfy the formula represented by the called object.
*/
virtual mrmc::storage::BitVector *check(const mrmc::modelChecker::DtmcPrctlModelChecker<T>& modelChecker) const {
- return modelChecker.checkAnd(this);
+ return modelChecker.checkAnd(*this);
}
private:
diff --git a/src/formula/BoundedUntil.h b/src/formula/BoundedUntil.h
index 93355b7f3..51131602d 100644
--- a/src/formula/BoundedUntil.h
+++ b/src/formula/BoundedUntil.h
@@ -11,7 +11,6 @@
#include "PCTLPathFormula.h"
#include "PCTLStateFormula.h"
#include "boost/integer/integer_mask.hpp"
-#include "boost/lexical_cast.hpp"
#include <string>
namespace mrmc {
@@ -131,7 +130,7 @@ public:
std::string result = "(";
result += left->toString();
result += " U<=";
- result += boost::lexical_cast<std::string>(bound);
+ result += std::to_string(bound);
result += " ";
result += right->toString();
result += ")";
@@ -168,7 +167,7 @@ public:
* @returns A vector indicating the probability that the formula holds for each state.
*/
virtual std::vector<T> *check(const mrmc::modelChecker::DtmcPrctlModelChecker<T>& modelChecker) const {
- return modelChecker.checkBoundedUntil(this);
+ return modelChecker.checkBoundedUntil(*this);
}
private:
diff --git a/src/formula/Next.h b/src/formula/Next.h
index 1a5acb1ec..2eb00be05 100644
--- a/src/formula/Next.h
+++ b/src/formula/Next.h
@@ -113,7 +113,7 @@ public:
* @returns A vector indicating the probability that the formula holds for each state.
*/
virtual std::vector<T> *check(const mrmc::modelChecker::DtmcPrctlModelChecker<T>& modelChecker) const {
- return modelChecker.checkNext(this);
+ return modelChecker.checkNext(*this);
}
private:
diff --git a/src/formula/Not.h b/src/formula/Not.h
index c816a827b..574d287a1 100644
--- a/src/formula/Not.h
+++ b/src/formula/Not.h
@@ -106,7 +106,7 @@ public:
* @returns A bit vector indicating all states that satisfy the formula represented by the called object.
*/
virtual mrmc::storage::BitVector *check(const mrmc::modelChecker::DtmcPrctlModelChecker<T>& modelChecker) const {
- return modelChecker.checkNot(this);
+ return modelChecker.checkNot(*this);
}
private:
diff --git a/src/formula/Or.h b/src/formula/Or.h
index 78185b0d5..5a60d9770 100644
--- a/src/formula/Or.h
+++ b/src/formula/Or.h
@@ -141,7 +141,7 @@ public:
* @returns A bit vector indicating all states that satisfy the formula represented by the called object.
*/
virtual mrmc::storage::BitVector *check(const mrmc::modelChecker::DtmcPrctlModelChecker<T>& modelChecker) const {
- return modelChecker.checkOr(this);
+ return modelChecker.checkOr(*this);
}
private:
diff --git a/src/formula/ProbabilisticIntervalOperator.h b/src/formula/ProbabilisticIntervalOperator.h
index acc6f5b5f..8b50da26d 100644
--- a/src/formula/ProbabilisticIntervalOperator.h
+++ b/src/formula/ProbabilisticIntervalOperator.h
@@ -125,9 +125,9 @@ public:
virtual std::string toString() const {
std::string result = "(";
result += " P[";
- result += lower;
+ result += std::to_string(lower);
result += ";";
- result += upper;
+ result += std::to_string(upper);
result += "] ";
result += pathFormula->toString();
result += ")";
@@ -160,7 +160,7 @@ public:
* @returns A bit vector indicating all states that satisfy the formula represented by the called object.
*/
virtual mrmc::storage::BitVector *check(const mrmc::modelChecker::DtmcPrctlModelChecker<T>& modelChecker) const {
- return modelChecker.checkProbabilisticIntervalOperator(this);
+ return modelChecker.checkProbabilisticIntervalOperator(*this);
}
private:
diff --git a/src/formula/ProbabilisticOperator.h b/src/formula/ProbabilisticOperator.h
index 0e3876237..43962d6d4 100644
--- a/src/formula/ProbabilisticOperator.h
+++ b/src/formula/ProbabilisticOperator.h
@@ -77,9 +77,9 @@ public:
}
/*!
- * @returns the lower bound for the probability
+ * @returns the bound for the probability
*/
- const T& getLowerBound() const {
+ const T& getBound() const {
return bound;
}
@@ -97,7 +97,7 @@ public:
*
* @param bound The bound for the probability
*/
- void setInterval(T bound) {
+ void setBound(T bound) {
this->bound = bound;
}
@@ -129,9 +129,18 @@ public:
*/
virtual mrmc::storage::BitVector *check(
const mrmc::modelChecker::DtmcPrctlModelChecker<T>& modelChecker) const {
- return modelChecker.checkProbabilisticOperator(this);
+ return modelChecker.checkProbabilisticOperator(*this);
}
+ /*!
+ * Returns a string representation of this PCTLStateFormula
+ *
+ * @returns a string representation of this PCTLStateFormula
+ */
+ virtual std::string toString() const {
+ // TODO
+ return "";
+ }
private:
T bound;
PCTLPathFormula<T>* pathFormula;
diff --git a/src/models/AtomicPropositionsLabeling.h b/src/models/AtomicPropositionsLabeling.h
index 457d2f6a1..34c2da73b 100644
--- a/src/models/AtomicPropositionsLabeling.h
+++ b/src/models/AtomicPropositionsLabeling.h
@@ -33,10 +33,10 @@ public:
* @param stateCount The number of states of the model.
* @param apCountMax The number of atomic propositions.
*/
- AtomicPropositionsLabeling(const uint_fast32_t stateCount, const uint_fast32_t apCountMax)
+ AtomicPropositionsLabeling(const uint_fast64_t stateCount, const uint_fast64_t apCountMax)
: stateCount(stateCount), apCountMax(apCountMax), apsCurrent(0) {
this->singleLabelings = new mrmc::storage::BitVector*[apCountMax];
- for (uint_fast32_t i = 0; i < apCountMax; ++i) {
+ for (uint_fast64_t i = 0; i < apCountMax; ++i) {
this->singleLabelings[i] = new mrmc::storage::BitVector(stateCount);
}
}
@@ -53,7 +53,7 @@ public:
apsCurrent(atomicPropositionsLabeling.apsCurrent),
nameToLabelingMap(atomicPropositionsLabeling.nameToLabelingMap) {
this->singleLabelings = new mrmc::storage::BitVector*[apCountMax];
- for (uint_fast32_t i = 0; i < apCountMax; ++i) {
+ for (uint_fast64_t i = 0; i < apCountMax; ++i) {
this->singleLabelings[i] = new mrmc::storage::BitVector(*atomicPropositionsLabeling.singleLabelings[i]);
}
}
@@ -64,7 +64,7 @@ public:
*/
virtual ~AtomicPropositionsLabeling() {
// delete all the single atomic proposition labelings in the map
- for (uint_fast32_t i = 0; i < apCountMax; ++i) {
+ for (uint_fast64_t i = 0; i < apCountMax; ++i) {
delete this->singleLabelings[i];
this->singleLabelings[i] = NULL;
}
@@ -79,7 +79,7 @@ public:
* @param ap The name of the atomic proposition to add.
* @return The index of the new proposition.
*/
- uint_fast32_t addAtomicProposition(std::string ap) {
+ uint_fast64_t addAtomicProposition(std::string ap) {
if (nameToLabelingMap.count(ap) != 0) {
throw std::out_of_range("Atomic Proposition already exists.");
}
@@ -89,7 +89,7 @@ public:
}
nameToLabelingMap[ap] = apsCurrent;
- uint_fast32_t returnValue = apsCurrent++;
+ uint_fast64_t returnValue = apsCurrent++;
return returnValue;
}
@@ -107,7 +107,7 @@ public:
* @param ap The name of the atomic proposition.
* @param state The index of the state to label.
*/
- void addAtomicPropositionToState(std::string ap, const uint_fast32_t state) {
+ void addAtomicPropositionToState(std::string ap, const uint_fast64_t state) {
if (nameToLabelingMap.count(ap) == 0) {
throw std::out_of_range("Atomic Proposition '" + ap + "' unknown.");
}
@@ -122,7 +122,7 @@ public:
* @param state The index of a state
* @returns The list of propositions for the given state
*/
- std::set<std::string> getPropositionsForState(uint_fast32_t state) {
+ std::set<std::string> getPropositionsForState(uint_fast64_t state) {
if (state >= stateCount) {
throw std::out_of_range("State index out of range.");
}
@@ -144,7 +144,7 @@ public:
* @return True if the node is labeled with the atomic proposition, false
* otherwise.
*/
- bool stateHasAtomicProposition(std::string ap, const uint_fast32_t state) {
+ bool stateHasAtomicProposition(std::string ap, const uint_fast64_t state) {
return this->singleLabelings[nameToLabelingMap[ap]]->get(state);
}
@@ -153,7 +153,7 @@ public:
* the initialization).
* @return The number of atomic propositions.
*/
- uint_fast32_t getNumberOfAtomicPropositions() {
+ uint_fast64_t getNumberOfAtomicPropositions() {
return apCountMax;
}
@@ -174,7 +174,7 @@ public:
uint_fast64_t getSizeInMemory() {
uint_fast64_t size = sizeof(*this);
// Add sizes of all single labelings.
- for (uint_fast32_t i = 0; i < apCountMax; i++) {
+ for (uint_fast64_t i = 0; i < apCountMax; i++) {
size += this->singleLabelings[i]->getSizeInMemory();
}
return size;
@@ -197,24 +197,24 @@ public:
private:
/*! The number of states whose labels are to be stored by this object. */
- uint_fast32_t stateCount;
+ uint_fast64_t stateCount;
/*! The number of different atomic propositions this object can store. */
- uint_fast32_t apCountMax;
+ uint_fast64_t apCountMax;
/*!
* The number of different atomic propositions currently associated with
* this labeling. Used to prevent too many atomic propositions from being
* added to this object.
*/
- uint_fast32_t apsCurrent;
+ uint_fast64_t apsCurrent;
/*!
* Associates a name of an atomic proposition to its corresponding labeling
* by mapping the name to a specific index in the array of all
* individual labelings.
*/
- std::unordered_map<std::string, uint_fast32_t> nameToLabelingMap;
+ std::unordered_map<std::string, uint_fast64_t> nameToLabelingMap;
/*!
* Stores all individual labelings. To find the labeling associated with
diff --git a/src/models/Dtmc.h b/src/models/Dtmc.h
index 83bba3d6e..8fa263f54 100644
--- a/src/models/Dtmc.h
+++ b/src/models/Dtmc.h
@@ -102,7 +102,7 @@ public:
/*!
*
*/
- std::set<std::string> getPropositionsForState(uint_fast32_t state) {
+ std::set<std::string> getPropositionsForState(uint_fast64_t state) {
return stateLabeling->getPropositionsForState(state);
}
diff --git a/src/mrmc.cpp b/src/mrmc.cpp
index c531102f5..cb5510530 100644
--- a/src/mrmc.cpp
+++ b/src/mrmc.cpp
@@ -22,6 +22,7 @@
#include "src/models/Dtmc.h"
#include "src/storage/SquareSparseMatrix.h"
#include "src/models/AtomicPropositionsLabeling.h"
+#include "src/modelChecker/EigenDtmcPrctlModelChecker.h"
#include "src/modelChecker/GmmxxDtmcPrctlModelChecker.h"
#include "src/parser/readLabFile.h"
#include "src/parser/readTraFile.h"
@@ -106,14 +107,37 @@ int main(const int argc, const char* argv[]) {
dtmc.printModelInformationToStream(std::cout);
// Uncomment this if you want to see the first model checking procedure in action. :)
- /*
- mrmc::modelChecker::GmmxxDtmcPrctlModelChecker<double> mc(dtmc);
+ mrmc::modelChecker::EigenDtmcPrctlModelChecker<double> mc(dtmc);
mrmc::formula::AP<double>* trueFormula = new mrmc::formula::AP<double>(std::string("true"));
mrmc::formula::AP<double>* ap = new mrmc::formula::AP<double>(std::string("observe0Greater1"));
mrmc::formula::Until<double>* until = new mrmc::formula::Until<double>(trueFormula, ap);
- mc.checkPathFormula(*until);
+ std::vector<double>* eigenResult = mc.checkPathFormula(*until);
delete until;
- */
+
+ mrmc::modelChecker::GmmxxDtmcPrctlModelChecker<double> mcG(dtmc);
+ mrmc::formula::AP<double>* trueFormulaG = new mrmc::formula::AP<double>(std::string("true"));
+ mrmc::formula::AP<double>* apG = new mrmc::formula::AP<double>(std::string("observe0Greater1"));
+ mrmc::formula::Until<double>* untilG = new mrmc::formula::Until<double>(trueFormulaG, apG);
+ std::vector<double>* gmmResult = mcG.checkPathFormula(*untilG);
+ delete untilG;
+
+ if (eigenResult->size() != gmmResult->size()) {
+ LOG4CPLUS_ERROR(logger, "Warning: Eigen and GMM produced different results (Eigen: " << eigenResult->size() << ", Gmm: " << gmmResult->size() << ") in size!");
+ } else {
+ LOG4CPLUS_INFO(logger, "Testing for different entries");
+ for (int i = 0; i < eigenResult->size(); ++i) {
+ if (std::abs((eigenResult->at(i) - gmmResult->at(i))) > 0) {
+ LOG4CPLUS_ERROR(logger, "Warning: Eigen and GMM produced different results in entry " << i << " (Eigen: " << eigenResult->at(i) << ", Gmm: " << gmmResult->at(i) << ")!");
+ }
+ }
+ }
+
+ /*
+ LOG4CPLUS_INFO(logger, "Result: ");
+ LOG4CPLUS_INFO(logger, "Entry : EigenResult at Entry : GmmResult at Entry");
+ for (int i = 0; i < eigenResult->size(); ++i) {
+ LOG4CPLUS_INFO(logger, i << " : " << eigenResult->at(i) << " : " << gmmResult->at(i));
+ }*/
if (s != nullptr) {
delete s;
diff --git a/src/parser/readLabFile.cpp b/src/parser/readLabFile.cpp
index 7bb020e5a..3ef488373 100644
--- a/src/parser/readLabFile.cpp
+++ b/src/parser/readLabFile.cpp
@@ -163,7 +163,7 @@ LabParser::LabParser(uint_fast64_t node_count, const char * filename)
/*
* now parse node label assignments
*/
- uint_fast32_t node;
+ uint_fast64_t node;
char proposition[128];
size_t cnt;
/*
diff --git a/src/parser/readTraFile.cpp b/src/parser/readTraFile.cpp
index 6a73bff0a..902259f54 100644
--- a/src/parser/readTraFile.cpp
+++ b/src/parser/readTraFile.cpp
@@ -48,9 +48,9 @@ namespace parser{
* @param buf Data to scan. Is expected to be some char array.
* @param maxnode Is set to highest id of all nodes.
*/
-uint_fast32_t TraParser::firstPass(char* buf, uint_fast32_t &maxnode)
+uint_fast64_t TraParser::firstPass(char* buf, uint_fast64_t &maxnode)
{
- uint_fast32_t non_zero = 0;
+ uint_fast64_t non_zero = 0;
/*
* check file header and extract number of transitions
@@ -74,7 +74,7 @@ uint_fast32_t TraParser::firstPass(char* buf, uint_fast32_t &maxnode)
/*
* check all transitions for non-zero diagonal entrys
*/
- uint_fast32_t row, col;
+ uint_fast64_t row, col;
double val;
maxnode = 0;
char* tmp;
@@ -134,8 +134,8 @@ TraParser::TraParser(const char * filename)
/*
* perform first pass, i.e. count entries that are not zero and not on the diagonal
*/
- uint_fast32_t maxnode;
- uint_fast32_t non_zero = this->firstPass(file.data, maxnode);
+ uint_fast64_t maxnode;
+ uint_fast64_t non_zero = this->firstPass(file.data, maxnode);
/*
* if first pass returned zero, the file format was wrong
*/
diff --git a/src/parser/readTraFile.h b/src/parser/readTraFile.h
index c46167e37..cf2886b18 100644
--- a/src/parser/readTraFile.h
+++ b/src/parser/readTraFile.h
@@ -30,7 +30,7 @@ class TraParser : Parser
private:
std::shared_ptr<mrmc::storage::SquareSparseMatrix<double>> matrix;
- uint_fast32_t firstPass(char* buf, uint_fast32_t &maxnode);
+ uint_fast64_t firstPass(char* buf, uint_fast64_t &maxnode);
};
diff --git a/src/storage/SquareSparseMatrix.h b/src/storage/SquareSparseMatrix.h
index 5f322de01..d57d9ddb6 100644
--- a/src/storage/SquareSparseMatrix.h
+++ b/src/storage/SquareSparseMatrix.h
@@ -509,7 +509,7 @@ public:
rowEnd = rowIndications[row + 1];
while (rowStart < rowEnd) {
if (valueStorage[rowStart] == 0) zeroCount++;
- tripletList.push_back(IntTriplet(row, columnIndications[rowStart], valueStorage[rowStart]));
+ tripletList.push_back(IntTriplet(static_cast<int_fast32_t>(row), static_cast<int_fast32_t>(columnIndications[rowStart]), valueStorage[rowStart]));
++rowStart;
}
}
@@ -517,7 +517,7 @@ public:
// Then add the elements on the diagonal.
for (uint_fast64_t i = 0; i < rowCount; ++i) {
if (diagonalStorage[i] == 0) zeroCount++;
- tripletList.push_back(IntTriplet(i, i, diagonalStorage[i]));
+ tripletList.push_back(IntTriplet(static_cast<int_fast32_t>(i), static_cast<int_fast32_t>(i), diagonalStorage[i]));
}
// Let Eigen create a matrix from the given list of triplets.
diff --git a/src/utility/vector.h b/src/utility/vector.h
index eff5f02b9..d744fdc35 100644
--- a/src/utility/vector.h
+++ b/src/utility/vector.h
@@ -8,6 +8,8 @@
#ifndef VECTOR_H_
#define VECTOR_H_
+#include "Eigen/src/Core/Matrix.h"
+
namespace mrmc {
namespace utility {
@@ -27,6 +29,13 @@ void setVectorValues(std::vector<T>* vector, const mrmc::storage::BitVector& pos
}
}
+template<class T>
+void setVectorValues(Eigen::Matrix<T, -1, 1, 0, -1, 1>* eigenVector, const mrmc::storage::BitVector& positions, T value) {
+ for (auto position : positions) {
+ (*vector)(position, 0) = value;
+ }
+}
+
} //namespace utility
} //namespace mrmc